Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems

Radu Mateescu

Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2002 (Grenoble, France), April 2002

Full version available as INRIA Research Report RR-4430.

Abstract:

Model-checking is a popular technique for verifying finite-state concurrent systems, the behaviour of which can be modeled using Labeled Transition Systems (LTSs). In this report, we study the model-checking problem for the modal mu-calculus on acyclic LTSs. This has various applications of practical interest such as trace analysis, log information auditing, run-time monitoring, etc. We show that on acyclic LTSs, the full mu-calculus has the same expressive power as its alternation-free fragment. We also present two new algorithms for local model-checking of mu-calculus formulas on acyclic LTSs. Our algorithms are based upon a translation to boolean equation systems and exhibit a better performance than existing model-checking algorithms applied to acyclic LTSs. The first algorithm handles mu-calculus formulas F with alternation depth ad (F) >= 2 and has time complexity O (|F|^2 * (|S|+|T|)) and space complexity O (|F|^2 * |S|), where |S| and |T| are the number of states and transitions of the acyclic LTS and |F| is the number of operators in F. The second algorithm handles formulas F with alternation depth ad(F) = 1 and has time complexity O (|F| * (|S|+|T|)) and space complexity O (|F| * |S|).

36 pages

PDF

PostScript

Slides of R. Mateescu's lecture at TACAS'02

PDF