Showing 1–2 of 2 results for author: Cerna, I

Optimal Observation Mode Scheduling for Systems under Temporal Constraints

Authors: Eva Tesarova, Maria Svorenova, Jiri Barnat, Ivana Cerna

Abstract: Autonomous control systems use various sensors to decrease the amount of uncertainty under which they operate. While providing partial observation of the current state of the system, sensors require resources such as energy, time and communication. We consider discrete systems with non-deterministic transitions and multiple observation modes. The observation modes provide different information abo… ▽ More Autonomous control systems use various sensors to decrease the amount of uncertainty under which they operate. While providing partial observation of the current state of the system, sensors require resources such as energy, time and communication. We consider discrete systems with non-deterministic transitions and multiple observation modes. The observation modes provide different information about the states of the system and are associated with non-negative costs. We consider two control problems. First, we aim to construct a control and observation mode switching strategy that guarantees satisfaction of a finite-time temporal property given as a formula of syntactically co-safe fragment of LTL (scLTL) and at the same time, minimizes the worst-case cost accumulated until the point of satisfaction. Second, the bounded version of the problem is considered, where the temporal property must be satisfied within given finite time bound. We present correct and optimal solutions to both problems and demonstrate their usability on a case study motivated by robotic applications. △ Less

Submitted 26 February, 2016; originally announced February 2016.

Comments: Technical report accompanying ACC'16 paper

Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games

Authors: Maria Svorenova, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cerna, Calin Belta

Abstract: We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over lin… ▽ More We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study. △ Less

Submitted 23 February, 2015; v1 submitted 20 October, 2014; originally announced October 2014.

Comments: Technical report accompanying HSCC'15 paper