Partial Order Reduction for the full Class of State/Event Linear Temporal Logic

摘要

State/event linear temporal logic (SE-LTL) provides a concise and intuitive way to express properties incorporating both states and events. Automata-theoretic LTL model checking can be applied to verify SE-LTL properties. However, as SE-LTL is not preserved under classical stutter-equivalence, conventional partial order reduction (POR) cannot be directly used to check them. In this paper, we propose a novel approach to exploit POR for reducing the state space with respect to SE-LTL formulas. This approach detects a ‘state part’ of a Büchi automaton (BA) translated from an SE-LTL formula. Based on ‘state part’, we introduce a definition of SPs of BAs and labeled Kripke structures (LKS) with the integration of POR for reducing the state spaces of the products. The integrated POR modifies conventional POR by introducing an identification of visible actions with respect to events. Moreover, in order to apply POR to the full class of SE-LTL, we provide techniques to exploit POR for checking SE-LTL with the nexttime operator. We have implemented our techniques in SPIN model checker. The experimental results illustrate the potential of the techniques for reduction compared with pure state-based model checking and SE-LTL model checking without POR.