Yde Venema (ILLC) will present "Bisimulation invariance for monadic second-order logics" on Friday\, 9 February at 11 in Old Arts 156. \;

\nAbstract: \;of modal logics as a language for describing Kripke structures is compared \;to that of more classical languages such as first-order logic. An important \;notion in this theory is that of a bisimulation between two models. In many \;applications\, it is natural to identify bisimilar states (i.e.\, states that \;are linked by some bisimulation)\, and so properties of states that are not \;invariant under bisimulations are irrrelevant. In this context\, results that \;identify the bisimulation invariant fragment of some yardstick logic can be \;read as expressive completeness results: If M is the bisimulation-invariant \;fragment of L:

\n \; \; M = L/~\,

then M is strong enough to express all relevant properties of L.

\; \; The first result of this kind was van Benthem's Characterisation Theorem \;that identifies basic modal logic as the bisimulation-invariant fragment of \;first-order logic. His result was strengthened to monadic second-order logic \;by Janin &\; Walukiewicz\, who characterised the modal mu-calculus\, basic modal \;logic extended with fixpoint operators\, as its bisimulation-invariant \;fragment.

\; \; In the talk we discuss three variants of the Janin-Walukiewicz theorem\, \;where in the equation L = M/~\, we consider the cases where L is weak \;second-order logic\, and where M is respectively the alternation-free \;fragment of the modal mu-calculus\, and propositional dynamic logic (PDL).