Project topics and materials
Get Complete Project Material File(s) Now! »
Reactive Synthesis and the Church Problem
Overall, a specification relates infinite sequences of inputs to a set of infinite sequences of outputs that form acceptable behaviours. Since we are interested in reactive systems that are in constant interaction with their environment, it is often more convenient to see a specification as the set of words that consists in the interleaving of an infinite sequence of input with a corresponding acceptable behaviour. For instance, in the above example, if one asks that pour_coffee eventually happens after order_coffee is met, the corresponding specification consists in interleavings of an input sequence with any output sequence that satisfy this property. Then, the reactive synthesis problem asks, given a finitely represented specification, to generate a reactive program that satisfies the specification if it exists, and to provide a witness that the specification cannot be fulfilled otherwise. The problem was first posed in 1957 by Church, who asked what is now known as the Church problem [5]: Given a requirement which a circuit is to satisfy, we may suppose the requirement expressed in some suitable logistic system which is an extension of restricted arithmetic. The synthesis problem is then to find recursion equivalences representing a circuit that satisfies the given requirement (or alternatively, to determine that there is no such circuit). ([4]) Reactive systems are notoriously difficult to design correctly, and the main appealing idea of synthesis is to automatically generate systems that are correct by construction. In Church’s setting, the class of implementations consists in reactive programs that can be executed by Boolean circuits, i.e. that use a fixed finite amount of memory, which can be modelled by $-transducers.
Monadic Second-Order Logic
As for the specification formalism, Church mainly considered Monadic Second Order logic (MSO) over infinite words with the predicate ‚1 (or, equivalently, ) and predicates for letters of the alphabet. This logic is able to express the various specifications that we described above. For instance, asking that pour_coffee eventually occurs after order_coffee can be written as follows:
Synthesis as a Game
In an unpublished technical report [6], McNaughton pointed out that the problem can be seen as an infinite duration game between two players [7] that we call the Church game. One player models the system, and the other the environment. The goal of the system is to satisfy the specification and is antagonist to that of the environment, which aims at violating it∗. Then, a winning strategy for the system corresponds to an implementation of the specification, and a winning strategy for the environment witnesses that no such implementation exists. In 1969, J.R. Büchi and L.H. Landweber solved the problem for MSO specifications with game-theoretic techniques [8]. The method relies on converting the specification to a finite-state machine (more precisely an $-automaton, i.e. a finite-state automaton over $-words) that accepts the interactions which satisfy the specification. Then, such a machine is used as an observer for the game, and defines its winning condition. Later on, Rabin elaborated a solution that relies on tree automata [10]. In this thesis, we adopt the game-theoretic presentation, which allows to leverage known results about parity games, and provides an elegant formalism to describe implementations. We broadly follow the approach of [5] to the Church problem.
[6]: McNaughton (1965), Finite-state infi-nite games, cited in [5].
[7]: McNaughton (1993), ‘Infinite Games Played on Finite Graphs’
They cannot both have a winning strat-egy, since their objectives are antagonis-tic.
[8]: J.R. Büchi and L.H. Landweber (1969), ‘Solving sequential conditions finite-state strategies’ Recall that an interaction is modelled as an infinite sequence that alternates between input and output signals.
Linear Temporal Logic
For MSO specifications, Church’s problem inherits the non-elementary lower bound on the satisfiability of Monadic Second-Order Logic [11]. This skyrocketing complexity has long prevented any practical applications of synthesis algorithms. A first attempt to tame it was made with the introduction of Linear Temporal Logic (LTL) [12] in the context of model-checking for formal verification. The latter problem is the (better behaved) twin of the synthesis problem which, given a specification and a system, asks to determine whether the system satisfies the specification (in contrast, synthesis is about building the system from the specification). The authors showed that such a problem is PSpace-complete, and later on established that the reactive synthesis problem is 2-ExpTime-complete [13]. This complexity gap between the two problems is the reason why, as of today, formal verification has reached a wider level of practical applicability than its synthesis counterpart [14]. However, in the last decade, efficient methods and implementations have triggered a renewed.
[11]: Meyer (1975), ‘Weak monadic sec-ond order theory of succesor is not elementary-recursive’
[12]: Pnueli (1977), ‘The Temporal Logic of Programs’
[13]: Pnueli and Rosner (1989), ‘On the Synthesis of a Reactive Module’
[14]: Finkbeiner (2016), ‘Synthesis of Re-active Systems’
∗ Computer science modelling thus yields the unexpected situation of a coffee machine that is pitted against its users. interest for this field [3, 15, 16], and it is now a very active area of research [9, 17–20]. To get an idea of this formalism, let us point out that asking that pour_coffee eventually occurs after order_coffee can be written as G„order_coffee ) Fpour_coffee”, where G means that the property holds along the whole interaction, and F that it holds at some point in the future. Thus, this reads as ‘Along the entire run, it should be the case that if order_coffee is met, pour_coffee should be met in the future’.
Automata and Logics over Data Words
Contrary to the finite alphabet case, there is no known correspondence between automata and logics that can be exploited to solve the synthesis problem for specifications expressed in a logical formalism following a path similar to the Church problem for MSO specifications, that consists in representing the winning condition of the Church game with an automaton. In [28], the authors relate LTL with the freeze quantifier [33], that allows to ‘store’ a data value that appears in the formula, and register automata. They demonstrate that LTL with freeze formulas can be recognised by two-way alternating register automata, with a number of registers that is the same as the number of data variables that can be frozen [28, Theorem 4.1]. However, the emptiness problem of such a model is undecidable, already with one register when considering infinite words [28, Theorem 5.2]. Later on, Demri, D’Souza, and Gascon considered the Logic of Repeated Values, which limits the use of the freeze quantifier so as to get a logic that is both decidable and closed under negation [34]. However, it was shown in [35, Theorem 4.1] that games with objectives given as LRV formulas are undecidable. The case of single-sided specifications is decidable, and inspired our treatment of the synthesis problem for specifications expressed as deterministic register automata, triggering the introduction of the one-sided restriction. Yet, for lack of a suitable logic for expressing specifications that is expressive enough and allows both the system and the environment to manipulate data values, as a first step, we study the case of specifications expressed by register automata, that we call data automatic.
[28]: Demri and Lazic (2009), ‘LTL with the freeze quantifier and register au-tomata’
[33]: French (2003), ‘Quantified Propo-sitional Temporal Logic with Repeating States’
[34]: Demri, D’Souza, and Gascon (2012), ‘Temporal Logics of Repeating Values’
We say that a class of games is undecid-able if it is undecidable whether a given player has a winning strategy in them.
[35]: Figueira, Majumdar, and Praveen (2020), ‘Playing with Repetitions in Data Words Using Energy Games’
Control and Data Processing
Equipping finite-state automata with registers also allows to separate two aspects of the behaviour of the system, namely control and data processing, which demonstrates the relevance of the model already with a finite set of data values. Indeed, existing synthesis algorithms do not scale well when the size of the alphabet increases. For instance, if you come back to our running example, consider the setting where the machine can serve various types of beverages. There are finitely many, yet what matters is not so much the precise nature of the beverage as the fact that if a client orders G, they receive G. This parametricity cannot be captured by a finite alphabet with no further structure. This is illustrated by the following setting: assume the users make their choice in a set , and that clients can order at the same time. Then, the machine has to keep in memory the set of beverages that has been ordered. Any subset of size : of is possible, which means that the smallest automaton that represents the specification needs memory j j . In contrast, it can be represented : with a register automaton with : registers, that stores the order of each client in the corresponding register, and later on checks that each order has been correctly served. This is reflected on the implementation side: j j : machine with registers can store the orders in memory and serve them back in order using : states and : registers. This direction of research has been more specifically explored for spec-ifications expressed in (fragments of) first-order logic over data words under the name of parameterised synthesis, that operate under the assump-tion that there is a fixed but arbitrary number of distinct elements that interact with the system [36].
Restricting to Functional Specifications
However, already in the finite alphabet setting, the problem of deciding if a specification given as some non-deterministic synchronous transducer is realisable by some $-computable function is open. The particular case of realisability by $-computable functions of universal domain (the set of all $-words) is known to be decidable [51, Corollary 15]. In the asynchronous setting, the undecidability proof of [50, Theorem 17] can be easily adapted to show the undecidability of realisability of specifications given by non-deterministic (asynchronous) transducers by $-computable functions. In general, a specification is a relation from inputs to outputs. If this relation is a function, we call it functional. Due to the negative results just mentioned about the synthesis of $-computable functions from non-functional specifications, we instead here focus on the case of functional specifications and address the following general question: given the spec-ification of a function of data $-words, is this function ‘implementable’, where we define implementable as being $-computable by some Turing machine. Moreover, if it is implementable, then we want a procedure to automatically generate an algorithm that computes it. This raises another important question: how to decide whether a specification is functional? We investigate these questions for asynchronous register transducers, here called register transducers. This asynchrony allows for much more expressive power, but is a source of technical challenge.
Table of contents :
Affidavit
Digest / Propos
Abstract
Résumé
Contents
1. Introduction en français
1.1. Synthèse de programmes
1.2. Les systèmes réactifs
1.3. La synthèse réactive et le problème de Church
1.4. Extension aux alphabets infinis
1.5. Extension au cas asynchrone
1.6. Plan
1.7. Comment lire cette thèse ?
2. Introduction in English
2.1. Program Synthesis
2.2. Reactive Systems
2.3. Reactive Synthesis and the Church Problem
2.4. Extension to the Infinite Alphabet Case
2.5. Further Extension to the Asynchronous Case
2.6. Outline
2.7. How to Read this Thesis?
I. Reactive Synthesis
3. Reactive Synthesis over Finite Alphabets
3.1. Relations and Functions
3.2. Uniformisation and Program Synthesis
3.3. The Reactive Synthesis Problem
3.4. The Church Synthesis Problem
3.5. Games for Reactive Synthesis
4. Register Automata over a Data Domain
4.1. DataWords
4.2. Tests and Valuations
4.3. Register Automata
4.4. General Properties
4.5. Non-Deterministic Register Automata with Equality
4.6. Non-Deterministic Register Automata with a Dense Order
4.7. Register Automata with a Discrete Order
4.8. Universal Register Automata
4.9. Register Automata and Arithmetic
4.10. Extensions of the Model
5. Synthesis Problems over DataWords
5.1. Reactive Synthesis over DataWords
5.2. Data Automatic Specifications
5.3. Register Transducers
5.4. The Church Synthesis Problem
6. Register-Bounded Synthesis of Register Transducers
6.1. A Generic Approach
6.2. Universal Register Automata Specifications
6.3. Non-Deterministic Register Automata Specifications
7. Unbounded Synthesis of Register Transducers
7.1. Non-Deterministic Register Automata Specifications
7.2. Universal Register Automata Specifications
7.3. Deterministic Register Automata Specifications
8. Partial Versus Total Domain
8.1. Domains of Specification Automata
8.2. Uniformisation Problem
8.3. Good-Enough Synthesis
9. Conclusion
II. Computability of Functions Defined by Transducers over Infinite Alphabets
10. Non-Deterministic Asynchronous Register Transducers
10.1. The Model
10.2. Register Transducers and Register Automata
10.3. Functions Recognised by Transducers
10.4. Closure under Composition
11. $-Computability and Continuity
11.1. Computability
11.2. Continuity
11.3. $-Computability versus Continuity
12. Exploration of Various Data Domains
12.1. Data Domains with Equality
12.2. Oligomorphic Data Domains
12.3. Discretely Ordered Data Domains
13. Conclusion
14. Thesis Conclusion
14.1. Abstraction of the Behaviour of Register Automata
14.2. Generalisation to Other Formalisms
14.3. Minimisation and Learning
Appendix
A. Graphical Conventions
A.1. Relations and Functions, Input and Output
A.2. Reactive Synthesis
A.3. $-Automata
A.4. Register Automata
A.5. Synchronous Sequential Register Transducers
A.6. Non-Deterministic Asynchronous Register Transducers
B. Details of Chapter 3
B.1. Section 3.4.1 (Logics for Specifications)
B.2. Section 3.4.3 (Automata)
C. Details of Part II
C.1. Section 12.3.1 (Register Automata over a Discrete Domain)
Bibliography
