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.