Reactive Synthesis: Branching Logics and Parameterized Systems

Reactive synthesis is an automatic way to translate a human intention expressed in some logic into a system of some kind. This thesis has two parts, devoted to logic and to systems. In Part I, we develop two new approaches to CTL* synthesis. The first approach consists of two extensions of the SMT-based bounded synthesis: one follows bottom-up CTL* model checking, another one follows the automata framework. The second approach reduces CTL* synthesis to LTL synthesis. The reduction turns any LTL synthesiser into a CTL* synthesiser. The two approaches were implemented and are available online. In Part II, we study parameterized synthesis for two system architectures. The first architecture is guarded systems and is inspired by cache coherence protocols. In guarded systems, processes transitions are enabled or disabled depending on the existence of other processes in certain local states. The existing cutoff results for guarded protocols are restricted to closed systems, and are of limited use for liveness properties. We close these gaps and prove tight cutoffs for open systems with liveness properties, and also cutoffs for detecting deadlocks. The second architecture is token-ring systems, where the single token circulates processes arranged in a ring. The experiments with the existing parameterized synthesis method showed that it does not scale to large specifications. First, we optimize the method by refining the cutoff reduction, using modularity and abstraction. The evaluation show several orders of magnitude speed-ups. Second, we perform parameterized synthesis case study on the industrial arbiter protocol AMBA. We describe new tricks —a new cutoff extension and decompositional synthesis— that, together with the previously described optimizations, allowed us to synthesize AMBA in a parameterized setting, for the first time.