Maxence Dutreix

Cesar Santoyo, Maxence Dutreix, Samuel Coogan

This paper studies the problem of enforcing safety of a stochastic dynamical system over a finite time horizon. We use stochastic barrier functions as a means to quantify the probability that a system exits a given safe region of the state space in finite time. A barrier certificate condition that bounds the infinitesimal generator of the system, and hence bounds the expected value of the barrier function over the time horizon, is recast as a sum-of-squares optimization problem for efficient numerical computation. Unlike prior works, the proposed certificate condition includes a state-dependent bound on the infinitesimal generator, allowing for tighter probability bounds. Moreover, for stochastic systems for which the drift dynamics are affine-in-control, we propose a method for synthesizing polynomial state feedback controllers that achieve a specified probability of safety. Two case studies are presented that benchmark and illustrate the performance of our method.

Maxence Dutreix, Samuel Coogan

We derive an algorithm to compute satisfiability bounds for arbitrary ω-regular properties in an Interval-valued Markov Chain (IMC) interpreted in the adversarial sense. IMCs generalize regular Markov Chains by assigning a range of possible values to the transition probabilities between states. In particular, we expand the automata-based theory of ω-regular property verification in Markov Chains to apply it to IMCs. Any ω-regular property can be represented by a Deterministic Rabin Automata (DRA) with acceptance conditions expressed by Rabin pairs. Previous works on Markov Chains have shown that computing the probability of satisfying a given ω-regular property reduces to a reachability problem in the product between the Markov Chain and the corresponding DRA. We similarly define the notion of a product between an IMC and a DRA. Then, we show that in a product IMC, there exists a particular assignment of the transition values that generates a largest set of non-accepting states. Subsequently, we prove that a lower bound is found by solving a reachability problem in that refined version of the original product IMC. We derive a similar approach for computing a satisfiability upper bound in a product IMC with one Rabin pair. For product IMCs with more than one Rabin pair, we establish that computing a satisfiability upper bound is equivalent to lower-bounding the satisfiability of the complement of the original property. A search algorithm for finding the largest accepting and non-accepting sets of states in a product IMC is proposed. Finally, we demonstrate our findings in a case study.