Search for: All records

We revisit the problem of computing (robust) controlled invariant sets 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 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. To validate the proposed method, we present thorough case studies illustrating that in safety-critical scenarios the implicit representation suffices in place of the explicit invariant set. The proposed method is complete in the absence of disturbances, and we provide a weak completeness result when disturbances are present. 

In this paper, we derive closed-form expressions for implicit controlled invariant sets for discrete-time controllable linear systems with measurable disturbances. In particular, a disturbance-reactive (or disturbance feedback) controller in the form of a parameterized finite automaton is considered. We show that, for a class of automata, the robust positively invariant sets of the corresponding closed-loop systems can be expressed by a set of linear inequality constraints in the joint space of system states and controller parameters. This leads to an implicit representation of the invariant set in a lifted space. We further show how the same parameterization can be used to compute invariant sets when the disturbance is not available for measurement. 

In this paper, we derive closed-form expressions for implicit controlled invariant sets for discrete-time controllable linear systems with measurable disturbances. In particular, a disturbance-reactive (or disturbance feedback) controller in the form of a parameterized finite automaton is considered. We show that, for a class of automata, the robust positively invariant sets of the corresponding closed-loop systems can be expressed by a set of linear inequality constraints in the joint space of system states and controller parameters. This leads to an implicit representation of the invariant set in a lifted space. We further show how the same parameterization can be used to compute invariant sets when the disturbance is not available for measurement. 

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. 

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.