Improving model checking stateful timed CSP with non-zenoness through clock-symmetry reduction
Abstract
Real-time system verification must deal with a special notion of ‘fairness’, i.e., clocks must always be able to progress. A system run which prevents clocks from progressing unboundedly is known as Zeno. Zeno runs are infeasible in reality and thus must be pruned during system verification. Though zone abstraction is an effective technique for model checking real-time systems, it is known that zone graphs (e.g., those generated from Timed Automata models) are too abstract to directly infer time progress and hence non-Zenoness. As a result, model checking with non-Zenoness (i.e., existence of a non-Zeno counterexample) based on zone graphs only is infeasible. In our previous work [23], we show that model checking Stateful Timed CSP with non-Zenoness based on zone graphs only is feasible, due to the difference between Stateful Timed CSP and Timed Automata. Nonetheless, the algorithm proposed in [23] requires to associate each time process construct with a unique clock, which could enlarge the state space (compared to model checking without non-Zenoness) significantly. In this paper, we improve our previous work by combining the checking algorithm with a clock-symmetry reduction method. The proposed algorithm has been realized in the PAT model checker for model checking LTL properties with non-Zenoness. The experimental results show that the improved algorithm significantly outperforms the previous work.