Formal Techniques for Realizability Checking and Synthesis of Infinite-State Reactive Systems

Abstract

Reactive systems are fundamental building blocks in the development of critical safety systems. The are called "reactive" due to the necessity of them interacting with (or against) an unpredictable and uncontrollable environment, for an indefinite amount of time. As a consequence, the verification of a critical system more often than not in- volves the process of writing requirements, modeling, implementing and testing reactive subcomponents. Research in formal verification for reactive systems attempts to solve fundamental problems in each of these processes, with an emphasis given on the cre- ation of mathematical proofs regarding the system's safety. More importantly, it has been shown that such proofs can lead to significant savings both in development time as well as overall production cost. This dissertation explores the problem of reactive synthesis, where the goal is the development of decision procedures that are able to (dis)prove the realizability of reactive system specifications, as well as produce artifacts that essentially serve as witnesses to the decision. Reactive synthesis is a problem closely related to formal verification, as it requires the development of precise, mathematical proofs of realizability. The overwhelming majority of research conducted in this area has so far been focused in its application to propositional specification, where only operations over the Boolean domain can be performed. For the first part of this thesis, we propose novel, efficient reactive synthesis algorithms that extend the support for propositional specification to also generate implementations when the requirements involve the use of richer theories, such as integer and real arithmetic. We discuss the advantages and disadvantages of each algorithm, and accompany their implementation with a formal proof of soundness. In the second part of this dissertation, we delve into an unexplored sub-problem in reactive iv synthesis, where we present the first attempt ever to synthesize witnesses for infinite-state problems in which the implementation behaves in a random, diverse manner. While the product of synthesis is typically expected to be a deterministic witness, we argue that randomness can still be valuable in practice. To that end, we evaluate the application of randomly-behaving solutions to problems related to fuzz testing and robot motion planning, demonstrating how reactive synthesis can be used in an innovative way in software engineering concepts that have not been considered before.