Converting Reconfigurable Petri Nets to Maude

TL;DR

This paper presents a method to convert reconfigurable Petri nets into Maude, enabling the verification of properties like deadlocks and liveness using Maude's model checking capabilities.

Contribution

It introduces a novel transformation approach from reconfigurable Petri nets to Maude, facilitating property verification for dynamic net reconfigurations.

Findings

Enables verification of reconfigurable Petri nets in Maude.

Supports analysis of properties like deadlocks and liveness.

Utilizes Maude's equation- and rewrite logic with LTLR model checker.

Abstract

Model checking is an important aim of the theoretical computer science. It enables the verification of a model with a set of properties such as liveness, deadlock or safety. One of the typical modelling techniques are Petri nets they are well understood and can be used for a model checking. Reconfigurable Petri nets are based on a Petri nets with a set of rules. These rules can be used dynamically to change the net. Missing is the possibility to verify a reconfigurable net and properties such as deadlocks or liveness. This paper introduces a conversion from reconfigurable Petri net to Maude, that allows us to fill the gap. It presents a net transformation approach which is based on Maude's equation- and rewrite logic as well as the LTLR model checker.