To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

On closure ordinals for t… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

On closure ordinals for the modal μ-calculus

Conference paper
Authors Bahareh Afshari
Graham E. Leigh
Published in Leibniz International Proceedings in Informatics, LIPIcs
ISSN 1868-8969
Publication year 2013
Published at
Language en
Keywords Closure ordinals, Modal mu-calculus, Tableaux
Subject categories Mathematical logic, Theoretical computer science

Abstract

The closure ordinal of a formula of modal μ-calculus μXℓ is the least ordinal κ, if it exists, such that the denotation of the formula and the κ-th iteration of the monotone operator induced by ℓ coincide across all transition systems (finite and infinite). It is known that for every α < ω2 there is a formula ℓ of modal logic such that μXℓ has closure ordinal α [3]. We prove that the closure ordinals arising from the alternation-free fragment of modal μ-calculus (the syntactic class capturing 2 ∩ ∏2) are bounded by ω2. In this logic satisfaction can be characterised in terms of the existence of tableaux, trees generated by systematically breaking down formulæ into their constituents according to the semantics of the calculus. To obtain optimal upper bounds we utilise the connection between closure ordinals of formulæ and embedded order-types of the corresponding tableaux. © Bahareh Afshari and Graham E. Leigh.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?