A finite model theorem for the propositional \(\mu\)-calculus (Q1117213): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
| Property / cites work | |||
| Property / cites work: Propositional dynamic logic of regular programs / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Well-quasi-orderings and sets of finite sequences / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Q3890740 / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Q5520569 / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Q5537629 / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Q3219755 / rank | |||
Normal rank | |||
Latest revision as of 14:30, 19 June 2024
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
