Reachability tree in liveness analysis of Petri net-based cyber-physical systems

Abstract

Liveness is one of the crucial properties in the analysis of the Petri net-based cyber-physical systems. The paper proposes two algorithms related to the analysis of the liveness. The first one is dedicated to the construction of the reachability tree of the analysed Petri net, and the second one to the analysis of the liveness of the net (based on the generated reachability tree). Operation of both algorithms was explained with the use of the multi-robot CPS case-study.