Invited talks

The program of GandALF 23 is enriched by a number of interesting invited talks.

Laure Daviaud

Weighted Automata at the border of decidability

In this talk I will review some results about weighted automata: what is decidable (or not) when it comes to describing their behaviour and what are the mathematical tools that are used to prove such results. In particular, I will describe Simon’s factorisation theorem, how it plays a major role in several of these results and how it could be used more widely.

Juha Kontinen

Complexity aspects of logics in team semantics

Team Semantics is the mathematical basis of modern logics for reasoning about dependence, independence, and imperfect information. During the past decade research on team semantics has flourished with interesting connections to fields such as database theory, statistics, formal linguistics, hyperproperties and causality, just to mention a few examples. I will give a short introduction to first-order team semantics and review the expressivity and complexity of the most prominent logics of the area. I will also discuss probabilistic variants of these logics and their connections to the existential theory of the reals.

Sophie Pinchinat

Strategic Reasoning under Imperfect Information – The Case of Synchronous Recall

We first briefly survey various formal settings for Strategic Reasoning under Imperfect Information in multi-player games. From the point of view of automated verification and/or synthesis, we motivate the assumption of Synchronous Recall, that enforces particular properties on players’ observation capabilities.

Second, with the focus on aforementioned Synchronous Recall assumption, we consider arenas that arise from Dynamic Epistemic Logic, a modal logic dedicated to specifying information changes in a multi-player game. Such arenas are described in a symbolic manner, with an initial epistemic state and rules for player moves to attain new epistemic state, thus reflecting the information change that takes place.

We then explain how such symbolic arenas denote a possibly infinite first-order structure – reminiscent of the trees considered for interpreting Epistemic Temporal Logic. Second, we exploit this angle of view to go through the current state-of-the-art for reasoning (including planning) about these structures, and analyse the frontier of this overall setting regarding Strategic Reasoning.

Alexander Rabinovich

The Church Synthesis Problem Over Continuous Time

Church’s Problem asks for the construction of a procedure which, given a logical specification
ϕ(I, O) between input ω-strings I and output ω-strings O, determines whether there exists an op-
erator F that implements the specification in the sense that ϕ(I, F(I)) holds for all inputs I. Büchi
and Landweber gave a procedure to solve Church’s problem for MSO specifications and operators
computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time of the non-negative reals. It turns out that in the continuous time there are phenomena which are very different from the canonical discrete time domain of the natural numbers.