Skip to main content
SpringerLink
Log in

Synthesis of Petri Nets with Whole-Place Operations and Localities

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2016 (ICTAC 2016)

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

Included in the following conference series:

  • 501 Accesses

Abstract

Synthesising systems from behavioural specifications is an attractive way of constructing implementations which are correct-by-design and thus requiring no costly validation efforts. In this paper, systems are modelled by Petri nets and the behavioural specifications are provided in the form of step transition systems, where arcs are labelled by multisets of executed actions. We focus on the problem of synthesising Petri nets with whole-place operations and localities (wpol-nets), which are a class of Petri nets powerful enough to express a wide range of system behaviours, including inhibition of actions, resetting of local states, and locally maximal executions.

The synthesis problem was solved for several specific net classes and later a general approach was developed within the framework of \(\tau \)-nets. In this paper, we follow the synthesis techniques introduced for \(\tau \)-nets that are based on the notion of a region of a transition system, which we suitably adapt to work for wpol-nets.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Transition functions are not related to (Petri) net-transitions.

  2. 2.

    Control disabled steps mappings are defined in [7] in the context of \(\tau \)-nets, and this is how \({ cds}_{lmax}\) will be used in Sect. 4.

  3. 3.

    As will be explained later, the same net-type can be defined for a given kind of nets to be executed without any specific policy or with some policy. Therefore, we can re-use here the \(\tau _{ wpo }^k\) net-type introduced in [12], which coincides with \(\tau ^k\).

References

  1. Abdulla, P.A., Delzanno, G., Van Begin, L.: A language-based comparison of extensions of Petri nets with and without whole-place operations. In: Dediu, A.H., Ionescu, A.M., Martín-Vide, C. (eds.) LATA 2009. LNCS, vol. 5457, pp. 71–82. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00982-2_6

    Google Scholar 

  2. Badouel, E., Bernardinello, L., Darondeau, P.: Petri Net Synthesis. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2015)

    MATH  Google Scholar 

  3. Badouel, E., Darondeau, P.: Theory of regions. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 529–586. Springer, Heidelberg (1998). doi:10.1007/3-540-65306-6_22

    Chapter  Google Scholar 

  4. Bernardinello, L., De Michelis, G., Petruni, K., Vigna, S.: On the synchronic structure of transition systems. In: Desel, J. (ed.) Structures in Concurrency Theory. Workshops in Computing, pp. 69–84. Springer, London (1995)

    Chapter  Google Scholar 

  5. Busi, N., Pinna, G.M.: Synthesis of nets with inhibitor arcs. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 151–165. Springer, Heidelberg (1997). doi:10.1007/3-540-63141-0_11

    Chapter  Google Scholar 

  6. Chernikova, N.: Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. USSR Comput. Math. Math. Phys. 5, 228–233 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  7. Darondeau, P., Koutny, M., Pietkiewicz-Koutny, M., Yakovlev, A.: Synthesis of nets with step firing policies. Fundam. Informaticae 94, 275–303 (2009)

    MathSciNet  MATH  Google Scholar 

  8. Desel, J., Reisig, W.: The synthesis problem of Petri nets. Acta Informatica 33, 297–315 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  9. Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998). doi:10.1007/BFb0055044

    Chapter  Google Scholar 

  10. Ehrenfeucht, A., Rozenberg, G.: Partial 2-structures; Part I: basic notions and the representation problem, and Part II: state spaces of concurrent systems. Acta Informatica 27, 315–368 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  11. Finkel, A., McKenzie, P., Picaronny, C.: A well-structured framework for analysing Petri net extensions. Inf. Comput. 195, 1–29 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  12. Kleijn, J., Koutny, M., Pietkiewicz-Koutny, M., Rozenberg, G.: Applying Regions. Theoret. Comput. Sci. (2016)

    Google Scholar 

  13. Koutny, M., Pietkiewicz-Koutny, M.: Synthesis of Petri nets with localities. Sci. Ann. Comp. Sci. 19, 1–23 (2009)

    MathSciNet  MATH  Google Scholar 

  14. Mukund, M.: Petri nets and step transition systems. Int. J. Found. Comput. Sci. 3, 443–478 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  15. Nielsen, M., Rozenberg, G., Thiagarajan, P.S.: Elementary transition systems. Theoret. Comput. Sci. 96, 3–33 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  16. Pietkiewicz-Koutny, M.: Transition systems of elementary net systems with inhibitor arcs. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 310–327. Springer, Heidelberg (1997). doi:10.1007/3-540-63139-9_43

    Chapter  Google Scholar 

  17. Schmitt, V.: Flip-flop nets. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 517–528. Springer, Heidelberg (1996). doi:10.1007/3-540-60922-9_42

    Chapter  Google Scholar 

Download references

Acknowledgements

We would like to thank the anonymous reviewers for useful comments and suggestions.

Author information

Authors and Affiliations

  1. LIACS, Leiden University, P.O. Box 9512, 2300 RA, Leiden, The Netherlands

    Jetty Kleijn

  2. School of Computing Science, Newcastle University, Newcastle upon Tyne, NE1 7RU, UK

    Maciej Koutny & Marta Pietkiewicz-Koutny

Authors
  1. Jetty Kleijn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maciej Koutny
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marta Pietkiewicz-Koutny
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marta Pietkiewicz-Koutny .

Editor information

Editors and Affiliations

  1. Universidade Federal de Pernambuco Centro de Informática, Recife, Pernambuco, Brazil

    Augusto Sampaio

  2. Deptartment of Electrical Engineering BL, National Taiwan University, Taipei, Taiwan

    Farn Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Kleijn, J., Koutny, M., Pietkiewicz-Koutny, M. (2016). Synthesis of Petri Nets with Whole-Place Operations and Localities. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46750-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46749-8

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation