Document Open Access Logo

Separability and Non-Determinizability of WSTS

Authors Eren Keskin, Roland Meyer

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.8.pdf
  • Filesize: 0.68 MB
  • 17 pages

Document Identifiers

Author Details

Eren Keskin
  • TU Braunschweig, Germany
Roland Meyer
  • TU Braunschweig, Germany

Funding

This work was supported by the DFG project EDS@SYN: Effective Denotational Semantics for Synthesis.

Cite As Get BibTex

Eren Keskin and Roland Meyer. Separability and Non-Determinizability of WSTS. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.8

Abstract

There is a recent separability result for the languages of well-structured transition systems (WSTS) that is surprisingly general: disjoint WSTS languages are always separated by a regular language. The result assumes that one of the languages is accepted by a deterministic WSTS, and it is not known whether this assumption is needed. There are two ways to get rid of the assumption, none of which has led to conclusions so far: (i) show that WSTS can be determinized or (ii) generalize the separability result to non-deterministic WSTS languages. Our contribution is to show that (i) does not work but (ii) does. As for (i), we give a non-deterministic WSTS language that we prove cannot be accepted by a deterministic WSTS. The proof relies on a novel characterization of the languages accepted by deterministic WSTS. As for (ii), we show how to find finitely represented inductive invariants without having the tool of ideal decompositions at hand. Instead, we work with closures under converging sequences. Our results hold for upward- and downward-compatible WSTS.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Regular languages
Keywords
  • WSTS
  • regular separability
  • determinization

Metrics

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

Related Versions

