Updated cv and deploy script

config/_default/params.toml

@@ -57,7 +57,7 @@ description = ""
 # Enable source code highlighting? true/false
 # Documentation: https://wowchemy.com/docs/writing-markdown-latex/#highlighting-options
 highlight = true
-highlight_languages = ["r"]  # Add support for highlighting additional languages
+highlight_languages = ["r", "python"]  # Add support for highlighting additional languages
 # highlight_style = "github"  # For supported styles, see https://cdnjs.com/libraries/highlight.js/
 
 # Enable LaTeX math rendering? true/false
@@ -158,7 +158,7 @@ section_pager = false
 docs_section_pager = true  # Display pager in Docs layout (e.g. tutorials)?
 
 # Enable in-built social sharing buttons? (true/false)
-sharing = true
+sharing = false
 
 # Show a copyright license from creativecommons.org in the site footer?
 # Page specific copyright licenses are also possible by adding this option to a page's front matter.

content/authors/admin/_index.md

@@ -76,8 +76,8 @@ email: ""
 highlight_name: false
 ---
 
-I am a recent graduate from [Boston University](http://www.bu.edu), where I obtained my PhD in Systems Engineering in 2020 from the [Division of Systems Engineering](http://www.bu.edu/eng/departments/se/), where I worked in the [BU Robotics Laboratory](http://sites.bu.edu/robotics/). In 2014, I obtained a BS degree in Computer Science from the [Polytechnic School](http://www.uam.es/ss/Satellite/EscuelaPolitecnica/es/home.htm), as well as a BS degree in Mathematics from the [College of Science](https://www.uam.es/Ciencias/Home.htm), both part of the [Autonomous University of Madrid](http://uam.es/UAM/Home.htm).
+I am a recent PhD graduate from [Boston University](http://www.bu.edu), where I obtained my PhD in Systems Engineering in 2020 from the [Division of Systems Engineering](http://www.bu.edu/eng/departments/se/). There, I worked in the [BU Robotics Laboratory](http://sites.bu.edu/robotics/). In 2014, I obtained a BS degree in Computer Science from the [Polytechnic School](http://www.uam.es/ss/Satellite/EscuelaPolitecnica/es/home.htm), as well as a BS degree in Mathematics from the [College of Science](https://www.uam.es/Ciencias/Home.htm), both part of the [Autonomous University of Madrid](http://uam.es/UAM/Home.htm).
 
-My research centers around the development of a framework to automatically synthesize and verify physical systems, specifically those modeled by partial differential equations, with constraints expressed in a user-friendly language. To this end, I employ tools and techniques from formal methods, temporal logics, optimization, machine learning and control theory.
+My research centers around the development of a framework to automatically synthesize and verify physical systems, specifically those modeled by partial differential equations, with constraints expressed in a formal, but user-friendly, language. To this end, I employ tools and techniques from formal methods, temporal logics, optimization, machine learning and control theory.
 
 {{< icon name="download" pack="fas" >}} You can find my full resumé here: {{< staticref "media/cv.pdf" >}}PDF{{< /staticref >}}/{{< staticref "media/cv.html" >}}HTML{{< /staticref >}}.

content/home/projects.md

@@ -24,13 +24,13 @@ content:
   # To show all items, set `tag` to "*".
   # To filter by a specific tag, set `tag` to an existing tag name.
   # To remove the toolbar, delete the entire `filter_button` block.
-  filter_button:
-  - name: All
-    tag: '*'
-  - name: Deep Learning
-    tag: Deep Learning
-  - name: Other
-    tag: Demo
+#  filter_button:
+#  - name: All
+#    tag: '*'
+#  - name: Deep Learning
+#    tag: Deep Learning
+#  - name: Other
+#    tag: Demo
 
 design:
   # Choose how many columns the section has. Valid values: '1' or '2'.

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.

content/project/femformal/index.md

@@ -0,0 +1,206 @@
+---
+title: Formal Methods for PDEs
+summary: A Formal Methods Approach to Synthesis and Verification of Systems Governed by Partial Differential Equations
+tags: []
+date: "2021-02-18"
+
+# 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/femformal"
+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: ""
+---
+Partial differential equations (PDEs) model nearly all of the physical systems
+and processes of interest to scientists and engineers. Some well-known examples
+include the Navier-Stokes equation for fluid mechanics, the Maxwell equations
+for electromagnetics, the Schrödinger equation for quantum mechanics, the heat
+equation and the wave equation. The analysis of these and other PDEs has had a
+tremendous impact on society by enabling our understanding of thermal,
+electrical, fluidic and mechanical processes.
+
+While a mature field, the study of PDEs is often approached through simulations
+in which approximate models obtained through spatio-temporal
+discretization techniques, such as the Finite Element Method (FEM),
+are solved numerically. These methods, however,
+do not allow for rigorous guarantees that a system satisfies a complex
+specification. Other approaches generalizing classic Ordinary Differential
+Equations (ODEs) tools such as Lyapunov
+analysis and backstepping do provide some guarantees
+and can be used to obtain boundary control strategies for a wide variety of
+PDEs. However, they are restricted to classical control objectives such as
+stabilization and cost optimization.
+
+The formal statement of specifications and the development of
+analysis techniques that can guarantee their satisfaction by design has been the main
+focus of the formal methods field. During the past decades, many specification
+languages have been defined, such as Linear Temporal
+Logic (LTL) and Signal Temporal Logic (STL).
+Originally, these logics have been applied to the
+study of finite systems, although more recently
+abstraction procedures have been developed to reduce problems with ODEs
+to finite models (for example through state space
+discretization or mixed-integer linear program (MILP) encodings).
+However, these techniques cannot be immediately applied to the analysis of PDEs
+due to the lack of spatial information in the formal language. This issue was
+first addressed in in the context of spatially
+distributed systems, which can be viewed as PDEs in a discretized spatial domain.
+In their work, the authors view the system state as an image and define a formal
+language with explicit spatial information called Linear Superposition Logic (LSSL)
+based on quadtrees, a tree-based
+abstraction of the system. A variant of LSSL with quantitative semantics, 
+Tree Spatial Superposition Logic (TSSL), was used 
+for (steady-state) pattern synthesis in reaction
+diffusion systems, and a formal
+language combining TSSL and STL, Spatial Temporal Logic (SpaTeL), allows the
+synthesis of dynamical patterns. The specification of patterns in these logics
+is difficult, however, and machine learning techniques are needed in order to
+obtain logic formulas corresponding to a set of examples of the desired pattern,
+which is not always available or desirable for some applications where
+the system behavior must be specified a priori. More recently, a new
+spatio-temporal logic called STREL was introduced in
+to specify the behavior of mobile and
+spatially distributed Cyber-Physical Systems.
+
+One of the major drawbacks of these methods is the issue of scalability. Both of the
+main approaches, automata and optimization, quickly become unfeasible when the system dimension
+increases, which poses a problem when dealing with infinite-dimensional systems such as
+PDEs. In the case of optimization based techniques, a recent trend has focused on
+decentralized synthesis and verification where the coupling between subsystems is
+formally captured in Assume-Guarantee Contracts (AGCs). However, the key
+assumption of monotonicity is not present in PDE systems.
+
+Besides classical problems that focus on the
+temporal evolution of the state of the system, PDEs allow for a different kind of
+problems where the aim is to specify the intrinsic behavior of the system through its so
+called constitutive response. In this case, instead of designing boundary control
+inputs, the engineer is tasked with the design of the geometry of a structure that
+exhibits the desired mechanical or thermal properties. The traditional
+approach to this problem, topology optimization is not enough to tackle
+both geometric and material nonlinearity.
+
+## Boundary Control
+
+In order to solve the classical boundary control problems through the use of formal
+methods, we've developed a formal language called Spatial-STL (S-STL) and a framework
+that reformulates a verification or control synthesis problem for a PDE system into an
+optimization problem for a system of difference equations that can be encoded and solved
+as a Mixed-Integer Linear Program (MILP). As an example of the kind of properties we
+can describe with S-STL, consider the following: 
+
+Consider a metallic rod of 100mm. The
+temperature at one end of the rod is fixed at 300 kelvin, while a
+heat source is applied to the other end. The temperature of the rod follows
+a linear 1D heat equation. We want the temperature distribution of the
+rod to be within 3 kelvin of the linear profile $\mu(x) = \frac{x}{4} + 300$ 
+at all times between 4 and 5 seconds in the section between 30 and 60
+mm. Furthermore, the temperature should never exceed 345 kelvin
+at the point where the heat source is applied ($x=100$).
+We can formulate such a specification using the following S-STL formula:
+
+\begin{equation}\label{eq:phi_ex}
+    \begin{aligned}
+    \phi_{ex} = &\mathbf{G}_{[4,5]} 
+    \big((\forall x \in [30,60] : u(x) - (\frac{x}{4} + 303) < 0 )  \land \\\\
+          &\quad (\forall x \in [30, 60] : u(x) - (\frac{x}{4} + 297) >
+        0)\big) \land \\\\
+      &\mathbf{G}_{[0, 5]} (\forall x \in [100, 100] : u(x) -
+    345 < 0)
+    \end{aligned}
+\end{equation}
+
+Note that S-STL admits quantitative semantics similar to STL (see the [templogic project
+page](/project/templogic) for a quick introduction.)
+
+We implemented this framework in a Python tool
+called [FEMFormal](https://github.com/fran-penedo/femformal). In FEMFormal, you can
+define boundary control problems in 1D and 2D linear heat and wave equations, as well as
+some non-linear 1D wave equations. Then, you can solve verification and synthesis
+problems with S-STL specifications such as the one above. For example, for a mixed steel
+and brass rod, our tool obtains the following solution:
+
+![Heat equation synthesis trajectory](/media/femformal_heat.gif)
+![Heat equation synthesis inputs](/media/femformal_heat_inputs.png)
+
+You can see more solved examples as well as how to use FEMFormal
+[here](https://github.com/fran-penedo/femformal).
+
+## Constitutive Response Design
+
+Suppose we now want to produce a wide variety of mechanical behaviors out of a
+single material. For example, can we give an elastic material a tunable,
+effective yield point, or make it strain harden or soften at a specified amount
+of displacement? This response to loading can be determined from the
+stress-strain curve, which serves as a fundamental piece of information that
+describes the global mechanical properties of structures and materials. Recent
+advances in mechanical metamaterials have shown that it is possible to tailor
+the relationship between stress and strain of a particular material through
+structural patterning.
+
+{{< figure src="/media/femformal_bertoldi.png" title="Metamaterial design (from Shim et al., 2013)" >}}
+
+In order to formally specify the desired response
+of the structure, we developed a formal language over stress-strain curves and
+adapted S-STL for this purpose. Then, we proposed an optimization
+procedure based on gradient-free optimization algorithms and simulation.
+
+Consider the following example of this process: a square sheet of rubber
+of side $L = 8cm$ and thickness $h = 1cm$ is drilled with
+circular holes of radius $r$ constrained to be within the interval
+$[0.3cm, 0.4cm]$ and distributed in a lattice given by the
+vectors $v_1, v_2 \in \mathbb{R}^2$ such that they do not intersect. 
+The constitutive response was obtained as a
+positive force-displacement curve by loading the material with a force $F(t)$ applied
+uniformly across the top surface such that the discplacement at the top surface
+increases linearly from 0 to 1.05cm in 3.5 seconds. 
+The specification in this case is to have the
+force-displacement curve of the material to be within $\epsilon$ tolerance of a
+target curve $p$, which can be expressed in S-STL as the following formula:
+
+\begin{equation}
+\begin{aligned}
+    \phi = \forall x \in \{(0, L)\} : \mathbf{G}_{[0, T]} 
+        (F < p(d_2(x)) + \epsilon \land F > p(d_2(x)) - \epsilon) \\\\
+        p(d) = \begin{cases}
+            \frac{40}{7.5 \cdot 10^{-3}} d & d < 7.5 \cdot 10^{-3} \\\\
+            40 & d > 7.5 \cdot 10^{-3} 
+         \end{cases}
+\end{aligned}
+\end{equation}
+
+where $d_2(x)$ represents the displacement of the top boundary at $x$, $F$ is
+the applied force, the temporal operator $\mathbf{G}_{[0, T]} \psi$ means that
+$\psi$ must be satisfied at all times in the interval and the spatial 
+operator $\forall x \in \{(0, L)\} : \psi$ means that $\psi$ must be satisfied at all points in the
+interval.
+
+We solved this problem using differential evolution to find the best pattern
+with respect to the S-STL score of the specification
+$\phi$. We generate simulations of the system using the Finite Element Method simulator 
+[ANSYS](https://www.ansys.com/).
+After 280 evaluations performed in about 38 hours, we obtained the following pattern:
+
+![Constitutive Response Results](/media/const_design1.png)
+![Constitutive Response Results](/media/const_design2.png)
+
+This pattern results in a S-STL score of 0.641, with the following force-displacement
+curve (compared to the target curve and its tolerance):
+
+![Constitutive Response F-D Curve](/media/const_design_response.png)

content/project/templogic/index.md

@@ -0,0 +1,236 @@
+---
+title: Temporal Logics Library
+summary: A collection of utilities for temporal logics with quantitative semantics, including inference and MILP encoding
+tags: []
+date: "2021-02-08"
+
+# Optional external URL for project (replaces project detail page).
+external_link: ""
+
+image:
+  caption: "Taken from Alexandre Donzé's lecture at UC Berkeley, 2014"
+  focal_point: Smart
+
+links:
+# - icon: twitter
+#   icon_pack: fab
+#   name: Follow
+#   url: https://twitter.com/georgecushen
+url_code: "https://github.com/fran-penedo/templogic"
+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: ""
+---
+
+Temporal logics are formal languages capable of expressing properties of system
+(time-varying) trajectories. Besides the usual boolean operators, temporal logics
+introduce temporal operators that capture notions of safety ("the system should *always*
+operate outside the danger zone"), reachability ("the system is *eventually* able to enter a desired
+state"), liveness ("the system *always eventually* reaches desired states"), and others.
+Once a property is expressed, automatic tools based on automata theory, optimization or
+probability theory are able to check wether a system satisfies the property, or
+synthesize a controller such that the system is guaranteed to satisfy the specification.
+
+I have organized most of the Python code implementing a few of the temporal logics used
+in my thesis in the library [Templogic](https://github.com/fran-penedo/templogic). In particular, 
+I have included several logics that admit quantitative semantics (see below), along with
+functionality that pertains to the logic itself, such as parsing, inference and
+mixed-integer encodings.
+
+## Quantitative Semantics
+
+For some scenarios, a binary measure of satisfaction is not enough. For
+example, one might want to operate a system such that safety is not only guaranteed but
+*robustly* guaranteed. In other applications, a not satisfying best effort might provide
+an engineer with clues about mistakes in the specification or guide more expensive
+algorithms towards satisfaction. For these situations, some temporal logics can be
+equiped with *quantitative semantics*, i.e., a real score $r$ such that a trajectory
+satisfies a specification if and only if $r > 0$. If one considers a temporal logic
+formula as the subset of trajectories that satisfy it, the score $r$ can be interpreted
+as the distance of a trajectory to the boundary of this set.
+
+Consider for example Signal Temporal Logic (STL), a temporal logic based on Lineal
+Temporal Logic (LTL) that defines temporal bounds for its temporal operators and uses
+inequalities over functions of the system state as predicates. For example in STL one
+can express the property "*always* between 0 and 100 seconds the $x$ component of the
+system state cannot exceed the value 50, and *eventually* between 0 and 50 seconds the
+$x$ component of the system must reach a value between 5 and 10 and stay within those
+bounds *at all times* for 10 seconds", which would be written as the formula:
+
+$$
+  \phi = G_{[0, 100]} x < 50 \wedge F_{[0, 50]} (G_{[0, 10]} (\lnot (x < 5) \wedge x < 10))
+$$
+
+You can define $\phi$ using Templogic as follows:
+
+```python
+from templogic.stlmilp import stl 
+
+# `labels` tells the model how each state component at time `t` is represented
+# It can also be a function of t that returns the list of variables at time `t`
+labels = [lambda t: t]
+
+# Predicates are defined as signal > 0
+signal1 = stl.Signal(labels, lambda x: 50 - x[0])
+signal2 = stl.Signal(labels, lambda x: 5 - x[0])
+signal3 = stl.Signal(labels, lambda x: 10 - x[0])
+
+f = stl.STLAnd(
+      stl.STLAlways(bounds=(0, 100), arg=stl.STLPred(signal1))
+      stl.STLEventually(
+        bounds=(0, 50),
+        arg=stl.STLAlways(
+          bounds=(0, 10),
+          arg=stl.STLAnd(
+            args=[
+              stl.STLNot(stl.STLPred(signal2)),
+              stl.STLPred(signal3)
+            ]))))
+```
+
+The score or robustness of a trajectory $x(t)$ with respect to the specification $\phi$
+can be defined as follows:
+
+$$
+\begin{multline}
+  r(x(t), \phi) = \min \\{\min_{t \in [0, 100]} 50 - x(t), \\\\
+      \max_{t \in [0, 50]} (\min_{t \in [0, 10]} (\min \\{-(5 - x(t)), 10 - x(t)\\}))
+    \\}
+\end{multline}
+$$
+
+In Templogic, you must define a model that understands how to translate state variables
+at time `t` used in signals:
+
+```python
+class Model(stl.STLModel):
+  def __init__(self, s) -> None:
+    self.s = s
+    # Time interval for the time discretization of the model
+    self.tinter = 1
+
+  def getVarByName(self, j):
+    # Here `j` is an object that identifies a state variable at time `t` 
+    # in the model, generated by the functions in `labels` above. 
+    # In our case it is simply the index in the array that contains the 
+    # trajectory
+    return self.s[j]
+```
+
+You can then compute the score for a particular model:
+
+```python
+s = [0, 1, 2, 4, 8, 4, 2, 1, 0, 1, 2, 6, 2, 1, 5, 7, 8, 1]
+model = Model(s)
+score = stl.robustness(f, model)
+```
+
+## Mixed-Integer Linear Programming
+
+An obvious framework to work with temporal logics with quantitative semantics would be
+to reformulate verification and synthesis problems as optimization problems, where the
+objective is to maximize the score $r$. However, as can be seen above, the definition of
+the score is non-convex and discontinuous, which makes it particularly difficult to
+include directly either as an objective function or as a constraint in efficient
+optimization algorithms, such as those used in Linear Programming. Instead, an
+equivalent reformulation can be used to transform the score definition into a series of
+mixed-integer linear constraints. The solution of Mixed-Integer Linear Programs (MILPs)
+is in general very expensive (double exponential), but very good heuristic techniques
+can be used to efficiently solve interesting problems in practice. As an example,
+consider the following MILP reformulation of the function $\min \\{x, y\\}$:
+
+$$
+\begin{aligned}
+  r \leq x \\\\
+  r \leq y \\\\
+  r > x - Md \\\\
+  r > y - Md \\\\
+  d \in \\{0, 1\\}
+\end{aligned}
+$$
+
+where $M$ is a sufficiently big number chosen a priori. The auxiliary variable $r$ can
+now be used as optimization objective or as a constraint (for example $r > 0$ for satisfaction).
+As seen above, robustness in STL are defined as nested $\max$ and $\min$ operations and
+can be fully encoded in this fashion. In Templogic, we define encodings for the popular
+MILP solver [Gurobi](https://www.gurobi.com/). You can create an MILP model and add
+the robustness of the STL formula `f` defined above as follows:
+
+```python
+from templogic.stlmilp import stl_milp_encode as milp
+
+m = milp.create_milp("test")
+
+# Define here your model. Make sure you label each variable representing
+# a system variable at time `t` consistently with the `labels` parameter
+# to the STL Signals. For example labels may be defined as:
+# labels = [lambda t: f"X_0_{t}"]
+# which would, for t=5, fetch the variable `X_0_5` from the Gurobi model
+m.addVar(...)
+m.addConstr(...)
+
+# `r` contains a Gurobi variable with the robustness of f.
+r, _ = milp.add_stl_constr(m, "robustness", f)
+
+# You can use this variable in constraints
+m.addConstr(r > 0)
+
+# or set a weight in the objective function for it
+r.setAttr("obj", weight)
+```
+
+You can find more helper functions in the `stl_milp_encode` module.
+
+## STL Inference
+
+![Naval Surveillance Scenario](/media/naval.png)
+
+STL inference is the problem of constructing an STL formula that represents "valid" or
+"interesting" behavior from samples of "valid" and "invalid" behavior. This is often
+called the two-class classification problem in machine learning.
+We developed a decision-tree based framework for solving the
+two-class classification problem involving signals using STL formulae as data
+classifiers. We refer to it as framework because we didn't just proposing a single
+algorithm but a class of algorithms. Every algorithm produces a binary decision tree
+which can be translated to an STL formula and used for classification purposes. Each
+node of a tree is associated with a simple formula, chosen from a finite set of
+primitives. Nodes are created by finding the best primitive, along with its optimal
+parameters, within a greedy growing procedure. The optimality at each step is assessed
+using impurity measures, which capture how well a primitive splits the signals in the
+training data. The impurity measures described in this paper are modified versions of
+the usual impurity measures to handle signals, and were obtained by exploiting the
+robustness score of STL formulas.
+
+Our STL inference framework is implemented in the `templogic.stlmilp.inference` package,
+and a command line interface is provided. As an example, consider the following naval
+surveillance scenario: assume you have a set of trajectories of boats approaching a harbor. A subset
+of trajectories corresponding with normal behavior are labeled as "valid", while the others,
+corresponding with behavior consistent with smuggling or terrorist activity, are labeled
+"invalid". 
+
+You can encode this data in a Matlab file with three matrices: 
+
+- A `data` matrix with the trajectories (with shape: number of trajectories x dimensions
+  x number of samples), 
+- a `t` column vector representing the sampling times, and 
+- a `labels` column vector with the labels (in minus-one-plus-one encoding).
+
+You can find the `.mat` file for this example in
+`templogic/stlmilp/inference/data/Naval/naval_preproc_data_online.mat`. In order to
+obtain an STL formula that represents "valid" behavior, you can run the command:
+
+```shell
+$ lltinf learn templogic/stlmilp/inference/data/Naval/naval_preproc_data_online.mat
+Classifier:
+(((F_[74.35, 200.76] G_[0.00, 19.84] (x_1 > 33.60)) & (((G_[237.43, 245.13] ...
+```
+
+
+![Naval Surveillance Scenario Result](/media/naval_res.png)

content/publication/cdc2018/index.md

@@ -67,7 +67,8 @@ image:
 #   E.g. `internal-project` references `content/project/internal-project/index.md`.
 #   Otherwise, set `projects: []`.
 projects:
-- formal-pde
+- femformal
+- templogic
 
 # Slides (optional).
 #   Associate this publication with Markdown slides.

content/publication/hscc16/index.md

@@ -69,7 +69,7 @@ image:
 #   E.g. `internal-project` references `content/project/internal-project/index.md`.
 #   Otherwise, set `projects: []`.
 projects:
-- stl-inference
+- templogic
 
 # Slides (optional).
 #   Associate this publication with Markdown slides.

content/publication/thesis/cite.bib

@@ -0,0 +1,12 @@
+
+@article{penedoalvarezFormalMethodsPartial2020,
+  title = {Formal Methods for Partial Differential Equations},
+  author = {Penedo Alvarez, Francisco},
+  year = {2020},
+  abstract = {Partial differential equations (PDEs) model nearly all of the physical systems and processes of interest to scientists and engineers. The  analysis of PDEs has had a tremendous impact on society by enabling our understanding of thermal, electrical, fluidic and mechanical processes. However, the study of PDEs is often approached with methods that do not allow for rigorous guarantees that a system satisfies complex design objectives. In contrast, formal methods have recently been developed to allow the formal statement of specifications, while also developing analysis techniques that can guarantee their satisfaction by design. In this dissertation new design methodologies are introduced that enable the systematic creation of structures whose mechanical properties, shape and functionality can be time-varying.    A formal methods formulation and solution to the tunable fields problem is first introduced, where a prescribed time evolution of the displacement field for different spatial regions of the structure is to be achieved using boundary control inputs. A spatial and temporal logic is defined that allows the specification of interesting properties in a user-friendly fashion and can provide a satisfaction score for the designed inputs. This score is used to formulate an optimization procedure based on Mixed Integer Programming (MIP) to find the best design.    In the second part, a sampling based assumption mining algorithm is introduced, which is the first step towards a divide and  conquer strategy to solve the tunable fields problem using assume-guarantee contracts. The algorithm produces a temporal logic formula that represents initial conditions and external inputs of a system that satisfy a goal given as a temporal logic formula over its state. An online supervised learning algorithm is presented, based on decision tree learning, that is used to produce a temporal logic  formula from assumption samples.    The third part focuses on the tunable constitutive properties problem, where the goal is to create structures satisfying a stress-strain response by designing their geometry. The goal is represented as a logic formula that captures the allowed deviation from a reference and provides a satisfaction score. An optimization procedure is used to obtain the best geometric design.},
+  annotation = {Accepted: 2020-05-20T12:56:32Z},
+  file = {/home/fran/.zotero/zotero/okavn86u.default/zotero/storage/C2PFVIGG/Penedo Alvarez - 2020 - Formal methods for partial differential equations.pdf},
+  language = {en\_US}
+}
+
+

content/publication/thesis/index.md

@@ -0,0 +1,87 @@
+---
+title: "Formal Methods for Partial Differential Equations"
+
+# Authors
+# If you created a profile for a user (e.g. the default `admin` user), write the username (folder name) here 
+# and it will be replaced with their full name and linked to their profile.
+authors:
+- admin
+
+# Author notes (optional)
+# author_notes:
+# - "Equal contribution"
+# - "Equal contribution"
+
+date: "2020-05-19"
+doi: ""
+
+# Schedule page publish date (NOT publication's date).
+# publishDate: "2017-01-01T00:00:00Z"
+
+# Publication type.
+# Legend: 0 = Uncategorized; 1 = Conference paper; 2 = Journal article;
+# 3 = Preprint / Working Paper; 4 = Report; 5 = Book; 6 = Book section;
+# 7 = Thesis; 8 = Patent
+publication_types: ["7"]
+
+# Publication name and optional abbreviated publication name.
+publication: ""
+publication_short: ""
+
+abstract: "Partial differential equations (PDEs) model nearly all of the physical systems and processes of interest to scientists and engineers. The 
+analysis of PDEs has had a tremendous impact on society by enabling our understanding of thermal, electrical, fluidic and mechanical processes. However, the study of PDEs is often approached with methods that do not allow for rigorous guarantees that a system satisfies complex design objectives. In contrast, formal methods have recently been developed to allow the formal statement of specifications, while also developing analysis techniques that can guarantee their satisfaction by design. In this dissertation new design methodologies are introduced that enable the systematic creation of structures whose mechanical properties, shape and functionality can be time-varying. <p>
+ 
+A formal methods formulation and solution to the tunable fields problem is first introduced, where a prescribed time evolution of the displacement field for different spatial regions of the structure is to be achieved using boundary control inputs. A spatial and temporal logic is defined that allows the specification of interesting properties in a user-friendly fashion and can provide a satisfaction score for the designed inputs. This score is used to formulate an optimization procedure based on Mixed Integer Programming (MIP) to find the best design. <p>
+ 
+In the second part, a sampling based assumption mining algorithm is introduced, which is the first step towards a divide and 
+conquer strategy to solve the tunable fields problem using assume-guarantee contracts. The algorithm produces a temporal logic formula that represents initial conditions and external inputs of a system that satisfy a goal given as a temporal logic formula over its state. An online supervised learning algorithm is presented, based on decision tree learning, that is used to produce a temporal logic 
+formula from assumption samples. <p>
+ 
+The third part focuses on the tunable constitutive properties problem, where the goal is to create structures satisfying a stress-strain response by designing their geometry. The goal is represented as a logic formula that captures the allowed deviation from a reference and provides a satisfaction score. An optimization procedure is used to obtain the best geometric design."
+
+# Summary. An optional shortened abstract.
+# summary: Lorem ipsum dolor sit amet, consectetur adipiscing elit. Duis posuere tellus ac convallis placerat. Proin tincidunt magna sed ex sollicitudin condimentum.
+
+tags: []
+
+# Display this page in the Featured widget?
+featured: true
+
+# Custom links (uncomment lines below)
+links:
+- name: BU Library Permanent Link
+  url: https://hdl.handle.net/2144/41039
+
+url_pdf: ''
+url_code: ''
+url_dataset: ''
+url_poster: ''
+url_project: ''
+url_slides: ''
+url_source: ''
+url_video: ''
+
+# Featured image
+# To use, add an image named `featured.jpg/png` to your page's folder. 
+image:
+  caption: ""
+  focal_point: ""
+  preview_only: false
+
+# Associated Projects (optional).
+#   Associate this publication with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `internal-project` references `content/project/internal-project/index.md`.
+#   Otherwise, set `projects: []`.
+projects:
+- femformal
+- templogic
+- agmilp
+
+# Slides (optional).
+#   Associate this publication with Markdown slides.
+#   Simply enter your slide deck's filename without extension.
+#   E.g. `slides: "example"` references `content/slides/example/index.md`.
+#   Otherwise, set `slides: ""`.
+slides: ""
+---

deploy.sh

@@ -0,0 +1,97 @@
+#!/usr/bin/env bash
+
+set -Eeuo pipefail
+trap cleanup SIGINT SIGTERM ERR EXIT
+
+# If you need to cd to the script directory:
+script_dir=$(cd "$(dirname "${BASH_SOURCE[0]}")" &>/dev/null && pwd -P)
+
+usage() {
+  cat <<EOF
+Usage: $(basename "${BASH_SOURCE[0]}") [-h] [-v] TARGET
+
+Deploy site to TARGET
+
+Available options:
+
+-h, --help      Print this help and exit
+-v, --verbose   Print script debug info
+EOF
+  exit
+}
+
+cleanup() {
+  trap - SIGINT SIGTERM ERR EXIT
+  # script cleanup here
+}
+
+setup_colors() {
+  if [[ -t 2 ]] && [[ -z "${NO_COLOR-}" ]] && [[ "${TERM-}" != "dumb" ]]; then
+    NOFORMAT='\033[0m' RED='\033[0;31m' GREEN='\033[0;32m' ORANGE='\033[0;33m' BLUE='\033[0;34m' PURPLE='\033[0;35m' CYAN='\033[0;36m' YELLOW='\033[1;33m'
+  else
+    NOFORMAT='' RED='' GREEN='' ORANGE='' BLUE='' PURPLE='' CYAN='' YELLOW=''
+  fi
+}
+
+msg() {
+  echo >&2 -e "${1-}"
+}
+
+die() {
+  local msg=$1
+  local code=${2-1} # default exit status 1
+  msg "$msg"
+  exit "$code"
+}
+
+parse_params() {
+  # default values of variables set from params
+  flag=0
+  param=''
+
+  while :; do
+    case "${1-}" in
+    -h | --help) usage ;;
+    -v | --verbose) set -x ;;
+    --no-color) NO_COLOR=1 ;;
+    # -f | --flag) flag=1 ;; # example flag
+    # -p | --param) # example named parameter
+    #   param="${2-}"
+    #   shift
+    #   ;;
+    -?*) die "Unknown option: $1" ;;
+    *) break ;;
+    esac
+    shift
+  done
+
+  args=("$@")
+
+  # check required params and arguments
+  # [[ -z "${param-}" ]] && die "Missing required parameter: param"
+  [[ ${#args[@]} -eq 0 ]] && die "Missing TARGET"
+  [[ ${#args[@]} -ne 1 ]] && die "Can only deploy to one TARGET"
+
+  return 0
+}
+
+parse_params "$@"
+setup_colors
+
+# script logic here
+
+# msg "${RED}Read parameters:${NOFORMAT}"
+# msg "- flag: ${flag}"
+# msg "- param: ${param}"
+# msg "- arguments: ${args[0]}"
+
+TARGET=${args[0]}
+cd ${script_dir}
+rm -rf public/
+for f in "cv.html" "cv.pdf"; do
+  if [ ~/dev/drafts/cv/${f} -nt static/media/${f} ]; then
+    cp -f ~/dev/drafts/cv/${f} static/media/${f}
+  fi
+done
+hugo && rsync -avz --delete public/ ${TARGET}
+cd -

go.sum

@@ -1,2 +1,4 @@
+github.com/wowchemy/wowchemy-hugo-modules/netlify-cms-academic v0.0.0-20210127225730-4ac1c6aa1a40 h1:qTDiwSNIpSWvBepaw1PlZj4QBvo75Nf5DxsSP8JZtbo=
 github.com/wowchemy/wowchemy-hugo-modules/netlify-cms-academic v0.0.0-20210127225730-4ac1c6aa1a40/go.mod h1:TU3QDPUdBSQnvDP5QVCwjAkBIdVMS/bKFA8jr3eI5AY=
+github.com/wowchemy/wowchemy-hugo-modules/wowchemy v0.0.0-20210127225730-4ac1c6aa1a40 h1:mheZDz5DcXq/x8APxFv7pOLtUkuD2qMgz8GGBO1BXrM=
 github.com/wowchemy/wowchemy-hugo-modules/wowchemy v0.0.0-20210127225730-4ac1c6aa1a40/go.mod h1:H22qfH9qj3FWwsk7+bAZpmT24yRGNQURah2/IRwjbn8=

static/media/cv.html

@@ -3,7 +3,7 @@
 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
 <html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
 <head>
-<!-- 2021-01-31 Sun 19:18 -->
+<!-- 2021-07-20 Tue 17:54 -->
 <meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
 <meta name="viewport" content="width=device-width, initial-scale=1" />
 <title>Francisco Penedo Álvarez</title>
@@ -51,7 +51,7 @@
     padding: 3px;
     border: 1px solid black;
   }
-  pre.src:hover:before { display: inline;}
+  pre.src:hover:before { display: inline; margin-top: 14px;}
   /* Languages per Org manual */
   pre.src-asymptote:before { content: 'Asymptote'; }
   pre.src-awk:before { content: 'Awk'; }
@@ -219,8 +219,8 @@
 <div id="content">
 <h1 class="title">Francisco Penedo Álvarez</h1>
 
-<div id="outline-container-org507c813" class="outline-2">
-<h2 id="org507c813"><span class="section-number-2">1</span> Contact Information</h2>
+<div id="outline-container-org9c3621d" class="outline-2">
+<h2 id="org9c3621d"><span class="section-number-2">1</span> Contact Information</h2>
 <div class="outline-text-2" id="text-1">
 <ul class="org-ul">
 <li>Email: <a href="mailto:contact@franpenedo.com">contact@franpenedo.com</a></li>
@@ -229,8 +229,8 @@
 </div>
 </div>
 
-<div id="outline-container-org8dda112" class="outline-2">
-<h2 id="org8dda112"><span class="section-number-2">2</span> Education</h2>
+<div id="outline-container-orgd67d96e" class="outline-2">
+<h2 id="orgd67d96e"><span class="section-number-2">2</span> Education</h2>
 <div class="outline-text-2" id="text-2">
 <table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
 
@@ -260,8 +260,8 @@
 </div>
 </div>
 
-<div id="outline-container-org0fb7a6e" class="outline-2">
-<h2 id="org0fb7a6e"><span class="section-number-2">3</span> Fellowships and Awards</h2>
+<div id="outline-container-org97d0243" class="outline-2">
+<h2 id="org97d0243"><span class="section-number-2">3</span> Fellowships and Awards</h2>
 <div class="outline-text-2" id="text-3">
 <table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
 
@@ -301,8 +301,8 @@
 </div>
 </div>
 
-<div id="outline-container-orge8dfbdc" class="outline-2">
-<h2 id="orge8dfbdc"><span class="section-number-2">4</span> Publications</h2>
+<div id="outline-container-org9d5b70e" class="outline-2">
+<h2 id="org9d5b70e"><span class="section-number-2">4</span> Publications</h2>
 <div class="outline-text-2" id="text-4">
 <ul class="org-ul">
 <li>Penedo, F., H. Park, and C. Belta. “Control Synthesis for Partial Differential
@@ -327,8 +327,8 @@ in Turning Processes.” IEEE Transactions on Industrial Informatics 8, no. 4 (N
 </div>
 </div>
 
-<div id="outline-container-orgd7d7e5f" class="outline-2">
-<h2 id="orgd7d7e5f"><span class="section-number-2">5</span> Talks</h2>
+<div id="outline-container-org2ddb372" class="outline-2">
+<h2 id="org2ddb372"><span class="section-number-2">5</span> Talks</h2>
 <div class="outline-text-2" id="text-5">
 <table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
 
@@ -348,8 +348,8 @@ in Turning Processes.” IEEE Transactions on Industrial Informatics 8, no. 4 (N
 </div>
 </div>
 
-<div id="outline-container-org7d1e11b" class="outline-2">
-<h2 id="org7d1e11b"><span class="section-number-2">6</span> Research Experience</h2>
+<div id="outline-container-org4673ea4" class="outline-2">
+<h2 id="org4673ea4"><span class="section-number-2">6</span> Research Experience</h2>
 <div class="outline-text-2" id="text-6">
 <table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
 
@@ -379,8 +379,8 @@ in Turning Processes.” IEEE Transactions on Industrial Informatics 8, no. 4 (N
 </div>
 </div>
 
-<div id="outline-container-org314499f" class="outline-2">
-<h2 id="org314499f"><span class="section-number-2">7</span> Teaching</h2>
+<div id="outline-container-org5187058" class="outline-2">
+<h2 id="org5187058"><span class="section-number-2">7</span> Teaching</h2>
 <div class="outline-text-2" id="text-7">
 <table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
 
@@ -405,12 +405,12 @@ in Turning Processes.” IEEE Transactions on Industrial Informatics 8, no. 4 (N
 </div>
 </div>
 
-<div id="outline-container-org4eb3090" class="outline-2">
-<h2 id="org4eb3090"><span class="section-number-2">8</span> Skills</h2>
+<div id="outline-container-org8d4e2b9" class="outline-2">
+<h2 id="org8d4e2b9"><span class="section-number-2">8</span> Skills</h2>
 <div class="outline-text-2" id="text-8">
 </div>
-<div id="outline-container-orga87f10f" class="outline-3">
-<h3 id="orga87f10f"><span class="section-number-3">8.1</span> Languages</h3>
+<div id="outline-container-orgef78c4f" class="outline-3">
+<h3 id="orgef78c4f"><span class="section-number-3">8.1</span> Languages</h3>
 <div class="outline-text-3" id="text-8-1">
 <table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
 
@@ -445,8 +445,8 @@ in Turning Processes.” IEEE Transactions on Industrial Informatics 8, no. 4 (N
 </div>
 </div>
 
-<div id="outline-container-org025a554" class="outline-3">
-<h3 id="org025a554"><span class="section-number-3">8.2</span> Computer Skills</h3>
+<div id="outline-container-org1e1a713" class="outline-3">
+<h3 id="org1e1a713"><span class="section-number-3">8.2</span> Computer Skills</h3>
 <div class="outline-text-3" id="text-8-2">
 <table border="2" cellspacing="0" cellpadding="6" rules="groups" frame="hsides">
 
@@ -458,13 +458,23 @@ in Turning Processes.” IEEE Transactions on Industrial Informatics 8, no. 4 (N
 </colgroup>
 <tbody>
 <tr>
-<td class="org-left">Programming languages</td>
-<td class="org-left">Python, Java, C.</td>
+<td class="org-left">Programming languages (proficient)</td>
+<td class="org-left">Python, Java, C</td>
+</tr>
+
+<tr>
+<td class="org-left">Programming languages (some skill)</td>
+<td class="org-left">Haskell, Lisp, JavaScript, Bash, VHDL, HTML, CSS</td>
+</tr>
+
+<tr>
+<td class="org-left">Databases</td>
+<td class="org-left">PostgreSQL, SQLite</td>
 </tr>
 
 <tr>
 <td class="org-left">Frameworks</td>
-<td class="org-left">numpy, scipy, matplotlib.</td>
+<td class="org-left">numpy, scipy, matplotlib, scikit-learn, pandas</td>
 </tr>
 </tbody>
 </table>
@@ -473,7 +483,7 @@ in Turning Processes.” IEEE Transactions on Industrial Informatics 8, no. 4 (N
 </div>
 </div>
 <div id="postamble" class="status">
- <p class="date">Last Updated: 2021-01-31 Sun 19:18</p>
+ <p class="date">Last Updated: 2021-07-20 Tue 17:54</p>
 </div>
 </body>
 </html>