Similarity quantification for linear stochastic systems: A coupling compensator approach

TL;DR

This paper introduces a coupling compensator method for quantifying similarity between linear stochastic systems, enabling precise control system verification with explicit error bounds and probabilistic guarantees.

Contribution

It develops a novel computational approach to characterize simulation relations and error trade-offs for linear stochastic systems, enhancing abstraction accuracy.

Findings

The method effectively quantifies output deviations and transition probability errors.

It provides a systematic way to analyze the impact of errors on satisfaction probabilities.

Case studies demonstrate improved formal verification accuracy.

Abstract

For the formal verification and design of control systems, abstractions with quantified accuracy are crucial. This is especially the case when considering accurate deviation bounds between a stochastic continuous-state model and its finite (reduced-order) abstraction. In this work, we introduce a coupling compensator to parameterize the set of relevant couplings and we give a comprehensive computational approach and analysis for linear stochastic systems. More precisely, we develop a computational method that characterizes the set of possible simulation relations and gives a trade-off between the error contributions on the systems output and deviations in the transition probability. We show the effect of this error trade-off on the guaranteed satisfaction probability for case studies where a formal specification is given as a temporal logic formula.