RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PERSONAL OFFICE
 Video Library Archive Most viewed videos Search RSS New in collection

You may need the following programs to see the files

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
 Video records: Windows Media 223.8 Mb Flash Video 374.6 Mb MP4 374.6 Mb

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})$.