diff --git a/config/_default/params.toml b/config/_default/params.toml index 39a26d5..38009c8 100644 --- a/config/_default/params.toml +++ b/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 diff --git a/content/project/templogic/featured.png b/content/project/templogic/featured.png new file mode 100644 index 0000000..bbfca4a Binary files /dev/null and b/content/project/templogic/featured.png differ diff --git a/content/project/templogic/index.md b/content/project/templogic/index.md new file mode 100644 index 0000000..bb1d97c --- /dev/null +++ b/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) diff --git a/content/publication/cdc2018/index.md b/content/publication/cdc2018/index.md index b9b6ec0..079c98c 100644 --- a/content/publication/cdc2018/index.md +++ b/content/publication/cdc2018/index.md @@ -68,6 +68,7 @@ image: # Otherwise, set `projects: []`. projects: - formal-pde +- templogic # Slides (optional). # Associate this publication with Markdown slides. diff --git a/content/publication/hscc16/index.md b/content/publication/hscc16/index.md index b013cbf..89ba9d7 100644 --- a/content/publication/hscc16/index.md +++ b/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.