CTL formula evaluation by term rewriting inversion
Mihai-Lică Pura, Iulian Aciobăniţei, Ștefan-Adrian Toma, Didier Buchs · 2017
In the classical approaches of model checking (explicit and symbolic), the tools encode the state space, as well as the transition relation between the states. This way, when the predecessor of a state is needed, as in the case of CTL formulas evaluation, it can be extracted from the state space in a straightforward manner. Practical experience indicates that renouncing at encoding the transition relation would considerably increase the efficiency of the tools by allowing them to handle larger state spaces. The question is how can CTL formulas be evaluated in the absence of the transition relations? In some very simple cases, like Place/Transition nets, the predecessors of the states can be obtained by inversing the transition relation. But so far no solution was proposed for the general case of high level formalisms, such as Algebraic Petri nets. Our paper proposes a solution to this open problem by using the theory of inversing term rewriting systems. The idea is to transform Algebraic Petri nets into term rewriting systems and to compute the predecessor by using the inverses of the rewriting rules used in state space computation. These predecessors are then used to evaluate CTL formulas. In this paper the general theory is presented and a proof of concept is given for this approach.