Tableau-based model checking in the propositional mu-calculus (Q1122572): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set OpenAlex properties. |
||
| (One intermediate revision by one other user not shown) | |||
| Property / MaRDI profile type | |||
| Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1007/bf00264284 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2057260173 / rank | |||
Normal rank | |||
Latest revision as of 10:24, 30 July 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Tableau-based model checking in the propositional mu-calculus |
scientific article |
Statements
Tableau-based model checking in the propositional mu-calculus (English)
0 references
1990
0 references
This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems.
0 references
automated analysis of concurrent systems
0 references
finite-state systems
0 references
propositional mu-calculus
0 references
tableau-based proof system
0 references
