Abstraction-based Synthesis for Stochastic Systems with Omega-Regular Objectives

This paper studies the synthesis of controllers for discrete-time, continuous state stochastic systems subject to omega-regular specifications using finite-state abstractions. We present a synthesis algorithm for minimizing or maximizing the probability that a discrete-time stochastic system with fi...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2020-09
Main Authors: Dutreix, Maxence, Huh, Jeongmin, Coogan, Samuel
Format: Article
Language:English
Subjects:
Algorithms
Controllers
Discrete time systems
Domains
Markov analysis
Markov chains
Maximization
Optimization
Partitions
Probability
Probability theory
Process parameters
Specifications
Stochastic systems
Synthesis
Transition probabilities
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper studies the synthesis of controllers for discrete-time, continuous state stochastic systems subject to omega-regular specifications using finite-state abstractions. We present a synthesis algorithm for minimizing or maximizing the probability that a discrete-time stochastic system with finite number of modes satisfies an omega-regular property. Our approach uses a finite-state abstraction of the underlying dynamics in the form of a Bounded-parameter Markov Decision Process (BMDP) arising from a finite partition of the system's domain. Such abstractions allow for a range of transition probabilities between states for each action. Our method analyzes the product between the abstraction and a Deterministic Rabin Automaton encoding the specification. Synthesis is decomposed into a qualitative problem, where the greatest permanent winning components of the product are created, and a quantitative problem, which requires maximizing the probability of reaching this component. We propose a metric for the quality of the controller with respect to the abstracted states and devise a domain partition refinement technique to reach a quality target. Next, we present a method for computing controllers for stochastic systems with a continuous input set. The system is assumed to be affine in input and disturbance, and we derive a technique for solving the qualitative and quantitative problems in the abstractions of such systems called Controlled Interval-valued Markov Chains. The greatest permanent component of such abstractions are found by partitioning the input space to generate a BMDP accounting for all possible qualitative transitions between states. Maximizing the probability of reaching this component is cast as an optimization problem. Quality of the synthesized controller and a refinement scheme are described for this framework.
ISSN:2331-8422