Skip to main content
SpringerLink
Log in

Petri Net Synthesis for Restricted Classes of Nets

  • Conference paper
  • First Online:
Application and Theory of Petri Nets and Concurrency (PETRI NETS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9698))

Abstract

This paper first recapitulates an algorithm for Petri net synthesis. Then, this algorithm is extended to special classes of Petri nets. For this purpose, any combination of the properties plain, pure, conflict-free, homogeneous, k-bounded, generalized T-net, generalized marked graph, place-output-nonbranching and distributed can be specified. Finally, a fast heuristic and an algorithm for minimizing the number of places in the synthesized Petri net is presented and evaluated experimentally.

U. Schlachter—The author is supported by the German Research Foundation (DFG) project ARS (Algorithms for Reengineering and Synthesis), reference number Be 1267/15-1.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    Elementary nets correspond to pure, plain and 1-bounded Petri nets.

  2. 2.

    The reachability graph of a Petri net is always deterministic and totally reachable. Thus, these properties can be assumed without loss of generality.

  3. 3.

    This occurs because all smallest cycles contain each label exactly once.

  4. 4.

    Plain and two transitions with non-disjoint presets must have the same presets.

  5. 5.

    For all \(M\in [M_0\rangle : M[t_1\rangle \wedge M[t_2\rangle \wedge t_1\ne t_2\Rightarrow {}^\bullet t_1\cap {}^\bullet t_2=\emptyset \).

  6. 6.

    In general it suffices to evaluate this disjunction for the subset of locations that can appear in the image of the location function. In our case this is \(\lbrace t_1,t_2,t_3,t_4\rbrace \).

  7. 7.

    No comparison with other tools was done, because e.g. the proposed algorithm needs more than 10 s to solve \(w_9\) plainly while Petrify only needs 0.01 s. Similar results are produced with GENET and rw-mutex-r8-w5. The strength of our approach is its flexibility. Thus, only the proposed heuristics are evaluated.

  8. 8.

    The restriction to plain nets was chosen, because the Petri nets that generate these lts are also plain. Thus, the results can be compared with the input.

  9. 9.

    And even the Petri nets produced by hand and used for generating the lts.

References

  1. Badouel, E., Bernardinello, L., Darondeau, P.: Polynomial algorithms for the synthesis of bounded nets. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds.) TAPSOFT 1995. LNCS, vol. 915, pp. 364–378. Springer, Heidelberg (1995)

    MATH  Google Scholar 

  2. Badouel, E., Bernardinello, L., Darondeau, P.: Petri Net Synthesis. Springer, Heidelberg (2015). http://dx.doi.org/10.1007/978-3-662-47967-4

    Book  MATH  Google Scholar 

  3. Badouel, E., Caillaud, B., Darondeau, P.: Distributing finite automata through Petri Net synthesis. Formal Asp. Comput. 13(6), 447–470 (2002). http://dx.doi.org/10.1007/s001650200022

    Article  MATH  Google Scholar 

  4. Badouel, E., Darondeau, P.: Theory of regions. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the Volumes are Based on the Advanced Course on Petri Nets, vol. 1491, pp. 529–586. Springer, Heidelberg (1996). http://dx.doi.org/10.1007/3-540-65306-6_22

    Google Scholar 

  5. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)

    Google Scholar 

  6. Best, E., Darondeau, P.: Petri Net distributability. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 1–18. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Best, E., Devillers, R.: Characterisation of the state spaces of live and bounded marked graph Petri Nets. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 161–172. Springer, Heidelberg (2014)

    Chapter  MATH  Google Scholar 

  8. Best, E., Devillers, R.R.: State space axioms for t-systems. Acta Informatica 52(2–3), 133–152 (2015). http://dx.doi.org/10.1007/s00236-015-0219-0

    Article  MathSciNet  MATH  Google Scholar 

  9. Best, E., Devillers, R.R.: Synthesis of bounded choice-free Petri Nets. In: Aceto, L., de Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1–4, 2015. LIPIcs, vol. 42, pp. 128–141. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015). http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.128

  10. Best, E., Schlachter, U.: Analysis of Petri Nets and transition systems. In: Knight, S., Lanese, I., Lluch-Lafuente, A., Vieira, H.T. (eds.) Proceedings 8th Interaction and Concurrency Experience, ICE 2015, Grenoble, France, 4–5 June 2015. EPTCS, vol. 189, pp. 53–67 (2015). http://dx.doi.org/10.4204/EPTCS.189.6

  11. Borde, D., Dierkes, S., Ferrari, R., Gieseking, M., Göbel, V., Grunwald, R., von der Linde, B., Lückehe, D., Schlachter, U., Schierholz, C., Schwammberger, M., Spreckels, V.: APT: analysis of Petri nets and labeled transition systems. https://github.com/CvO-Theory/apt

  12. Cabasino, M.P., Giua, A., Seatzu, C.: Identification of Petri Nets from knowledge of their language. Discrete Event Dyn. Syst. 17(4), 447–474 (2007). http://dx.doi.org/10.1007/s10626-007-0025-0

    Article  MathSciNet  MATH  Google Scholar 

  13. Caillaud, B.: Synet: a synthesizer of distributable bounded Petri-nets from finite automata. https://www.irisa.fr/s4/tools/synet/

  14. Carmona, J.: GENET: GEneralised NET synthesis. http://www.cs.upc.edu/~jcarmona/genet.html

  15. Carmona, J.A., Cortadella, J., Kishinevsky, M.: A region-based algorithm for discovering Petri Nets from event logs. In: Dumas, M., Reichert, M., Shan, M.-C. (eds.) BPM 2008. LNCS, vol. 5240, pp. 358–373. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Carmona, J., Cortadella, J., Kishinevsky, M.: New region-based algorithms for deriving bounded petri nets. IEEE Trans. Comput. 59(3), 371–384 (2010). http://dx.doi.org/10.1109/TC.2009.131

    Article  MathSciNet  MATH  Google Scholar 

  17. Carmona, J., Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: A symbolic algorithm for the synthesis of bounded petri nets. In: van Hee and Valk [27], pp. 92–111. http://dx.doi.org/10.1007/978-3-540-68746-7_10

  18. Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 124–138. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  19. Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers (1996)

    Google Scholar 

  20. Cortadella, J., Kishinevsky, M., Lavagno, L., Yakovlev, A.: Synthesizing petri nets from state-based models. In: Rudell, R.L. (ed.) Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1995, San Jose, California, USA, November 5–9, 1995, pp. 164–171. IEEE Computer Society/ACM (1995). http://dx.doi.org/10.1109/ICCAD.1995.480008

  21. Cortadella, J., Kishinevsky, M., Lavagno, L., Yakovlev, A.: Deriving petri nets for finite transition systems. IEEE Trans. Computers 47(8), 859–882 (1998). http://dx.doi.org/10.1109/12.707587

    Article  MathSciNet  MATH  Google Scholar 

  22. Cortadella, J., et al.: Petrify: a tool for synthesis of Petri nets and asynchronous circuits. http://www.cs.upc.edu/~jordicf/petrify/

  23. Darondeau, P.: Deriving unbounded Petri Nets from formal languages. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 533–548. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  24. Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1, 115–138 (1971). http://dx.doi.org/10.1007/BF00289519

    Article  MathSciNet  Google Scholar 

  25. Ehrenfeucht, A., Rozenberg, G.: Partial (set) 2-structures. Part I: basic notions and the representation problem. Acta Informatica 27(4), 315–342 (1990). http://dx.doi.org/10.1007/BF00264611

    Article  MathSciNet  MATH  Google Scholar 

  26. Ehrenfeucht, A., Rozenberg, G.: Partial (set) 2-structures. Part II: state spaces of concurrent systems. Acta Inf 27(4), 343–368 (1990)

    Article  MATH  Google Scholar 

  27. van Hee, K.M., Valk, R. (eds.): Applications and Theory of Petri Nets, 29th International Conference, PETRI NETS 2008, Xi’an, China, 23–27, June 2008. Lecture Notes in Computer Science, vol. 5062 Springer (2008)

    Google Scholar 

  28. Lorenz, R., Mauser, S., Juhás, G.: How to synthesize nets from languages: a survey. In: Henderson, S.G., Biller, B., Hsieh, M., Shortle, J., Tew, J.D., Barton, R.R. (eds.) Proceedings of the Winter Simulation Conference, WSC 2007, Washington, DC, USA, December 9–12, 2007, pp. 637–647. WSC (2007). http://dx.doi.org/10.1109/WSC.2007.4419657

  29. van der Werf, J.M.E.M., van Dongen, B.F., Hurkens, C.A.J., Serebrenik, A.: Process discovery using integer linear programming. In: van Hee and Valk [27], pp. 368–387. http://dx.doi.org/10.1007/978-3-540-68746-7_24

Download references

Acknowledgements

I would like to thank Harro Wimmel and Eike Best for their helpful comments. Special thanks go to Valentin Spreckels for the incorporation of homogeneity. Also, I am grateful for the anonymous reviewers’ careful reading and valuable comments.

Author information

Authors and Affiliations

  1. Department of Computing Science, Carl von Ossietzky Universität, 26111, Oldenburg, Germany

    Uli Schlachter

Authors
  1. Uli Schlachter
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Uli Schlachter .

Editor information

Editors and Affiliations

  1. Université Pierre and Marie Curie, Paris, France

    Fabrice Kordon

  2. Department Informatik, Universität Hamburg Department Informatik, Hamburg, Germany

    Daniel Moldt

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Schlachter, U. (2016). Petri Net Synthesis for Restricted Classes of Nets. In: Kordon, F., Moldt, D. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2016. Lecture Notes in Computer Science(), vol 9698. Springer, Cham. https://doi.org/10.1007/978-3-319-39086-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-39086-4_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-39085-7

  • Online ISBN: 978-3-319-39086-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation