Document Open Access Logo

Bounded Reachability Problems Are Decidable in FIFO Machines

Authors Benedikt Bollig, Alain Finkel, Amrita Suresh

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.49.pdf
  • Filesize: 0.61 MB
  • 17 pages

Document Identifiers

Author Details

Benedikt Bollig
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
Alain Finkel
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
Amrita Suresh
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France

Cite As Get BibTex

Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded Reachability Problems Are Decidable in FIFO Machines. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 49:1-49:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.49

Abstract

The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular channel belongs to a given bounded language). We prove, by reducing this model to a counter machine with restricted zero tests, that the rational-reachability problem (and by extension, control-state reachability, unboundedness, deadlock, etc.) is decidable. This class of machines subsumes input-letter-bounded machines, flat machines, linear FIFO nets, and monogeneous machines, for which some of these problems were already shown to be decidable. These theoretical results can form the foundations to build a tool to verify general FIFO machines based on the analysis of input-bounded machines.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • FIFO machines
  • reachability
  • underapproximation
  • counter machines

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, and Bengt Jonsson. Using forward reachability analysis for verification of lossy channel systems. Formal Methods Syst. Des., 25(1):39-65, 2004. URL: https://doi.org/10.1023/B:FORM.0000033962.51898.1a.
  2. C. Aiswarya, Paul Gastin, and K. Narayan Kumar. Verifying communicating multi-pushdown systems via split-width. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, volume 8837 of Lecture Notes in Computer Science, pages 1-17. Springer, 2014. Google Scholar
  3. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. FAST: Acceleration from theory to practice. International Journal on Software Tools for Technology Transfer, 10(5):401-424, October 2008. URL: https://doi.org/10.1007/s10009-008-0064-3.
  4. Jean Berstel. Transductions and context-free languages, volume 38 of Teubner Studienbücher : Informatik. Teubner, 1979. Google Scholar
  5. Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 372-391. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96142-2_23.
  6. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. URL: https://doi.org/10.1145/322374.322380.
  7. Gérard Cécé and Alain Finkel. Verification of programs with half-duplex communication. Inf. Comput., 202(2):166-190, 2005. URL: https://doi.org/10.1016/j.ic.2005.05.006.
  8. Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Forward analysis and model checking for trace bounded WSTS. In Lars M. Kristensen and Laure Petrucci, editors, Proceedings of the 32nd International Conference on Applications and Theory of Petri Nets (PETRI NETS'11), volume 6709 of Lecture Notes in Computer Science. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21834-7_4.
  9. Pierre Chambart and Philippe Schnoebelen. The ordinal recursive complexity of lossy channel systems. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, pages 205-216. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.47.
  10. Christian Choffrut. Relations over words and logic: A chronology. Bulletin of the EATCS, 89:159-163, 2006. Google Scholar
  11. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, pages 24-33. ACM, 2019. Google Scholar
  12. Stéphane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking CTL^* over flat Presburger counter systems. Journal of Applied Non-Classical Logics, 20(4):313-344, 2010. URL: https://doi.org/10.3166/jancl.20.313-344.
  13. Catherine Dufourd and Alain Finkel. Polynomial-Time Many-One Reductions for Petri Nets. In S. Ramesh and G. Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science, 17th Conference, volume 1346 of Lecture Notes in Computer Science, pages 312-326. Springer, 1997. URL: https://doi.org/10.1007/BFb0058039.
  14. Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pages 285-294. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.39.
  15. Alain Finkel. About monogeneous fifo Petri nets. In Proceedings of the 3rd International Conference on Applications and Theory of Petri Nets (APN'82), Varenna, Italy, September 1982. Google Scholar
  16. Alain Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3):129-135, 1994. URL: https://doi.org/10.1007/BF02277857.
  17. Alain Finkel and Annie Choquet. Simulation of linear fifo nets by Petri nets having a structured set of terminal markings. In Proceedings of the 8th International Conference on Applications and Theory of Petri Nets (APN'87), Zaragoza, Spain, June 1987. Google Scholar
  18. Alain Finkel and M. Praveen. Verification of flat FIFO systems. In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.12.
  19. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  20. Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundam. Inform., 80(1-3):147-167, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09.
  21. Seymour Ginsburg and Edwin H. Spanier. Bounded Algol-Like Languages. Transactions of the American Mathematical Society, 113(2):333-368, 1964. URL: http://www.jstor.org/stable/1994067.
  22. Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. On the k-synchronizability of systems. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, volume 12077 of Lecture Notes in Computer Science, pages 157-176. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_9.
  23. M. G. Gouda, E. M. Gurari, T. H. Lai, and L. E. Rosier. On deadlock detection in systems of communicating finite state machines. Comput. Artif. Intell., 6(3):209–228, July 1987. Google Scholar
  24. Alexander Heußner, Jérôme Leroux, Anca Muscholl, and Grégoire Sutre. Reachability analysis of communicating pushdown systems. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, volume 6014 of Lecture Notes in Computer Science, pages 267-281. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_19.
  25. Thierry Jéron. Testing for unboundedness of FIFO channels. In Christian Choffrut and Matthias Jantzen, editors, STACS 91, 8th Annual Symposium on Theoretical Aspects of Computer Science, volume 480 of Lecture Notes in Computer Science, pages 322-333. Springer, 1991. URL: https://doi.org/10.1007/BFb0020809.
  26. Thierry Jéron and Claude Jard. Testing for unboundedness of FIFO channels. Theor. Comput. Sci., 113(1):93-117, 1993. URL: https://doi.org/10.1016/0304-3975(93)90212-C.
  27. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Context-bounded analysis of concurrent queue systems. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, volume 4963 of Lecture Notes in Computer Science, pages 299-314. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_21.
  28. P. Madhusudan and Gennaro Parlato. The tree width of auxiliary storage. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pages 283-294. ACM, 2011. Google Scholar
  29. Ernst W. Mayr. An algorithm for the general petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. Google Scholar
  30. Gérard Memmi and Alain Finkel. An introduction to fifo nets-monogeneous nets: A subclass of fifo nets. Theor. Comput. Sci., 35:191-214, 1985. URL: https://doi.org/10.1016/0304-3975(85)90014-3.
  31. Bernard Vauquelin and Paul Franchi-Zannettacci. Automates a file. Theor. Comput. Sci., 11:221-225, 1980. URL: https://doi.org/10.1016/0304-3975(80)90047-X.
  32. Yao-Tin Yu and Mohamed G. Gouda. Unboundedness detection for a class of communicating finite-state machines. Inf. Process. Lett., 17(5):235-240, 1983. URL: https://doi.org/10.1016/0020-0190(83)90105-9.
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