Added templogic project

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)