Correct-by-Design Control of Parametric Stochastic Systems Oliver Sch on1 Birgit van Huijgevoort2 Soﬁe Haesaert2 and Sadegh Soudjani1 Abstract This paper addresses the problem of computing

2025-05-06 0 0 1.15MB 8 页 10玖币

侵权投诉

Correct-by-Design Control of Parametric Stochastic Systems*

Oliver Sch¨

on1, Birgit van Huijgevoort2, Soﬁe Haesaert2, and Sadegh Soudjani1

Abstract— This paper addresses the problem of computing

controllers that are correct by design for safety-critical systems

and can provably satisfy (complex) functional requirements.

We develop new methods for models of systems subject to both

stochastic and parametric uncertainties. We provide for the ﬁrst

time novel simulation relations for enabling correct-by-design

control reﬁnement, that are founded on coupling uncertainties

of stochastic systems via sub-probability measures. Such new

relations are essential for constructing abstract models that are

related to not only one model but to a set of parameterized

models. We provide theoretical results for establishing this new

class of relations and the associated closeness guarantees for

both linear and nonlinear parametric systems with additive

Gaussian uncertainty. The results are demonstrated on a linear

model and the nonlinear model of the Van der Pol Oscillator.

I. INTRODUCTION

Engineered systems in safety-critical applications are re-

quired to satisfy complex speciﬁcations to ensure safe auton-

omy of the system. Examples of such application domains

include autonomous cars, smart grids, robotic systems, and

medical monitoring devices. It is challenging to design

control software embedded in these systems with guarantees

on the satisfaction of the speciﬁcations. This is mainly due

to the fact that most safety-critical systems operate in an

uncertain environment (i.e., their state evolution is subject

to uncertainty) and that their state is comprised of both

continuous and discrete variables.

Synthesis of controllers for systems on continuous and

hybrid spaces generally does not grant analytical or closed-

form solutions even when an exact model of the system

is known. A promising direction for formal synthesis of

controllers w.r.t. high-level requirements is to use formal

abstractions [2], [25]. The abstract models are built using

model order reduction and space discretizations and are

better suited for formal veriﬁcation and control synthesis

due to their ﬁnite space being amenable to exact, efﬁcient,

symbolic computational methods [1], [19], [23]. Controllers

designed on these ﬁnite-state abstractions can be reﬁned to

the respective original models by leveraging (approximate)

similarity relations and control reﬁnements [10].

In the past two decades, formal controller synthesis for

stochastic systems has witnessed a growing interest. The

survey paper [16] provides an overview of the current state

*This work is supported by the NWO Veni project CODEC (18244), the

UK EPSRC New Investigator Award CodeCPS (EP/V043676/1), and the

Horizon Europe EIC project SymAware (101070802).

1Oliver Sch¨

on and Sadegh Soudjani are with the School of

Computing, Newcastle University, Newcastle, NE4 5TG, UK.

o.schoen2@ncl.ac.uk,sadegh.soudjani@ncl.ac.uk

2Birgit van Huijgevoort and Soﬁe Haesaert are with the

Electrical Engineering Department, TU Eindhoven, The Netherlands

b.c.v.huijgevoort@tue.nl, s.haesaert@tue.nl

of the art in this line of research. Unfortunately, most of

the available results require prior knowledge of the exact

stochastic model of the system, which means any guarantee

on the correctness of the closed-loop system only holds

for that speciﬁc model. With the ever-increasing use of

data-driven modeling and systems with learning-enabled

components we are able to construct accurate parameterized

models with the associated conﬁdence bounds. This includes

conﬁdence sets that capture the model uncertainty via either

Bayesian inference or frequentist approaches. The former in-

cludes representations of conﬁdence sets via Bayesian system

identiﬁcation [21], while the latter include non-asymptotic

conﬁdence set computations [4], [13], [14].

Although existing results on similarity quantiﬁcation can

be extended to relate a model with a model set [10], these

results would lead to controllers parameterized in a similar

fashion as the model set. To design a single controller that

works homogeneously for all models in the model set, a

new type of simulation relation needs to be developed. In

this paper, we provide an abstraction-based approach that is

suitable for stochastic systems with model parametric uncer-

tainty. We assume that we are given an uncertainty set that

contains the true parameters, and design a controller such that

the controlled system satisﬁes a given temporal speciﬁcation

uniformly on this uncertainty set without knowing the true

parameters.

Problem 1: Can we design a controller such that

the controlled system satisﬁes a given temporal logic

speciﬁcation with at least probability pif the unknown

true model belongs to a given set of models?

The main contribution of this paper is to provide an answer

to this question for the class of parameterized discrete-time

stochastic systems and the class of syntactically co-safe

linear temporal logic (scLTL) speciﬁcations. We deﬁne a

novel simulation relation between a class of models and an

abstract model, which is founded on coupling uncertainties in

stochastic systems via sub-probability measures. We provide

theoretical results for establishing this new relation and the

associated closeness guarantees for both linear and nonlinear

parametric systems with additive Gaussian uncertainty.

The rest of the paper is organized as follows. After

reviewing related work, we introduce in Sec. II the necessary

notions to deal with the stochasticity and uncertainty. We

also give the class of models, the class of speciﬁcations, and

the problem statement. In Sec. III, we introduce our new

notions of sub-simulation relations and control reﬁnement

arXiv:2210.08269v1 [eess.SY] 15 Oct 2022

that are based on partial coupling. We also show how to

design a controller and use this new relation to give lower

bounds on the satisfaction probability of the speciﬁcation. In

Sec. IV, we establish the relation between parametric linear

and nonlinear models and their simpliﬁed abstract models.

Finally, we demonstrate the application of the proposed

approach on a linear system and the nonlinear Van der Pol

Oscillator in Sec. V. Due to space limitations, the proofs of

statements will be provided in an extended journal version.

Related work: There are several approaches developed

for parametric systems with no stochastic state transitions

[12], [20], [22]. One approach to dealing with epistemic

uncertainty in stochastic systems is to model it as a stochastic

two-player game, where the objective of the ﬁrst player is

to create the best performance considering the worst-case

epistemic uncertainty. The literature on solving stochastic

two-player games is relatively mature for ﬁnite state systems

[5], [6]. There is a limited number of papers addressing this

problem for continuous-state systems. The papers [18], [19]

look at satisfying temporal logic speciﬁcations on nonlinear

systems utilizing mu-calculus and space discretization. Our

approach builds on the concepts presented in [11] to design

controllers for stochastic systems with parametric uncertainty

that is compatible with both model order reduction and

discretization.

II. PRELIMINARIES AND PROBLEM STATEMENT

A. Preliminaries

The following notions are used. A measurable space

is a pair (X,F)with sample space Xand σ-algebra F

deﬁned over X, which is equipped with a topology. As a

speciﬁc instance of F, consider Borel measurable spaces,

i.e., (X,B(X)), where B(X)is the Borel σ-algebra on X,

that is the smallest σ-algebra containing open subsets of X.

In this work, we restrict our attention to Polish spaces [3].

A positive measure νon (X,B(X)) is a non-negative map

ν:B(X)→R≥0such that for all countable collections

{Ai}∞

i=1 of pairwise disjoint sets in B(X)it holds that

ν(SiAi) = Piν(Ai). A positive measure νis called a

probability measure if ν(X)=1, and is called a sub-

probability measure if ν(X)≤1.

A probability measure ptogether with the measurable

space (X,B(X)) deﬁnes a probability space denoted by

(X,B(X), p)and has realizations x∼p. We denote the

set of all probability measures for a given measurable space

(X,B(X)) as P(X). For two measurable spaces (X,B(X))

