Skip to main content
SpringerLink
Log in

Modal Open Petri Nets

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

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

  • 646 Accesses

Abstract

Open nets have an interface of input and output places for modelling asynchronous communication; these places serve as channels when open nets are composed. We study a variant that inherits modalities from Larsen’s modal transition systems. Instantiating a framework for open nets we have developed in the past, we present a refinement preorder in the spirit of modal refinement. The preorder supports modular reasoning since it is a precongruence, and we justify it by a coarsest-precongruence result. We compare our approach to the one of Haddad et al., which considers a restricted class of nets and a stricter refinement. Our studies are conducted in an extended class of nets, which additionally have transition labels for synchronous communication.

Research support provided by the DFG (German Research Foundation) under grant no. VO 615/12-2.

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.

    The term open in this sense presumably stems from [1].

References

  1. Baldan, P., Corradini, A., Ehrig, H., Heckel, R.: Compositional modeling of reactive systems using open nets. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 502–518. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44685-0_34

    Chapter  Google Scholar 

  2. Baldan, P., Corradini, A., Ehrig, H., Heckel, R., König, B.: Bisimilarity and behaviour-preserving reconfigurations of open Petri Nets. Log. Methods Comput. Sci. 4(4) (2008). https://doi.org/10.2168/LMCS-4(4:3)2008

  3. Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_15

    Chapter  MATH  Google Scholar 

  4. Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theoret. Comput. Sci. 642, 24–53 (2016)

    Article  MathSciNet  Google Scholar 

  5. de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, T. (eds.) Engineering Theories of Software Intensive Systems. NSS, vol. 195, pp. 83–104. Springer, Dordrecht (2005). https://doi.org/10.1007/1-4020-3532-2_3

    Chapter  Google Scholar 

  6. Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal petri nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 96–120. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29072-5_4

    Chapter  MATH  Google Scholar 

  7. Glabbeek, R.J.: The linear time — branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_6

    Chapter  Google Scholar 

  8. Haddad, S., Hennicker, R., Møller, M.H.: Specification of asynchronous component systems with modal I/O-petri nets. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 219–234. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05119-2_13

    Chapter  Google Scholar 

  9. Hüttel, H., Larsen, K.G.: The use of static constructs in a model process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 163–180. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51237-3_14

    Chapter  Google Scholar 

  10. Kindler, E.: A compositional partial order semantics for Petri net components. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 235–252. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63139-9_39

    Chapter  Google Scholar 

  11. Larsen, K.G., Thomsen, B.: A modal process logic. In: Logic in Computer Science 1988, pp. 203–210. IEEE (1988)

    Google Scholar 

  12. Massuthe, P., Reisig, W., Schmidt, K.: An operating guideline approach to the SOA. Ann. Math. Comput. Teleinformatics 1, 35–43 (2005)

    Google Scholar 

  13. Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)

    MATH  Google Scholar 

  14. Pomello, L.: Some equivalence notions for concurrent systems. An overview. In: Rozenberg, G. (ed.) APN 1985. LNCS, vol. 222, pp. 381–400. Springer, Heidelberg (1986). https://doi.org/10.1007/BFb0016222

    Chapter  Google Scholar 

  15. Raclet, J.B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93–110 (2008)

    Article  Google Scholar 

  16. Reisig, W.: Deterministic buffer synchronization of sequential processes. Acta Inf. 18, 117–134 (1982)

    Article  MathSciNet  Google Scholar 

  17. Schneider, V.: A better semantics for asynchronously communicating Petri nets. M.Sc. Thesis, Universität Augsburg (2017)

    Google Scholar 

  18. Souissi, Y.: On liveness preservation by composition of nets via a set of places. In: Rozenberg, G. (ed.) ICATPN 1990. LNCS, vol. 524, pp. 277–295. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0019979

    Chapter  Google Scholar 

  19. Stahl, C., Vogler, W.: A trace-based service semantics guaranteeing deadlock freedom. Acta Inf. 49, 69–103 (2012)

    Article  MathSciNet  Google Scholar 

  20. Vogler, W.: Behaviour preserving refinements of Petri nets. In: Tinhofer, G., Schmidt, G. (eds.) WG 1986. LNCS, vol. 246, pp. 82–93. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-17218-1_51

    Chapter  Google Scholar 

  21. Vogler, W.: Modular Construction and Partial Order Semantics of Petri Nets. LNCS, vol. 625. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55767-9

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, University of Augsburg, Augsburg, Germany

    Vitali Schneider & Walter Vogler

Authors
  1. Vitali Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Walter Vogler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Walter Vogler .

Editor information

Editors and Affiliations

  1. Università di Torino, Turin, Italy

    Susanna Donatelli

  2. Inria and LSV, CNRS & ENS Paris-Saclay, Cachan Cedex, France

    Stefan Haar

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Schneider, V., Vogler, W. (2019). Modal Open Petri Nets. In: Donatelli, S., Haar, S. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2019. Lecture Notes in Computer Science(), vol 11522. Springer, Cham. https://doi.org/10.1007/978-3-030-21571-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-21571-2_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-21570-5

  • Online ISBN: 978-3-030-21571-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation