Skip to main content
Top

2016 | OriginalPaper | Chapter

Petri Net Synthesis for Restricted Classes of Nets

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Elementary nets correspond to pure, plain and 1-bounded Petri nets.
 
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
This occurs because all smallest cycles contain each label exactly once.
 
4
Plain and two transitions with non-disjoint presets must have the same presets.
 
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
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
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
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
And even the Petri nets produced by hand and used for generating the lts.
 
Literature
1.
go back to reference 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 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
4.
go back to reference 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 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
5.
go back to reference 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) 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)
6.
go back to reference 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)CrossRef 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)CrossRef
7.
go back to reference 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)CrossRefMATH 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)CrossRefMATH
9.
go back to reference 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 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.
go back to reference 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 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.
go back to reference 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 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
15.
go back to reference 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)CrossRef 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)CrossRef
18.
go back to reference 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)CrossRef 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)CrossRef
19.
go back to reference Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers (1996) Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers (1996)
20.
go back to reference 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 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
23.
go back to reference 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)CrossRef 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)CrossRef
26.
go back to reference Ehrenfeucht, A., Rozenberg, G.: Partial (set) 2-structures. Part II: state spaces of concurrent systems. Acta Inf 27(4), 343–368 (1990)CrossRefMATH Ehrenfeucht, A., Rozenberg, G.: Partial (set) 2-structures. Part II: state spaces of concurrent systems. Acta Inf 27(4), 343–368 (1990)CrossRefMATH
27.
go back to reference 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) 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)
28.
go back to reference 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 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
Metadata
Title
Petri Net Synthesis for Restricted Classes of Nets
Author
Uli Schlachter
Copyright Year
2016
DOI
https://doi.org/10.1007/978-3-319-39086-4_6

Premium Partner