PhD Defense
I will defend my thesis, titled "Expressivity of first-order logic,
star-free propositional dynamic logic and communicating automata",
on Friday, November 27th at 10:30.
The defense will take place fully online.
Manuscript
The manuscript is available
here.
Jury
- Volker Diekert (Universität Stuttgart), Reviewer
- Blaise Genest (CNRS, Université de Rennes), Reviewer
- Sylvain Conchon (Université Paris-Saclay), Examiner
- Cristina Sirangelo (Université de Paris), Examiner
- Jean-Marc Talbot (Aix-Marseille Université), Examiner
- Paul Gastin (ENS Paris-Saclay), Advisor
- Benedikt Bollig (CNRS, ENS Paris-Saclay), Advisor
Abstract
This thesis is concerned with the expressive power of first-order logic and other formalisms over different classes of ordered structures, among which MSCs (Message Sequence Charts), a standard model for executions of message-passing systems. This study is motivated by two classic problems: the k-variable property, that is, the equivalence of first-order logic and its k-variable fragment over certain classes of structures, and the study of logic-automata connections, in the spirit of Büchi-Elgot-Trakhtenbrot theorem. Our approach relies on star-free propositional dynamic logic (star-free PDL), a variant of PDL with the same expressive power as the 3-variable fragment of first-order logic. We start by studying the expressive power of star-free PDL over linearly ordered structures with unary and binary predicates. We show that under certain monotonicity conditions, star-free PDL becomes as expressive as first-order logic. This implies that any first-order formula can then be rewritten into an equivalent formula with at most 3 variables. This result applies to various natural classes of structures, generalizing several known results and answering some open questions.
We then focus on MSCs, to which this first result also applies. We use star-free PDL to address another important problem: the synthesis of communicating finite-state machines (CFMs) from first-order specifications. CFMs are a model of concurrent systems in which a fixed number of finite-state automata communicate through unbounded FIFO channels. They accept languages of MSCs. While logical characterizations of the expressive power of CFMs have been established under different restrictions (bounding the size of the communication channels, or removing the "happened-before" relation from the logic), the following question had remained open in the general case: can every first-order formula over MSCs be translated into an equivalent CFM? We prove that this is the case, using star-free PDL as an intermediate language.