Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems

This article addresses the problem of verifying discrete-time stochastic systems against omega-regular specifications using finite-state abstractions. Omega-regular properties allow specifying complex behavior and encompass, for example, linear temporal logic. We focus on a class of systems with mix...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on automatic control 2021-07, Vol.66 (7), p.2975-2990
Main Authors: Dutreix, Maxence, Coogan, Samuel
Format: Article
Language:English
Subjects:
Algorithms
Automata
Cartesian coordinates
Computational modeling
Discrete time systems
Finite-state abstractions
interval-valued Markov chains (IMCs)
Markov chains
Markov processes
mixed monotone systems
Partitioning algorithms
Specifications
Stochastic systems
Temporal logic
Upper bound
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This article addresses the problem of verifying discrete-time stochastic systems against omega-regular specifications using finite-state abstractions. Omega-regular properties allow specifying complex behavior and encompass, for example, linear temporal logic. We focus on a class of systems with mixed monotone dynamics. This class is shown to be amenable to efficient reachable set computation and models a wide range of physically relevant systems. In general, finite-state abstractions of continuous state stochastic systems give rise to augmented Markov chains wherein the probabilities of transition between states are restricted to an interval. We present a procedure to compute a finite-state interval-valued Markov chain (IMC) abstraction of discrete-time, mixed monotone stochastic systems subject to affine disturbances given a rectangular partition of the state space. Then, we suggest an algorithm for performing verification against omega-regular properties in IMCs. Specifically, we aim to compute bounds on the probability of satisfying a specification from any initial state in the IMC. This is achieved by solving a reachability problem on the sets of so-called winning and losing components in the Cartesian product between the IMC and a Rabin automaton representing the specification. Next, the verification of IMCs may yield a set of states whose acceptance status is undecided with respect to the specification, requiring a refinement of the abstraction. We describe a specification-guided approach that compares the best and worst case behaviors of accepting paths in the IMC and targets the appropriate states accordingly. Finally, we show a case study.
ISSN:0018-9286
1558-2523
DOI:10.1109/TAC.2020.3014142