On-the-fly Incremental Liveness Verification Based on Bounding Depth Sub B\"{u}chi Automata
Jianpei Zhang · Journal of Information and Computational Science · 2013
In this paper we propose an on-the-fly incremental liveness verification method based on Bounding Depth Sub Buchi Automata (BDSBAs), which is an improvement of the Gaiser model checking algorithm [1]. Given a bounding depth, at first the method on-the-fly computes a bounding depth state set as the key factor of a BDSBA by a bounding depth DFS procedure, and then makes nested depth-first search as Gaiser algorithm explore an accepting lasso of the BDSBA as a counterexample of the liveness property under verification. With the increment of the bounding depth, our method can incrementally verify a liveness property. The empirical results indicate that our new method outperforms the original one.