Justifying induction on modal μ-formulae

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

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 and 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: 23 Jan 2015 14:57
Publisher DOI: 10.1093/jigpal/jzu001
BORIS DOI: 10.7892/boris.61785
URI: http://boris.unibe.ch/id/eprint/61785

Actions (login required)

Edit item Edit item
Provide Feedback