Document Open Access Logo

Regular Separability of Well-Structured Transition Systems

Authors Wojciech Czerwinski , Slawomir Lasota , Roland Meyer , Sebastian Muskalla , K. Narayan Kumar, Prakash Saivasan

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.35.pdf
  • Filesize: 0.53 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Regular languages
  • Theory of computation → Parallel computing models
Keywords
  • regular separability
  • wsts
  • coverability languages
  • Petri nets

Metrics

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

Abstract

We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.

Cite As Get BibTex

Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.35

Author Details

Wojciech Czerwinski
  • University of Warsaw, Poland
Slawomir Lasota
  • University of Warsaw, Poland
Roland Meyer
  • TU Braunschweig, Germany
Sebastian Muskalla
  • TU Braunschweig, Germany
K. Narayan Kumar
  • Chennai Mathematical Institute and UMI RELAX, India
Prakash Saivasan
  • TU Braunschweig, Germany

Funding

  • Czerwinski, Wojciech: Supported by the Polish National Science Centre under grant 2016/21/D/ST6/01376.
  • Lasota, Slawomir: Partially supported by the European Research Council (ERC) project Lipa under the EU Horizon 2020 research and innovation programme (grant agreement No. 683080).
  • Narayan Kumar, K.: Partially supported by the Indo-French project AVeCSo, the Infosys Foundation, and DST-VR Project P-02/2014.

