Partial Order Reduction for the full Class of State/Event Linear Temporal Logic. (4th July 2017)

• Record Type: Journal Article
• Authors: Kan, Shuanglong; Huang, Zhiqiu
• Is Part Of: Computer journal. Volume 61:Number 5(2018)
• Page Start: 629
• Page End: 644
• Publication Date: 2017-07-04
• Subjects: partial order reduction -- state/event linear temporal logic -- model checking -- labeled Kripke structure -- synchronous products -- nexttime operator; Computers -- Periodicals; 005.1
• DOI: 10.1093/comjnl/bxx064
• Languages: English
• ISSNs: 0010-4620

Abstract

Abstract: 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.