Document Open Access Logo

On Flat Lossy Channel Machines

Author Philippe Schnoebelen

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.37.pdf
  • Filesize: 0.61 MB
  • 22 pages

Document Identifiers

Author Details

Philippe Schnoebelen
  • LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay

Funding

Supported by ANR project BRAVAS (grant ANR-17-CE40-0028).

Acknowledgements

We thank A. Finkel who raised the issue of flatness in lossy channel systems. We also thank J. Leroux and S. Halfon for useful comments that helped improve this paper.

Cite AsGet BibTex

Philippe Schnoebelen. On Flat Lossy Channel Machines. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 37:1-37:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.37

Abstract

We show that reachability, repeated reachability, nontermination and unboundedness are NP-complete for Lossy Channel Machines that are flat, i.e., with no nested cycles in the control graph. The upper complexity bound relies on a fine analysis of iterations of lossy channel actions and uses compressed word techniques for efficiently reasoning with paths of exponential lengths. The lower bounds already apply to acyclic or single-path machines.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Infinite state systems
  • Automated verification
  • Flat systems
  • Lossy channels

Metrics

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

References

  1. P. A. Abdulla, K. Čerāns, B. Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1/2):109-127, 2000. URL: https://doi.org/10.1006/inco.1999.2843.
  2. P. A. Abdulla, A. Collomb-Annichini, A. Bouajjani, and B. 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.
  3. P. A. Abdulla, J. Deneux, J. Ouaknine, and J. Worrell. Decidability and complexity results for timed automata via channel machines. In Proc. ICALP 2005, volume 3580 of Lecture Notes in Computer Science, pages 1089-1101. Springer, 2005. URL: https://doi.org/10.1007/11523468_88.
  4. P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. URL: https://doi.org/10.1006/inco.1996.0053.
  5. B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. Formal Methods in System Design, 14(3):237-255, 1999. URL: https://doi.org/10.1023/A:1008719024240.
  6. B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. CAV '94, volume 818 of Lecture Notes in Computer Science, pages 55-67. Springer, 1994. URL: https://doi.org/10.1007/3-540-58179-0_43.
  7. A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theoretical Computer Science, 221(1-2):211-250, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00033-X.
  8. M. Bozga, R. Iosif, and F. Konecný. Safety problems are NP-complete for flat integer programs with octagonal loops. In Proc. VMCAI 2014, volume 8318 of Lecture Notes in Computer Science, pages 242-261. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54013-4_14.
  9. M. Bozga, R. Iosif, and Y. Lakhnech. Flat parametric counter automata. Fundamenta Informaticae, 91(2):275-303, 2009. URL: https://doi.org/10.3233/FI-2009-0044.
  10. D. Brand and P. Zafiropulo. On communicating finite-state machines. JACM, 30(2):323-342, 1983. URL: https://doi.org/10.1145/322374.322380.
  11. G. Cécé, A. Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20-31, 1996. URL: https://doi.org/10.1006/inco.1996.0003.
  12. P. Cégielski, I. Guessarian, Y. Lifshits, and Y. V. Matiyasevich. Window subsequence problems for compressed texts. In Proc. CSR 2006, volume 3967 of Lecture Notes in Computer Science, pages 127-136. Springer, 2006. URL: https://doi.org/10.1007/11753728_15.
  13. P. Chambart and Ph. Schnoebelen. The ordinal recursive complexity of lossy channel systems. In Proc. LICS 2008, pages 205-216. IEEE Comp. Soc. Press, 2008. URL: https://doi.org/10.1109/LICS.2008.47.
  14. P. Chambart and Ph. Schnoebelen. Toward a compositional theory of leftist grammars and transformations. In Proc. FOSSACS 2010, volume 6014 of Lecture Notes in Computer Science, pages 237-251. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_17.
  15. H. Comon and Y. Jurski. Multiple counters automata, safety analysis, and Presburger arithmetic. In Proc. CAV '98, volume 1427 of Lecture Notes in Computer Science, pages 268-279. Springer, 1998. URL: https://doi.org/10.1007/BFb0028751.
  16. N. Decker, P. Habermehl, M. Leucker, A. Sangnier, and D. Thoma. Model-checking counting temporal logics on flat structures. In Proc. CONCUR 2017, volume 85 of Leibniz International Proceedings in Informatics, pages 29:1-29:17. Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.29.
  17. S. Demri, A. K. Dhar, and A. Sangnier. Taming past LTL and flat counter systems. Information and Computation, 242:306-339, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.007.
  18. S. Demri, A. Finkel, V. Goranko, and G. 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.
  19. S. Demri, F. Laroussinie, and Ph. Schnoebelen. A parametric analysis of the state explosion problem in model checking. Journal of Computer and System Sciences, 72(4):547-575, 2006. URL: https://doi.org/10.1016/j.jcss.2005.11.003.
  20. J. Esparza, P. Ganty, and R. Majumdar. A perfect model for bounded verification. In Proc. LICS 2012, pages 285-294. IEEE Comp. Soc. Press, 2012. URL: https://doi.org/10.1109/LICS.2012.39.
  21. A. Finkel. Decidability of the termination problem for completely specificied protocols. Distributed Computing, 7(3):129-135, 1994. URL: https://doi.org/10.1007/BF02277857.
  22. A. Finkel and M. Praveen. Verification of flat FIFO systems. In Proc. CONCUR 2019, volume 140 of Leibniz International Proceedings in Informatics, pages 12:1-12:17. Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.12.
  23. A. Finkel and M. Praveen. Verification of flat FIFO systems. Logical Methods in Comp. Science, 16(4), 2020. Google Scholar
  24. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  25. L. Fribourg and H. Olsén. A decompositional approach for computing least fixed-points of datalog programs with 𝒵-counters. Constraints, 2(3/4):305-335, 1997. URL: https://doi.org/10.1023/A:1009747629591.
  26. D. Gabelaia, A. Kurucz, F. Wolter, and M. Zakharyaschev. Non-primitive recursive decidability of products of modal logics with expanding domains. Annals of Pure and Applied Logic, 142(1-3):245-268, 2006. URL: https://doi.org/10.1016/j.apal.2006.01.001.
  27. P. Ganty and R. Iosif. Interprocedural reachability for flat integer programs. In Proc. FCT 2015, volume 9210 of Lecture Notes in Computer Science, pages 133-145. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22177-9_11.
  28. J. Goubault-Larrecq, S. Halfon, P. Karandikar, K. Narayan Kumar, and Ph. Schnoebelen. The ideal approach to computing closed subsets in well-quasi-orderings. In Well Quasi-Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends in Logic, chapter 3, pages 55-105. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-30229-0_3.
  29. Ch. Haase, S. Schmitz, and Ph. Schnoebelen. The power of priority channel systems. Logical Methods in Comp. Science, 10(4:4), 2014. URL: https://doi.org/10.2168/LMCS-10(4:4)2014.
  30. J. Hopcroft and J.-J. Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8(2):135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  31. P. Karandikar and Ph. Schnoebelen. Generalized Post embedding problems. Theory of Computing Systems, 56(4):697-716, 2015. URL: https://doi.org/10.1007/s00224-014-9561-9.
  32. Ch. Köcher. Reachability problems on partially lossy queue automata. In Proc. RP 2019, volume 11674 of Lecture Notes in Computer Science, pages 149-163. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30806-3_12.
  33. L. Kuhtz and B. Finkbeiner. Weak Kripke structures and LTL. In Proc. CONCUR 2011, volume 6901 of Lecture Notes in Computer Science, pages 419-433. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_28.
  34. S. Lasota and I. Walukiewicz. Alternating timed automata. ACM Trans. Computational Logic, 9(2), 2008. URL: https://doi.org/10.1145/1342991.1342994.
  35. J. Leroux, V. Penelle, and G. Sutre. The context-freeness problem is coNP-complete for flat counter systems. In Proc. ATVA 2014, volume 8837 of Lecture Notes in Computer Science, pages 248-263. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11936-6_19.
  36. J. Leroux and G. Sutre. Flat counter automata almost everywhere! In Proc. ATVA 2005, volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005. URL: https://doi.org/10.1007/11562948_36.
  37. M. Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241-299, 2012. URL: https://doi.org/10.1515/gcc-2012-0016.
  38. N. Markey and Ph. Schnoebelen. A PTIME-complete matching problem for SLP-compressed words. Information Processing Letters, 90(1):3-6, 2004. URL: https://doi.org/10.1016/j.ipl.2004.01.002.
  39. S. Schmitz. Complexity hierarchies beyond Elementary. ACM Trans. Computation Theory, 8(1), 2016. URL: https://doi.org/10.1145/2858784.
  40. S. Schmitz and Ph. Schnoebelen. Multiply-recursive upper bounds with Higman’s lemma. In Proc. ICALP 2011, volume 6756 of Lecture Notes in Computer Science, pages 441-452. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_35.
  41. Ph. Schnoebelen. Lossy counter machines decidability cheat sheet. In Proc. RP 2010, volume 6227 of Lecture Notes in Computer Science, pages 51-75. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15349-5_4.
  42. B. Vauquelin and P. Franchi-Zannettacci. Automates à file. Theoretical Computer Science, 11(2):221-225, 1980. URL: https://doi.org/10.1016/0304-3975(80)90047-X.
  43. T. Yamamoto, H. Bannai, S. Inenaga, and M. Takeda. Faster subsequence and don't-care pattern matching on compressed texts. In Proc. CPM 2011, volume 6661 of Lecture Notes in Computer Science, pages 309-322. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21458-5_27.
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