State space analysis of Petri nets with relation-algebraic methods |
| |
Authors: | Alexander Fronk Britta Kehden |
| |
Affiliation: | 1. Software Technology, Technical University of Dortmund, Germany;2. Institute of Computer Science and Applied Mathematics, University of Kiel, Germany |
| |
Abstract: | A large variety of systems can be modelled by Petri nets. Their formal semantics are based on linear algebra which in particular allows the calculation of a Petri net’s state space. Since state space explosion is still a serious problem, efficiently calculating, representing, and analysing the state space is mandatory. We propose a formal semantics of Petri nets based on executable relation-algebraic specifications. Thereupon, we suggest how to calculate the markings reachable from a given one simultaneously. We provide an efficient representation of reachability graphs and show in a correct-by-construction approach how to efficiently analyse their properties. Therewith we cover two aspects: modelling and model checking systems by means of one and the same logic-based approach. On a practical side, we explore the power and limits of relation-algebraic concepts for concurrent system analysis. |
| |
Keywords: | Relation algebra Petri nets Reachability graph State space analysis Systems analysis |
本文献已被 ScienceDirect 等数据库收录! |
|