Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus

Radu Mateescu

Proceedings of the 2nd International Workshop on Verification, Model Checking and Abstract Interpretation VMCAI'98 (Pisa, Italy), September 1998.

Abstract:

Programs written in value-passing description languages such as muCRL and LOTOS can be naturally translated into Labelled Transition Systems (LTSs) containing data values. In order to express temporal properties interpreted over these LTSs, we define a value-based alternation-free modal mu-calculus built from typed variables, pattern-matching modalities, and parameterised fixed point operators. The verification of a temporal formula over a (finite) LTS is reduced to the (partial) resolution of a Parameterised Boolean Equation System (PBES). We propose a resolution method for PBESs that leads to a local model-checking algorithm, which could also be applied in the framework of abstract interpretation.

8 pages

PDF

PostScript

Slides of R. Mateescu's lecture at VMCAI'98

PDF