Document Open Access Logo

Forward Analysis for WSTS, Part III: Karp-Miller Trees

Authors Michael Blondin, Alain Finkel, Jean Goubault-Larrecq

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.16.pdf
  • Filesize: 0.58 MB
  • 15 pages

Document Identifiers

Author Details

Michael Blondin
Alain Finkel
Jean Goubault-Larrecq

Cite As Get BibTex

Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.16

Abstract

This paper is a sequel of "Forward Analysis for WSTS, Part I: Completions" [STACS 2009, LZI Intl. Proc. in Informatics 3, 433–444] and "Forward Analysis for WSTS, Part II: Complete WSTS" [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downwards-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 assumptions on positive sequences, 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.

Subject Classification

Keywords
  • WSTS
  • model checking
  • coverability
  • Karp-Miller algorithm
  • ideals

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Proc. 11^th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 313-321, 1996. Google Scholar
  2. 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. Google Scholar
  3. Parosh Aziz Abdulla and Bengt Jonsson. Undecidable verification problems for programs with unreliable channels. In Proc. 21^st International Colloquium on Automata, Languages and Programming (ICALP), pages 316-327, 1994. Google Scholar
  4. Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen. On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems. In Proc. 13^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, (LPAR), pages 347-361, 2006. Google Scholar
  5. Nathalie Bertrand and Philippe Schnoebelen. Computable fixpoints in well-structured symbolic model checking. Formal Methods in System Design, 43(2):233-267, 2013. Google Scholar
  6. Michael Blondin, Alain Finkel, and Pierre McKenzie. Handling infinitely branching WSTS. In Proc. 41^st International Colloquium on Automata, Languages, and Programming (ICALP), pages 13-25, 2014. Google Scholar
  7. Michael Blondin, Alain Finkel, and Pierre McKenzie. Well behaved transition systems. Logical Methods in Computer Science, 2017 (accepted). Google Scholar
  8. Robert Bonnet. On the cardinality of the set of initial intervals of a partially ordered set. In Infinite and finite sets: to Paul Erdős on his 60^textth birthday, pages 189-198. North-Holland, 1975. Google Scholar
  9. Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Forward analysis and model checking for trace bounded WSTS. In Proc. 32^nd International Conference on Applications and Theory of Petri Nets, 2011. Google Scholar
  10. Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Forward analysis and model checking for trace bounded WSTS. Theor. Comput. Sci., 637:1-29, 2016. Google Scholar
  11. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In Proc. 25^th International Colloquium Automata, Languages and Programming (ICALP), pages 103-115, 1998. Google Scholar
  12. E. Allen Emerson and Kedar S. Namjoshi. On model checking for non-deterministic infinite-state systems. In Proc. 13^th IEEE Symposium on Logic in Computer Science (LICS), pages 70-80, 1998. Google Scholar
  13. Paul Erdős and Alfred Tarski. On families of mutually exclusive sets. Annals of Mathematics, 2(44):315-329, 1943. Google Scholar
  14. Javier Esparza. On the decidability of model checking for several μ-calculi and Petri nets. In Proc. 19^th International Colloquium on Trees in Algebra and Programming (CAAP), pages 115-129, 1994. Google Scholar
  15. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In Proc. 14^th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 352-359, 1999. Google Scholar
  16. Alain Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. In Proc. 14^th International Colloquium on Automata, Languages and Programming (ICALP), pages 499-508, 1987. Google Scholar
  17. Alain Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89(2):144-179, 1990. Google Scholar
  18. 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ür Informatik, Intl. Proc. in Informatics 3. Google Scholar
  19. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: complete WSTS. Logical Methods in Computer Science, 8(3), 2012. Google Scholar
  20. 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. Google Scholar
  21. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. Google Scholar
  22. Thomas Forster. A tutorial on countable ordinals. Available from the Web at https://www.dpmms.cam.ac.uk/~tf/fundamentalsequence.pdf, 2010. Read on Feb. 03, 2017.
  23. Roland Fraïssé. Theory of relations. Studies in Logic and the Foundations of Mathematics, 118:1-456, 1986. Google Scholar
  24. Gilles Geeraerts, Alexander Heußner, M. Praveen, and Jean-François Raskin. ω-Petri nets: Algorithms and complexity. Fundamenta Informaticae, 137(1):29-60, 2015. Google Scholar
  25. Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, enlarge and check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci., 72(1):180-203, 2006. URL: http://dx.doi.org/10.1016/j.jcss.2005.09.001.
  26. Serge Haddad and Denis Poitrenaud. Recursive Petri nets. Acta Inf., 44(7-8):463-508, 2007. Google Scholar
  27. Piotr Hofman, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke. Coverability trees for Petri nets with unordered data. In FoSSaCS, pages 445-461, 2016. Google Scholar
  28. Reiner Hüchting, Rupak Majumdar, and Roland Meyer. Bounds on mobility. In Proc. 25^th International Conference on Concurrency Theory (CONCUR), pages 357-371, 2014. Google Scholar
  29. Richard M. Karp and Raymond E. Miller. Parallel program schemata: a mathematical model for parallel computation. In Proc. 8^th Annual Symposium on Switching and Automata Theory, pages 55-61. IEEE Computer Society, 1967. Google Scholar
  30. E. V. Kouzmin, Nikolay V. Shilov, and Valery A. Sokolov. Model checking mu-calculus in well-structured transition systems. In Proc. 11^th International Symposium on Temporal Representation and Reasoning (TIME), pages 152-155, 2004. Google Scholar
  31. J.D. Lawson, M. Mislove, and H. Priestley. Ordered sets with no infinite antichains. Discrete Mathematics, 63(2):225-230, 1987. Google Scholar
  32. Rohit J. Parikh. On context-free languages. Journal of the ACM, 13(4):570-581, 1966. Google Scholar
  33. Maurice Pouzet. Relations non reconstructibles par leurs restrictions. Journal of Combinatorial Theory, Series B, 26(1):22-34, 1979. Google Scholar
  34. Maurice Pouzet and Nejib Zaguia. Dimension de Krull des ensembles ordonnés. Discrete Mathematics, 53:173-192, 1985. Google Scholar
  35. 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. Google Scholar
  36. 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. Google Scholar
  37. Philippe Schnoebelen. Lossy counter machines decidability cheat sheet. In Proc. 4^th International Workshop on Reachability Problems (RP), pages 51-75, 2010. Google Scholar
  38. Rüdiger Valk. Self-modifying nets, a natural extension of Petri nets. In Proc. 5^th International Colloquium on Automata, Languages and Programming (ICALP), pages 464-476, 1978. Google Scholar
  39. Rüdiger Valk and Matthias Jantzen. The residue of vector sets with applications to decidability problems in Petri nets. Acta Inf., 21:643-674, 1985. Google Scholar
  40. 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. Google Scholar
  41. Damien Zufferey, Thomas Wies, and Thomas A. Henzinger. Ideal abstractions for well-structured transition systems. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 445-460. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-27940-9_29.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact