Alberucci, Luca; Krähenbühl, Jürg; Studer, Thomas (2014). Justifying induction on modal μformulae. Logic Journal of IGPL, 22(6), pp. 805817. 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 and Studer, Thomas 
Subjects:  000 Computer science, knowledge & systems 500 Science > 510 Mathematics 
ISSN:  13670751 
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 