Synthesis for first order specifications over data words

Speaker(s)

Mathieu Lehaut

Affiliation

University of Gothenburg

Language of the talk

English

Date

Nov. 6, 2024, 2:15 p.m.

Room

room 5440

Title in Polish

Synthesis for first order specifications over data words

Seminar

Seminar Automata Theory

---

We study the reactive synthesis problem for distributed systems with a 
finite but unbounded number of participants interacting with an 
uncontrollable environment. Executions of those systems are modelled by 
data words, and specifications are given as  first-order logic formulas. 
The goal for the system is to build a strategy so that any possible 
execution satisfies the given specification.
There are many parameters for this problem. First, there is a difference 
whether we consider an unbounded but finite amount of data, or if the 
set of data is infinite. Then, whether both player have access to the 
same set of data or if the set of data is partitioned between system 
data and environment data. Finally, we have to consider which predicates 
are allowed in the first order specification, as when the logic becomes 
more expressive, the synthesis problem becomes less decidable.
We will give an overview of different results for this setting, both 
positive and negative.

---