Skip to Main content Skip to Navigation
Reports

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

Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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 phi with alternation depth ad (phi) greater or equal than 2 and has time complexity O (|phi|^2 * (|S|+|T|)) and space complexity O (|phi|^2 * |S|), where |S| and |T| are the number of states and transitions of the acyclic Lts and |phi| is the number of operators in phi. The second algorithm handles formulas with alternation depth ad (phi) = 1 and has time complexity O (|phi| * (|S|+|T|)) and space complexity O (|phi| * |S|).
Document type :
Reports
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072158
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:55:54 PM
Last modification on : Thursday, November 19, 2020 - 1:00:27 PM
Long-term archiving on: : Sunday, April 4, 2010 - 10:56:09 PM

Identifiers

  • HAL Id : inria-00072158, version 1

Collections

Citation

Radu Mateescu. Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. RR-4430, INRIA. 2002. ⟨inria-00072158⟩

Share

Metrics

Record views

244

Files downloads

364