Zigzag games, alternating infinite word automata and linear Monadic-Second order logic

Add to your list(s) Download to your calendar using vCal

• Pierre Pradic (University of Swansea)
• Friday 08 April 2022, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact George Kaye.

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

Abstract

(Joint work with Colin Riba)

Automata theory over infinite word is typically connected to logic through Büchi’s decidability theorem, which assert that ω-regular languages correspond exactly to denotations of formulas in Monadic Second-Order (MSO) logic over the structure (ω, <) ( MSO ). This correspondance yields Büchi’s celebrated ‘62 theorem that states that MSO is decidable, which has since then been extended in many directions.

One natural question is to ask about constructive variants of MSO ; for instance, to the best of my knowledge, it is unknown whether the MSO theory (restricted to decidable sets for the second-order part) in the effective topos is decidable, or if it is distinct from the theory obtained by considering type-2 realizability.

With Colin, we investigated a much simpler issue, partially motivated by extraction algorithms for finite-state synchronous transducers (Mealy machines). We gave a theory LMSO , refining MSO , tailored to enable the extraction of Mealy machines from ∀∃ statements through a straightforward realizability-like interpretation. In this talk I will discuss that theory, how the Büchi logic-automata correspondence is refined using the language of linear logic and its similarities with linear Dialectica.

(While this talk mentions automata theory and linear logic (and Dialectica), I would like to stress that the connection made here is apparently not the same as the one explored in Tito’s talk the previous week.)

Sources:

• Part II of my PhD thesis: https://cs-web.swan.ac.uk/~pierrepradic/thesis.pdf
• A Dialectica-Like Interpretation of a Linear MSO on Infinite Words, with Colin Riba, FOSSACS 2019 , https://hal.archives-ouvertes.fr/hal-01925701/document
• LMSO : A Curry-Howard Approach to Church’s Synthesis via Linear Logic, with Colin Riba, LICS 2018 , https://hal.archives-ouvertes.fr/hal-01698648v2/document
• A Curry-Howard Approach to Church’s Synthesis, with Colin Riba, FSCD 2017 /LMCS 2019, https://arxiv.org/pdf/1803.08958.pdf

This talk will be chaired by Anupam Das.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.