Abstract
This work extends our previous work [20] with the iteration operator. This new operator allows for representing more general networks and thus enhancing the former propositional logic for Petri Nets. We provide an axiomatization and a new semantics and prove soundness and completeness with respect with its semantics. In order to illustrate its usage, we also provide some examples.
M.R.F. Benevides, B. Lopes and E.H. Haeusler—This work was supported by the Brazilian research agencies CNPq, FAPERJ and CAPES.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
For the sake of clarity we avoid using the \(\varGamma \) subscripts.
- 2.
For the sake of clarity we avoid using the \(\varGamma \) superscripts.
References
Abrahamson, K.R.: Decidability and expressiveness of logics of processes. Ph.D. thesis, Department of Computer Science, University of Washington (1980)
Balbiani, P., Vakarelov, D.: PDL with intersection of programs: a complete axiomatization. J. Appl. Non-Classical Logics 13(3–4), 231–276 (2003)
Benevides, M.R.F., Schechter, L.M.: A propositional dynamic logic for CCS programs. In: Hodges, W., de Queiroz, R. (eds.) Logic, Language, Information and Computation. LNCS (LNAI), vol. 5110, pp. 83–97. Springer, Heidelberg (2008)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Theoretical Tracts in Computer Science. Cambridge University Press, Cambridge (2001)
Braga, C., Lopes, B.: Towards reasoning in dynamic logics with rewriting logic: the Petri-PDL case. In: Cornélio, M., Roscoe, B. (eds.) SBMF 2015. LNCS, vol. 9526, pp. 74–89. Springer, Heidelberg (2016). doi:10.1007/978-3-319-29473-5_5
de Almeida, E.S., Haeusler, E.H.: Proving properties in ordinary Petri Nets using LoRes logical language. Petri Net Newslett. 57, 23–36 (1999)
del Cerro, L.F., Orlowska, E.: DAL - a logic for data analysis. Theoretical Comput. Sci. 36, 251–264 (1985)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.: Reasoning About Knowledge. MIT Press, Cambridge (2004)
Gargov, G., Passy, S.: A note on boolean modal logic. In: Petkov, P.P. (ed.) Mathematical Logic, pp. 299–309. Springer, US, New York (1990)
Goldblatt, R.: Parallel action: concurrent dynamic logic with independent modalities. Stud. Logica. 51, 551–558 (1992)
Harel, D., Kaminsky, M.: Strengthened results on nonregular PDL. Technical Report MCS99-13, Faculty of Mathematics and Computer Science, Weizmann Institute of Science (1999)
Harel, D., Raz, D.: Deciding properties of nonregular programs. SIAM J. Comput. 22(4), 857–874 (1993)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing Series. MIT Press, Cambridge (2000)
Hull, R.: Web services composition: a story of models, automata, and logics. In: Proceedings of the 2005 IEEE International Conference on Web Services (2005)
Hull, R., Jianwen, S.: Tools for composite web services: a short overview. ACM SIGMOD 34(2), 86–95 (2005)
Khosravifar, S.: Modeling multi agent communication activities with Petri Nets. Int. J. Inf. Educ. Technol. 3(3), 310–314 (2013)
Kracht, M.: Synctatic codes and grammar refinement. J. Logic Lang. Inform. 4(1), 41–60 (1995)
Lenzerini, M.: Boosting the correspondence between description logics and propositional dynamic logics. In: Proceedings of the Twelfth National Conference on Artificial Intelligence, pp. 205–212. AAAI Press (1994)
Löding, C., Lutz, C., Serre, O.: Propositional dynamic logic with recursive programs. J. Logic Algebraic Programm. 73(1–2), 51–69 (2007)
Lopes, B., Benevides, M., Haeusler, H.: Propositional dynamic logic for Petri nets. Logic J. IGPL 22, 721–736 (2014)
Lopes, B., Benevides, M., Haeusler, E.H.: Extending propositional dynamic logic for Petri Nets. Electronic Notes Theoretical Comput. Sci. 305(11), 67–83 (2014)
Lopes, B., Benevides, M., Haeusler, E.H.: Reasoning about multi-agent systems using stochastic Petri Nets. In: Bajo, J., Hernández, J.Z., Mathieu, P., Campbell, A., Fernández-Caballero, A., Moreno, M.N., Julián, V., Alonso-Betanzos, A., Jiménez-López, M.D., Botti, V. (eds.) Trends in Practical Applications of Agents, Multi-Agent Systems and Sustainability. AISC, vol. 372, pp. 75–86. Springer, Heidelberg (2015). doi:10.1007/978-3-319-19629-9_9
Meyer, J.-J.C.: A different approach to deontic logic: deontic logic viewed as a variant of dynamic logic. Notre Dame J. Formal Logic 29(1), 109–136 (1987)
Mirkowska, G.: PAL - Propositional algorithmic logic. Fundam. Informaticæ 4, 675–760 (1981)
Peleg, D.: Concurrent dynamic logic. J. Assoc. Comput. Mach. 34(2), 450–479 (1897)
Peleg, D.: Communication in concurrent dynamic logic. J. Comput. Syst. Sci. 35(1), 23–58 (1987)
Petkov, A.: Propositional Dynamic Logic in Two and More Dimensions. Mathematical Logic and its Applications. Plenum Press, New York (1987)
Petri, C.A.: Fundamentals of a theory of asynchronous information flow. Commun. ACM 5(6), 319 (1962)
Tuominen, H.: Elementary net systems and dynamic logic. In: Rozenberg, G. (ed.) Advances in Petri Nets 1989. LNCS, pp. 453–466. Springer, Berlin Heidelberg (1990)
van Benthem, J.: Logic and Information Flow. Foundations of Computing. MIT Press, Cambridge (1994)
Wolter, F., Zakharyaschev, M.: Dynamic description logics. In: Proceedings of AiML1998, pp. 290–300. CSLI Publications (2000)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Benevides, M.R.F., Lopes, B., Haeusler, E.H. (2016). Propositional Dynamic Logic for Petri Nets with Iteration. 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_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-46750-4_25
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)