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

Author Philippe Schnoebelen

Thumbnail 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)


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.
  • Well-structured systems and verification
  • Order theory


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


  1. P. A. Abdulla. Well (and better) quasi-ordered transition systems. Bull. Symbolic Logic, 16(4):457-515, 2010. URL:
  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:
  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:
  4. P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. URL:
  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:
  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:
  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:
  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:
  9. A. Finkel. The ideal theory for WSTS. In RP 2016, LNCS 9899, pages 1-22. Springer, 2016. URL:
  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:
  11. A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: Complete WSTS. Logical Methods in Comp. Science, 8(4), 2012. URL:
  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:
  13. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. URL:
  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:
  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:
  17. Ch. Haase, S. Schmitz, and Ph. Schnoebelen. The power of priority channel systems. Logical Methods in Comp. Science, 10(4:4), 2014. URL:
  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:
  19. R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147-195, 1969. URL:
  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:
  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:
  23. S. Schmitz and Ph. Schnoebelen. The power of well-structured systems. In CONCUR 2013, LNCS 8052, pages 5-24. Springer, 2013. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail