×
Joshi, Salil; König, Barbara

Applying the graph minor theorem to the verification of graph transformation systems. (English) Zbl 1155.68410

Gupta, Aarti (ed.) et al., Computer aided verification. 20th international conference, CAV 2008, Princeton, NJ, USA, July 7–14, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-70543-7/pbk). Lecture Notes in Computer Science 5123, 214-226 (2008).
Summary: We show how to view certain subclasses of (single-pushout) graph transformation systems as well-structured transition systems, which leads to decidability of the covering problem via a backward analysis. As the well-quasi order required for a well-structured transition system we use the graph minor ordering. We give an explicit construction of the backward step and apply our theory in order to show the correctness of a leader election protocol.
For the entire collection see [Zbl 1139.68005].

Cited in 7 Documents

MSC:

68Q42 Grammars and rewriting systems
05C83 Graph minors
05C90 Applications of graph theory
68R10 Graph theory (including graph drawing) in computer science
PDFBibTeX XMLCite
\textit{S. Joshi} and \textit{B. König}, Lect. Notes Comput. Sci. 5123, 214--226 (2008; Zbl 1155.68410)
Full Text: DOI

References:

[1] Abdulla, P. A.; Jonsson, B.; Kindahl, M.; Peled, D.; Y. Vardi, M., A general approach to partial order reductions in symbolic verification, Computer Aided Verification, 379-390 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0028760
[2] Baldan, P.; Corradini, A.; König, B.; Larsen, K. G.; Nielsen, M., A static analysis technique for graph transformation systems, CONCUR 2001 - Concurrency Theory, 381-395 (2001), Heidelberg: Springer, Heidelberg · Zbl 1006.68529 · doi:10.1007/3-540-44685-0_26
[3] Ehrig, H.; Heckel, R.; Korff, M.; Löwe, M.; Ribeiro, L.; Wagner, A.; Corradini, A.; Rozenberg, G., Algebraic approaches to graph transformation—part II: Single pushout approach and comparison with double pushout approach, Handbook of Graph Grammars and Computing by Graph Transformation, ch. 4 (1997), Singapore: World Scientific, Singapore
[4] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theoretical Computer Science, 256, 1-2, 63-92 (2001) · Zbl 0973.68170 · doi:10.1016/S0304-3975(00)00102-X
[5] Löwe, M., Algebraic approach to single-pushout graph transformation, Theoretical Computer Science, 109, 181-224 (1993) · Zbl 0787.18001 · doi:10.1016/0304-3975(93)90068-5
[6] Rensink, A., Distefano, D.: Abstract graph transformation. In: Proc. of SVV 2005 (3rd International Workshop on Software Verification and Validation). ENTCS, vol. 157.1, pp. 39-59 (2005) · Zbl 1273.68196
[7] Robertson, N.; Seymour, P., Graph minors. XX. Wagner’s conjecture, Journal of Combinatorial Theory, Series B, 92, 2, 325-357 (2004) · Zbl 1061.05088 · doi:10.1016/j.jctb.2004.08.001
[8] Robertson, N., Seymour, P.: Graph minors. XXIII. Nash-Williams’ immersion conjecture (2006) (submitted for publication), http://www.math.princeton.edu/ pds/papers/GM23/GM23.pdf · Zbl 1216.05151
[9] Saksena, M.; Wibling, O.; Jonsson, B., Graph grammar modeling and verification of ad hoc routing protocols, Proc. of TACAS 2008, 18-32 (2008), Heidelberg: Springer, Heidelberg · Zbl 1134.68418
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.