×

zbMATH — the first resource for mathematics

Verification of flat FIFO systems. (English) Zbl 07269251
Summary: The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, 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 machines, generalizing similar existing results for flat counter machines. We also show that reachability is NP-complete for flat lossy FIFO machines and for flat front-lossy FIFO machines. We construct a trace-flattable system of many counter machines communicating via rendez-vous that is bisimilar to a given flat FIFO machine, which allows to model-check the original flat FIFO machine. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO machines based on analysis of flat sub-machines.
MSC:
03B70 Logic in computer science
68 Computer science
Software:
FAST; FLATA; TREX
PDF BibTeX XML Cite
Full Text: Link arXiv
References:
[1] Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. InCAV, volume 1427 ofLecture Notes in Computer Science, pages 305-318. Springer, 1998.
[2] 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. · Zbl 1073.68675
[3] Aurore Annichini, Ahmed Bouajjani, and Mihaela Sighireanu. Trex: A tool for reachability analysis of complex systems. In G´erard Berry, Hubert Comon, and Alain Finkel, editors,Computer Aided · Zbl 0991.68645
[4] S´ebastien Bardin, Alain Finkel, J´erˆome Leroux, and Laure Petrucci. FAST: Fast Acceleration of Symbolic Transition systems. In Warren A. Hunt, Jr and Fabio Somenzi, editors,Proceedings of the
[5] S´ebastien Bardin, Alain Finkel, J´erˆome Leroux, and Laure Petrucci. FAST: Acceleration from theory to practice.International Journal on Software Tools for Technology Transfer, 10(5):401-424, October 2008.
[6] S´ebastien Bardin, Alain Finkel, J´erˆome 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 ofLecture Notes in Computer Science, pages 474-488, Taipei, Taiwan, October 2005. Springer. · Zbl 1170.68507
[7] Bernard Boigelot. Domain-specific regular acceleration.STTT, 14(2):193-206, 2012.
[8] 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 ofLecture Notes in Computer Science, pages 172-186. Springer, 1997.
[9] Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded reachability problems are decidable in FIFO machines. In Igor Konnov and Laura Kovacs, editors,Proceedings of the 31st International Conference
[10] 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. · Zbl 0933.68089
[11] 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 ofElectronic Notes in Theoretical Computer Science, pages 15-24, Bologna, Italy, July 1997. Elsevier Science Publishers. · Zbl 0907.68131
[12] Marius Bozga, Radu Iosif, and Filip Konecn´y. Safety problems are np-complete for flat integer programs with octagonal loops.CoRR, abs/1307.5321, 2013. · Zbl 1428.68160
[13] Marius Bozga, Radu Iosif, Filip Konecn´y, and Tom´as Vojnar. Tool demonstration of the FLATA counter automata toolset. In Andrei Voronkov, Laura Kov´acs, and Nikolaj Bjørner, editors,Second International
[14] Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines.J. ACM, 30(2):323-342, 1983. · Zbl 0512.68039
[15] 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, · Zbl 0983.68521
[16] G´erard C´ec´e and Alain Finkel. Verification of programs with half-duplex communication.Information and Computation, 202(2):166-190, November 2005. · Zbl 1101.68676
[17] Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Modelchecking counting temporal logics on flat structures. In28th International Conference on Concurrency · Zbl 1442.68105
[18] 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. · Zbl 1161.68563
[19] St´ephane 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.
[20] St´ephane Demri, Amit Kumar Dhar, and Arnaud Sangnier. On the complexity of verifying regular properties on flat counter systems. In Fedor V. Fomin, R¯usi¸nˇs Freivalds, Marta Kwiatkowska, and David Peleg, editors,Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP’13) - Part II, volume 7966 ofLecture Notes in Computer Science, pages 162-173, Riga, Latvia, July 2013. Springer. · Zbl 1334.68130
[21] St´ephane Demri, Amit Kumar Dhar, and Arnaud Sangnier. Taming past LTL and flat counter systems. Inf. Comput., 242:306-339, 2015. · Zbl 1378.68112
[22] St´ephane 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. · Zbl 1242.68157
[23] Frank Drewes and J´erˆome Leroux. Structurally cyclic petri nets.Logical Methods in Computer Science, 11(4), 2015.
[24] 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. · Zbl 1362.68168
[25] Alain Finkel.Structuration des syst‘emes de transitions: applications au contrˆole du parall´elisme par files fifo, Th‘ese d’Etat. PhD thesis, Universit´e Paris-Sud, Orsay, 1986.
[26] Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS.Logical Methods in Computer Science, 8(3:28), September 2012. · Zbl 1248.68329
[27] Alain Finkel and ´Etienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Anca Muscholl, and Fabian Kuhn, editors,Proceedings of · Zbl 1442.68138
[28] Alain Finkel, S. Purushothaman Iyer, and Gr´egoire Sutre. Well-abstracted transition systems: Application to FIFO automata.Information and Computation, 181(1):1-31, February 2003. · Zbl 1054.68092
[29] Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundam. Inform., 80(1-3):147-167, 2007. · Zbl 1137.68447
[30] Christoph Haase.On the complexity of model checking counter automata. PhD thesis, University of Oxford, UK, 2012.
[31] 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 · Zbl 1398.68311
[32] Thierry J´eron and Claude Jard. Testing for unboundedness of FIFO channels.Theor. Comput. Sci., 113(1):93-117, 1993. · Zbl 0781.68085
[33] Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating session automata.CoRR, abs/1901.09606, 2019.
[34] Christos H. Papadimitriou. On the complexity of integer programming.J. ACM, 28(4):765-768, October 1981. · Zbl 0468.68050
[35] Sylvain Schmitz. Complexity hierarchies beyond elementary.TOCT, 8(1):3:1-3:36, 2016. · Zbl 1347.68162
[36] Philippe Schnoebelen. On flat lossy channel machines.CoRR, abs/2007.05269, 2020.
[37] Gregoire Sutre. Personal communication, 2018.
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.