and (Y,B(Y)), a kernel is a mapping p:X× B(Y)→R≥0

such that p(x, ·) : B(Y)→R≥0is a measure for all x∈X,

and p(·, B) : X→R≥0is measurable for all B∈ B(Y).

A kernel associates to each point x∈Xa measure denoted

by p(·|x). We refer to pas a (sub-)probability kernel if

in addition p(·|x) : B(Y)→[0,1] is a (sub-)probability

measure. The Dirac delta measure δa:B(X)→[0,1]

concentrated at a point a∈Xis deﬁned as δa(A) = 1 if

a∈Aand δa(A)=0otherwise, for any measurable A.

For given sets Aand B, a relation R ⊂ A×Bis a subset

of the Cartesian product A×B. The relation Rrelates x∈A

with y∈Bif (x, y)∈ R, written equivalently as xRy. For

a given set Y, a metric or distance function dYis a function

dY:Y×Y→R≥0satisfying the following conditions for

all y1, y2, y3∈Y:dY(y1, y2) = 0 iff y1=y2;dY(y1, y2) =

dY(y2, y1); and dY(y1, y3)≤dY(y1, y2) + dY(y2, y3).

B. Discrete-time uncertain stochastic systems

We consider discrete-time nonlinear systems perturbed by

additive stochastic noise under model-parametric uncertainty.

This modeling formalism is essential if we can only access

an uncertain model of this stochastic system. Consider the

set of models {M(θ)with θ∈Θ}, parametrized with θ:

M(θ) : xk+1 =f(xk, uk;θ) + wk

yk=h(xk),(1)

where the system state, input, and observation at the kth time-

step are denoted by xk, uk, yk, respectively. The functions f

and hspecify, respectively, the parameterized state evolution

of the system and the observation map. The additive noise

is denoted by wk, which is an independent, identically

distributed noise sequence with distribution wk∼pw(·). We

assume throughout this paper that the uncertain parameter θ

belongs to a known, bounded polytope Θ⊂Rpfor some p.

A controller for the model (1) is denoted by Cand is im-

plemented as depicted in Fig. 1. We denote the composition

of the controller Cwith the model M(θ)as C×M(θ).

M(θ)

Fig. 1: Control design for a parameterized stochastic model.

C. Problem statement

Consider a parameterized model in (1) with θ∈Θ. We

are interested in designing a controller Cto satisfy temporal

speciﬁcations ψon the output of the model. This is denoted

by C×M(θ)ψ. Since the true θis unknown, can

we design a controller that does not depend on θand that

ensures the satisfaction of ψwith at least probability pψ?

We formalize this problem as follows:

Problem 2: For a given speciﬁcation ψand a threshold

pψ∈(0,1), design a controller Cfor M(θ)that does

not depend on the parameter θand that

P(C×M(θ)ψ)≥pψ,∀θ∈Θ.

The controller synthesis for stochastic models is studied in

[10] through coupled simulation relations. Although these

simulation relations can relate one abstract model to a set of

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

Correct-by-DesignControlofParametricStochasticSystems*OliverSch¨on1,BirgitvanHuijgevoort2,SoeHaesaert2,andSadeghSoudjani1AbstractThispaperaddressestheproblemofcomputingcontrollersthatarecorrectbydesignforsafety-criticalsystemsandcanprovablysatisfy(complex)functionalrequirements.Wedevelopnewmethods...

展开>> 收起<<

Correct-by-Design Control of Parametric Stochastic Systems Oliver Sch on1 Birgit van Huijgevoort2 Soﬁe Haesaert2 and Sadegh Soudjani1 Abstract This paper addresses the problem of computing.pdf

共8页,预览2页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Correct-by-Design Control of Parametric Stochastic Systems Oliver Sch on1 Birgit van Huijgevoort2 Soﬁe Haesaert2 and Sadegh Soudjani1 Abstract This paper addresses the problem of computing

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: