arXiv subjects

Tzanis Anevlavis

Publications and source records attributed to Tzanis Anevlavis.

3 recordsLinked to original sources

arXiv2022

Controlled invariant sets: implicit closed-form representations and applications

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.

math.OC↗

arXiv2021

Being correct is not enough: efficient verification using robust linear temporal logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this paper 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 $\mathcal{O} \left( 3^{ |φ|} \right)$, where $|φ|$ is the length of $φ$. This result improves upon the previously known bound of $\mathcal{O}\left(5^{|φ|} \right)$ for rLTL verification and is closer to the LTL bound of $\mathcal{O}\left( 2^{|φ|} \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.

cs.LO↗

arXiv2021

Automaton-based Implicit Controlled Invariant Set Computation for Discrete-Time Linear Systems

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.

eess.SY↗