Abstract
Given a transition system and a partial order on its states, the coverability problem is the question to decide whether a state can be reached that is larger than some given state. For graphs, a typical such partial order is the minor ordering, which allows to specify “bad graphs” as those graphs having a given graph as a minor. Well-structuredness of the transition system enables a finite representation of upward-closed sets and gives rise to a backward search algorithm for deciding coverability.
It is known that graph tranformation systems without negative application conditions form well-structured transition systems (WSTS) if the minor ordering is used and certain condition on the rules are satisfied. We study graph transformation systems with negative application conditions and show under which conditions they are well-structured and are hence amenable to a backwards search decision procedure for checking coverability.
Research partially supported by DFG project GaReV.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proc. of LICS 1996, pp. 313–321. IEEE (1996)
Bertrand, N., Delzanno, G., König, B., Sangnier, A., Stückrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: Proc. of RTA 2012. LIPIcs. Schloss Dagstuhl – Leibniz Center for Informatics (2012)
Bouajjani, A., Mayr, R.: Model Checking Lossy Vector Addition Systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 323–333. Springer, Heidelberg (1999)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer (2006)
Esparza, J., Nielsen, M.: Decidability issues for Petri nets. Technical Report RS-94-8, BRICS (May 1994)
Fellows, M.R., Hermelin, D., Rosamond, F.A.: Well-Quasi-Orders in Subclasses of Bounded Treewidth Graphs. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 149–160. Springer, Heidelberg (2009)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)
Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inf. 26(3-4), 287–313 (1996)
Habel, A., Pennemann, K.-H.: Nested Constraints and Application Conditions for High-Level Structures. In: Kreowski, H.-J., Montanari, U., Yu, Y., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 293–308. Springer, Heidelberg (2005)
Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. Technical Report 2012-01, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen (2012)
Joshi, S., König, B.: Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008)
König, B., Stückrath, J.: Well-structured graph transformation systems with negative application conditions. Technical Report 2012-03, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen (2012)
Löwe, M.: Algebraic approach to single-pushout graph transformation. Theoretical Computer Science 109, 181–224 (1993)
Rensink, A.: Representing First-Order Logic Using Graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 319–335. Springer, Heidelberg (2004)
Robertson, N., Seymour, P.: Graph minors XX. Wagner’s conjecture. Journal of Combinatorial Theory Series B 92, 325–357 (2004)
Robertson, N., Seymour, P.: Graph minors XXIII. Nash-Williams’ immersion conjecture. Journal of Combinatorial Theory Series B 100, 181–205 (2010)
Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol. 1. World Scientific (1997)
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
König, B., Stückrath, J. (2012). Well-Structured Graph Transformation Systems with Negative Application Conditions. 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_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-33654-6_6
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)