Afshari, Bahareh ;
Leigh, Graham E.
On closure ordinals for the modal mucalculus
Abstract
The closure ordinal of a formula of modal mucalculus mu X phi is the least ordinal kappa, if it exists, such that the denotation of the formula and the kappath iteration of the monotone operator induced by phi coincide across all transition systems (finite and infinite). It is known that for every alpha < omega^2 there is a formula phi of modal logic such that mu X phi has closure ordinal alpha (Czarnecki 2010). We prove that the closure ordinals arising from the alternationfree fragment of modal mucalculus (the syntactic class capturing Sigma_2 \cap Pi_2) are bounded by omega^2. In this logic satisfaction can be characterised in terms of the existence of tableaux, trees generated by systematically breaking down formulae into their constituents according to the semantics of the calculus. To obtain optimal upper bounds we utilise the connection between closure ordinals of formulae and embedded ordertypes of the corresponding tableaux.
BibTeX  Entry
@InProceedings{afshari_et_al:LIPIcs:2013:4188,
author = {Bahareh Afshari and Graham E. Leigh},
title = {{On closure ordinals for the modal mucalculus}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {3044},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897606},
ISSN = {18688969},
year = {2013},
volume = {23},
editor = {Simona Ronchi Della Rocca},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4188},
URN = {urn:nbn:de:0030drops41889},
doi = {10.4230/LIPIcs.CSL.2013.30},
annote = {Keywords: Closure ordinals, Modal mucalculus, Tableaux}
}
2013
Keywords: 

Closure ordinals, Modal mucalculus, Tableaux 
Seminar: 

Computer Science Logic 2013 (CSL 2013)

Issue date: 

2013 
Date of publication: 

2013 