Document Open Access Logo

Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable

Author Uli Schlachter

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2016.15.pdf
  • Filesize: 0.53 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • Petri net synthesis
  • conjunctive nu-Calculus
  • modal transition systems

Metrics

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

Abstract

In this paper, the synthesis of bounded Petri nets from deterministic modal transition systems is shown to be undecidable.  The proof is built from three components.  First, it is shown that the problem of synthesising bounded Petri nets satisfying a given formula of the conjunctive nu-calculus (a suitable fragment of the mu-calculus) is undecidable.  Then, an equivalence between deterministic modal transition systems and a language-based formalism called modal specifications is developed.  Finally, the claim follows from a known equivalence between the conjunctive nu-calculus and modal specifications.

Cite As Get BibTex

Uli Schlachter. Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.15

Author Details

Uli Schlachter

References

  1. Adam Antonik, Michael Huth, Kim G. Larsen, Ulrik Nyman, and Andrzej Wasowski. 20 years of modal and mixed specifications. Bulletin of the EATCS, 95:94-129, 2008. Google Scholar
  2. André Arnold and Damian Niwiński. Rudiments of μ-calculus. North Holland, 2001. Google Scholar
  3. Eric Badouel, Luca Bernardinello, and Philippe Darondeau. Petri Net Synthesis. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47967-4.
  4. Eric Badouel, Benoît Caillaud, and Philippe Darondeau. Distributing finite automata through petri net synthesis. Formal Aspects of Computing, 13(6):447-470, 2002. URL: http://dx.doi.org/10.1007/s001650200022.
  5. Nikola Benes, Benoît Delahaye, Uli Fahrenberg, Jan Kretínský, and Axel Legay. Hennessy-milner logic with greatest fixed points as a complete behavioural specification theory. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR 2013, volume 8052 of LNCS, pages 76-90. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40184-8_7.
  6. Nikola Benes, Jan Kretínský, Kim Larsen, and Jirí Srba. On determinism in modal transition systems. Theoretical Computer Science, 410(41):4026-4043, 2009. URL: http://dx.doi.org/10.1016/j.tcs.2009.06.009.
  7. Eike Best and Philippe Darondeau. Petri net distributability. In Edmund M. Clarke, Irina Virbitskaite, and Andrei Voronkov, editors, PSI 2011, Revised Selected Papers, volume 7162 of LNCS, pages 1-18. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-29709-0_1.
  8. Glenn Bruns. An industrial application of modal process logic. Science of Computer Programming, 29(1-2):3-22, 1997. URL: http://dx.doi.org/10.1016/S0167-6423(96)00027-5.
  9. Philippe Darondeau. Distributed implementations of Ramadge-Wonham supervisory control with Petri nets. In Eduardo Camacho, editor, Proceedings of the 44th IEEE CDC-ECC 2005, pages 2107-2112. IEEE, 2005. URL: http://dx.doi.org/10.1109/CDC.2005.1582472.
  10. Javier Esparza. On the decidability of model checking for several μ-calculi and petri nets. In Sophie Tison, editor, CAAP 1994, volume 787 of LNCS, pages 115-129. Springer, 1994. URL: http://dx.doi.org/10.1007/BFb0017477.
  11. Guillaume Feuillade. Modal specifications are a syntactic fragment of the Mu-calculus. Research Report RR-5612, INRIA, 2005. URL: https://hal.inria.fr/inria-00070396.
  12. Guillaume Feuillade. Spécification logique de réseaux de Petri. PhD thesis, Université de Rennes I, 2005. Google Scholar
  13. Guillaume Feuillade and Sophie Pinchinat. Modal specifications for the control theory of discrete event systems. DEDS, 17(2):211-232, 2007. URL: http://dx.doi.org/10.1007/s10626-006-0008-6.
  14. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading, Mass, 1st edition, 1979. Google Scholar
  15. Petr Jancar. Nonprimitive recursive complexity and undecidability for petri net equivalences. Theoretical Computer Science, 256(1-2):23-30, 2001. URL: http://dx.doi.org/10.1016/S0304-3975(00)00100-6.
  16. Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333-354, 1983. URL: http://dx.doi.org/10.1016/0304-3975(82)90125-6.
  17. Jan Kretínský and Salomon Sickert. MoTraS: A tool for modal transition systems and their extensions. In Dang Van Hung and Mizuhito Ogawa, editors, ATVA 2013, volume 8172 of LNCS, pages 487-491. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-02444-8_41.
  18. Kim Larsen. Modal specifications. In Joseph Sifakis, editor, AVMFSS, volume 407 of LNCS, pages 232-246. Springer, 1989. URL: http://dx.doi.org/10.1007/3-540-52148-8_19.
  19. Kim Larsen and Bent Thomsen. A modal process logic. In LICS 1988, pages 203-210. IEEE, 1988. URL: http://dx.doi.org/10.1109/LICS.1988.5119.
  20. Marvin Lee Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1967. Google Scholar
  21. Rob J. van Glabbeek, Ursula Goltz, and Jens-Wolfhard Schicke-Uffmann. On characterising distributability. Logical Methods in Computer Science, 9(3), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(3:17)2013.
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