Towards Reasoning in Dynamic Logics with Rewriting Logic: The Petri-PDL Case

Safety is a desired property in software to ensure that no unforeseen scenarios will be achieved and in concurrent systems the variety of scenarios increase with complexity. Dynamic Logics (DL) present a large body of techniques to reason about and certify systems. Modelling and assessing concurrent systems with a formal semantics leads to the possibility of proving that they comply with their specification. Petri nets fulfill these requirements as a formal modelling language comprising a wide body of tools and an intuitive graphical interpretation. Petri-PDL puts together DL with Petri nets, providing a theoretical background to reason about Petri nets, inheriting their properties with all the techniques available for DL. This work presents a prototype implementation, in the Rewriting Logic language Maude, of a bounded model checker for Petri-PDL. The Petri-PDL model checker is formally designed following the representation of Kripke models as rewrite theories defined for the Linear Temporal Logic model checker available in the Maude system.