zbMATH — the first resource for mathematics

Forward analysis for WSTS. III: Karp-Miller trees. (English) Zbl 07215292
Summary: This paper is a sequel of [A. Finkel and J. Goubault-Larrecq, LIPIcs – Leibniz Int. Proc. Inform. 3, 433–444 (2009; Zbl 1236.68183)] and [A. Finkel and J. Goubault-Larrecq, Log. Methods Comput. Sci. 8, No. 3, Paper No. 28, 35 p. (2012; Zbl 1248.68329)]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downward-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural effectiveness assumptions, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.
03B70 Logic in computer science
68 Computer science
Full Text: Link arXiv
[1] Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, and Bengt Jonsson. Using forward reachability analysis for verification of lossy channel systems.Formal Methods in System · Zbl 1073.68675
[2] Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. InProc. 11thAnnual IEEE Symposium on Logic in Computer
[3] Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains.Inf. Comput., 160(1-2):109-127, 2000. · Zbl 1046.68567
[4] Mohamed Faouzi Atig and Peter Habermehl. On Yen’s path logic for Petri nets.International Journal of Foundations of Computer Science, 22(4):783-799, 2011. · Zbl 1230.68153
[5] Parosh Aziz Abdulla and Bengt Jonsson. Undecidable verification problems for programs with unreliable channels. InProc.21stInternational Colloquium on Automata, Languages and Programming (ICALP), pages 316-327, 1994. · Zbl 1418.68123
[6] Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen. On computing fixpoints in wellstructured regular model checking, with applications to lossy channel systems. InProc.13th · Zbl 1165.68397
[7] Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq. Forward analysis for WSTS, part III: Karp-Miller trees. InProc.37thIARCS Annual Conference on Foundations of Software · Zbl 1248.68352
[8] Michael Blondin, Alain Finkel, and Pierre McKenzie. Well behaved transition systems.Logical Methods in Computer Science, 13(3), 2017. · Zbl 06790161
[9] Michael Blondin, Alain Finkel, and Pierre McKenzie. Handling infinitely branching wellstructured transition systems.Information and Computation, 258:28-49, 2018. · Zbl 1383.68054
[10] R´emi Bonnet, Alain Finkel, and M. Praveen. Extending the Rackoff technique to affine nets. InProc. IARCS Annual Conference on Foundations of Software Technology and Theoretical · Zbl 1354.68190
[11] Aaron R. Bradley and Zohar Manna.The calculus of computation - Decision procedures with applications to verification. Springer, 2007. · Zbl 1126.03001
[12] Robert Bonnet. On the cardinality of the set of initial intervals of a partially ordered set. In Infinite and finite sets: to Paul Erd˝os on his60thbirthday, pages 189-198. North-Holland, 1975.
[13] Nathalie Bertrand and Philippe Schnoebelen. Computable fixpoints in well-structured symbolic model checking.Formal Methods in System Design, 43(2):233-267, 2013. · Zbl 1291.68247
[14] Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Forward analysis and model checking for trace bounded WSTS. InProc.32ndInternational Conference on Applications and Theory of · Zbl 1343.68162
[15] Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Forward analysis and model checking for trace bounded WSTS.Theor. Comput. Sci., 637:1-29, 2016. · Zbl 1343.68162
[16] Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. InProc.25thInternational Colloquium Automata, Languages and Programming
[17] Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In Proc.14thAnnual IEEE Symposium on Logic in Computer Science (LICS), pages 352-359, 1999.
[18] E. Allen Emerson and Kedar S. Namjoshi. On model checking for non-deterministic infinite-state systems. InProc.13thIEEE Symposium on Logic in Computer Science (LICS), pages 70-80, · Zbl 0945.68523
[19] Javier Esparza. On the decidability of model checking for severalµ-calculi and Petri nets. InProc. 19thInternational Colloquium on Trees in Algebra and Programming (CAAP), pages 115-129, 1994. · Zbl 0938.03537
[20] Paul Erd˝os and Alfred Tarski. On families of mutually exclusive sets.Annals of Mathematics, 2(44):315-329, 1943.
[21] Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part I: Completions. In STACS’09, pages 433-444, Freiburg, Germany, 2009. Leibniz-Zentrum f¨ur Informatik, Intl. Proc. · Zbl 1236.68183
[22] Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: complete WSTS. Logical Methods in Computer Science, 8(3), 2012. · Zbl 1248.68329
[23] Finkel.Structuration des syst‘emes de transitions-applications au contrˆole du parall´elisme par Files FIFO. PhD thesis, Universit´e Paris Sud Orsay, 1986.
[24] Alain Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. InProc.14thInternational Colloquium on Automata, Languages and Programming · Zbl 0633.68052
[25] Alain Finkel. Reduction and covering of infinite reachability trees.Information and Computation, 89(2):144-179, 1990. · Zbl 0753.68073
[26] Emanuele Frittaion and Alberto Marcone. Reverse mathematics and initial intervals.Ann. Pure Appl. Logic, 165(3):858-879, 2014. · Zbl 1284.03137
[27] Alain Finkel, Pierre McKenzie, and Claudine Picaronny. A well-structured framework for analysing Petri net extensions.Information and Computation, 195(1-2):1-29, 2004. · Zbl 1101.68696
[28] Thomas Forster. A tutorial on countable ordinals. Available from the Web athttps://www. dpmms.cam.ac.uk/ tf/fundamentalsequence.pdf, November 2010. Read on Feb. 03, 2017.
[29] Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere!Theoretical Computer Science, 256(1-2):63-92, 2001. · Zbl 0973.68170
[30] Roland Fra¨ıss´e. Theory of relations.Studies in Logic and the Foundations of Mathematics, 118:1-456, 1986.
[31] Gilles Geeraerts, Alexander Heußner, M. Praveen, and Jean-Fran¸cois Raskin.ω-Petri nets: Algorithms and complexity.Fundamenta Informaticae, 137(1):29-60, 2015. · Zbl 1335.68172
[32] Jean Goubault-Larrecq. A constructive proof of the topological Kruskal theorem. InProc.38th International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 22-41, 2013. · Zbl 1403.03126
[33] Gilles Geeraerts, Jean-Fran¸cois Raskin, and Laurent Van Begin. Expand, enlarge and check: New algorithms for the coverability problem of WSTS.Journal of Computer and System Sciences, · Zbl 1105.68353
[34] Peter Habermehl. On the complexity of the linear-timeµ-calculus for Petri nets. InProc.18th International Conference on Application and Theory of Petri Nets (ICATPN), pages 102-116, 1997.
[35] Reiner H¨uchting, Rupak Majumdar, and Roland Meyer. Bounds on mobility. InProc.25th International Conference on Concurrency Theory (CONCUR), pages 357-371, 2014. · Zbl 1417.68132
[36] Serge Haddad and Denis Poitrenaud. Recursive Petri nets.Acta Informatica, 44(7-8):463-508, 2007. · Zbl 1133.68056
[37] Richard M. Karp and Raymond E. Miller. Parallel program schemata: a mathematical model for parallel computation. InProc. 8thAnnual Symposium on Switching and Automata Theory, pages 55-61. IEEE Computer Society, 1967.
[38] M. Kabil and M. Pouzet. Une extension d’un th´eor‘eme de P. Julien sur les ˆages de mots. Informatique th´eorique et applications, 26(5):449-482, 1992. · Zbl 0754.68067
[39] E. V. Kouzmin, Nikolay V. Shilov, and Valery A. Sokolov. Model checking mu-calculus in wellstructured transition systems. InProc.11thInternational Symposium on Temporal Representation
[40] J.D. Lawson, M. Mislove, and H. Priestley. Ordered sets with no infinite antichains.Discrete Mathematics, 63(2):225-230, 1987. · Zbl 0624.06001
[41] Rohit J. Parikh. On context-free languages.Journal of the ACM, 13(4):570-581, 1966. · Zbl 0154.25801
[42] Maurice Pouzet. Relations non reconstructibles par leurs restrictions.Journal of Combinatorial Theory, Series B, 26(1):22-34, 1979. · Zbl 0322.04002
[43] Moj˙zesz Presburger. ¨Uber die Vollst¨andigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.Comptes Rendus du1er · JFM 56.0825.04
[44] Maurice Pouzet and Nejib Zaguia. Dimension de Krull des ensembles ordonn´es.Discrete Mathematics, 53:173-192, 1985. · Zbl 0579.06002
[45] Fernando Rosa-Velardo and Mar´ıa Martos-Salgado. Multiset rewriting for the verification of depth-bounded processes with name binding.Inf. Comput., 215:68-87, 2012. · Zbl 1277.68204
[46] Fernando Rosa-Velardo, Mar´ıa Martos-Salgado, and David de Frutos-Escrig. Accelerations for the coverability set of Petri nets with names.Fundamenta Informaticae, 113(3-4):313-341, 2011. · Zbl 1248.68357
[47] Philippe Schnoebelen. Lossy counter machines decidability cheat sheet. InProc.4thInternational Workshop on Reachability Problems (RP), pages 51-75, 2010. · Zbl 1287.68101
[48] R¨udiger Valk. Self-modifying nets, a natural extension of Petri nets. InProc.5thInternational Colloquium on Automata, Languages and Programming (ICALP), pages 464-476, 1978.
[49] Kumar N. Verma and Jean Goubault-Larrecq. Karp-Miller trees for a branching extension of VASS.Discrete Mathematics & Theoretical Computer Science, 7(1):217-230, 2005. · Zbl 1152.68462
[50] R¨udiger Valk and Matthias Jantzen. The residue of vector sets with applications to decidability problems in Petri nets.Acta Informatica, 21:643-674, 1985. · Zbl 0545.68051
[51] Hsu-Chun Yen. A unified approach for deciding the existence of certain Petri net paths.Information and Computation, 96(1):119-137, 1992. · Zbl 0753.68078
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.