Advertisement

Modal Open Petri Nets

  • Vitali Schneider
  • Walter VoglerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11522)

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.

References

  1. 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_34CrossRefGoogle Scholar
  2. 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. 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_15CrossRefzbMATHGoogle Scholar
  4. 4.
    Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theoret. Comput. Sci. 642, 24–53 (2016)MathSciNetCrossRefGoogle Scholar
  5. 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_3CrossRefGoogle Scholar
  6. 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_4CrossRefzbMATHGoogle Scholar
  7. 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_6CrossRefGoogle Scholar
  8. 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_13CrossRefGoogle Scholar
  9. 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_14CrossRefGoogle Scholar
  10. 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_39CrossRefGoogle Scholar
  11. 11.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: Logic in Computer Science 1988, pp. 203–210. IEEE (1988)Google Scholar
  12. 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. 13.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)zbMATHGoogle Scholar
  14. 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/BFb0016222CrossRefGoogle Scholar
  15. 15.
    Raclet, J.B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93–110 (2008)CrossRefGoogle Scholar
  16. 16.
    Reisig, W.: Deterministic buffer synchronization of sequential processes. Acta Inf. 18, 117–134 (1982)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Schneider, V.: A better semantics for asynchronously communicating Petri nets. M.Sc. Thesis, Universität Augsburg (2017)Google Scholar
  18. 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/BFb0019979CrossRefGoogle Scholar
  19. 19.
    Stahl, C., Vogler, W.: A trace-based service semantics guaranteeing deadlock freedom. Acta Inf. 49, 69–103 (2012)MathSciNetCrossRefGoogle Scholar
  20. 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_51CrossRefGoogle Scholar
  21. 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-9CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Institut für InformatikUniversity of AugsburgAugsburgGermany

Personalised recommendations