Petri-PDL

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.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Braga, Christiano; Lopes, Bruno: Towards reasoning in dynamic logics with rewriting logic: the Petri-PDL case (2016)