A finite model theorem for the propositional \(\mu\)-calculus (Q1117213)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A finite model theorem for the propositional \(\mu\)-calculus |
scientific article |
Statements
A finite model theorem for the propositional \(\mu\)-calculus (English)
0 references
1989
0 references
The propositional \(\mu\)-calculus \(L_{\mu}\) was introduced by this author [Lect. Notes Comput. Sci. 140, 348-359 (1982; Zbl 0507.03005)] and a nonelementary decision procedure for it was given by the author and \textit{R. Parikh} [Lect. Notes Comput. Sci. 164, 313-325 (1984; Zbl 0564.03012)]. The present paper establishes a finite model property for \(L_{\mu}\) by showing that the size of a minimal model for a given satisfiable \(L_{\mu}\) formula is related to the size of a maximal set of pairwise incomparable elements in a particular ordered structure which involves sets of ordinals.
0 references
filtration method
0 references
propositional \(\mu\)-calculus
0 references
finite model property
0 references
minimal model
0 references
