Mateescu-02

**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 | PostScript |

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