While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this article, we present and study the logic rLTL, which provides a means to formally reason about both correctness and robustness in system design. Furthermore, 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 φ, of size at most O(3 |φ |), where |φ | is the length of φ. This result improves upon the previously known bound of O(5|φ |) for rLTL verification and is closer to the LTL bound of O(2|φ |). 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.

Supervision of a nominal controller, to enforce safety, is concerned with appropriately modifying the generated control inputs, if needed, in order to keep a control system within a set of safe states. An integral component in supervision is a controlled invariant set contained in the set of safe states. In this paper, we build on recent results on the computation of polytopic controlled invariant sets to present a supervision framework that computes the corrected inputs analytically and, hence, suitable for real-time control. The framework is validated on the task of quadrotor obstacle avoidance by forcing the vehicle to navigate within controlled invariant sets of the obstacle-free space. The results are experimentally demonstrated on a Crazyflie 2.0 quadrotor.

In this paper we revisit the problem of computing controlled invariant sets for controllable discrete-time linear systems and present a novel hierarchy for their computation. The key insight is to lift the problem to a higher dimensional space where the maximal controlled invariant set can be computed exactly and in closed-form for the lifted system. By projecting this set into the original space we obtain a controlled invariant set that is a subset of the maximal controlled invariant set for the original system. Building upon this insight we describe in this paper a hierarchy of spaces where the original problem can be lifted into so as to obtain a sequence of increasing controlled invariant sets. The algorithm that results from the proposed hierarchy does not rely on iterative computations. We illustrate the performance of the proposed method on a variety of scenarios exemplifying its appeal.

Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic (LTL) specifications. Technically, robustness was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem. In general, model checking an rLTL formula relies on constructing a generalized Büchi automaton of size 5 | φ | where | φ | denotes the length of an rLTL formula φ. It was recently shown that the size of this automaton can be reduced to 3 | φ | (and even smaller) when the formulas to be model checked come from a fragment of rLTL. In this paper, we introduce Evrostos, the first tool for model checking formulas in this fragment. We also present several empirical studies, based on models and LTL formulas reported in the literature, confirming that rLTL model checking for the aforementioned fragment incurs in a time overhead that makes the verification of rLTL practical.