- Complete axiomatization of the stutter-invariant fragment of the linear time µ-calculus
- Advances in Modal Logic
- Pages (from-to)
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
The logic µ(U) is the fixpoint extension of the "Until"-only fragment of linear-time temporal logic. It also happens to be the stutter-invariant fragment of linear-time µ-calculus µ(◊). We provide complete axiomatizations of µ(U) on the class of finite words and on the class of ω-words. We introduce for this end another logic, which we call µ(◊_Γ), and which is a variation of µ(◊) where the Next time operator is replaced by the family of its stutter-invariant counterparts. This logic has exactly the same expressive power as µ(U). Using already known results for µ(◊), we first prove completeness for µ(◊_Γ), which finally allows us to obtain completeness for µ(U).
- Publisher: College Publications
Place of publication: London
Editors: L. Beklemishev, V. Goranko, V. Shehtman
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.