Document Open Access Logo

Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems (Invited Talk)

Author Philippe Schnoebelen

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.85.pdf
  • Filesize: 345 kB
  • 4 pages

Document Identifiers

Author Details

Philippe Schnoebelen

Cite AsGet BibTex

Philippe Schnoebelen. Ideal-Based Algorithms for the Symbolic Verification of Well-Structured Systems (Invited Talk). In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 85:1-85:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.MFCS.2017.85

Abstract

We explain how the downward-closed subsets of a well-quasi-ordering (X,\leq) can be represented via the ideals of X and how this leads to simple and efficient algorithms for the verification of well-structured systems.
Keywords
  • Well-structured systems and verification
  • Order theory

Metrics

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

References

  1. P. A. Abdulla. Well (and better) quasi-ordered transition systems. Bull. Symbolic Logic, 16(4):457-515, 2010. URL: http://dx.doi.org/10.2178/bsl/1294171129.
  2. 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: http://dx.doi.org/10.1006/inco.1999.2843.
  3. 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: http://dx.doi.org/10.1023/B:FORM.0000033962.51898.1a.
  4. P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. URL: http://dx.doi.org/10.1006/inco.1996.0053.
  5. B. Bérard, F. Cassez, S. Haddad, D. Lime, and O. H. Roux. The expressive power of time Petri nets. Theoretical Computer Science, 474, 2012. URL: http://dx.doi.org/10.1016/j.tcs.2012.12.005.
  6. M. Blondin, A. Finkel, and P. McKenzie. Well behaved transition systems. arXiv:1608.02636 [cs.LO], August 2016. To appear in Logical Meth. Comp. Sci. URL: http://arxiv.org/abs/1608.02636.
  7. 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: http://dx.doi.org/10.1006/inco.1996.0003.
  8. C. Dufourd, P. Jančar, and Ph. Schnoebelen. Boundedness of Reset P/T nets. In CONCUR '99, LNCS 1644, pages 301-310. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-48523-6_27.
  9. A. Finkel. The ideal theory for WSTS. In RP 2016, LNCS 9899, pages 1-22. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-45994-3_1.
  10. A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part I: Completions. In STACS 2009, LIPIcs 3, pages 433-444. Leibniz-Zentrum für Informatik, 2009. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2009.1844.
  11. A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Comp. Science, 8(4), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:28)2012.
  12. A. Finkel, P. McKenzie, and C. Picaronny. A well-structured framework for analysing Petri nets extensions. Information and Computation, 195(1-2):1-29, 2004. URL: http://dx.doi.org/10.1016/j.ic.2004.01.005.
  13. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. URL: http://dx.doi.org/10.1016/S0304-3975(00)00102-X.
  14. G. Geeraerts, J.-F. Raskin, and L. Van Begin. Expand, enlarge and check: New algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 72(1):180-203, 2006. URL: http://dx.doi.org/10.1016/j.jcss.2005.09.001.
  15. 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 preparation, 2017. Google Scholar
  16. J. Goubault-Larrecq and S. Schmitz. Deciding piecewise testable separability for regular tree languages. In ICALP 2016, LIPIcs 55, pages 97:1-97:15. Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.97.
  17. Ch. Haase, S. Schmitz, and Ph. Schnoebelen. The power of priority channel systems. Logical Methods in Comp. Science, 10(4:4), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(4:4)2014.
  18. T. A. Henzinger, R. Majumdar, and J.-F. Raskin. A classification of symbolic transition systems. ACM Trans. Computational Logic, 6(1):1-32, 2005. URL: http://dx.doi.org/10.1145/1042038.1042039.
  19. R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147-195, 1969. URL: http://dx.doi.org/10.1016/S0022-0000(69)80011-5.
  20. R. Lazić, T. Newcomb, J. Ouaknine, A. W. Roscoe, and J. Worrell. Nets with tokens which carry data. Fundamenta Informaticae, 88(3):251-274, 2008. Google Scholar
  21. R. Lazić and S. Schmitz. The complexity of coverability in ν-Petri nets. In LICS 2016, pages 467-476. ACM Press, 2016. URL: http://dx.doi.org/10.1145/2933575.2933593.
  22. J. Leroux and S. Schmitz. Ideal decompositions for vector addition systems. In STACS 2016, LIPIcs 47, pages 1:1-1:13. Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2016.1.
  23. S. Schmitz and Ph. Schnoebelen. The power of well-structured systems. In CONCUR 2013, LNCS 8052, pages 5-24. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40184-8_2.
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