Contract Duration in Continuoustime in R

• Access throughyour institution

Assume-guarantee contracts for continuous-time systems☆

Abstract

Many techniques for verifying properties of continuous-time systems are limited to systems of moderate size. In this paper, we propose an approach based on assume-guarantee contracts and compositional reasoning for verifying properties of a broad class of continuous-time systems consisting of interconnected components. The notion of assume-guarantee contracts makes it possible to divide responsibilities among the system components: a contract specifies the property that a component must fulfill under some assumptions on the behavior of its environment (i.e. of the other components). We define weak and strong semantics of assume-guarantee contracts. We then establish a certain number of results for compositional reasoning, which allow us to show that a global assume-guarantee contract of the whole system is satisfied when all components satisfy their own contracts. We show that the weak satisfaction of the contract is sufficient to deal with interconnections described by a directed acyclic graph, while strong satisfaction is needed to reason about general interconnections containing cycles. Specific results for systems described by differential inclusions and invariance assume-guarantee contracts are then developed. Finally, we show how the proposed assume-guarantee framework can recast different versions of the small-gain theorem as a particular case. Throughout the paper, the main results are illustrated using simple examples.

Introduction

Cyber–physical systems (CPS) result from integrations of computational devices with physical processes and are to become ubiquitous in modern societies (autonomous vehicles, smart buildings, robots, etc.) (see Lee & Seshia, 2016 and the references therein). Despite considerable progress in the field, current techniques apply to system of moderate complexity (the complexity is quantified by the number of interacting components). Thus, the design of complex CPS requires to divide large design problems in smaller sub-problems that can be solved using existing tools.

Compositional approaches for the analysis and the design of dynamical systems have been long known in the field of control theory, where the celebrated small-gain theorem (Desoer and Vidyasagar, 1975, Jiang et al., 1994, Khalil, 1996) makes it possible to prove stability of a system from the stability of its components. Other compositional approaches for the analysis and design of cyber–physical systems have been mainly initiated in the field of computer science (Alur et al., 2001, Frehse, 2005, Henzinger et al., 2001).

The study of properties of dynamical systems using decentralized approaches has been an ongoing research area in recent years (Arcak et al., 2016, Conte et al., 2012, Coogan and Arcak, 2015, El-Guindy et al., 2017, Nilsson and Ozay, 2016, Raković et al., 2010, Sloth et al., 2012). Other compositional approaches, using formal methods and symbolic techniques, are presented in Dallal and Tabuada, 2015, Kim et al., 2015, Le Coënt et al., 2016, Mallik et al., 2018, Meyer and Dimarogonas, 2018, Meyer et al., 2017, Saoud et al., 2018, Saoud et al., 2018, Smith et al., 2016 and Zamani and Arcak (2017). All these works develop efficient computational techniques by making specific assumptions on the classes of dynamical systems and of properties to which they can be applied.

In the current work, we aim at proposing a general theoretical framework and thus we make weak assumptions on systems and properties. We initiate a high-level framework for verifying properties of complex systems, consisting of interconnected components, using a contract-based approach (Benveniste et al., 2018). Each component is assigned an assume-guarantee contract, which specifies the property that the component must fulfill under assumption about its environment (i.e. the other components). We introduce contracts and define weak and strong semantics. We then establish results that allow us to reason compositionally using assume-guarantee contracts: i.e. if all components satisfy their own contract then a global contract of the whole system is satisfied. We show that the weak satisfaction of the contract is sufficient to deal with interconnections described by a directed acyclic graph, while strong satisfaction is needed to reason about general interconnections containing cycles. We then show that for systems described by differential inclusions and invariance assume-guarantee contracts, weak satisfaction of contracts is sufficient to reason on general interconnections. Finally, we show how the proposed assume-guarantee framework can recast different versions of the small-gain theorem as a particular case.

There are several advantages in using contract based design for CPS. Firstly, by dividing a complex design problem into several smaller sub-problems, one is able to address design challenges that would be out of reach of current state-of-the-art design methods. Secondly, contract-based design makes it possible to replace a component without jeopardizing the behavior of the overall system: one just has to make sure that the new component satisfies the assigned contract. Thirdly, components are re-usable when similar contracts appear in the decomposition of a global contract.

Let us emphasize that the main objective of the paper is to provide compositionality rules on how to go from the satisfaction of local contracts for the components to the satisfaction of a global contract for the whole interconnected system. The question on how to construct the local contracts from the global one is not investigated in this paper, but have been explored in other works in the literature for continuous-time in Zonetti, Saoud, Girard, and Fribourg (2019) and Benveniste et al. (2018, Section 8.6), and for discrete-time (Chen et al., 2019, Eqtami and Girard, 2019, Ghasemi et al., 2020) systems.

The present paper focuses on the theoretical development of a general framework for contract-based reasoning. Applications of this framework to the design of symbolic controllers are reported in Saoud et al., 2018, Saoud et al., 2018 and Zonetti et al. (2019).

Contract based design for CPS has been widely studied in Benveniste et al. (2018). Our approach differs from the one proposed in Benveniste et al. (2018) in several directions:

•

In Benveniste et al. (2018) the contracts need to be checked for the whole time domain on which trajectories are defined. In this paper, the satisfaction of contracts is defined in a progressive and time-dependent way, which makes it possible to detect the instant at which the contract is violated.

•

While in Benveniste et al. (2018) assumptions and guarantees are defined over all the set of variables, namely inputs and outputs, in this paper, we focus on the case where assumptions are defined on the inputs and guarantees on the states and outputs. Indeed, this restriction allows us to provide simple compositionality results.

•

The use of saturated contracts is crucial in applying the contract framework proposed in Benveniste et al. (2018), which requires being able to compute unions and complements of different assertions. In this paper, saturation of the contracts is not required, and one can deal directly with the contracts as they are.

Assume-guarantee reasoning has been previously used in control theory. The authors in Kerber and Van Der Schaft (2009) presented a compositionality result for linear dynamical systems based on the notion of simulation introduced in Van der Schaft (2004). In spirit, our work is closer to the framework presented in Kim, Arcak, and Seshia (2017) for verifying general properties using parametric assume-guarantee contracts and compositional reasoning by means of small-gain theorems. Our approach differs from the one proposed in Kim et al. (2017) in the following directions:

•

The approach proposed in Kim et al. (2017) follows the framework of Benveniste et al. (2018), which makes a noticeable difference with our results;

•

In Kim et al. (2017), the results hold only for discrete-time systems, while our approach makes it possible to deal with both continuous and discrete-time systems.

•

The main compositionality result in Kim et al. (2017) requires to assume that at least one component satisfies a contract (for some parameter value), independently of the behavior of other components. This breaks the circularity of implications of the assume-guarantee contracts, which is arguably the main difficulty in contract-based design, and the reason why we introduce weak and strong semantics for assume-guarantee contracts, which has not been done in Kim et al. (2017).

•

In Kim et al. (2017), the authors show how their framework makes it possible to reprove the classical bounded input bounded output small-gain theorem for discrete-time systems. In our paper we show how the proposed framework allows to recast the bounded input bounded output small gain theorem for continuous-time systems. Moreover, we provide a new small-gain result for the notion of growth bound, which has not been proposed before in the control literature.

The paper is organized as follows. In Section 2, we introduce the class of prefix-closed properties. In Section 3, we introduce the class of systems and interconnections considered throughout the paper. In Section 4, we introduce assume-guarantee contracts, their weak and strong semantics. We then establish compositionality results for reasoning about interconnected systems in Section 5. In Section 6, we develop specific results for systems described by differential inclusions and invariance assume-guarantee contracts. Finally, in Section 7, we show that different versions of the classical small-gain theorem can be recast as particular applications of our framework. Throughout the paper, simple examples are used as illustrations of the main results.

Due to space constraints, the results for discrete-time systems and contracts are omitted and can be found in Saoud (2019, Chapter 2). A preliminary version of this work has been presented in the conference paper (Saoud, Girard, & Fribourg, 2018). The current paper extends the approach in different directions. First, we generalize the approach from cascade and feedback compositions to any composition structure and from invariance to more general properties. Second, while in Saoud et al. (2018), we have shown that for systems described by Lipschitz differential inclusions, the notion of invariance relative to assume-guarantee contracts implies the weak satisfaction. In the current work, we show the converse result. Finally, in the current work, we show that different versions of the classical small-gain theorem can be recovered using our framework.

Notation

$\mathbb{R}$ , ${\mathbb{R}}_0^{+}$ , ${\mathbb{R}}^{+}$ and $\mathbb{N}$ denote the set or reals, nonnegative reals, positive reals and positive integers respectively. The set of continuous-time domains is $\mathbb{E}\left({\mathbb{R}}_0^{+}\right)=\{[0,a],a\in {\mathbb{R}}_0^{+}\}\cup \{[0,a),a\in {\mathbb{R}}^{+}\}\cup \left\{{\mathbb{R}}_0^{+}\right\}$ . For $Z\subseteq {\mathbb{R}}^n$ , we denote by $M\left(Z\right)$ the set of continuous-time maps $z:E\to Z$ , where $E\in \mathbb{E}\left({\mathbb{R}}_0^{+}\right)$ . For $q\in {\mathbb{N}}_0^{+}$ , ${\mathcal{D}}^q$ denotes the set of continuous-time maps q times differentiable. For $x\in {\mathbb{R}}^n$ , $\Vert x\Vert$ denotes the infinity norm. For a continuous-time map $x:E\to {\mathbb{R}}^n$ and for $t\in E$ , ${\Vert x_{\mid [0,t]}\Vert }_{\infty }$ denotes the essential supremum of $x:E\to {\mathbb{R}}^n$ on $[0,t]$ . Given a space $X$ equipped with a metric $d:X\times X\to {\mathbb{R}}_0^{+}$ , the closure of the set $A\subseteq X$ is denoted $\mathrm{cl}\left(A\right)$ and its complement is denoted $\overline{A}$ . For $\varepsilon >0$ and $x\in X$ , the ball with center in $x$ and a radius $\varepsilon$ is ${\mathcal{R}}_{\varepsilon }\left(x\right)=\{y\in X\mid d(x,y)\le \varepsilon \}$ . A continuous function $\gamma :{\mathbb{R}}_0^{+}\to {\mathbb{R}}_0^{+}$ is said to belong to class $\mathcal{K}$ if it is strictly increasing and $\gamma \left(0\right)=0$ ; $\gamma$ is said to belong to class ${\mathcal{K}}_{\infty }$ if $\gamma$ is $\mathcal{K}$ and $\gamma \left(r\right)\to \infty$ as $r\to \infty$ . A continuous function $\beta :{\mathbb{R}}_0^{+}\times {\mathbb{R}}_0^{+}\to {\mathbb{R}}_0^{+}$ is said to belong to class $\mathcal{KL}$ if, for each fixed $s$ , the map $\beta (\cdot ,s)$ belongs to class $\mathcal{K}$ , and for each fixed nonzero $r$ , the map $\beta (r,\cdot )$ is strictly decreasing and $\beta (r,s)\to 0$ as $s\to \infty$ . Given a set $X$ , $2^X$ is used to denote its power set.

Section snippets

Preliminaries on prefix-closed sets

Given a set $Z\subseteq {\mathbb{R}}^n$ , prefix closed sets are subsets $P\subseteq M\left(Z\right)$ that can be defined as follows: if a trajectory $z:E\to Z$ belongs to the prefix-closed set $P$ , then any prefix of $z$ belongs to $P$ . In this part, we first give a formal definition of a prefix-closed set, we then give a necessary and sufficient condition for a set to be prefix-closed, finally we give some examples of such sets.

Definition 1

Let $Z\subseteq {\mathbb{R}}^n$ . Let $z:E\to Z$ and $z^{\prime }:E^{\prime }\to Z$ in $M\left(Z\right)$ . $z$ is said to be a prefix of $z^{\prime }$ and denoted $z\in \text{pref}\left(z^{\prime }\right)$ if $E\subseteq E^{\prime }$ and for all $t\in E$ , $z(t$

Systems

In this section, we introduce the classes of systems and interconnections considered throughout this paper, it is important to note that the classes of systems used in the paper are quite general, and includes deterministic and nondeterministic systems, described by difference or differential equations and inclusions and allows us to deal with phenomena such as sampling, time delays.

Definition 3

A continuous-time system is a tuple $\Sigma =(W_1,W_2,X,Y,\mathcal{T})$ where

•

$W_1\subseteq {\mathbb{R}}^{m_1}$ , $W_2\subseteq {\mathbb{R}}^{m_2}$ , $X\subseteq {\mathbb{R}}^n$ and $Y\subseteq {\mathbb{R}}^p$ , are the sets in which

Assume-guarantee contracts

An assume-guarantee contract is a compositional tool that specifies how a system behaves under assumptions about its inputs (Benveniste et al., 2018). The use of assume-guarantee contracts makes it possible to reason on a global system based on properties of its components. In this section, we introduce assume-guarantee contracts to reason on properties for continuous-time systems. These contracts are equipped with a weak and a strong semantic, which will allow us to establish compositionality

Compositional reasoning

In this section we provide results allowing us to reason about interconnected systems based on contracts satisfied by the components.

Compositional invariants for differential inclusions

In this section, we focus on continuous-time systems $\Sigma =(W_1,W_2,X,Y,\mathcal{T})$ defined by differential inclusions, and invariance assume-guarantee contracts, where assumptions and guarantees are defined as in Example 1. We use the classical characterization of invariant sets for differential inclusions developed using the concept of contingent cone (see Aubin, 2009 and the references therein) to derive necessary and sufficient conditions for weak satisfaction of assume-guarantee contracts. We also show

Small gain results

In this part, we show how the proposed framework can recover different versions of the classical small gain theorem as a particular case. Indeed, we show how the framework allows to recover the classical BIBO stability result (Desoer & Vidyasagar, 1975). Moreover, we construct a new small-gain result for the concept of growth bound (Angeli & Sontag, 1999). To the best of our knowledge, this result is new and have not been investigated before in the literature. We suppose for the sake of

Conclusion

In this paper, we proposed a contract based approach for verifying compositionally properties of continuous-time interconnected systems. The main notions considered in the paper and their relationships are sketched in Fig. 5. The main contributions are summarized below. We introduced a notion of assume-guarantee contracts equipped with a weak and strong semantics. We showed that weak semantics are sufficient to deal with acyclic interconnections (Theorem 1), strong semantics are required to

Acknowledgments

This research was supported by Labex DigiCosme (project ANR-11-LABEX-0045-DIGICOSME) operated by ANR, France as part of the program "Investissement d'Avenir" Idex Paris Saclay (ANR-11-IDEX-0003-02). This project was partially supported by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 725144).

Adnane Saoud is a Postdoctoral Research Fellow in the Electrical and Computer Engineering Department at the University of California, Berkeley, since February 2021. In 2020, he was a Postdoctoral Research Fellow in the Electrical and Computer Engineering Department at the University of California, Santa-Cruz. He received the Ph.D. degree in Control from CentraleSupelec, France, in 2019. During his Ph.D. studies, he was selected as one of the top three finalists for the Best student paper award

References (42)

• et al.

  Compositional abstraction-based synthesis for cascade discrete-time control systems

  IFAC-PapersOnLine

  (2018)

• MeyerP.-J. et al.

  Compositional abstraction refinement for control synthesis

  Nonlinear Analysis. Hybrid Systems

  (2018)

• AngeliDavid et al.

  Forward completeness, unboundedness observability, and their Lyapunov characterizations

  Systems & Control Letters

  (1999)

• AlurR. et al.

  Compositional refinement for hierarchical hybrid systems

• ArcakM. et al.

  Networks of dissipative systems: compositional certification of stability, performance, and safety

  (2016)

• AubinJ.-P.

  Viability theory

  (2009)

• BaierChristel et al.

  Principles of model checking

  (2008)

• BenvenisteAlbert et al.

  Contracts for system design

  Foundations and Trends in Electronic Design Automation

  (2018)

• ChenYuxiao et al.

  Compositional set invariance in network systems with assume-guarantee contracts

• Conte, C., Voellmy, N. R., Zeilinger, M. N., Morari, M., & Jones, C. N. (2012). Distributed synthesis and control of...

CooganS. et al.

A dissipativity approach to safety verification for interconnected systems

IEEE Transactions on Automatic Control

(2015)

Dallal, E., & Tabuada, P. (2015). On compositional symbolic controller synthesis inspired by small-gain theorems. In...

DashkovskiyS. et al.

An ISS small gain theorem for general networks

Mathematics of Control, Signals, and Systems

(2007)

DesoerC.A. et al.

Feedback systems: Input-output properties, volume 55

(1975)

El-GuindyA. et al.

Compositional transient stability analysis of power systems via the computation of reachable sets

EqtamiAlina et al.

A quantitative approach on assume-guarantee contracts for safety of interconnected systems

FrehseGoran Fedja

Compositional verification of hybrid systems using simulation relations

(2005)

Ghasemi, Kasra, Sadraddini, Sadra, & Belta, Calin (2020). Compositional synthesis via a convex parameterization of...

GoebelR. et al.

Hybrid dynamical systems: Modeling, stability, and robustness

(2012)

HenzingerT.A. et al.

Assume-guarantee reasoning for hierarchical hybrid systems

JiangZ.-P. et al.

Small-gain theorem for ISS systems and applications

Mathematics of Control, Signals, and Systems

(1994)

Cited by (7)

Recommended articles (6)

Adnane Saoud is a Postdoctoral Research Fellow in the Electrical and Computer Engineering Department at the University of California, Berkeley, since February 2021. In 2020, he was a Postdoctoral Research Fellow in the Electrical and Computer Engineering Department at the University of California, Santa-Cruz. He received the Ph.D. degree in Control from CentraleSupelec, France, in 2019. During his Ph.D. studies, he was selected as one of the top three finalists for the Best student paper award at the European Control Conference, ECC, 2018. He obtained the M.Sc. degree in control from University Paris-Saclay, France, in 2016, and Electrical Engineering degree from Ecole Mohammadia d'ingénieurs, (EMI), Morocco, in 2014. His current research interests include formal methods for cyber–physical systems, compositional analysis and synthesis of interconnected system and learning-based control of dynamical systems.

Antoine Girard is a Senior Researcher at CNRS and a member of the Laboratory of Signals and Systems. He received the Ph.D. degree in applied mathematics from Grenoble Institute of Technology, in 2004. From 2004 to 2006, he held postdoctoral positions at University of Pennsylvania and Université Grenoble-Alpes. From 2006 to 2015, he was an Assistant/Associate Professor at the Université Grenoble-Alpes.

His main research interests deal with analysis and control of hybrid systems with an emphasis on computational approaches, formal methods and applications to cyber–physical systems. He received the George S. Axelby Outstanding Paper Award from the IEEE Control Systems Society in 2009. In 2014, he was awarded the CNRS Bronze Medal. In 2015, he was appointed as a junior member of the Institut Universitaire de France (IUF). In 2016, he was awarded an ERC Consolidator Grant. In 2018, he received the first HSCC Test of Time Award and the European Control Award.

Laurent Fribourg received a civil engineering degree in 1980 from Aeronautics School Sup'Aero/Toulouse, and a Ph.D. in computer science in 1982 from University Paris 7. He was appointed by CNRS  in 1984 as a  full-time researcher. He co-founded the CNRS laboratory of computer science LSV at ENS Cachan (now ENS Paris-Saclay) in 1997, and became head of the CNRS interdisciplinary "Institut Farman" at ENS Paris-Saclay  in 2018. He has written more than 100 papers in the area of formal methods, several of them in collaboration with industrial partners.

View full text

© 2021 Published by Elsevier Ltd.

knottnevency1974.blogspot.com

Source: https://www.sciencedirect.com/science/article/abs/pii/S0005109821004337