English

Converting Reconfigurable Petri Nets to Maude

Formal Languages and Automata Theory 2014-11-13 v5 Logic in Computer Science

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.

Keywords

Cite

@article{arxiv.1409.8404,
  title  = {Converting Reconfigurable Petri Nets to Maude},
  author = {Alexander Schulz},
  journal= {arXiv preprint arXiv:1409.8404},
  year   = {2014}
}
R2 v1 2026-06-22T06:09:05.925Z