Document Open Access Logo

k-Bounded Petri Net Synthesis from Modal Transition Systems

Authors Uli Schlachter, Harro Wimmel

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.6.pdf
  • Filesize: 0.55 MB
  • 15 pages

Document Identifiers

Author Details

Uli Schlachter
Harro Wimmel

Cite AsGet BibTex

Uli Schlachter and Harro Wimmel. k-Bounded Petri Net Synthesis from Modal Transition Systems. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.6

Abstract

We present a goal-oriented algorithm that can synthesise k-bounded Petri nets (k in N^+) from hyper modal transition systems (hMTS), an extension of labelled transition systems with optional and required behaviour. The algorithm builds a potential reachability graph of a Petri net from scratch, extending it stepwise with required behaviour from the given MTS and over-approximating the result to a new valid reachability graph. Termination occurs if either the MTS yields no additional requirements or the resulting net of the second step shows a conflict with the behaviour allowed by the MTS, making it non-sythesisable.
Keywords
  • Modal transition system
  • bounded Petri net
  • synthesis

Metrics

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

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. Polynomial algorithms for the synthesis of bounded nets. In Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach, editors, TAPSOFT'95, volume 915 of LNCS, pages 364-378. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-59293-8_207.
  4. Eric Badouel, Luca Bernardinello, and Philippe Darondeau. The synthesis problem for elementary net systems is NP-complete. Theoretical Computer Science, 186(1-2):107-134, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00219-8.
  5. Eric Badouel, Luca Bernardinello, and Philippe Darondeau. Petri Net Synthesis. Texts in Theoretical Computer Science. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47967-4.
  6. 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.
  7. Eric Badouel and Philippe Darondeau. Theory of regions. In Wolfgang Reisig and Grzegorz Rozenberg, editors, Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, volume 1491 of LNCS, pages 529-586. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-65306-6_22.
  8. Eike Best and Philippe Darondeau. Petri net distributability. In Edmund M. Clarke, Irina Virbitskaite, and Andrei Voronkov, editors, PSI 2011, volume 7162 of LNCS, pages 1-18. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-29709-0_1.
  9. 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.
  10. Josep Carmona, Jordi Cortadella, and Michael Kishinevsky. New region-based algorithms for deriving bounded Petri nets. IEEE Transactions on Computers, 59(3):371-384, 2010. URL: http://dx.doi.org/10.1109/TC.2009.131.
  11. Josep Carmona, Jordi Cortadella, Michael Kishinevsky, Alex Kondratyev, Luciano Lavagno, and Alexandre Yakovlev. A symbolic algorithm for the synthesis of bounded Petri nets. In Kees M. van Hee and Rüdiger Valk, editors, PETRI NETS 2008, volume 5062 of LNCS, pages 92-111. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-68746-7_10.
  12. Philippe Darondeau. Distributed implementations of Ramadge-Wonham supervisory control with Petri nets. In Eduardo Camacho, editor, IEEE CDC-ECC 2005, pages 2107-2112. IEEE, 2005. URL: http://dx.doi.org/10.1109/CDC.2005.1582472.
  13. Andrzej Ehrenfeucht and Grzegorz Rozenberg. Partial (set) 2-structures. Part I: basic notions and the representation problem and Part II: state spaces of concurrent systems. Acta Informatica, 27(4):315-368, 1990. URL: http://dx.doi.org/10.1007/BF00264611.
  14. Guillaume Feuillade. Spécification logique de réseaux de Petri. PhD thesis, Université de Rennes I, 2005. Google Scholar
  15. 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.
  16. 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.
  17. 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.
  18. Kim Guldstrand Larsen and Liu Xinxin. Equation solving using modal transition systems. In LICS 1990, pages 108-117. IEEE Computer Society, 1990. URL: http://dx.doi.org/10.1109/LICS.1990.113738.
  19. Jean-Baptiste Raclet. Residual for component specifications. Electr. Notes Theor. Comput. Sci., 215:93-110, 2008. URL: http://dx.doi.org/10.1016/j.entcs.2008.06.023.
  20. Uli Schlachter. Bounded Petri net synthesis from modal transition systems is undecidable. In Josée Desharnais and Radha Jagadeesan, editors, CONCUR 2016, volume 59 of LIPIcs, pages 15:1-15:14. Schloss Dagstuhl, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.15.
  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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact