PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Maxence Dutreix, Jeongmin Huh, Samuel Coogan

arXiv:2001.09236v2eess.SYcs.SY

TL;DR

The paper addresses how to synthesize policies for stochastic systems when randomness makes satisfaction of ω-regular specifications probabilistic. It uses finite-state abstractions and automata-based synthesis, extending the method to affine systems with continuous inputs; the approach targets maximizing or minimizing satisfaction probability and assesses controller quality through abstraction-relative measures and refinement.

  • Problem

    Because stochastic disturbances mean a specification may never be fully guaranteed, the paper seeks policies that maximize or minimize its satisfaction probability for discrete-time, continuous-state systems.

    Source: §1 · p. 3

  • Method

    The paper combines finite-state BMDP or CIMC abstractions with a Deterministic Rabin Automaton, finding permanent winning components and solving a reachability optimization problem.

    Source: §1 · pp. 5–6

  • Results

    The approach provides synthesis procedures for finite-mode systems without a BMDP connectivity assumption and for affine-in-input, affine-in-disturbance systems with continuous inputs.

    Source: §1 · pp. 5–6

  • Takeaways & Limitations

    The methods pair abstraction-based synthesis with controller-quality measures and partition refinement aimed at a desired optimality level.

    Source: §1 · pp. 5–7

    The system formulation places the state in a domain D and models mode-specific disturbances through continuous dynamics maps.

    Source: §3 · p. 9

Abstract

from arXiv · show

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.

1. Introduction

The paper develops finite-state abstraction methods for synthesizing policies that maximize or minimize satisfaction probabilities for ω-regular specifications. It extends the approach from finite-mode systems to affine stochastic systems with continuous inputs, with controller-quality measures and partition refinement in both settings.

1. Introduction

  • ω-regular specifications include LTL properties and can express liveness and persistence conditions beyond PCTL and cosafe LTL.The paper notes examples such as requiring an event to occur infinitely often.Source: §1 · pp. 2–4
  • The synthesis problem seeks policies that maximize or minimize the probability of satisfying an ω-regular specification because stochastic disturbances can prevent full guarantees.The paper considers both finite-mode and continuous-input control choices.Source: §1 · p. 3
  • The BMDP–DRA product reduces maximizing or minimizing ω-regular satisfaction probabilities to reachability of permanent winning components, without assuming a particular BMDP connectivity structure.For minimization, the product uses the complement of the specification; the paper also introduces a controller-quality measure and partition refinement, but does not formally prove refinement convergence.Source: §1 · p. 5
  • The method extends synthesis to affine-in-input and affine-in-disturbance stochastic systems with continuous input sets using Controlled Interval-valued Markov Chain abstractions.Finding permanent winning components uses a CIMC–DRA product; maximizing reachability is formulated as an optimization problem that may be non-convex.Source: §1 · pp. 6–7
  • For finite-mode systems, the paper constructs BMDP abstractions from domain partitions and synthesizes switching policies for ω-regular specifications.The resulting policy is mapped onto the continuous abstracted states.Source: §1 · p. 6
  • The paper measures policy quality relative to the original abstracted system states and proposes specification-guided partition refinement to target user-defined optimality.The refinement strategy selects states to refine and discusses properties passed from coarser to refined abstractions.Source: §1 · pp. 6–7

2. Preliminaries

The preliminaries define deterministic Rabin automata as a way to represent properties over infinite words. Their acceptance condition requires some states to recur infinitely often while states in a paired set occur only finitely often.

2. Preliminaries

  • A DRA is defined as a five-tuple containing states, an alphabet, a transition function, an initial state, and an acceptance condition.The supplied definition identifies the tuple components as S, Π, δ, s0, and Acc.Source: §2 · pp. 7–8
  • A DRA accepts an infinite word when, for some acceptance pair, states in F_i occur infinitely often and all states in E_i occur finitely often.A property is the set of words accepted by the automaton; ω-regular properties are characterized by such automata.Source: §2 · p. 8
  • Every LTL-defined property is ω-regular, including properties expressed with eventuality and infinite-repetition operators.The text gives “Eventually reach A” as an example of an LTL property with an equivalent ω-regular expression.Source: §2 · p. 8

3. Problem Formulation

The section formulates probability-minimizing or -maximizing control for omega-regular properties in stochastic systems, using finite abstractions for both finite-mode and continuous-input settings. It also specifies how abstraction quality can be improved through partition refinement.

3. Problem Formulation

  • The control objective is to minimize or maximize the probability that a system trajectory satisfies an omega-regular property from a given initial state.The formulation covers both finite-mode systems and systems with continuous inputs.Source: §3 · pp. 9, 10, 17
  • A finite partition abstracts the continuous domain, with BMDP transition-probability intervals accommodating variation among continuous states in the same abstract state.The abstraction is assumed available; the paper focuses on refining the partition rather than computing the abstraction.Source: §3 · pp. 10–12
  • For a BMDP policy, the method maximizes the lower satisfaction-probability bound or minimizes the upper bound, which contain the original system’s probability.A single abstract-state action is applied to all continuous states represented by that state.Source: §3 · p. 15
  • The partition is selectively refined toward a user-defined quality threshold, targeting states at higher risk of suboptimal control or responsible for substantial uncertainty.Selective refinement aims to avoid unnecessary growth of the abstraction’s state space.Source: §3 · p. 16
  • For continuous-input systems, the formulation assumes dynamics affine in input and disturbance and introduces CIMC abstractions with a continuous input set.The framework also considers partition refinement to reach a user-defined policy-quality threshold.Source: §3 · pp. 16–18

4. CONTROLLER SYNTHESIS FOR FINITE MODE SYSTEMS

This section develops controller synthesis for finite-mode systems by analyzing the BMDP–DRA product and characterizing switching policies for winning components. It reduces policy selection to reachability-probability optimization on a fixed state set.

4.1. BMDP CONTROLLER SYNTHESIS

  • The BMDP–DRA product monitors paths against the ω-regular property and supports switching-policy synthesis for maximizing or minimizing satisfaction probabilities.The DRA acts as finite memory, tracking transitions and the property status along each path.Source: §4.1 · pp. 19–20

Lemma 1. A lower bound maximizing and upper bound minimizing switching

  • Minimizing the upper-bound probability for a property is reduced to maximizing the lower-bound probability for its complement, using the corresponding product and memoryless reachability policies.The paper states that optimal switching policies for BMDP reachability objectives are memoryless.Source: §4.1 · pp. 22, 27, Lemma 1. A lower bound maximizing and… · p. 28

4.1. BMDP CONTROLLER SYNTHESIS

  • Zero-lower-bound transitions can be switched on or off, changing accepting and non-accepting BSCCs; the largest winning and losing components characterize the corresponding probability bounds.The upper bound on satisfying the property equals the upper-bound reachability probability of the largest winning component; the lower bound is obtained using the largest losing component.Source: §4.1 · pp. 24–25

P and U(W C)G

  • For maximizing satisfaction, memoryless product policies generate the greatest permanent winning component, and the induced controller maximizes the lower-bound probability of reaching it.The greatest permanent winning component is the largest set of states that remains winning across the relevant induced product IMCs.Source: §4.1 · p. 27, Lemma 1. A lower bound maximizing and… · p. 28

Lemma 1. A lower bound maximizing and upper bound minimizing switching

  • Desired policies are computed by maximizing lower-bound reachability on a fixed state set, using the value-iteration scheme in.The passage says an algorithm for finding the winning sets and associated control actions follows in the next subsection.Source: Lemma 1. A lower bound maximizing and… · p. 29
  • Auxiliary policies maximize upper-bound and minimize lower-bound winning-component reachability to assess the quality of the lower-bound maximizing policy.These policies are not mapped onto the original system states; the upper-bound maximization is solved on the Greatest Winning Component.Source: Lemma 1. A lower bound maximizing and… · p. 29
  • A set of memoryless switching policies yields the largest winning component of the product BMDP for each policy in that set.The passage names this set the Greatest Winning Component.Source: Lemma 1. A lower bound maximizing and… · pp. 29–30

L and U(W C)G

This section develops graph-based methods for identifying permanent accepting and winning components in product abstractions and constructing policies that generate them. It describes SCC searches and acceptance and transition checks, including an alternative target set for upper-bound maximizing and lower-bound minimizing policies.

L and U(W C)G

  • Upper- and lower-bound probabilities are associated with switching policies that maximize and minimize, respectively, and replacing greatest winning components with greatest accepting BSCCs preserves the bounds.The components and their generating control actions are found by graph search.Source: L and U(W C)G · pp. 30–31

4.2. WINNING COMPONENTS SEARCH ALGORITHMS

  • The search first finds an extended greatest permanent accepting BSCC, then alternates graph search with reachability maximization to construct the greatest permanent winning component and a generating switching policy.The second step recovers states outside the extended set whose lower-bound probability of reaching an accepting BSCC is nevertheless one under some policy.Source: §4.2 · p. 31

4.2.1. GREATEST PERMANENT BSCC SEARCH ALGORITHMS

  • The BSCC search starts from SCCs with all actions, prunes states and actions permitting transitions outside, then tests acceptance and whether any subset can form a non-accepting BSCC.It maximizes the lower-bound probability of reaching unmatched Rabin-accepting states; a zero-probability subset is treated as potentially non-accepting, while an empty such set certifies acceptance for all adversaries.Source: §4.2.1 · pp. 32, 33, 35

4.2.2. GREATEST PERMANENT COMPONENTS SEARCH ALGORITHMS

  • States outside permanent BSCCs can still belong to a permanent winning component if they cannot escape their set together with those BSCCs and no subset can form a non-accepting BSCC.These include permanent sink states that reach another winning set with lower-bound probability one, as well as states that may be sinks or part of a winning component reaching a non-permanent accepting BSCC with probability one.Source: §4.2.2 · p. 36
  • Algorithm 2 finds states in the product BMDP where a control policy induces one of the permanent-component scenarios.It returns the greatest permanent winning component together with its associated control actions.Source: §4.2.2 · pp. 37–38
  • The algorithm initializes from extended permanent accepting BSCCs, then adds states that can be made permanent sinks by maximizing the lower-bound probability of reaching the component.States with a lower-bound probability of 1 are added to the greatest permanent winning component.Source: §4.2.2 · p. 37
  • For potential accepting BSCCs, the algorithm tests whether a policy keeps transitions within the candidate set and winning component for every transition-interval instantiation.It then excludes states with zero lower-bound reachability to unmatched Rabin accepting states, so retained states form sinks or accepting BSCCs under all adversaries.Source: §4.2.2 · pp. 37–38
  • A slight modification computes (WC)G_L, using (U+)G_L as the target for upper-bound maximizing and lower-bound minimizing policies.Source: §4.2.2 · p. 38

P 4: repeat

This section examines BMDP synthesis for omega-regular objectives, including policy suboptimality measures and partition refinement guided by product structure and transition-probability assignments. It also considers CIMC abstractions for continuous-input systems, while noting that refinement is not guaranteed to improve quality monotonically and convergence remains conjectural.

P 4: repeat

  • The synthesis procedure finds a greatest permanent winning component in the product with a DRA, then optimizes reachability to it for the remaining states.It maximizes the lower-bound satisfaction probability for the specification or minimizes the upper bound using the complement specification.Source: P 4: repeat · p. 40

4.3.1. QUALITY OF COMPUTED POLICY

  • The quality measure captures policy suboptimality in the abstraction, and the value-iteration bounds can also identify actions that are provably suboptimal or optimal.The measure and discussion apply to probability maximization and, by duality, to minimization.Source: §4.3.1 · pp. 40, 42

4.3.2. REFINEMENT PROCEDURE

  • The refinement procedure scores partition states by uncertainty and influence, refines states with high scores, and repeats synthesis until the optimality factor meets the target.The score reflects differences between best- and worst-case behavior and whether a state can affect other states known to be suboptimally controlled.Source: §4.3.2 · pp. 45–46
  • The refinement score may depend on the chosen best- and worst-case Markov chains, but the authors expect this to have negligible long-term effect except in pathological cases.Differences within permanent components do not affect scores, while ambiguous states are specifically targeted during refinement.Source: §4.3.2 · pp. 47–48
  • An action suboptimal in a product BMDP is suboptimal for every concrete state in its partition, so it can be removed during refinement.The proposition also covers minimization; further actions that cannot generate winning components may be excluded from qualitative component search.Source: §4.3.2 · pp. 50–51
  • Specification-guided refinement removes actions as partitions become finer and is presented as reducing computation versus StocHy [19], FAUST2 [30], and the refinement method in.Unlike single-gridding approaches, it tailors refinement to the specification and targets states using the abstraction's structure.Source: §4.3.2 · p. 54

4.3.3. MONOTONICITY AND CONVERGENCE OF SYNTHESIS PROCEDURE

  • Refinement need not monotonically decrease the greatest suboptimality factor ϵmax, because finer abstractions can change winning components and reachability bounds.The method saves coarse-partition component states to address component changes, but the reachability-bound effect also disrupts monotonicity in the value-iteration algorithm of [16].Source: §4.3.3 · p. 57
  • The authors conjecture convergence under continuity and adequate BMDP abstractions if non-permanent discrete states shrink to zero, but leave a formal proof for future work.They also identify enforcing monotonicity by modifying value iteration to use information from coarser partitions as future work.Source: §4.3.3 · pp. 57–58
  • The suboptimality factor bounds how much a continuous state’s specification-satisfaction probability could improve by changing the computed memoryless product policy’s action.It compares the computed policy’s worst-case interval assignment with the most optimistic best-case assignment.Source: §4.3.3 · p. 58
  • Worst- and best-case transition scenarios identify certainly suboptimal actions and guide selective state-space refinement toward a user-defined precision threshold.The iterative heuristic targets regions by comparing these two extreme scenarios.Source: §4.3.3 · p. 58
  • Propositions 2 and 3 establish structural properties preserved from coarser to refined abstractions, reducing computations after each refinement step.Source: §4.3.3 · p. 58
  • Continuous-input stochastic systems cannot be abstracted into BMDPs, so their synthesis uses CIMC abstractions instead.Source: §4.3.3 · p. 59

5. CONTROLLER SYNTHESIS FOR CONTINUOUS INPUT SYSTEMS

This section extends controller synthesis to continuous-input stochastic systems using CIMC abstractions. It constructs winning components, optimizes lower-bound reachability over continuous inputs, and refines state and input partitions to improve controller quality.

5. CONTROLLER SYNTHESIS FOR CONTINUOUS INPUT SYSTEMS

  • The continuous-input framework forms a CIMC abstraction and a product with a DRA, then solves qualitative component construction and quantitative maximization of lower-bound reachability, with partition refinement for controller quality.The method aims to reach a specified level of optimality with respect to the abstracted system.Source: §5 · pp. 59, 62, 63
  • Because exhaustive action search cannot handle uncountably many inputs, the method exploits the underlying dynamics and CIMC transition bounds under additional assumptions.The assumptions enable closed-form transition-bound expressions as functions of the input; additive inputs shift rectangular reachable-set over-approximations.Source: §5 · pp. 60–61

5.1. COMPONENTS CONSTRUCTION

  • Geometric trigger regions classify inputs as making a transition off, on, or undecided, and their overlaps identify inputs that induce qualitatively different outgoing-transition profiles.Overlaps involving multiple undecided transitions may require further examination because similar transition types can produce different qualitative profiles.Source: §5.1 · pp. 65, 67
  • For component construction, the method partitions each state’s input space into trigger-region overlaps and selects representative inputs, reducing CIMC search to a finite-action product BMDP.Different overlaps yield qualitatively different transition profiles; some overlaps may require multiple control actions to capture different combinations of inactive uncertain transitions.Source: §5.1 · pp. 64, 65, 67, 69
  • The input-selection procedure may choose more actions than necessary, and its optimization problem is non-convex under the stated system assumptions and generally hard to solve.Different combinations of inactive uncertain transitions may need to be distinguished within overlaps of undecided trigger regions.Source: §5.1 · p. 69
  • Algorithm 6 constructs the greatest permanent winning component and greatest winning component of the abstraction by building a BMDP and searching its product with the specification automaton.The procedure computes overlap sets and input actions for partition states before applying component search. Its action space may be larger than necessary because distinct achievable transition combinations can be handled by one action, but the procedure may select different actions for each.Source: §5.1 · p. 71

5.2. REACHABILITY MAXIMIZATION

  • For continuous inputs, lower-bound reachability maximization in the product CIMC requires solving an optimization problem to select inputs, rather than enumerating finite actions.The resulting problem is non-convex under the stated system assumptions, and the case study uses numerical heuristics; because value iteration is not guaranteed to converge finitely, the method stops when the maximum probability change reaches a user-defined threshold.Source: §5.2 · pp. 72–73

5.3. STATE SPACE REFINEMENT

  • Partition refinement assesses controller quality using best- and worst-case product Markov chains and removes input subsets whose upper-bound reachability is below the current lower bound.Finer input discretization can discard more suboptimal inputs per iteration, at the cost of more optimization problems; computational complexity also depends strongly on the reachability optimization method.Source: §5.3 · pp. 73–75
Loading 2001.09236v2…