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

[img]
Preview
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 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:

https://boris.unibe.ch/id/eprint/61785

Actions (login required)

Edit item Edit item
Provide Feedback