Abstract
We consider asynchronously composed I/O-Petri nets (AIOPNs) with built-in communication channels. They are equipped with a compositional semantics in terms of asynchronous I/O-transition systems (AIOTSs) admitting infinite state spaces. We study various channel properties that deal with the production and consumption of messages exchanged via the communication channels and establish useful relationships between them. In order to support incremental design we show that the channel properties considered in this work are preserved by asynchronous composition, i.e. they are compositional. As a crucial result we prove that the channel properties are decidable for AIOPNs.
This work has been partially sponsored by the EU project ASCENS, 257414.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alfaro, L., Henzinger, T.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, T. (eds.) Engineering Theories of Software Intensive Systems. NATO Science Series, vol. 195, pp. 83–104. Springer, Netherlands (2005)
Basu, S., Bultan, T., Ouederni, M.: Synchronizability for verification of asynchronously communicating systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 56–71. Springer, Heidelberg (2012)
Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer Publishing Company, Incorporated (2001)
Best, E., Devillers, R., Koutny, M.: Petri net algebra. Springer-Verlag New York, Inc., New York (2001)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)
Carstensen, H.: Decidability questions for fairness in petri nets. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 396–407. Springer, Heidelberg (1987)
Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005)
Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal petri nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V, LNCS, vol. 6900, pp. 96–120. Springer, Heidelberg (2012)
de Frutos-Escrig, D., Johnen, C.: Decidability of Home Space Property. Rapports de recherche. Université Paris-Sud. Centre d’Orsay. Laboratoire de recherche en informatique (1989)
Ginsburg, S., Spanier, E.H.: Semigroups, presburger formulas and languages. Pacific Journal of Mathematics 16(2), 285–296 (1966)
Gomes, L., Barros, J.P.: Structuring and composability issues in petri nets modeling. IEEE Transactions on Industrial Informatics 1(2), 112–123 (2005)
Haddad, S., Hennicker, R., Møller, M.H.: Channel properties of asynchronously composed petri nets. Tech. Rep. LSV-13-05, Laboratoire Spécification et Vérification, ENS Cachan, France (2013)
Hennicker, R., Janisch, S., Knapp, A.: Refinement of components in connection-safe assemblies with synchronous and asynchronous communication. In: Choppy, C., Sokolsky, O. (eds.) Monterey Workshop 2008. LNCS, vol. 6028, pp. 154–180. Springer, Heidelberg (2010)
Hennicker, R., Knapp, A.: Modal interface theories for communication-safe component assemblies. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 135–153. Springer, Heidelberg (2011)
Jančar, P.: Decidability of a temporal logic problem for petri nets. Theor. Comput. Sci. 74(1), 71–93 (1990)
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)
Lohmann, N., Massuthe, P., Wolf, K.: Operating guidelines for finite-state services. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 321–341. Springer, Heidelberg (2007)
Mayr, E.W.: An algorithm for the general petri net reachability problem. In: Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, STOC 1981, pp. 238–246. ACM, New York (1981)
Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River (1981)
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 223–231 (1978)
Reisig, W.: Simple composition of nets. In: Franceschinis, G., Wolf, K. (eds.) PETRI NETS 2009. LNCS, vol. 5606, pp. 23–42. Springer, Heidelberg (2009)
Souissi, Y.: On liveness preservation by composition of nets via a set of places. In: Rozenberg, G. (ed.) APN 1991. LNCS, vol. 524, pp. 277–295. Springer, Heidelberg (1991)
Souissi, Y., Memmi, G.: Composition of nets via a communication medium. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 457–470. Springer, Heidelberg (1991)
Stahl, C., Vogler, W.: A trace-based service semantics guaranteeing deadlock freedom. Acta Informatica 49(2), 69–103 (2012)
Stahl, C., Wolf, K.: Deciding service composition and substitutability using extended operating guidelines. Data Knowl. Eng. 68(9), 819–833 (2009)
Valk, R., Jantzen, M.: The residue of vector sets with applications to decidability problems in petri nets. Acta Informatica 21(6), 643–674 (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haddad, S., Hennicker, R., Møller, M.H. (2013). Channel Properties of Asynchronously Composed Petri Nets. In: Colom, JM., Desel, J. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2013. Lecture Notes in Computer Science, vol 7927. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38697-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-38697-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38696-1
Online ISBN: 978-3-642-38697-8
eBook Packages: Computer ScienceComputer Science (R0)