|
|
The eighth International сonference "Advances in Modal Logic" (AiML 2010)
August 24, 2010 12:20, Moscow
|
|
|
|
|
|
Complete axiomatization of the Stutter-invariant fragment of the linear time $\mu$-calculus
Amélie Gheerbrant |
Number of views: |
This page: | 930 | Video files: | 456 |
|
Abstract:
The logic $\mu\mathsf{TL}(\mathsf{U})$ is the fixpoint extension of the “Until”-only fragment of linear-time temporal logic. It also happens to be the stutterinvariant fragment of linear-time $\mu$-calculus $\mu\mathsf{TL}$. We provide complete axiomatizations of $\mu\mathsf{TL}(\mathsf{U})$ on the class of finite words and on the class of $\omega$-words. We introduce for this end another logic, which we call $\mu\mathsf{TL}(\diamondsuit_\Gamma)$, and which is a variation of $\mu\mathsf{TL}$ where the Next time operator is replaced by the family of its stutter-invariant counterparts. This logic has exactly the same expressive power as $\mu\mathsf{TL}(\mathsf{U})$. Using already known results for $\mu\mathsf{TL}$, we first prove completeness for $\mu\mathsf{TL}(\diamondsuit_\Gamma)$, which finally allows us to obtain completeness for $\mu\mathsf{TL}(\mathsf{U})$.
Language: English
|
|