Document Open Access Logo

On the Upward/Downward Closures of Petri Nets

Authors Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, Prakash Saivasan

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.49.pdf
  • Filesize: 0.51 MB
  • 14 pages

Document Identifiers

Author Details

Mohamed Faouzi Atig
Roland Meyer
Sebastian Muskalla
Prakash Saivasan

Cite AsGet BibTex

Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan. On the Upward/Downward Closures of Petri Nets. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 49:1-49:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.MFCS.2017.49

Abstract

We study the size and the complexity of computing finite state automata (FSA) representing and approximating the downward and the upward closure of Petri net languages with coverability as the acceptance condition. We show how to construct an FSA recognizing the upward closure of a Petri net language in doubly-exponential time, and therefore the size is at most doubly exponential. For downward closures, we prove that the size of the minimal automata can be non-primitive recursive. In the case of BPP nets, a well-known subclass of Petri nets, we show that an FSA accepting the downward/upward closure can be constructed in exponential time. Furthermore, we consider the problem of checking whether a simple regular language is included in the downward/upward closure of a Petri net/BPP net language. We show that this problem is EXPSPACE-complete (resp. NP-complete) in the case of Petri nets (resp. BPP nets). Finally, we show that it is decidable whether a Petri net language is upward/downward closed.
Keywords
  • Petri nets
  • BPP nets
  • downward closure
  • upward closure

Metrics

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

References

  1. P. A. Abdulla, A. Collomb-Annichini, A. Bouajjani, and B. Jonsson. Using forward reachability analysis for verification of lossy channel systems. FMSD, 25(1), 2004. Google Scholar
  2. P. A. Abdulla, G. Delzanno, and L. V. Begin. Comparing the expressive power of well-structured transition systems. In CSL, LNCS. Springer, 2007. Google Scholar
  3. M. F. Atig, A. Bouajjani, K. Narayan Kumar, and P. Saivasan. On bounded reachability analysis of shared memory systems. In FSTTCS, LIPIcs. Dagstuhl, 2014. Google Scholar
  4. M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. LMCS, 7(4), 2011. Google Scholar
  5. M. F. Atig, A. Bouajjani, and T. Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR, LNCS. Springer, 2008. Google Scholar
  6. M. F. Atig, D. Chistikov, P. Hofman, K. N. Kumar, P. Saivasan, and G. Zetzsche. Complexity of regular abstractions of one-counter languages. In LICS, pages 207-216. ACM, 2016. Google Scholar
  7. M. F. Atig, R. Meyer, S. Muskalla, and P. Saivasan. On the upward/downward closures of petri nets. CoRR, abs/1701.02927, 2017. URL: http://arxiv.org/abs/1701.02927.
  8. G. Bachmeier, M. Luttenberger, and M. Schlund. Finite automata for the sub- and superword closure of CFLs: Descriptional and computational complexity. In LATA, LNCS. Springer, 2015. Google Scholar
  9. L. Clemente, P. Parys, S. Salvati, and I. Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In LICS, pages 96-105. ACM, 2016. Google Scholar
  10. B. Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 1991. Google Scholar
  11. S. Demri. On selective unboundedness of VASS. JCSS, 79(5), 2013. Google Scholar
  12. S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 79(1):23-38, 2013. Google Scholar
  13. J. Esparza. Petri Nets, commutative context-free grammars, and basic parallel processes. Fundam. Inf., 31(1), 1997. Google Scholar
  14. J. Esparza and M. Nielsen. Decidability issues for Petri nets - a survey. Bulletin of the EATCS, 52, 1994. Google Scholar
  15. A. Finkel, G. Geeraerts, J. F. Raskin, and L. V. Begin. On the omega-language expressive power of extended Petri nets. ENTCS, 2005. Google Scholar
  16. H. Gruber, M. Holzer, and M. Kutrib. More on the size of Higman-Haines sets: Effective constructions. In MCU, LNCS. Springer, 2007. Google Scholar
  17. P. Habermehl, R. Meyer, and H. Wimmel. The downward-closure of Petri net languages. In ICALP, LNCS. Springer, 2010. Google Scholar
  18. M. Hague, J. Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In POPL. ACM, 2016. Google Scholar
  19. L. H. Haines. On free monoids partially ordered by embedding. Journal of Combinatorial Theory, 6(1), 1969. Google Scholar
  20. G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7), 1952. Google Scholar
  21. P. Jančar, J. Esparza, and F. Moller. Petri nets and regular processes. J. Comput. Syst. Sci., 59(3):476-503, December 1999. Google Scholar
  22. R. M. Karp and R. E. Miller. Parallel program schemata. JCSS, 3(2):147-195, 1969. Google Scholar
  23. S. R. Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In STOC. ACM, 1982. Google Scholar
  24. S. La Torre, A. Muscholl, and I. Walukiewicz. Safety of parametrized asynchronous shared-memory systems is almost always decidable. In CONCUR, LIPIcs. Dagstuhl, 2015. Google Scholar
  25. J. L. Lambert. A structure to decide reachability in Petri nets. TCS, 99(1), 1992. Google Scholar
  26. J. Leroux. Vector addition system reachability problem: a short self-contained proof. In POPL. ACM, 2011. Google Scholar
  27. J. Leroux, V. Penelle, and G. Sutre. On the context-freeness problem for vector addition systems. In LICS. IEEE, 2013. Google Scholar
  28. J. Leroux, M. Praveen, and G. Sutre. A relational trace logic for vector addition systems with application to context-freeness. In CONCUR, pages 137-151. Springer, 2013. Google Scholar
  29. R. J. Lipton. The reachability problem requires exponential space. Technical report, Yale University, Department of Computer Science, 1976. Google Scholar
  30. Z. Long, G. Calin, R. Majumdar, and R. Meyer. Language-theoretic abstraction refinement. In FASE, LNCS. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28872-2_25.
  31. E. W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comp., 13(3), 1984. Google Scholar
  32. E. W. Mayr and A. R. Meyer. The complexity of the finite containment problem for Petri nets. JACM, 28(3), 1981. Google Scholar
  33. R. Mayr. Undecidable problems in unreliable computations. TCS, 1-3(297), 2003. Google Scholar
  34. R. Parikh. On context-free languages. JACM, 13(4), 1966. Google Scholar
  35. C. Rackoff. The covering and boundedness problems for vector addition systems. TCS, 6(2), 1978. Google Scholar
  36. W. Reisig. Petri nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 1985. Google Scholar
  37. B. Scarpellini. Complexity of subcases of Presburger arithmetic. Transactions of the AMS, 284(1), 1984. Google Scholar
  38. S. R. Schwer. The context-freeness of the languages associated with vector addition systems is decidable. TCS, 1992. Google Scholar
  39. R. Valk and G. Vidal-Naquet. Petri nets and regular languages. JCSS, 23(3), 1981. Google Scholar
  40. J. van Leeuwen. Effective constructions in well-partially-ordered free monoids. Discrete Mathematics, 21(3), 1978. Google Scholar
  41. K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational Horn clauses. In CADE, pages 337-352. Springer, 2005. Google Scholar
  42. G. Zetzsche. An approach to computing downward closures. In ICALP, LNCS. Springer, 2015. Google Scholar
  43. G. Zetzsche. Computing downward closures for stacked counter automata. In STACS, LIPIcs. Dagstuhl, 2015. Google Scholar
  44. G. Zetzsche. The complexity of downward closure comparisons. In ICALP, volume 55 of LIPIcs, pages 123:1-123:14. Dagstuhl, 2016. 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 Imprint Privacy Contact