Document Open Access Logo

Verification of Flat FIFO Systems

Authors Alain Finkel, M. Praveen

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.12.pdf
  • Filesize: 0.57 MB
  • 17 pages

Document Identifiers

Author Details

Alain Finkel
  • LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
  • UMI ReLaX, French-Indian research laboratory in computer sciences, Chennaï, India
M. Praveen
  • Chennai Mathematical Institute, India
  • UMI ReLaX, French-Indian research laboratory in computer sciences, Chennaï, India

Funding

The work reported was carried out in the framework of ReLaX, UMI2000 (ENS Paris-Saclay, CNRS, Univ. Bordeaux, CMI, IMSc). This work was also supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS).
  • Praveen, M.: Partially supported by a grant from the Infosys foundation.

Cite AsGet BibTex

Alain Finkel and M. Praveen. Verification of Flat FIFO Systems. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.12

Abstract

The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
Keywords
  • Infinite state systems
  • FIFO
  • counters
  • flat systems
  • reachability
  • termination
  • complexity

Metrics

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

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 in System Design, 25(1):39-65, 2004. URL: https://doi.org/10.1023/B:FORM.0000033962.51898.1a.
  2. Aurore Annichini, Ahmed Bouajjani, and Mihaela Sighireanu. TReX: A Tool for Reachability Analysis of Complex Systems. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, Computer Aided Verification, pages 368-372, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  3. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. FAST: Fast Acceleration of Symbolic Transition systems. In Warren A. Hunt, Jr and Fabio Somenzi, editors, Proceedings of the 15th International Conference on Computer Aided Verification (CAV'03), volume 2725 of Lecture Notes in Computer Science, pages 118-121, Boulder, Colorado, USA, July 2003. Springer. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-cav03.ps.
  4. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Philippe Schnoebelen. Flat acceleration in symbolic model checking. In Doron A. Peled and Yih-Kuen Tsay, editors, Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 474-488, Taipei, Taiwan, October 2005. Springer. URL: https://doi.org/10.1007/11562948_35.
  5. Bernard Boigelot. Domain-specific regular acceleration. STTT, 14(2):193-206, 2012. URL: https://doi.org/10.1007/s10009-011-0206-x.
  6. Bernard Boigelot, Patrice Godefroid, Bernard Willems, and Pierre Wolper. The Power of QDDs (Extended Abstract). In Pascal Van Hentenryck, editor, Static Analysis, 4th International Symposium, SAS '97, Paris, France, September 8-10, 1997, Proceedings, volume 1302 of Lecture Notes in Computer Science, pages 172-186. Springer, 1997. URL: https://doi.org/10.1007/BFb0032741.
  7. Ahmed Bouajjani and Peter Habermehl. Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations. Theor. Comput. Sci., 221(1-2):211-250, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00033-X.
  8. Zakaria Bouziane and Alain Finkel. Cyclic Petri Net Reachability Sets are Semi-Linear Effectively Constructible. In Faron Moller, editor, Proceedings of the 2nd International Workshop on Verification of Infinite State Systems (INFINITY'97), volume 9 of Electronic Notes in Theoretical Computer Science, pages 15-24, Bologna, Italy, July 1997. Elsevier Science Publishers. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-infinity97.pdf.
  9. Marius Bozga, Radu Iosif, and Filip Konecný. Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops. CoRR, abs/1307.5321, 2013. URL: http://arxiv.org/abs/1307.5321.
  10. Marius Bozga, Radu Iosif, Filip Konecný, and Tomás Vojnar. Tool Demonstration of the FLATA Counter Automata Toolset. In Andrei Voronkov, Laura Kovács, and Nikolaj Bjørner, editors, Second International Workshop on Invariant Generation, WING 2009, York, UK, March 29, 2009 and Third International Workshop on Invariant Generation, WING 2010, Edinburgh, UK, July 21, 2010, volume 1 of EPiC Series in Computing, page 75. EasyChair, 2010. URL: http://www.easychair.org/publications/paper/51875.
  11. 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.
  12. Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, and Gianluigi Zavattaro. Choreography and Orchestration Conformance for System Design. In Paolo Ciancarini and Herbert Wiklicky, editors, Coordination Models and Languages, 8th International Conference, COORDINATION 2006, Bologna, Italy, June 14-16, 2006, Proceedings, volume 4038 of Lecture Notes in Computer Science, pages 63-81. Springer, 2006. URL: https://doi.org/10.1007/11767954_5.
  13. Gérard Cécé and Alain Finkel. Verification of Programs with Half-Duplex Communication. Information and Computation, 202(2):166-190, November 2005. URL: https://doi.org/10.1016/j.ic.2005.05.006.
  14. Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Model-checking Counting Temporal Logics on Flat Structures. In 28th International Conference on Concurrency Theory, CONCUR 2017, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  15. S. Demri, A. Finkel, V. Goranko, and G. van Drimmelen. Towards a Model-Checker for Counter Systems. In Susanne Graf and Wenhui Zhang, editors, Automated Technology for Verification and Analysis, pages 493-507, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  16. Stéphane Demri, Amit Dhar, and Arnaud Sangnier. Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic. Theoretical Computer Science, 2017. Special issue of RP'14, to appear. Google Scholar
  17. Stéphane Demri, Amit Kumar Dhar, and Arnaud Sangnier. On the Complexity of Verifying Regular Properties on Flat Counter Systems. In Fedor V. Fomin, Rūsiņš Freivalds, Marta Kwiatkowska, and David Peleg, editors, Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP'13) - Part II, volume 7966 of Lecture Notes in Computer Science, pages 162-173, Riga, Latvia, July 2013. Springer. URL: https://doi.org/10.1007/978-3-642-39212-2_17.
  18. Stéphane Demri, Amit Kumar Dhar, and Arnaud Sangnier. Taming past LTL and flat counter systems. Inf. Comput., 242:306-339, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.007.
  19. Stéphane Demri, Alain Finkel, Valentin Goranko, and Govert van Drimmelen. Model-checking CTLsuperscript* 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.
  20. Frank Drewes and Jérôme Leroux. Structurally Cyclic Petri Nets. Logical Methods in Computer Science, 11(4), 2015. URL: https://doi.org/10.2168/LMCS-11(4:15)2015.
  21. Javier Esparza, Pierre Ganty, and Rupak Majumdar. A Perfect Model for Bounded Verification. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, LICS '12, pages 285-294, Washington, DC, USA, 2012. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2012.39.
  22. Alain Finkel. Structuration des systèmes de transitions: applications au contrôle du parallélisme par files fifo, Thèse d'Etat. PhD thesis, Université Paris-Sud, Orsay, 1986. Google Scholar
  23. Alain Finkel and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. Logical Methods in Computer Science, 8(3:28), September 2012. URL: https://doi.org/10.2168/LMCS-8(3:28)2012.
  24. Alain Finkel and Étienne Lozes. Synchronizability of Communicating Finite State Machines is not Decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Anca Muscholl, and Fabian Kuhn, editors, Proceedings of the 44th International Colloquium on Automata, Languages and Programming (ICALP'17), volume 80 of Leibniz International Proceedings in Informatics, pages 122:1-122:14, Warsaw, Poland, July 2017. Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.122.
  25. Alain Finkel, S. Purushothaman Iyer, and Grégoire Sutre. Well-Abstracted Transition Systems: Application to FIFO Automata. Information and Computation, 181(1):1-31, February 2003. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FPS-ICOMP.ps.
  26. 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.
  27. Christoph Haase. On the complexity of model checking counter automata. PhD thesis, University of Oxford, UK, 2012. Google Scholar
  28. Radu Iosif and Arnaud Sangnier. How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property? In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 89-105, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_6.
  29. 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.
  30. Julien Lange and Nobuko Yoshida. Verifying Asynchronous Interactions via Communicating Session Automata. CoRR, abs/1901.09606, 2019. URL: http://arxiv.org/abs/1901.09606.
  31. Christos H. Papadimitriou. On the Complexity of Integer Programming. J. ACM, 28(4):765-768, October 1981. URL: https://doi.org/10.1145/322276.322287.
  32. Gregoire Sutre. Personal communication, 2018. Google Scholar
  33. Gregor von Bochmann. Communication protocols and error recovery procedures. Operating Systems Review, 9(3):45-50, 1975. Google Scholar
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 Imprint Privacy Contact