References

  1. P. A. Abdulla, M. F. Atig, V. Dave, and S. Narayanan Krishna. On the separability problem of string constraints. In CONCUR, volume 171 of LIPIcs, pages 16:1-16:19. Dagstuhl, 2020. Google Scholar
  2. P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In LICS, pages 313-321. IEEE, 1996. Google Scholar
  3. P. A. Abdulla, G. Delzanno, and L. Van Begin. Comparing the expressive power of well-structured transition systems. In CSL, volume 4646 of LNCS, pages 99-114. Springer, 2007. Google Scholar
  4. P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In LICS, pages 160-170. IEEE, 1993. Google Scholar
  5. G.Rozenberg A.Salomaa, editor. Handbook of Formal Languages. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59136-5.
  6. P. Baumann, R. Meyer, and G. Zetzsche. Regular separability in Büchi VASS. In STACS, volume 254 of LIPIcs, pages 9:1-9:19. Dagstuhl, 2023. Google Scholar
  7. M. Blondin, A. Finkel, and P. McKenzie. Handling infinitely branching WSTS. In ICALP, volume 8573 of LNCS, pages 13-25. Springer, 2014. Google Scholar
  8. P. Jančar. A note on well quasi-orderings for powersets. IPL, 72(5):155-160, 1999. Google Scholar
  9. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors. Handbook of Model Checking. Springer, 2018. Google Scholar
  10. L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman. Regular separability of Parikh automata. In ICALP, volume 80 of LIPIcs, pages 117:1-117:13. Dagstuhl, 2017. Google Scholar
  11. L. Clemente, W. Czerwiński, S. Lasota, and C. Paperman. Separability of reachability sets of vector addition systems. In STACS, volume 66 of LIPIcs, pages 24:1-24:14. Dagstuhl, 2017. Google Scholar
  12. L. Clemente, S. Lasota, and R. Piórkowski. Timed games and deterministic separability. In ICALP, volume 168 of LIPIcs, pages 121:1-121:16. Dagstuhl, 2020. Google Scholar
  13. P. Cousot. Principles of abstract interpretation. MIT Press, 2021. Google Scholar
  14. W. Czerwiński, P. Hofman, and G. Zetzsche. Unboundedness problems for languages of vector addition systems. In ICALP, volume 107 of LIPIcs, pages 119:1-119:15. Dagstuhl, 2018. Google Scholar
  15. W. Czerwiński and S. Lasota. Regular separability of one counter automata. In LICS, pages 1-12. IEEE, 2017. Google Scholar
  16. W. Czerwiński, S. Lasota, R. Meyer, S. Muskalla, K. Narayan Kumar, and P. Saivasan. Regular separability of well-structured transition systems. In CONCUR, volume 118 of LIPIcs, pages 35:1-35:18. Dagstuhl, 2018. Google Scholar
  17. W. Czerwiński, W. Martens, L. van Rooijen, M. Zeitoun, and G. Zetzsche. A characterization for decidable separability by piecewise testable languages. DMTCS, 19(4), 2017. Google Scholar
  18. W. Czerwiński and G. Zetzsche. An approach to regular separability in vector addition systems. In LICS, pages 341-354. ACM, 2020. Google Scholar
  19. C. Dufourd, A. Finkel, and Ph. Schnoebelen. Reset nets between decidability and undecidability. In ICALP, pages 103-115. Springer, 1998. Google Scholar
  20. A. Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. In ICALP, volume 267 of LNCS, pages 499-508. Springer, 1987. Google Scholar
  21. A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: complete WSTS. In ICALP, volume 5556 of LNCS, pages 188-199. Springer, 2009. Google Scholar
  22. A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part II: complete WSTS. LMCS, 8(3), 2012. Google Scholar
  23. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! TCS, 256(1-2):63-92, 2001. Google Scholar
  24. G. Geeraerts, J.-F. Raskin, and L. Van Begin. Well-structured languages. Acta Informatica, 44(3-4):249-288, 2007. Google Scholar
  25. A. R. Gingras. Convergence lattices. RMJ, 6(1):85-104, 1976. Google Scholar
  26. J. Goubault-Larrecq. On Noetherian spaces. In LICS, pages 453-462. IEEE, 2007. Google Scholar
  27. J. Goubault-Larrecq. Noetherian spaces in verification. In ICALP, volume 6199 of LNCS, pages 2-21. Springer, 2010. Google Scholar
  28. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. Google Scholar
  29. T. Jech. Set Theory. Springer, 2002. Google Scholar
  30. C. B. Jones. Tentative steps toward a development method for interfering programs. ACM TOPLAS, 5(4):596-619, 1983. Google Scholar
  31. M. Kabil and M. Pouzet. Une extension d'un théorème de P. Jullien sur les âges de mots. RAIRO Theor. Informatics Appl., 26:449-482, 1992. Google Scholar
  32. Eren Keskin and Roland Meyer. Separability and non-determinizability of WSTS (full version). CoRR, abs/2305.02736, 2023. URL: https://doi.org/10.48550/arXiv.2305.02736.
  33. J. Leroux and S. Schmitz. Demystifying reachability in vector addition systems. In LICS, pages 56-67. IEEE, 2015. Google Scholar
  34. G. Markowsky. Chain-complete posets and directed sets with applications. Algebra Universalis, 6:53-68, December 1976. URL: https://doi.org/10.1007/BF02485815.
  35. E. C. Milner. Basic WQO- and BQO-Theory, pages 487-502. Springer, 1985. Google Scholar
  36. R. Milner. An algebraic definition of simulation between programs. In IJCAI, pages 481-489. Kaufmann, 1971. Google Scholar
  37. M. O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3(2):114-125, 1959. Google Scholar
  38. R. Rado. Partial well-ordering of sets of vectors. Mathematika, 1(2):89-95, 1954. Google Scholar
  39. R. S. Thinniyam and G. Zetzsche. Regular separability and intersection emptiness are independent problems. In FSTTCS, volume 150 of LIPIcs, pages 51:1-51:15. Dagstuhl, 2019. Google Scholar
  40. G. Zetzsche. Separability by piecewise testable languages and downward closures beyond subwords. In LICS, pages 929-938. ACM, 2018. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact