UCLA

Every engineer dreams of and strives for the day that more and more aspects of the daily life become smart, efficient, and automated. Smart grids, smart cities, mobility on demand and autonomous vehicles, even medical devices are a few domains with already significant progress towards a fully autonomous future. In such an increasingly autonomous world, guaranteeing safety and correctness of design and implementation of Cyber-Physical Systems (CPSs) is constantly under the spotlight. There is no room for error when a system interacts with and affects human lives. Consequently, we want to design systems that are safe and correct even when interacting with unknown, changing environments. We want the algorithms designing those systems to be efficient upon execution and provide formal guarantees about safety and correctness. In other words, they should act as a lightweight and impenetrable armor for the system.

Such armors are found in the work of the father of modern fiction literature, J.R.R.Tolkien. He conceived in his work the metal mithril, and mithril armors are described as ``light and yet harder than tempered steel''. Inspired by this, the approaches presented in this dissertation are termed mithrilian as they are characterized by computational efficiency and provide formal safety and robustness guarantees. More specifically, this dissertation discusses formal methods in control systems and is separated in two parts:

1. The first part concerns the synthesis of safety controllers via Robust Controlled Invariant Sets (RCISs). A safety enforcing controller keeps the state of the system within a set of safe states notwithstanding the presence of uncertainties. Using RCISs to design safety controllers is natural, as any trajectory starting within these sets, can always be forced to remain therein. On these grounds, we revisit the problem of computing RCISs for discrete-time linear systems. Departing from previous approaches, we consider implicit, rather than explicit, representations for controlled invariant sets. Moreover, by considering such representations in the space of states and finite input sequences we obtain \emph{closed-form} expressions for controlled invariant sets. An immediate advantage is the ability to handle high-dimensional systems since the closed-form expression is computed in a single step rather than iteratively. We present thorough case studies illustrating that in safety-critical scenarios the implicit representation suffices in place of the explicit RCIS. The proposed method is complete in the absence of disturbances and we provide a weak completeness result when disturbances are present. 2. In the second part, we switch gears and consider the problem of guaranteeing robustness in system design. Robustness is introduced in system verification by robust Linear Temporal Logic (rLTL). As CPSs inevitably become increasingly complex, the ability to completely guarantee correctness of their design and implementation via exhaustive testing fades. Most work in formal methods has focused on system correctness, i.e., in ensuring that systems are guaranteed to meet their design specifications. We argue that correctness is necessary, but not sufficient for a good design when a reactive system interacts with an ever-changing uncontrolled environment.Thus, in addition to correctness, systems should also be designed to be robust, i.e., small deviations from the assumptions made at design time should lead to, at most, small violations of the design specifications. The contribution here lies in refining the current complexity upper bound of rLTL verification and developing a tool for rLTL verification. More specifically, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula $\varphi$, of size at most $\bigO \left( 3^{ |\varphi|} \right)$, where $|\varphi|$ is the length of $\varphi$. This result improves upon the previously known bound of $\bigO \left(5^{|\varphi|} \right)$ and is closer to the LTL bound of $\bigO \left( 2^{|\varphi|} \right)$. The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification. To perform rLTL verification, we developed Evrostos, the first tool for model-checking rLTL formulas in this fragment.