Alberucci, Luca; Krähenbühl, Jürg; Studer, Thomas (2014). Justifying induction on modal μ-formulae. Logic Journal of IGPL, 22(6), pp. 805-817. Oxford University Press 10.1093/jigpal/jzu001
|
Text
aks14.pdf - Submitted Version Available under License Publisher holds Copyright. Download (263kB) | Preview |
We define a rank function for formulae of the propositional modal μ-calculus such that the rank of a fixed point is strictly bigger than the rank of any of its finite approximations. A rank function of this kind is needed, for instance, to establish the collapse of the modal μ-hierarchy over transitive transition systems. We show that the range of the rank function is ωω. Further we establish that the rank is computable by primitive recursion, which gives us a uniform method to generate formulae of arbitrary rank below ωω.
Item Type: |
Journal Article (Original Article) |
|---|---|
Division/Institute: |
08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG) 08 Faculty of Science > Institute of Computer Science (INF) |
UniBE Contributor: |
Alberucci, Luca, Krähenbühl, Jürg, Studer, Thomas |
Subjects: |
000 Computer science, knowledge & systems 500 Science > 510 Mathematics |
ISSN: |
1367-0751 |
Publisher: |
Oxford University Press |
Language: |
English |
Submitter: |
Florian Ranzi |
Date Deposited: |
23 Jan 2015 14:57 |
Last Modified: |
05 Dec 2022 14:39 |
Publisher DOI: |
10.1093/jigpal/jzu001 |
BORIS DOI: |
10.7892/boris.61785 |
URI: |
https://boris.unibe.ch/id/eprint/61785 |
Actions (login required)
 |
Edit item |