Compositional Set Invariance in Network Systems with Assume-Guarantee Contracts

This paper presents an assume-guarantee reasoning approach to the computation of robust invariant sets for network systems. Parameterized signal temporal logic (pSTL) is used to formally describe the behaviors of the subsystems, which we use as the template for the contract. We show that set invariance can be proved with a valid assume-guarantee contract by reasoning about individual subsystems. If a valid assume-guarantee contract with monotonic pSTL template is known, it can be further refined by value iteration. When such a contract is not known, an epigraph method is proposed to solve for a contract that is valid, -an approach that has linear complexity for a sparse network. A microgrid example is used to demonstrate the proposed method. The simulation result shows that together with control barrier functions, the states of all the subsystems can be bounded inside the individual robust invariant sets.

I. Introduction

Correct-by-construction control synthesis has seen recent success in safety-critical applications such as vehicle control [1], [2] and robot navigation [3]. This approach bases the controller on concepts such as reachable set and control invariant sets to synthesize a controller that is capable of enforcing safety. However, reachability analysis and invariant set computation rely on computational tools such as Hamilton Jacobi [4], Linear Matrix Inequality (LMI) [5] and sum of squares (SOS) programming [6], [7] –these methods scale poorly with the dimension of the system. Because of this limitation, sometimes referred to as “the curse of dimensionality,” the applications of the correct-by-construction control synthesis have been limited to systems with low state dimension. There has been effort to break “the curse of dimensionality,” which typically utilizes either the compositional analysis or system symmetry [8]–[11]. For example, in [9], the weakly coupled longitudinal and lateral dynamics of the vehicle are treated independently by finding a bound on the coupling effect. In [10], when a large network system consists of small subsystems that are identical, the symmetry is utilized to compute invariant sets for a large number of subsystems. However, correct-by-construction synthesis for network systems with heterogeneous subsystems and strong coupling between them remains an open problem. One example is the power grid, which consists of various types of generation buses and load buses, as shown in Fig. 1. Fig. 1:

Power grid with generator buses and load buses