Local model checking in the modal mu-calculus (Q1177939)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Local model checking in the modal mu-calculus |
scientific article |
Statements
Local model checking in the modal mu-calculus (English)
0 references
26 June 1992
0 references
The modal mu-calculus introduced by Pratt and Kozen is an extension of dynamic logic towards temporal logic. Formulae of the mu-calculus when interpreted on labelled transition systems may be used for modelling concurrency. For a given finite model (transition system) the problem of satisfiability is solvable. The authors present a method which is a tableau system for testing whether or not a state \(s\) has the property expressed by a formula of mu-calculus in a finite model. A nice example of an application of the method is also provided (an analysis of Knuth's mutual exclusion algorithm).
0 references
CCS
0 references
tableau method
0 references
satisfiability in finite models
0 references
modal mu-calculus
0 references
dynamic logic
0 references
temporal logic
0 references
transition systems
0 references
concurrency
0 references
analysis of Knuth's mutual exclusion algorithm
0 references
