Added agmilp project
This commit is contained in:
BIN
content/project/agmilp/featured.png
Normal file
BIN
content/project/agmilp/featured.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 32 KiB |
138
content/project/agmilp/index.md
Normal file
138
content/project/agmilp/index.md
Normal file
@@ -0,0 +1,138 @@
|
||||
---
|
||||
title: Assume-Guarantee Contracts Mining
|
||||
summary: A tool for Signal Temporal Logic A-G contract mining using Mixed-Integer Linear Programming and STL inference
|
||||
tags: []
|
||||
date: "2021-02-15"
|
||||
|
||||
# Optional external URL for project (replaces project detail page).
|
||||
external_link: ""
|
||||
|
||||
image:
|
||||
caption: ""
|
||||
focal_point: Smart
|
||||
|
||||
links:
|
||||
# - icon: twitter
|
||||
# icon_pack: fab
|
||||
# name: Follow
|
||||
# url: https://twitter.com/georgecushen
|
||||
url_code: "https://github.com/fran-penedo/agmilp"
|
||||
url_pdf: ""
|
||||
url_slides: ""
|
||||
url_video: ""
|
||||
|
||||
# Slides (optional).
|
||||
# Associate this project with Markdown slides.
|
||||
# Simply enter your slide deck's filename without extension.
|
||||
# E.g. `slides = "example-slides"` references `content/slides/example-slides.md`.
|
||||
# Otherwise, set `slides = ""`.
|
||||
slides: ""
|
||||
---
|
||||
|
||||
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](https://github.com/fran-penedo/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](https://github.com/fran-penedo/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.
|
||||
Reference in New Issue
Block a user