BEGIN:VCALENDAR PRODID:-//Grails iCalendar plugin//NONSGML Grails iCalendar plugin//EN VERSION:2.0 CALSCALE:GREGORIAN METHOD:PUBLISH BEGIN:VEVENT DTSTAMP:20240328T171541Z DTSTART;TZID=Australia/Melbourne:20180209T060000 DTEND;TZID=Australia/Melbourne:20180209T080000 SUMMARY:Bisimulation invariance for monadic second-order logics UID:20240328T171541Z-iCalPlugin-Grails@philevents-web-6f97df9687-7c6q9 TZID:Australia/Melbourne LOCATION:Old Arts\, Parkville\, Australia\, 3010 DESCRIPTION:
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).