website/content/project/agmilp/index.md

title, summary, tags, date, external_link, image, links, url_code, url_pdf, url_slides, url_video, slides

title	summary	tags	date	external_link	image	links	url_code	url_pdf	url_slides	url_video	slides
Assume-Guarantee Contracts Mining	A tool for Signal Temporal Logic A-G contract mining using Mixed-Integer Linear Programming and STL inference		2021-02-15		caption focal_point Smart		https://github.com/fran-penedo/agmilp

In our work on formal methods for Partial Differential Equations, we developed a solution for a boundary control synthesis problem which suffers from scalability issues due to the encoding of a big system of Ordinary Differential Equations (ODEs) into a mixed-integer linear program. In order to address this issue, we've proposed an Assume-Guarante Contract approach, which represents a "divide-and-conquer" strategy. The full approach is a work in progress, but we have been able to design and implement a first step: a novel sampling based assumption mining algorithm which does not require the monotonicity of the system. The Python implementation can be found in AGMilp.

Distributed Control Synthesis and Assume-Guarantee Contracts

Let us formalize the distributed control synthesis problem and how it can be solved through the use of assume-guarantee contracts. Assumption mining is the first step towards the synthesis of assume-guarantee contracts for a distributed system. Let \Sigma(u) be the discrete-time system described by the following relation:

\begin{equation} \label{eq:agc-system} \Sigma(x_0, u) : x_{k+1} = Ax_k + Bu_k + F , \end{equation}

where $x_i \in \Omega \subset \mathbb{R}^n, u_i \in U \subset \mathbb{R}^m, u = u_0 u_1...$ and x_0 is given. Let the system be partitioned in l subsystems, \{\Sigma^i\}_{i=1}^{l}, where each subsystem has the following form:

\begin{equation} \label{eq:agc-subsystem} \Sigma^i(u) : x_{k+1}^i = A^i x_k^i + B^i u_k^i + \sum_{j \neq i} A^{j \to i} x_k^{j \to i} + F^i , \end{equation}

where the state vector x and control vector u have been partitioned (i.e., there are no shared states or controls), and the system matrices have been rewritten accordingly. Note that x^{j \to i} refers to the set of state variables corresponding to subsystem j that have direct influence in subsystem i.

Consider an STL formula \phi = \bigwedge_{i=1}^l \phi^i, where \phi^i is an STL formula over x^i. We define the distributed control synthesis problem as finding a control policy u = u_0 u_1 ..., with u_t^i dependent on the state and control history of subsystem i, such that \Sigma(u) \models \phi.

An Assume-Guarantee Contract (AGC) is an STL formula \psi^{i \to j} over x^{i \to j}. Our objective is to find a set of AGCs such that there exists local control policies u^i satisfying the following property:

\begin{equation} \forall i=1,...,l : (\forall j \neq i : \Sigma^j(u) \models \psi^{j \to i}) \implies \Sigma^i(u) \models \phi^i \land (\bigwedge_{j \neq i} \psi^{i \to j}) \end{equation}

In other words, if a subsystem has all its assumptions guaranteed, then it can satisfy the local specification and its guarantees. We call a set of contracts satisfying this property well posed.

Assumption Mining

We move now to assumption mining, a first step in the synthesis of well posed AGCs. Let \Sigma(x_0, z) be the discrete-time system described by the following relation:

\begin{equation} \label{eq:as-mine-system} \Sigma(x_0, z) : x_{k+1} = A x_k + D z_k + F , \end{equation}

where $x_i \in \Omega \subset \mathbb{R}^n, z_i \in Z \subset \mathbb{R}^m, z = z_0 z_1 ...$. Let \phi be an STL formula over x. We define the assumption mining problem as the following: find an STL formula \phi_a over x_0 and z such that if $(x_0, z) \models \phi_a$ then \Sigma(x_0, z) \models \phi. In addition, for any other STL formula \phi_a' such that \phi_a' \implies \phi_a and they are not logically equivalent, if (x_0, z) \models \phi_a' and (x_0, z) \not\models \phi_a then \Sigma(x_0, z) \not\models \phi.

Our solution to the assumption mining problem is an adaptation of the sampled based algorithm found in [1] such that it does not assume any kind of monotonicity of the system. This assumption does not generally hold in discretized PDE systems, which prevents us from using the cited algorithm as a basis for solving the distributed control synthesis problem for PDEs. When the monotonicity assumption is not met, the set of assumptions is no longer possible to describe as an STL formula of special form (so called directed specifications), which can be easily constructed from a set of valid and invalid assumptions. Instead, we must use a general inference algorithm that can provide us with an STL formula that describes the sets of assumption samples.

Informally, our algorithm can be described as the following:

1. Sample the space of x_0 and z(t).
2. Classify each sample as producing a satisfying system trajectory or not.
3. Use STL inference (implemented in templogic) to obtain an approximation to \phi_a from the satisfying samples.
4. Find a sample (x_0, z(t)) that satisfies \phi_a but produces a not satisfying trajectory using an MILP encoding of the system, \phi and \phi_a . If there is one, go to 3.
5. Find a sample (x_0, z(t)) that does not satisfy \phi_a but produces a satisfying trajectory. If there is one, go to 3.
6. Decrease tolerance and go to 4.

Note that our sampling based algorithm stops at a given tolerance tol_min after progressively reducing it from the initial value tol_init by factors of alpha. This tolerance must be understood as the following: our algorithm guarantees that the produced \phi_a is such that every initial state x_0 with STL robustness degree greater than tol_min produces a system trajectory that satisfies \phi.

[1] Kim, Eric S., Murat Arcak, and Sanjit A. Seshia. “Directed Specifications and Assumption Mining for Monotone Dynamical Systems.” In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 21–30. HSCC ’16. New York, NY, USA: ACM, 2016. https://doi.org/10.1145/2883817.2883833.