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

## TL;DR

This paper introduces a method for verifying mixed monotone stochastic systems against omega-regular specifications by constructing finite-state interval-valued Markov chain abstractions and iteratively refining them based on specification-guided analysis.

## Contribution

It presents a novel abstraction and verification framework for mixed monotone stochastic systems using interval Markov chains and a specification-guided refinement process.

## Key findings

- Efficient computation of finite-state abstractions for mixed monotone systems.
- Successful verification of complex specifications using the proposed method.
- Case study demonstrating practical applicability and effectiveness.

## Abstract

This paper 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 has recently been show 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 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 the specification of interest from any initial state in the IMC. This is achieved by solving a reachability problem on 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-case and worst-case behaviors of accepting paths in the IMC and targets the appropriate states accordingly. Finally, we show a case study.