Synthesis for first order specifications over data words

Prelegent(ci)

Mathieu Lehaut

Afiliacja

University of Gothenburg

Język referatu

angielski

Termin

6 listopada 2024 14:15

Pokój

p. 5440

Tytuł w języku polskim

Synthesis for first order specifications over data words

Seminarium

Seminarium „Teoria automatów”

---

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.

---