Propositional dynamic logic for Petri nets

Propositional Dynamic Logic (PDL) is a multi-modal logic used for specifying and reasoning on sequential programs. Petri Net is a widely used formalism to specify and to analyse concurrent programs with a very nice graphical representation. In this work, we propose a PDL to reasoning about Petri Nets. First we define a compositional encoding of Petri Nets from basic nets as terms. Second, we use these terms as PDL programs and provide a compositional semantics to PDL Formulas. Finally, we present an axiomatization and prove completeness w.r.t. our semantics. The advantage of our approach is that we can do reasoning about Petri Nets using our dynamic logic and we do not need to to translate it to other formalisms. Moreover our approach is compositional allowing for construction of complex nets using basic ones.