Reactive Synthesis: Branching Logics and Parameterized Systems

TL;DR

This paper advances reactive synthesis by developing new approaches for CTL* logic and addressing parameterized system synthesis, including practical implementations and case studies like the industrial arbiter protocol.

Contribution

It introduces two novel methods for CTL* synthesis and extends parameterized synthesis techniques to open systems with liveness properties, with practical case studies.

Findings

Implemented two new CTL* synthesis approaches.

Proved tight cutoffs for open guarded systems with liveness.

Successfully synthesized the industrial AMBA protocol in a parameterized setting.

Abstract

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.