Extending Propositional Dynamic Logic for Petri Nets

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 DS3 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.