Document Open Access Logo

Separability of Reachability Sets of Vector Addition Systems

Authors Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, Charles Paperman

PDF
Thumbnail PDF

File

LIPIcs.STACS.2017.24.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Lorenzo Clemente
Wojciech Czerwinski
Slawomir Lasota
Charles Paperman

Cite As Get BibTex

Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of Reachability Sets of Vector Addition Systems. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.STACS.2017.24

Abstract

Given two families of sets F and G, the F-separability problem for G asks whether for two given sets U, V in G there exists a set S in F, such that U is included in S and V is disjoint with S. We consider two families of sets F: modular sets S which are subsets of N^d, defined as unions of equivalence classes modulo some natural number n in N, and unary sets, which extend modular sets by requiring equality below a threshold n, and equivalence modulo n above n. Our main result is decidability of modular- and unary-separability for the class G of reachability sets of Vector Addition Systems, Petri Nets, Vector Addition Systems with States, and for sections thereof.

Subject Classification

Keywords
  • separability
  • Petri nets
  • modular sets
  • unary sets
  • decidability

Metrics

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

References

  1. Christian Choffrut and Serge Grigorieff. Separability of rational relations in A^* × ℕ^m by recognizable relations is decidable. Inf. Process. Lett., 99(1):27-32, 2006. Google Scholar
  2. Lorenzo Clemente, Wojciech Czerwiński, Sławomir Lasota, and Charles Paperman. Separability of reachability sets of vector addition systems, 2016. URL: https://arxiv.org/abs/1609.00214.
  3. Wojciech Czerwiński, Wim Martens, and Tomás Masopust. Efficient separability of regular languages by subsequences and suffixes. In Proc. of ICALP'13, pages 150-161, 2013. Google Scholar
  4. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, and Marc Zeitoun. A note on decidable separability by piecewise testable languages. In Proc. of FCT'15, pages 173-185, 2015. Google Scholar
  5. L. E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35((4)):413–422, 1913. Google Scholar
  6. Jean Goubault-Larrecq and Sylvain Schmitz. Deciding piecewise testable separability for regular tree languages. In Proc. of ICALP'16, pages 97:1-97:15, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.97.
  7. D. Hauschildt. Semilinearity of the reachability set is decidable for Petri nets. PhD thesis, University of Hamburg, 1990. Google Scholar
  8. G. Higman. Ordering by divisibility in abstract algebras. Proc. London Mathematical Society, 3((2)):326-336, 1952. Google Scholar
  9. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. Google Scholar
  10. Thomas W. Hungerford. Algebra, volume 73 of Graduate Texts in Mathematics. Springer, 1974. Google Scholar
  11. Harry B. Hunt III. On the decidability of grammar problems. Journal of the ACM, 29(2):429-447, 1982. Google Scholar
  12. Petr Jančar. Decidability of a temporal logic problem for Petri nets. Theor. Comput. Sci., 74(1):71-93, 1990. Google Scholar
  13. Eryk Kopczyński. Invisible pushdown languages. In Proc. of LICS'16, pages 867-872, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2933575.2933579.
  14. J. L. Lambert. Vector addition systems and semi-linearity. SIAM J. Comp., 1994. Accepted for publication. Google Scholar
  15. J. Leroux. Presburger vector addition systems. In Proc. of LICS'13, pages 23-32, 2013. Google Scholar
  16. Jérôme Leroux. The general vector addition system reachability problem by Presburger inductive invariants. In Proc. of LICS'09, pages 4-13, 2009. Google Scholar
  17. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In Proc. of LICS'15, pages 56-67, 2015. Google Scholar
  18. Richard J. Lipton. The reachability problem requires exponential space. Technical report, Yale University, 1976. Google Scholar
  19. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In Proc. of STOC'81, pages 238-246, 1981. Google Scholar
  20. Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating regular languages by locally testable and locally threshold testable languages. In Proc. of FSTTCS'13, pages 363-375, 2013. Google Scholar
  21. Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating regular languages by piecewise testable and unambiguous languages. In Proc. of MFCS'13, pages 729-740, 2013. Google Scholar
  22. Thomas Place and Marc Zeitoun. Going higher in the first-order quantifier alternation hierarchy on words. In Proc. of ICALP'14, pages 342-353, 2014. Google Scholar
  23. Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. Logical Methods in Computer Science, 12(1), 2016. Google Scholar
  24. Thomas G. Szymanski and John H. Williams. Noncanonical extensions of bottom-up parsing techniques. SIAM Journal on Computing, 5(2):231-250, 1976. 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