References

  1. P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In LICS, pages 313-321, 1996. Google Scholar
  2. P. A. Abdulla, G. Delzanno, and L. Van Begin. Comparing the expressive power of well-structured transition systems. In CSL, pages 99-114, 2007. Google Scholar
  3. P. A. Abdulla, G. Delzanno, O. Rezine, A. Sangnier, and R. Traverso. On the verification of timed ad hoc networks. In FORMATS, volume 6919 of LNCS, pages 256-270. Springer, 2011. Google Scholar
  4. P. A. Abdulla, J. Deneux, and P. Mahata. Multi-clock timed networks. In LICS, pages 345-354. IEEE, 2004. Google Scholar
  5. P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In LICS, pages 160-170. IEEE, 1993. Google Scholar
  6. M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. On the verification problem for weak memory models. In POPL, pages 7-18. ACM, 2010. Google Scholar
  7. M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. What’s decidable about weak memory models? In ESOP, volume 7211 of LNCS, pages 26-46. Springer, 2012. Google Scholar
  8. M. Blondin, A. Finkel, and P. McKenzie. Well behaved transition systems. Logical Methods in Computer Science, 13(3), 2017. Google Scholar
  9. M. Blondin, A. Finkel, and P McKenzie. Handling infinitely branching well-structured transition systems. Inf. Comput., 258:28-49, 2018. Google Scholar
  10. A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. In STACS, pages 323-333, 1999. Google Scholar
  11. L. Bozzelli and P. Ganty. Complexity analysis of the backward coverability algorithm for VASS. In RP, pages 96-109, 2011. Google Scholar
  12. D. Brand and P. Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. Google Scholar
  13. N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion, replication, and iteration in process calculi. In ICALP, volume 3142 of LNCS, pages 307-319. Springer, 2004. Google Scholar
  14. L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman. Regular separability of Parikh automata. In ICALP, pages 117:1-117:13, 2017. Google Scholar
  15. L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman. Separability of reachability sets of vector addition systems. In STACS 2017, pages 24:1-24:14, 2017. Google Scholar
  16. S. A. Cook. Soundness and completeness of an axiom system for program verification. SIAM J. Comput., 7(1):70-90, 1978. Google Scholar
  17. W. Czerwiński and S. Lasota. Regular separability of one counter automata. In LICS, pages 1-12, 2017. Google Scholar
  18. W. Czerwiński, S. Lasota, R. Meyer, S. Muskalla, K. Narayan Kumar, and P. Saivasan. Regular separability of well structured transition systems. CoRR, abs/1702.05334, 2018. URL: http://arxiv.org/abs/1702.05334.
  19. W. Czerwiński, W. Martens, and T. Masopust. Efficient separability of regular languages by subsequences and suffixes. In ICALP, pages 150-161, 2013. Google Scholar
  20. G. Delzanno and F. Rosa-Velardo. On the coverability and reachability languages of monotonic extensions of Petri nets. Theoretical Computer Science, 467:12-29, 2013. Google Scholar
  21. E. D'Osualdo. Verification of Message Passing Concurrent Systems. PhD thesis, University of Oxford, 2015. Google Scholar
  22. C. Dufourd, A. Finkel, and Ph. Schnoebelen. Reset nets between decidability and undecidability. In ICALP, volume 1443 of LNCS, pages 103-115. Springer, 1998. Google Scholar
  23. J. Esparza. Decidability and complexity of Petri net problems - an introduction. In Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, pages 374-428. Springer, 1998. Google Scholar
  24. A. Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. In ICALP, pages 499-508, 1987. Google Scholar
  25. A. Finkel. Reduction and covering of infinite reachability trees. Inf. Comput., 89(2):144-179, 1990. Google Scholar
  26. A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part I: completions. In STACS, pages 433-444, 2009. Google Scholar
  27. A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: complete WSTS. Logical Methods in Computer Science, 8(3), 2012. Google Scholar
  28. A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. Google Scholar
  29. P. Ganty, J.-F. Raskin, and L. Van Begin. A complete abstract interpretation framework for coverability properties of WSTS. In VMCAI, pages 49-64, 2006. Google Scholar
  30. W. Gasarch. A survey of recursive combinatorics. In Handbook of recursive mathematics, Vol. 2, volume 139 of Stud. Logic Found. Math., page 1041–1176. Amsterdam: North-Holland, 1998. Google Scholar
  31. 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. Google Scholar
  32. G. Geeraerts, J.-F. Raskin, and L. Van Begin. Well-Structured Languages. Acta Informatica, 44(3-4):249-288, 2007. Google Scholar
  33. M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, pages 471-482. ACM, 2010. Google Scholar
  34. H. B. Hunt III. On the decidability of grammar problems. Journal of the ACM, 29(2):429-447, 1982. Google Scholar
  35. P. Jancar. A note on well quasi-orderings for powersets. Inf. Process. Lett., 72(5-6):155-160, 1999. Google Scholar
  36. S. Joshi and B. König. Applying the graph minor theorem to the verification of graph transformation systems. In CAV, volume 5123 of LNCS, pages 214-226. Springer, 2008. Google Scholar
  37. M. Kabil and M. Pouzet. Une extension d'un théorème de P. Jullien sur les âges de mots. ITA, 26:449-484, 1992. Google Scholar
  38. E. Kopczynski. Invisible pushdown languages. In LICS, pages 867-872, 2016. Google Scholar
  39. D. Kozen. Automata and computability. Undergraduate texts in Computer Science. Springer, 1997. Google Scholar
  40. R. Lazic and S. Schmitz. The ideal view on rackoff’s coverability technique. In RP, pages 76-88, 2015. Google Scholar
  41. J. Leroux and S. Schmitz. Demystifying reachability in vector addition systems. In LICS, pages 56-67, 2015. Google Scholar
  42. R. J. Lipton. The reachability problem requires exponential space. Technical report, Yale University, Department of Computer Science, 1976. Google Scholar
  43. Z. Manna and A. Pnueli. Temporal verification of reactive systems - safety. Springer, 1995. Google Scholar
  44. A. Marcone. Foundations of bqo theory. Transactions of the American Mathematical Society, 345(2):641-660, 1994. Google Scholar
  45. M. Martos-Salgado and F. Rosa-Velardo. Dynamic networks of timed Petri nets. In Petri nets, pages 294-313, 2014. Google Scholar
  46. R. Mayr. Undecidable problems in unreliable computations. Theor. Comput. Sci., 1-3(297):337-354, 2003. Google Scholar
  47. R. Meyer. On boundedness in depth in the pi-calculus. In TCS, volume 273 of IFIP, pages 477-489. Springer, 2008. Google Scholar
  48. M. Mukund, K. N. Kumar, J. Radhakrishnan, and M. A. Sohoni. Robust asynchronous protocols are finite-state. In ICALP, pages 188-199, 1998. Google Scholar
  49. M. Mukund, K. N. Kumar, J. Radhakrishnan, and M. A. Sohoni. Towards a characterisation of finite-state message-passing systems. In ASIAN, pages 282-299, 1998. Google Scholar
  50. T. Place, L. van Rooijen, and M. Zeitoun. Separating regular languages by locally testable and locally threshold testable languages. In FSTTCS, pages 363-375, 2013. Google Scholar
  51. T. Place, L. van Rooijen, and M. Zeitoun. Separating regular languages by piecewise testable and unambiguous languages. In MFCS, pages 729-740, 2013. Google Scholar
  52. T. Place and M. Zeitoun. Going higher in the first-order quantifier alternation hierarchy on words. In ICALP, pages 342-353, 2014. Google Scholar
  53. T. Place and M. Zeitoun. Separating regular languages with first-order logic. Logical Methods in Computer Science, 12(1), 2016. Google Scholar
  54. F. Rosa-Velardo and M. Martos-Salgado. Multiset rewriting for the verification of depth-bounded processes with name binding. Inf. Comput., 215:68-87, 2012. Google Scholar
  55. S. Schmitz and Ph. Schnoebelen. Multiply-recursive upper bounds with Higman’s lemma. In ICALP, volume 6756 of LNCS, pages 441-452. Springer, 2011. Google Scholar
  56. T. G. Szymanski and J. H. Williams. Noncanonical extensions of bottom-up parsing techniques. SIAM Journal on Computing, 5(2):231-250, 1976. Google Scholar
  57. T. Wies, D. Zufferey, and T. A. Henzinger. Forward analysis of depth-bounded processes. In FOSSACS, volume 6014 of LNCS, pages 94-108. Springer, 2010. Google Scholar
  58. M. De Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. In CAV, volume 4144 of LNCS, pages 17-30. Springer, 2006. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact