Search for: All records

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. 

Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, a robust semantics for LTL was introduced to capture different degrees by which a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring — such as the realizability of all truth values — can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation. 

In this paper we revisit the problem of computing controlled invariant sets for controllable discrete-time linear systems. We propose a novel algorithm that does not rely on iterative computations. Instead, controlled invariant sets are computed in two moves: 1) we lift the problem to a higher dimensional space where a controlled invariant set is computed in closed-form; 2) we project the resulting set back to the original domain to obtain the desired controlled invariant set. One of the advantages of the proposed method is the ability to handle larger systems. 

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. 

The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of ``cyber'' components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming.