Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems

Nathalie Cauchi, Luca Laurenti, Morteza Lahijanian, Alessandro Abate, Marta Kwiatkowska, Luca Cardelli

TL;DR

The paper addresses scalable formal analysis and control synthesis for discrete-time stochastic hybrid systems with linear continuous dynamics. It introduces an exact-error, dynamics-aware abstraction to an IMDP by performing a dynamics-driven space discretization, embedding the abstraction error into transition probabilities, and synthesizing robust strategies on this IMDP; these strategies are then refined back to the SHS with provable guarantees. The key contributions include a dynamics-dependent discretization technique, closed-form or efficiently computable transition-bounds via a transformed space, and convex optimization (or KKT) methods to obtain tight bounds; these are integrated into a two-stage process (abstraction and synthesis) that mitigates state-space explosion. Experiments across three case studies demonstrate orders-of-magnitude improvements in abstraction accuracy, substantial speedups, and scalable verification/synthesis for models with high-dimensional continuous state spaces (including more than ten continuous variables). The approach advances formal verification and synthesis for SHS under csltl and bltl specifications, providing practical tools for safety-critical cyber-physical systems.

Abstract

This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process (IMDP). Then, a strategy that maximizes the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to finite-time properties and rely on conservative over-approximations, we show that the exact abstraction error can be computed as a solution of convex optimization problems and can be embedded into the IMDP abstraction. This is later used in the synthesis step over both finite- and infinite-horizon specifications, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) significant (orders of magnitude) reduction of the abstraction error; (ii) marked speed-ups; and (iii) boosted scalability, allowing in particular to verify models with more than 10 continuous variables.

Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems

TL;DR

The paper addresses scalable formal analysis and control synthesis for discrete-time stochastic hybrid systems with linear continuous dynamics. It introduces an exact-error, dynamics-aware abstraction to an IMDP by performing a dynamics-driven space discretization, embedding the abstraction error into transition probabilities, and synthesizing robust strategies on this IMDP; these strategies are then refined back to the SHS with provable guarantees. The key contributions include a dynamics-dependent discretization technique, closed-form or efficiently computable transition-bounds via a transformed space, and convex optimization (or KKT) methods to obtain tight bounds; these are integrated into a two-stage process (abstraction and synthesis) that mitigates state-space explosion. Experiments across three case studies demonstrate orders-of-magnitude improvements in abstraction accuracy, substantial speedups, and scalable verification/synthesis for models with high-dimensional continuous state spaces (including more than ten continuous variables). The approach advances formal verification and synthesis for SHS under csltl and bltl specifications, providing practical tools for safety-critical cyber-physical systems.

Abstract

This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process (IMDP). Then, a strategy that maximizes the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to finite-time properties and rely on conservative over-approximations, we show that the exact abstraction error can be computed as a solution of convex optimization problems and can be embedded into the IMDP abstraction. This is later used in the synthesis step over both finite- and infinite-horizon specifications, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) significant (orders of magnitude) reduction of the abstraction error; (ii) marked speed-ups; and (iii) boosted scalability, allowing in particular to verify models with more than 10 continuous variables.

Paper Structure

This paper contains 30 sections, 7 theorems, 65 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Problem Formulation
  3. Stochastic Hybrid Systems
  4. Temporal Logic Specifications
  5. Problem Statement
  6. Overview of Proposed Approach
  7. Preliminaries
  8. Markov Models
  9. Polytopes and their Post Images
  10. SHS Abstraction as an IMDP
  11. Computation of the IMDP
  12. Space Discretization
  13. Transition Probability Bounds
  14. Transitions to $q \in \bar{Q}$
  15. Transitions to sink state $q_\mathrm{u}$
  16. ...and 15 more sections

Key Result

Proposition 1

For process $\mathbf{x}$ in mode $a \in A$, let $\mathcal{T}_a = \Lambda_a^{-\frac{1}{2}} V_a^T$ be a transformation function (matrix), where $\Lambda_a = V_a^T {Cov}_\mathbf{x}(a) V_a$ is a diagonal matrix whose entries are eigenvalues of ${Cov}_\mathbf{x}(a)$ and $V_a$ is the corresponding orthono where $\mathrm{erf}(\cdot)$ is the error function, and $y^{(i)}$ is the $i$-th component of vector

Figures (3)

  • Figure 1: Maximum error incurred in satisfying $\varphi_1$ as a function of time horizon $k$.
  • Figure 2: Synthesis results for $\varphi_2$ with (a) original set $X$ with simulated trajectories under $\sigma^*_{\varphi_2}$, (b) maximum error incurred in satisfying $\varphi_2$ as function of time horizon $k$, and lower bound probabilities of satisfying $\varphi_2$ for modes (c) $a_1$ and (d) $a_2$.
  • Figure 3: Lower bound probabilities of satisfying $\varphi_1$ with $|\bar{Q}|$ = 3721 and $k = 2$.

Theorems & Definitions (30)

  • Definition 1: shs
  • Definition 2: Switching strategy
  • Definition 3: csltl syntax
  • Definition 4: bltl syntax
  • Definition 5: Semantics
  • Definition 6: mdp
  • Definition 7: Strategy
  • Definition 8: imdp
  • Definition 9: Adversary
  • Remark 1
  • ...and 20 more