Abstract
We introduce graph automata as a more automata-theoretic view on (bounded) automaton functors and we present how automaton-based techniques can be used for invariant checking in graph transformation systems. Since earlier related work on graph automata suffered from the explosion of the size of the automata and the need of approximations due to the non-determinism of the automata, we here employ symbolic bdd-based techniques and recent antichain algorithms for language inclusion to overcome these issues. We have implemented techniques for generating, manipulating and analyzing graph automata and perform an experimental evaluation.
This work is supported by the dfg-project GaReV.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010)
Andersen, H.R.: An introduction to binary decision diagrams. Course Notes (1997), http://www.configit.com/fileadmin/Configit/Documents/bdd-eap.pdf
Bauderon, M., Courcelle, B.: Graph expressions and graph rewritings. Mathematical Systems Theory 20(2-3), 83–127 (1987)
Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: Proc. of ICSE 2006 (International Conference on Software Engineering), pp. 72–81. ACM (2006)
Blume, C.: Graphsprachen für die Spezifikation von Invarianten bei verteilten und dynamischen Systemen. Master’s thesis, Universität Duisburg-Essen (2008)
Blume, C., Bruggink, S., Friedrich, M., König, B.: Treewidth, pathwidth and cospan decompositions. In: Proc. of GT-VMT 2011 (2011)
Blume, C., Bruggink, S., König, B.: Recognizable graph languages for checking invariants. In: Proc. of GT-VMT 2010. ECEASST, vol. 29 (2010)
Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 52–70. Springer, Heidelberg (2006)
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)
Bruggink, H.J.S., König, B.: On the Recognizability of Arrow and Graph Languages. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 336–350. Springer, Heidelberg (2008)
Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (October 12, 2007), http://www.grappa.univ-lille3.fr/tata
Courcelle, B.: The monadic second-order logic of graphs I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)
Courcelle, B., Durand, I.: Verifying monadic second order graph properties with tree automata. In: European Lisp Symposium (May 2010)
Flum, J., Frick, M., Grohe, M.: Query evaluation via tree-decompositions. Journal of the ACM 49(6), 716–752 (2002)
Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting. Applicable Algebra in Engineering, Communication and Computing 15(3-4), 149–171 (2004)
Gottlob, G., Pichler, R., Wei, F.: Bounded treewidth as a key to tractability of knowledge representation and reasoning. Journal of Artificial Intelligence 174(1), 105–132 (2010)
Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. International Journal of Foundations of Computer Science 13(4), 571–586 (2002)
Kneis, J., Langer, A., Rossmanith, P.: Courcelle’s theorem – a game-theoretic approach. Discrete Optimization (2011)
Sassone, V., Sobociński, P.: Reactive systems over cospans. In: Proc. of LICS 2005, pp. 311–320. IEEE (2005)
Soguet, D.: Génération automatique d’algorithmes linéaires. Ph.D. thesis, Université Paris-Sud (2008)
De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A New Algorithm for Checking Universality of Finite Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blume, C., Bruggink, H.J.S., Engelke, D., König, B. (2012). Efficient Symbolic Implementation of Graph Automata with Applications to Invariant Checking. In: Ehrig, H., Engels, G., Kreowski, HJ., Rozenberg, G. (eds) Graph Transformations. ICGT 2012. Lecture Notes in Computer Science, vol 7562. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33654-6_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-33654-6_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33653-9
Online ISBN: 978-3-642-33654-6
eBook Packages: Computer ScienceComputer Science (R0)