Extending propositional dynamic logic for Petri nets. (English) Zbl 1335.68175
Fernández, Maribel (ed.) et al., Proceedings of the 8th workshop on logical and semantic frameworks (LSFA 2013), São Paulo, Brazil, September 2–3, 2013. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 305, 67-83, electronic only (2014).
Summary: Propositional dynamic logic (PDL) is a multi-modal logic used for specifying and reasoning on sequential programs. Petri nets is a widely used formalism to specify and analyze concurrent programs with a very intuitive graphical representation. Petri-PDL is an extension of PDL, whose programs are Petri nets, which combines the advantages of both formalisms using a compositional and structural approach to deal with Petri nets.
In this work we present an extension of Petri-PDL to deal with stochastic Petri nets, the \(\mathcal{DS}_3\) logic. This system is an alternative to model performance evaluation in a compositional and structural approach. We discuss about its soundness, decidability and completeness regarding our semantics and present a proof of EXPTime-completeness of its SAT problem. A usage example is presented.
For the entire collection see [Zbl 1310.68008].
In this work we present an extension of Petri-PDL to deal with stochastic Petri nets, the \(\mathcal{DS}_3\) logic. This system is an alternative to model performance evaluation in a compositional and structural approach. We discuss about its soundness, decidability and completeness regarding our semantics and present a proof of EXPTime-completeness of its SAT problem. A usage example is presented.
For the entire collection see [Zbl 1310.68008].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
| 03B70 | Logic in computer science |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Benevides, Mario; Haeusler, Edward; Lopes, Bruno, Propositional Dynamic Logic for Petri Nets, (Annals of the 6th Workshop on Logical and Semantic Frameworks, with Applications (2011)) · Zbl 1335.68175 |
| [2] | Blackburn, P.; de Rijke, M.; Venema, Y., Modal Logic. Theoretical Tracts in Computer Science (2001), Cambridge University Press · Zbl 0988.03006 |
| [3] | Coleman, J. L.; Henderson, W.; Taylor, P. G., Product form equilibrium distributions and a convolution algorithm for Stochastic Petri Nets, Performance Evaluation, 26, 3, 159-180 (1996) · Zbl 0900.68321 |
| [4] | de Almeida, E. S.; Haeusler, E. H., Proving properties in ordinary Petri Nets using LoRes logical language, Petri Net Newsletter, 57, 23-36 (1999) |
| [5] | De Giacomo, Giuseppe; Massacci, Fabio, Combining deduction and model checking into tableaux and algorithms for Converse-PDL, Information and Computation, 160, 2000 (1998) · Zbl 1045.68090 |
| [6] | Feldman, Yishai A., A decidable Propositional Probabilistic Dynamic Logic, (Proceedings of the fifteenth annual ACM symposium on Theory of computing, STOC ’83 (1983), ACM), 298-309 |
| [7] | Feldman, Yishai A., A decidable Propositional Dynamic Logic with explicit probabilities, Information and Control, 63, 1-2, 11-38 (1984) · Zbl 0592.68031 |
| [8] | Feldman, Yishai A.; Harel, David, A Probabilistic Dynamic Logic, Journal of Computer and System Sciences, 28, 2, 193-215 (1984) · Zbl 0537.68036 |
| [9] | Fischer, Michael J.; Ladner, Richard E., Propositional Dynamic Logic of regular programs, Journal of Computer and System Sciences, 18, 194-211 (1979) · Zbl 0408.03014 |
| [10] | Goldblatt, R., Parallel action: Concurrent Dynamic Logic with independent modalities, Studia Logica, 51, 551-558 (1992) · Zbl 0784.03019 |
| [11] | Göller, Stefan; Lohrey, Markus, Infinite state model-checking of Propositional Dynamic Logics, (Ésik, Zoltán, Computer Science Logic. Computer Science Logic, Lecture Notes in Computer Science, vol. 4207 (2006), Springer: Springer Berlin Heidelberg), 349-364 · Zbl 1225.68116 |
| [12] | Haas, P. J., Stochastic Petri Nets: modelling, stability, simulation (2002), Springer · Zbl 1052.90001 |
| [13] | Harel, David; Kozen, Dexter; Tiuryn, Jerzy, Dynamic Logic. Foundations of Computing Series (2000), MIT Press · Zbl 0976.68108 |
| [14] | Henderson, W.; Lucic, D.; Taylor, P. G., A net level performance analysis of Stochastic Petri Nets, The Journal of the Australian Mathematical Society. Series B. Applied Mathematics, 31, 2, 1446-8735 (2009) |
| [15] | Kolmogorov, Andrey N., Foundations of the Theory of Probability (1956), Chelsea Publishing · Zbl 0074.12202 |
| [16] | Kozen, Dexter, A probabilistic PDL, (Proceedings of the fifteenth annual ACM symposium on Theory of computing, STOC ’83 (1983), ACM), 291-297 · Zbl 0575.03013 |
| [17] | Lange, Martin, Model checking Propositional Dynamic Logic with all extras, Journal of Applied Logic, 4, 1, 39-49 (2006) · Zbl 1095.68053 |
| [18] | Lopes, Bruno; Benevides, Mario; Haeusler, Edward Hermann, Propositional dynamic logic for Petri Nets, Logic Journal of the IGPL (2014) · Zbl 1335.68175 |
| [19] | Pablo López-Grao, Juan; Merseguer, José; Campos, Javier, From UML Activity Diagrams to Stochastic Petri Nets: Application to software performance engineering, SIGSOFT Software Engineering Notes, 29, 1, 25-36 (2004) |
| [20] | Lyon, Douglas, Using Stochastic Petri Nets for real-time nth-order stochastic composition, Computer Music Journal, 19, 4, 13-22 (1995) |
| [21] | Marin, Andrea; Balsamo, Simonetta; Harrison, Peter G., Analysis of Stochastic Petri Nets with signals, Performance Evaluation, 69, 11, 551-572 (2012) |
| [22] | Ajmone Marsan, M., Stochastic Petri Nets: An elementary introduction, (Rozenberg, Grzegorz, Advances in Petri Nets 1989. Advances in Petri Nets 1989, Lecture Notes in Computer Science, vol. 424 (1990), Springer: Springer Berlin Heidelberg), 1-29 |
| [23] | Ajmone Marsan, M., Stochastic Petri Nets: an elementary introduction, (Advances in Petri Nets 1989. Advances in Petri Nets 1989, Lecture Notes in Computer Science, vol. 429 (1990), Springer: Springer Berlin Heidelberg), 1-29 |
| [24] | Ajmone Marsan, M.; Balbo, G.; Conte, G., A class of Generalised Stochastic Petri Nets for the analysis of multiprocessor systems, ACM Transactions On Computer Systems, 2, 1 (1984) |
| [25] | Ajmone Marsan, M.; Balbo, Gianfranco; Conte, Gianni; Donatelli, Susanna; Franceschinis, Giuliana, Modelling with Generalised Stochastic Petri Nets (1995), Wiley · Zbl 0843.68080 |
| [26] | Ajmone Marsan, M.; Chiola, G., On Petri Nets with deterministic and exponentially distributed firing times, (Rozenberg, Grzegorz, Advances in Petri Nets 1987. Advances in Petri Nets 1987, Lecture Notes in Computer Science, vol. 266 (1987), Springer: Springer Berlin Heidelberg), 132-145 |
| [27] | Ajmone Marsan, M.; Chiola, Giovanni, On Petri Nets with deterministic and exponentially distributed firing times, (Advances in Petri Nets 1987 (1987), Springer: Springer Berlin Heidelberg), 132-145 |
| [28] | Mazurkiewicz, Antoni, Trace theory, (Brauer, W.; Reisig, W.; Rozenberg, G., Petri Nets: Applications and Relationships to Other Models of Concurrency. Petri Nets: Applications and Relationships to Other Models of Concurrency, Lecture Notes in Computer Science, vol. 255 (1987), Springer), 278-324 · Zbl 0633.68051 |
| [29] | Mazurkiewicz, Antoni, Basic notions of trace theory, (Bakker, J. W.; Roever, W.-P.; Rozenberg, G., Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science, vol. 354 (1989), Springer), 285-363 · Zbl 0683.68032 |
| [30] | Papadimitriou, Christos, Computational Complexity (1994), Addison-Wesley · Zbl 0833.68049 |
| [31] | Tiomkin, M.; Makowsky, J. A., Decidability of finite probabilistic Propositional Dynamic Logics, Information and Computation, 94, 2, 180-203 (1991) · Zbl 0732.03022 |
| [32] | Tiomkin, M. L.; Makowsky, J. A., Propositional Dynamic Logic with local assignment, Theoretical Computer Science, 36, 71-87 (1985) · Zbl 0574.03011 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
