diff --git a/content/project/agmilp/featured.png b/content/project/agmilp/featured.png
new file mode 100644
index 0000000..cd6bee3
Binary files /dev/null and b/content/project/agmilp/featured.png differ
diff --git a/content/project/agmilp/index.md b/content/project/agmilp/index.md
new file mode 100644
index 0000000..e771809
--- /dev/null
+++ b/content/project/agmilp/index.md
@@ -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.
diff --git a/static/media/agmilp.png b/static/media/agmilp.png
new file mode 100644
index 0000000..cd6bee3
Binary files /dev/null and b/static/media/agmilp.png differ