| dc.description.abstract | Reactive systems are ubiquitous, with various use cases ranging from controllers for cyber-physical systems to programs that run on multipurpose computers. A system is reactive if it continually behaves in a specific manner (for example, a CPU bus arbiter granting incoming requests to access the bus) or performs certain computations upon receiving input from an external environment (for example, updating a variable based on an external HTTP request). Intuitively, the system continuously ”reacts” to an external environment. Automatically synthesizing correct-by-construction controllers for reactive systems that satisfy a given temporal specification is a challenging problem because the problem becomes highly intractable when the state space is finite and undecidable when the state space is infinite. Although reactive synthesis for finite-state systems is a ripe area with fundamental advances and tools, this is not true in the case of infinite-state reactive systems, which are in a nascent stage. In this thesis, we target synthesizing such reactive systems, which have an infinite state space where the temporal specification is ω-regular. We propose solutions to variations of this problem, resulting in state-of-the-art approaches and tools that advance the area fundamentally in terms of quantitative and qualitative solutions, apart from being scalable in practice.
The reactive synthesis problem is known to be reducible to solving a two-player zerosum game with a temporal objective. Two-player games are a fruitful way to represent and reason about several important synthesis tasks. These tasks include controller synthesis (where one asks for a controller for a given plant such that the controlled plant satisfies a given temporal specification), program repair (setting values of variables to avoid exceptions), and synchronization synthesis (adding lock/unlock statements in multi-threaded programs to satisfy safety assertions). In all these applications, a solution directly corresponds to a winning strategy for one of the players in the induced game. In turn, logically-specified games offer a powerful way to model these tasks for large or infinite-state systems. Much of the techniques proposed for solving such games rely on abstraction-refinement or template-based solutions. The first part of the thesis shows how to apply classical fixpoint algorithms to a symbolic logical setting that has hitherto been used in explicit, finite-state settings. To achieve this, we model reactive systems as infinite-state two-player games that we call logical LTL games. We provide a bouquet of efficient algorithms to synthesize controllers for such games. We also show how elegant symbolic encodings, combined with quantifier elimination using SMT solvers, can be fruitful regarding scalability. We implement our techniques in a tool called GenSys-LTL and show that they are not only effective in synthesizing valid controllers for a variety of challenging benchmarks from the literature but often compute maximal winning regions and maximally permissive controllers. We achieve 206X/ 13X speed-up (arithmetic/geometric mean) over the state-of-the-art, scale well for non-trivial LTL specifications, and synthesize controllers for previously unsolved benchmarks. Leading tools in the requirement analysis and model checking space have used ideas from this part of the thesis to scale their approaches.
In the second part of this thesis, we focus on a quantitative solution to the infinite-state reactive synthesis problem. Specifically, we ask if we can synthesize resilient controllers for infinite-state reactive systems for a given temporal specification (i.e., controllers resilient to a fixed number of external environment disturbances). Thus, there is now an ordering over the space of correct controllers, with the notion of a controller being ”better” than another controller if it can withstand more disturbances (i.e., being more resilient). This problem of synthesizing resilient controllers is well known for finite-state reactive systems; in this part of the thesis, we show how to lift this approach to synthesize resilient controllers for infinite-state reactive systems using an abstraction-based approach under multiple disturbance bounds. Moreover, we now model infinite-state reactive systems as a perturbed non-linear dynamical system. We consider the synthesis of resilient controllers for such systems w.r.t a temporal logic specification. We address this through the Abstraction Based Controller Design (ABCD) paradigm, where a finite state abstraction is first constructed and utilized for controller synthesis by viewing it as a two-player game. In this context, our contribution is twofold: (I) We construct abstractions that model the impact of occasional high disturbance spikes on the system via so-called disturbance edges. (II) We show that applying resilient reactive synthesis techniques to these abstract models results in closed-loop systems optimally resilient to these occasional high disturbance spikes. We have implemented this resilient ABCD workflow in our tool RESCOT and showcase our method through multiple robot planning examples. | en_US |
