Cause Mining and Controller Synthesis with STL

TL;DR

This paper introduces a novel method for controlling cyber-physical systems by identifying causes of unwanted events using STL and synthesizing controllers to minimize these events, applicable to systems with finite control options.

Contribution

It presents an alternative cause-based approach for controller synthesis using STL, addressing limitations of formal methods in complex or stochastic systems.

Findings

Reduces the number of unwanted events in system traces

Applicable to systems with finitely many control choices

Validated on traffic congestion avoidance example

Abstract

Formal control of cyber-physical systems allows for synthesis of control strategies from rich specifications such as temporal logics. However, the classes of systems that the formal approaches can be applied to is limited due to the computational complexity. Furthermore, the synthesis problem becomes even harder when non-determinism or stochasticity is considered. In this work, we propose an alternative approach. First, we mark the unwanted events on the traces of the system and generate a controllable cause representing these events as a Signal Temporal Logic (STL) formula. Then, we synthesize a controller based on this formula to avoid the satisfaction of it. Our approach is applicable to any system with finitely many control choices. While we can not guarantee correctness, i.e., the unwanted events will never occur, we show on an example that the proposed approach reduces the number of the unwanted events. In particular, we validate it for the congestion avoidance problem in a traffic network.

Figures

Tables

Table 1. TABLE I : Violation counts after each iteration of Alg.  3

$Ex\#$	time	${𝒱}_0$	${𝒱}_1$	${𝒱}_2$	${𝒱}_3$	${𝒱}_4$	${𝒱}_5$	${𝒱}_6$	${𝒱}_7$
#1	630sec	911	143	23	5	2	0	-	-
#2	320sec	911	530	265	5	6	2	0	-
#3	115sec	911	617	149	80	70	48	10	0

Table 2. TABLE II : Parameters of Alg.  3

$Ex\#$	$\underset{¯}{oc}$	$\overline{oc}$	$\overline{p}$	$\underset{¯}{val}$
#1	0	$\infty$	$\infty$	0.01
#2	0	$\infty$	$\infty$	0.1
#3	0	0	1	0

Table 3. TABLE III : Congested traffic system: Violation counts and the optimized cause formulas for each iteration of Alg.  3 .

$i$	${𝒱}_i$	${\Phi }_i$	$tp$	$fp$
1	1591	$\left(G_{[1,2]}^{-}{u}^0=1\right)\wedge \left(F_{[1,1]}^{-}\left(x^0>20\right)\right)$	405	0
2	1549	$\left(G_{[1,2]}^{-}{u}^0=0\right)\wedge \left(F_{[1,1]}^{-}\left(x^3>10\right)\right)$	576	0
3	1557	$\left(G_{[1,2]}^{-}{u}^1=0\right)\wedge \left(F_{[1,1]}^{-}\left(u^1=0\right)\right)$	465	19
4	1763	$\left(G_{[1,2]}^{-}{u}^1=1\right)\wedge \left(F_{[1,1]}^{-}\left(u^1=1\right)\right)$	599	3
5	2	-	-	-

Table 4. TABLE IV : Region avoidance: Violation counts and the optimized cause formulas for each iteration of Alg.  3 .

$i$	${𝒱}_i$	${\Phi }_i$	$tp$	$fp$
1	705	$\left(G_{[1,1]}^{-}u=S\right)\wedge \left(F_{[1,1]}^{-}\left(x^1>3\wedge x^0>2\right)\right)$	126	0
2	429		125	0
3	109	$\left(G_{[1,1]}^{-}u=E\right)\wedge \left(F_{[1,1]}^{-}\left(x^1>2\wedge x^0>3\right)\right)$	42	0
4	77		52	0
5	0	–	–	–

Equations

$$x_{k+1}=f(x_k,u_k,w_k)$$

$$\mathbf{x}=(x_0,u_0),\dots ,(x_N,u_N),$$

$$\mathbf{l}=l_0,\dots ,l_N$$

$$\mathcal{D}=\{({\mathbf{x}}_i,{\mathbf{l}}_i){\}}_{i=1,\dots ,D}.$$

$$x^0<30\wedge x^1<30\wedge x^2<30\wedge x^3<15\wedge x^4<15$$

$$P:(\mathbb{X}\times \mathbb{U}{)}^{M+1}\to \{0,1\}.$$

$$tp$$

$$fp$$

$$F_{\beta }=\frac{(1+{\beta }^2)\ast precision\ast recall}{({\beta }^2\ast precision)+recall}$$

$$\varphi =$$

$$(\mathbf{x},k)\models x^i\sim c⟺x_k^i\sim c\text{ where }\sim \in \{>,<\}$$

$$(\mathbf{x},k)\models u^i=c⟺u_k^i=c$$

$$(\mathbf{x},k)\models \neg \varphi ⟺(\mathbf{x},k)/\models \varphi$$

$$(\mathbf{x},k)\models {\varphi }_1\wedge {\varphi }_2⟺(\mathbf{x},k)\models {\varphi }_1\text{ and }(\mathbf{x},k)\models {\varphi }_2$$

$$(\mathbf{x},k)\models {\varphi }_1{S}_{[a,b]}{\varphi }_2⟺\text{there exists}j\in ([k-b,k-a]\cap [0,k])$$

$$\text{ such that }(\mathbf{x},j)\models {\varphi }_2\text{ and for each }l\in [j,k],(\mathbf{x},l)\models {\varphi }_1$$

$$F_{[a,b]}^{-}\varphi :=true{S}_{[a,b]}\varphi G_{[a,b]}^{-}\varphi :=\neg F_{[a,b]}^{-}\neg \varphi$$

$$\mathfrak{l}(true)=\mathfrak{l}(x^i\sim c)=\mathfrak{l}(u^i=c)=0$$

$$\mathfrak{l}(\neg \varphi )=\mathfrak{l}(\varphi ),\mathfrak{l}({\varphi }_1\wedge {\varphi }_2)=\max (\mathfrak{l}({\varphi }_1),\mathfrak{l}({\varphi }_2))$$

$$\mathfrak{l}({\varphi }_1{S}_{[a,b]}{\varphi }_2)=b+\max (\mathfrak{l}({\varphi }_1),\mathfrak{l}({\varphi }_2))$$

$$(((x_{i-\mathfrak{l}(\varphi )+1},u_{i-\mathfrak{l}(\varphi )+1}),\dots ,(x_i,u_i)),\mathfrak{l}(\varphi ))\models \varphi$$

$$\Psi :={\Phi }_1\vee \dots \vee {\Phi }_p,$$

$$where$$

$${\Phi }_i:=(G_{[1,b_i]}^{-}{u}^j=c_i)\wedge (F_{[1,1]}^{-}{\varphi }_i),$$

$$\Phi =(G_{[1,1]}^{-}{u}^0=0)\wedge (F_{[1,1]}^{-}{x}^3>10)$$

$${\varphi }_{(oc=r)}:=$$

$$\neg {\varphi }_{(oc=r-1)}\mid F_{[a,b]}^{-}{\varphi }_{(oc=r-1)}\mid G_{[a,b]}^{-}{\varphi }_{(oc=r-1)}\mid$$

$${\varphi }_{(oc=r_1)}{S}_{[a,b]}{\varphi }_{(oc=r_2)}$$

$${\varphi }_{(oc=0)}$$

$${\Phi }_{(oc=r)}:=(G_{[1,b]}^{-}{u}^j=c)\wedge F_{[1,1]}^{-}{\varphi }_{(oc=r)},$$

$${\Psi }_{0.1}^{\ast }(v)$$

$${\Psi }_{0.01}^{\ast }(v)$$

$$((G_{[1,1]}^{-}{u}^0=0)\wedge (F_{[1,1]}^{-}(x^3>10)))\vee$$

$$((G_{[1,1]}^{-}{u}^1=0)\wedge (F_{[1,1]}^{-}(x^4>10)))$$

$$\mathbf{x}=(x_{k-\mathfrak{l}(\Phi )},u_{k-\mathfrak{l}(\Phi )}),\dots ,(x_{k-1},u_{k-1}),$$

$$[x_{k+1}^0,x_{k+1}^1]=\{\begin{array}{l}[\min (0,x_k^0-1),x_k^1]\text{ if }u=N\\ [x_k^0,\max (x_k^1+1,M_1-1)]\text{ if }u=E\\ [\max (x_k^0+1,M_0-1),x_k^1]\text{ if }u=S\\ [x_k^0,\min (0,x_k^1-1)]\text{ if }u=W\end{array}$$

Full text

I INTRODUCTION

In formal control, the goal is to synthesize control strategies from formal specifications expressed in rich specification languages. The main approach in formal control of dynamical systems is based on construction of a finite abstraction of the system, and then synthesis of a control strategy for the abstract model from the specification [1]. Finally, the strategy is mapped to the original system. This approach has been applied to linear, switched, and piecewise-affine, and hybrid systems [2, 1, 3]. In addition, game theoretic and probabilistic versions of the formal control problem has been studied for non-deterministic and stochastic systems [4, 1, 5]. Despite the promising results on synthesis of correct-by-construction controllers, the abstraction based approach suffers from scalability issues due to the complex operations involved in the abstraction process and the size of the resulting abstract model. Furthermore, the developed methods are specific to the underlying system and extensions to more complex systems such as systems with a variety of submodules, e.g. Simulink models [6], is not straightforward.

In this work, we propose an alternative approach that is applicable to any discrete-time dynamical system with finitely many control choices. In particular, we consider the following problem: given a discrete time control system with a finite control set, a function over the state and control spaces of the system that identifies the unwanted events, find a feedback control strategy to minimize the number of these events. We propose a two step solution to this problem. The first step is the identification of the controllable causes of the unwanted events in the form of past time signal temporal logic (STL) formulas. The second step is the synthesis of a feedback controller that avoids the satisfaction of the cause formula found in the first step. In addition, we iteratively apply these two steps, namely cause identification and controller synthesis, to refine the controller and further reduce the number of these events.

Synthesis of STL formulas from a dataset has been studied in different forms including generation of a classifier to decide whether a trace exhibit a desired (or undesired) behavior [7, 8], identification of high level system behaviors from traces [9, 10], and synthesis of monitoring rules [11, 12]. In [9], the goal is to synthesize parameters for a given template formula. For example, for the template formula $G_{[0,\infty]}x<p$, a valid valuation of the parameter $p$ gives an upper bound on the value of variable $x$ along all the traces in the dataset. On the other hand, in [7, 8, 10, 11, 12, 13], both the formula structure (e.g. a template formula), and the parameters of it are found simultaneously. These works differ based on the structure of the dataset. In [9, 10] only positive examples, whereas in [7, 8, 13], both positive and negative examples are considered. A common aspect of these works [7, 8, 9, 10, 13] is that traces are considered as a whole (e.g. single label for a trace). Whereas, similar to this work, in [11, 12], each time point has a label, and we build on the results from [11, 12].

In the cause identification step, we generate a past time STL formula in a particular structure so that a controller can prevent the satisfaction of it. The formula represents a set of causes that can yield to the unwanted events in a human interpretable way. Each cause has a control part over the control variables and a general part that can be any STL formula over the system’s state and control variables. The formula maps to a feedback controller that generates a control input violating each cause formula. As opposed to the abstraction based [1] and mixed integer linear program based controllers for STL specifications [14, 15], the proposed controller does not require any offline computation and the system dynamics are not explicitly considered. At each time step, it simply checks the trace against a past time STL formula to generate a control input by exploiting the particular structure of the formula.

The main contribution of this work is the novel dynamics-independent framework for synthesis of feedback controllers to avoid unwanted events. This framework can be applied to any discrete time system with a finite control set. However, correctness is not guaranteed, i.e., the unwanted events may occur on the traces of the closed loop system. For this reason, we only aim at reducing the number of these events. The reduction rate depends on the causality relation between the control inputs and the unwanted events. We show on an example that the proposed controller can reduce the number of unwanted events significantly when the formal control problem is infeasible.

The paper is structured as follows. Sec. II presents necessary preliminaries. Sec. III formulates the cause identification and the controller synthesis problems. Sec. IV presents our solution for the cause identification problem. Sec. VI describes the controller synthesis approach. Sec. VII concludes the paper with future research directions.

II Preliminary Information

II-A System Definition

Consider the discrete time control system

[TABLE]

where $x_{k}=[x_{k}^{0},\ldots,x_{k}^{n-1}]\in\mathbb{X}\subset\mathbb{R}^{n}$ is the state of the system, $u_{k}=[u_{k}^{0},\ldots,u_{k}^{m-1}]\in\mathbb{U}\subset\mathbb{R}^{m}$ is the control input and $w_{k}\in\mathbb{W}\subset\mathbb{R}^{l}$ is the noise at time step $k$. Each control input takes values from a finite set, i.e., $\mathbb{U}^{i}=\{c^{(i,1)},\ldots,c^{(i,M_{i})}\}\subset\mathbb{R},i=0,\ldots,m-1$ and $\mathbb{U}=\mathbb{U}^{0}\times\ldots\times\mathbb{U}^{m-1}$. A finite length trajectory of system (1) is denoted by

[TABLE]

where for each $k=0,\ldots,N-1$, $x_{k+1}=f(x_{k},u_{k},w_{k})$ for some $w_{k}\in\mathbb{W}$. The label of a trajectory $\mathbf{x}$ is a binary sequence of the same length

[TABLE]

where $l_{k}\in\{0,1\}$. The positive label, $l_{k}=1$, indicates that a bad event occurred at time step $k$. The label sequence can be generated by a function over the state and system traces, e.g. $g:\mathbb{X}\times\mathbb{U}\to\{0,1\}$, and $l_{k}=g(x_{k},u_{k})$. A set of labeled traces of system (1) is denoted as

[TABLE]

Example II.1

We use a traffic system composed of 5 links and 2 traffic signals shown in Fig. 1 as a running example. Each link of the system is modeled as a finite queue, which results in a piecewise-affine system. The details of the model can be found in [16]. In this model, the system state captures the number of vehicles on each link and the modes of the traffic signals are control inputs. For the considered system, the capacity of the horizontal and vertical links are $40$ and $20$, respectively, i.e. $x^{i}\in[0,40]$ for $i\in\{0,1,2\}$, and $x^{i}\in[0,20]$ for $i\in\{3,4\}$. The control inputs are defined as $\mathbb{U}^{1}=\mathbb{U}^{2}=\{0,1\}$, where [math] denotes horizontal actuation and $1$ denotes vertical actuation. The system parameters are defined as follows (see [16] for system dynamics): $c_{i}=20$ for $i\in\{0,1,2\}$ and $c_{i}=10$ for $i\in\{3,4\}$ (saturation flow), $d_{i}=5$, for $i\in\{0,3,4\}$ (exogenous flow bound), $\alpha^{0}_{0,1}=\alpha^{0}_{1,2}=1,\alpha^{1}_{3,1}=\alpha^{1}_{4,2}=1$ (supply ratios), $\beta_{0,1}=\beta_{1,2}=\beta_{2,3}=0.75$, $\beta_{3,1}=\beta_{4,1}=0.3$ (turn ratios).

We simulated the system from random initial conditions and picked control values from $\mathbb{U}$ randomly at each time step to generate a dataset. In addition, we used the following formula to label the system traces:

[TABLE]

Time points in which this formula is violated are labeled with $1$, all the other time points are labeled with [math]. Essentially, label 1 is generated whenever a link has more vehicles than $75\%$ of its capacity.We generate a dataset $\mathcal{D}$ with 20 labeled traces. Each trace has length $100$. Out of $2000$ data points, $911$ of them were labelled with 1, which indicates that the system is congested $46\%$ of the time.

II-B Binary Classification

The goal in the binary classification task is to assign a binary label to each data point. The success of a classifier over a labeled dataset is computed according to the four basic categories of the classifier results and original labels: true positives, false positives, true negatives and false negatives.

A binary classifier $P$ for traces of system (1) with length $M+1$ is defined as

[TABLE]

For such a classifier, the computation of the number of true positives ($tp$) and false positives ($fp$) over a dataset $\mathcal{D}$ (3) is shown in (6). The computation for the number of true negatives ($tn$) and false negatives ($fn$) are similar, and omitted for brevity.

[TABLE]

The ratio of correctly classified instances ( $(tp+tn)/(tp+tn+fp+fn)$), precision ($tp/(tp+fp)$), and recall ($tp/(tp+fn)$) are commonly used success measures for classifiers. Another widely used metric is $F_{\beta}$ score, which combines precision and recall via a weight parameter $\beta$:

[TABLE]

$F_{\beta}$ takes values between [math] (worst) and $1$ (best). Increasing $\beta$ puts more emphasis on recall (and false negatives), on the other hand , decreasing $\beta$ puts more emphasis on precision.

II-C Signal Temporal Logic

We express signal specifications as ptSTL formulas [17]. The syntax of ptSTL over the variables of system (1) is inductively defined as:111As the considered controls take values from finite sets, only equality constraints are used for controls.

[TABLE]

where $true$ stands for the Boolean constant true, $x^{i}$ is a state variable, $u^{i}$ is a control variable, $\sim\in\{>,<\}$, $c\in\mathbb{R}$ is a constant, $[a,b]\subset\mathbb{R}$ represents a time interval with $a\leq b$, and $S$ is ptSTL operator representing Since. The semantics of a ptSTL formula is defined over a signal for a given time point. The notation $(\mathbf{x},k)\models\phi$ is used to denote that the signal $\mathbf{x}$ satisfies $\phi$ at time $k$, which is defined as follows:

[TABLE]

The Previously—(Past Eventually)— ($F^{-}$), Always—(Past Globally)— ($G^{-}$) operators are defined for notational convenience as they are special cases of $S$ operator:

[TABLE]

Definition 1** (Parametric ptSTL Formula)**

Parametric ptSTL is an extension of STL that allows to represent some of the numeric constants with parameters [17]. Given a parametric ptSTL formula $\phi$ and a parameter valuation $v$, a ptSTL formula $\phi(v)$ is obtained by replacing parameters in $\phi$ from the corresponding constants in $v$, e.g. for formula $\phi=F^{-}_{[0,b]}(x>c)$, and valuation $v:b=3,c=5$, $\phi(v)$ is $F^{-}_{[0,3]}(x>5)$.

Definition 2** (Length of a formula)**

Informally, the length of a formula gives the oldest time point that is required to evaluate the formula. The length is denoted with $\mathfrak{l}(\phi)$ and computed as follows:

[TABLE]

Definition 3** (Operator count)**

The operator count of a formula is the total number of Boolean and temporal operators that appear in the formula.

A ptSTL formula $\phi$ can be used as classifier as given in  (5) for the traces of system (1). In particular, $\mathfrak{l}(\phi)$ is the length of the trace fragment, and the classification result is 1 when the considered fragment satisfies the formula:

[TABLE]

It is straightforward to derive the success measures, e.g. recall, precision, $F_{\beta}$-score, for a ptSTL formula $\phi$ over a dataset $\mathcal{D}$. In the remainder of the paper, $F_{\beta}(\phi(v),\mathcal{D})$ is used to denote the $F_{\beta}$ score of the parametric formula $\phi$ with valuation $v$ over the dataset $\mathcal{D}$. The dataset is omitted (e.g. $F_{\beta}(\phi(v))$) when it is clear from the context.

III Problem Formulation

In this work, our goal is to design a feedback controller for system (1) to reduce the occurence of unwanted events during the execution of the system. We propose a two step solution for this problem. In the first step, we identify the controllable causes of the unwanted events over a labeled dataset of system traces. To generate the dataset, we simulate the system with a nominal (or random) controller and label the traces. In the second step, we synthesize a controller that avoids the causes found in the first step.

We propose to identify the controllable causes of the unwanted events in the form of ptSTL formulas over the system’s state and control variables. In particular, the generated formula will represent the unwanted events (label 1). In addition, it will be in a particular structure, i.e, controllable, so that the satisfaction of the formula can be avoided by a controller. Thus the number of the unwanted events can be reduced by the controller. We call the formula found in the first step as the cause formula. The formula synthesis problem is formalized in Prob. III.1.

Problem III.1** (Finding a cause formula)**

Given a control system (1), a set of its labeled traces $\mathcal{D}$ (3), find a ptSTL formula in the following form

[TABLE]

[TABLE]

[TABLE]

and $\phi_{i}$ is any ptSTL formula over $\{x^{0},\ldots,x^{n-1}\}\cup\{u^{0},\ldots,u^{m-1}\}$ such that the valuation of the formula along the traces mimics the labels, i.e. for any $(\mathbf{x},\mathbf{l})\in\mathcal{D}$, whenever $l_{k}=1$, $(\mathbf{x},k)\models\Psi$.

The combined cause formula (9) is a disjunction of cause formulas in the form of (10) that represents a controllable cause. The controllable cause identifies the unwanted events in the previous time step. The first part ($G^{-}_{[1,b]}u^{j}=c_{i}$) of the formula can be violated with the choice of a suitable control input in the previous time step, and the second part ($F^{-}_{[1,1]}\phi_{i}$) captures the cause over the state and the control variables.

A formula that is satisfied at all of the time points with label $1$ (i.e. has no false negatives) and that is violated at all other time points (i.e. has no false positives) is an ideal formula. Due to the particular labeling process and the structure of the formula (9) considered in Prob. III.1, it might not be possible to find such an ideal formula. In our solution, we aim at generating the best formula representing the given dataset $\mathcal{D}$. Any success measure for the binary classification task can be used to determine how good the formula is with respect to the given dataset. We use $F_{\beta}$-score to balance the false negatives and false positives. To generate the formula, we first sort all parametric formulas in the given form (10) according to their operator counts. Then, iteratively perform parameter optimization and generate combined cause formulas as in (9).

In the second step of our solution, we synthesize a controller that avoids the combined cause formula $\Psi$ found at the first step.

Problem III.2** (Controller synthesis)**

Given a control system (1) and a ptSTL formula $\Psi$ of the form (9), generate a finite memory feedback controller $\mathcal{U}:(\mathbb{X}\times\mathbb{U})^{K}\to\mathbb{U}$ such that the trajectory of the closed loop system violates $\Psi$ at each time step.

The proposed controller as a solution to Prob. III.2 evaluates the trace of the system against the general and control parts of each cause formula, and produce the control inputs accordingly. In particular, at time step $k$, a control input $u\in\mathbb{U}$ that violates time-shifted formula $(G^{-}_{[0,b-1]}u^{j}=c_{i})\wedge\phi_{i}$ for each subformula $\Phi_{i}$ is generated to violate $\Psi$ at the next time step. As these represent the unwanted events in the given dataset, the generated control strategy is expected to reduce the number of these events. Essentially, the stronger the causality between the control inputs and the unwanted events is, the better our solution is going to be, i.e., the larger number of unwanted events will be avoided by the synthesized controller.

Example III.1

For the traffic system shown in Ex. II.1, a formula $\phi$ as in (10) represents the continuous actuation of a road for $b-1$ time units while blocking the neighbouring road, and the general part captures other properties in the system. For example, blocking $x^{3}$ when there is more than $10$ vehicles would lead to satisfaction of (4) at the next time step, which is captured in the following cause formula:

[TABLE]

IV Finding Controllable Causes

In this section, we present our solution for Prob. III.1. First, we define the set of all parametric cause formulas (10) with a given operator count limit. Then, we use an iterative formula synthesis approach to generate $\Psi$ (9). In particular, starting from $\Psi=false$, at each iteration, for each parametric cause formula $\Phi$, we synthesize parameters $v$ that optimize the valuation of the combined formula ($\Psi\vee\Phi(v)$), and choose the optimal one and concatenate it to $\Psi$ via disjunction. The iteration continues until a given cause or operator limit is reached or the improvement on the valuation is insufficient. We use $F_{\beta}$ score for formula evaluation to balance the errors (e.g. false positives and false negatives).

A parametric ptSTL formula with $r$ operators is denoted as $\phi_{(oc=r)}$. Such a formula over the state and input variables of system (1) is recursively defined as follows:

[TABLE]

where $a,b$ and $c$ are parameters, and $r_{1}+r_{2}=r-1$. We use $\Phi_{(oc=r)}$ to denote a parametric subformula (10) with $r$ operators in the general formula part, which is defined as:

[TABLE]

Note that the formula $(G^{-}_{[1,b]}u^{j}=c)\wedge(F^{-}_{[1,1]}true)$ with [math] operators in the general formula part is equivalent to $(G^{-}_{[1,b]}u^{j}=c)$. This formula represents the case when the unwanted event occurred exclusively due to the choice of the control input.

The proposed formula synthesis method is summarized in Alg. 1. In this algorithm, first, the current operator count $oc$ and the last used operator count ${oc}_{last}$ are set to the minimum operator count $\underline{oc}$. Then, the set of all parametric cause formulas $PF^{={oc}}$ with $oc$ operators (as defined in (13)) is computed (line 3). In the main loop from line 4 through line 16, parameter optimization is performed for parametric cause formulas to generate the combined cause formula in an iterative fashion. In particular, initially, the set of optimized cause formulas, $FS$, includes only formula $false$ and parameter optimization is performed for each parametric formula in $PF^{={\underline{oc}}}$ (lines 5-7). The optimum among these, $\Phi(v)^{*}$, is selected. If the difference of the evaluations of $\Phi(v)^{*}$ and formula $false$ is greater than the given bound $\underline{val}$, $\Phi(v)^{*}$ is added to the set of optimized cause formulas (line 13). Otherwise, considering that the valuation of the best cause formula with operator count $oc$ is below the limit, the operator count is incremented by one (line 10) and $PF^{=oc}$ is computed. In the subsequent iterations of the main loop, for the parametric cause formulas $\Phi\in PF^{=oc}$, the parameter optimization is performed on the combined cause formula $\bigvee(FS)\vee\Phi$ (line 6, $\bigvee(FS)$ is not parametric), and, again, the valuation of the combined formula, $F_{\beta}(\bigvee(FS)\vee\Phi(v))$, is used in formula selection (line 8). Thus, in both cases, the improvement achieved with the new cause formula $\Phi$ (13) is considered. At each iteration of the main loop, either a new formula is added to $FS$ or the operator count is incremented. The loop terminates when 1) the operator count exceeds the given bound $\overline{oc}$, or 2) a new cause was not added for the last $oc_{lim}$ different operator counts, or 3) the given cause limit $\overline{p}$ is reached. $FS$ is the set of all optimized cause formulas, and the disjunction of these is returned (line 17).

The ParameterOptimization method takes a dataset $\mathcal{D}$ (3), a parametric ptSTL formula $\Phi$, and a domain for each parameter type $\mathcal{P}$ as input. It iterates through all possible valuations $v$ for the parameters that appear in $\Phi$. In particular, each parameter in $\Phi$ is considered to be different and the optimization method iterates through the product of the corresponding parameter domains, e.g., for formula $G^{-}_{[1,b]}(u^{j}=c)\wedge F^{-}_{[1,1]}G^{-}_{[a,b]}(u^{j}=c)$ iterate through $\mathcal{P}(b)\times\mathcal{P}(c_{u,j})\times\mathcal{P}(a)\times\mathcal{P}(b)\times\mathcal{P}(c_{u,j})$. For each valuation $v$, it computes the formula $\Phi(v)$ as in Defn. 1 and its fitness $F_{\beta}(\Phi(v),\mathcal{D})$. Finally, it returns the valuation with the highest score, e.g., $\text{arg}\max\{F_{\beta}(\Phi(v),\mathcal{D})\mid v\text{ is a valuation for }\Phi\}$.

Example IV.1

We apply the parameter synthesis algorithm on the dataset defined in Ex. II.1 for the traffic system shown in Fig. 1 ($n=5$, $m=2$). The parameter domains are defined as follows: $\mathcal{P}(c_{x,i})=\{10,15,20,25,30,35\}$ for $i=0,1,2$, $\mathcal{P}(c_{x,i})=\{5,10,15\}$ for $i=3,4$, $\mathcal{P}(c_{u,i})=\{0,1\}$ for $i=0,1$, $\mathcal{P}(a)=\{0,1,2,3,4,5\}$, and $\mathcal{P}(b)=\{0,1,2,3,4,5\}$. We run Alg. 1 with parameters $\underline{oc}=0$, $\overline{oc}=\infty$, $oc_{lim}=2$, $\overline{p}=\infty$. Note that no upper bound is set on the number of cause formulas or on the number of operators. The algorithm only terminates when no formula from $PF^{oc}$ satisfies the valuation condition for the last 2 operator counts (line 9). The resulting formulas for $\underline{val}=0.1$ and $\underline{val}=0.01$ are:

[TABLE]

As expected, smaller valuation limit $\underline{val}$ resulted in longer formulas with higher fitness: $F_{0.3}(\Psi^{*}_{0.1}(v))=0.92$, $tp$ of $\Psi^{*}_{0.1}(v)$ is $427$, whereas $F_{0.3}(\Psi^{*}_{0.01}(v))=0.99$, and $tp$ of $\Psi^{*}_{0.01}(v)$ is $785$. The $fp$ for both of the formulas is [math] (see (6)). Essentially, when $\underline{val}=0.1$, only the formulas that improve the valuation significantly is added to the optimized formula set. The computation took $112$ and $260$ seconds for $\Phi^{*}_{0.1}(v)$, and $\Phi^{*}_{0.01}(v)$, respectively, on a laptop with $4GB$ memory and $1.6$ GHz Intel Core $i5$ processor. Formula $\Phi^{*}_{0.1}(v)$ shows that blocking link [math] or link $3$ for three consecutive time units will cause congestion (see Fig.1). The first part of the formula $\Phi^{*}_{0.01}(v)$ found in the second case is the same as $\Phi^{*}_{0.1}(v)$. The remaining part indicates that if the link 3 or link 4 is blocked when there are more than $10$ vehicles on them, there will be congestion in the next time step. A sample system trace, the label of it and the valuation of formula $\Psi^{*}_{0.01}(v)$ along the trace are shown in Fig. 2. In addition, we validated $\Psi^{*}_{0.01}(v)$ on $10$ other randomly generated datasets as defined in Ex. II.1 (using a random controller). Similar to this example, each dataset has $20$ traces with length $100$. The average number of positive labels in a dataset is $939.7$ (congestion for $47\%$ of the time in average). The average number of true positives and false positives for $\Psi^{*}_{0.01}(v)$ over these datasets are $803.9$ and $0.4$, respectively. These experiments show that the formula correctly identifies the causes for $85\%$ of the unwanted events, and rarely marks a normal event as bad. The minimality of the false positive rates is a result of using $F_{0.3}$-score.

Complexity. The time complexity of Alg. 1 is characterized by the operator count limit $\overline{oc}$, the cause limit $\overline{p}$ and the size of the parameter domain $s$, where $s=\max_{\mathcal{P}(\alpha)\in\mathcal{P}}|\mathcal{P}(\alpha)|$. The number of parameters $\#(\phi)$ of a parametric ptSTL formula $\phi$ with $r$ operators is upper bounded by $3r+1$, where the upper bound is attained when the formula has $r$ nested $S$ (since) operators. The complexity of the parameter optimization method is characterized by the number of fitness value computations, which is exponential in the number of parameters of the input formula $\phi$, $\#(\phi)$, and polynomial in $s$, e.g., $O(s^{\#(\phi)})$ due to the grid search. At each iteration, the parameter optimization is performed for each formula in $PF^{={oc}}$. The number of parametric formulas with ${oc}$ operators, i.e., $|PF^{={oc}}|$, is exponential in $oc$, and polynomial in $n$ (system dimension) and $m$ (control dimension). In particular, $|PF^{={0}}|=m\times(2n+m+1)$ is the number of parametric formulas with 0 operators (see (12)) and $|PF^{={oc}}|$ is in $O(|PF^{={0}}|^{{oc}})$. The algorithm terminates with in $\overline{oc}+\overline{p}$ iterations. Even though the parameter optimization method is exponential in the number of parameters, due to the iterative nature of the algorithm, at most $3\overline{oc}+3$ parameters are optimized simultaneously.

In Alg. 1, a grid search is performed for each candidate cause formula via the ParameterOptimization method. Alternative optimization methods such as formula synthesis via data mining [12] can be employed to improve the computational efficiency. In addition, monotonicity based efficient parameter synthesis methods can be adapted to the considered dataset when a monotone optimization criteria, such as the number of true positives, is used instead of $F_{\beta}$ score [9]. As the particular parameter optimization method is not the focus of this work, we used a simple search algorithm.

V Controller Synthesis

In this section, we present our solution for Prob. III.2. The proposed feedback controller generates a control input $u\in\mathbb{U}$ at each time step to avoid the satisfaction of the cause formula $\Psi=\Phi_{1}\vee\ldots\vee\Phi_{p}$ (9) found in the first step. Note that, at time step $k$, $\Psi$ is violated if and only if each subformula $\Phi_{i}$ for $i=1,\ldots,p$ is violated.

The controller is presented in Alg. 2. It takes the cause formula $\Psi$ and the partial trace $\mathbf{x}$ of the system that is required to compute the satisfaction of $\Psi$ at time step $k$ as inputs. In line 4 through line 10, the controller randomly picks a control input $u$ from $\mathbb{U}$, appends $(x_{k},u)$ to the partial trace $\mathbf{x}$, then for each sub-formula $\Phi_{i}=(G^{-}_{[1,b]}u^{j}=c)\wedge F^{-}_{[1,1]}\phi$, the controller evaluates the formula shifted by a time step, $(G^{-}_{[0,b-1]}u^{j}=c)\wedge\phi$, along the partial trace. $u$ is removed from the candidate set of controls (line  7) if the shifted-formula is satisfied for a cause formula $\Phi_{i}$. Otherwise, $u$ guarantees that each cause formula, thus $\Psi$ (9), will be violated at time step $k+1$, and the controller generates $u$.

If the candidate control set becomes empty, the controller generates a control input randomly (line 11). In this case, the control input that satisfies the minimum number of cause formulas can be generated with additional bookkeeping.In the following proposition, we establish the sufficient conditions under which the controller guarantees that $\neg\Psi$ is satisfied along the system trace.

Proposition V.1

Given a ptSTL formula $\Psi$ (9), control system (1),the state $x_{k}$, a partial trace

[TABLE]

the control $u_{k}$ generated by Alg. 2 guarantees that $\Psi$ is violated at time step $k$ when $b_{i}\geq 2$ for each cause formula $\Phi_{i}$ and $|\mathbb{U}^{j}|\geq 2$ for each $j=0,\ldots,m-1$.

Proof:

Let $\textbf{U}_{k}=\mathbb{U}^{0}\setminus\{u_{k-1}^{0}\}\times\ldots\times\mathbb{U}^{m-1}\setminus\{u_{k-1}^{m-1}\}$ where $u_{k-1}=[u_{k-1}^{0},\ldots,u_{k-1}^{m-1}]$ is the control input of time step $k-1$. Since $|\mathbb{U}^{j}|\geq 2$ for each $j$, $\textbf{U}_{k}\neq\emptyset$. Consider $u_{k}\in\textbf{U}_{k}$ and a shifted cause formula $\Phi^{s}_{i}=G^{-}_{[0,b_{i}-1]}u^{j}=c_{i}\wedge\phi_{i}$. Since $b_{i}-1\geq 1$ and $u_{k}^{j}\neq u_{k-1}^{j}$, it holds that $((\mathbf{x},(x_{k},u_{k})),k)\not\models\Phi^{s}_{i}$. Note that $({(}\mathbf{x},(x_{k},u_{k}){),k})\not\models\Phi^{s}_{i}$ implies that $({(}\mathbf{x},(x_{k},u_{k}),(x_{k+1},u_{k+1})),k+1)\not\models\Phi_{i}$ for any $x_{k+1}\in\mathbb{X}$ and $u_{k+1}\in\mathbb{U}$. Observe that $\textbf{U}_{k}\subset\mathbb{U}$, thus $u_{k}$ can be generated by Alg. 2. Consequently, formula $\Psi$ is violated at each time step since each cause formula $\Phi_{i}$ is violated. ∎

Example V.1

We simulated the traffic system from Ex. II.1 in closed loop with the controller generated from formula $\Psi^{*}_{0.01}(v)$ (see Ex. IV.1)as in Alg. 2. The congestion percentage is dropped to $7.5\%$ from $46\%$ (in average).

The developed framework identifies the controllable causes of the unwanted events from the labeled dataset, and reduces the occurrences of the labeled events via controller synthesis as illustrated in Ex. IV.1 and Ex. V.1. An insufficient reduction on the unwanted events can be analyzed in three aspects when there is a high correlation between the unwanted events and the control inputs. 1) The complex causes can not be explained with limited number of operators ($\overline{oc}$). 2) The number of different causes yielding the labelled events is higher than the bound used in the formula synthesis ($\overline{p}$). 3) Avoiding formula $\Psi$ results in formation of new causes. For the first and the second one, the parameters of the formula synthesis algorithm can be increased. However, due to the time complexity of Alg. 1, increasing both of them might not be practical. The second and third issues can be solved via iterative applications of the formula generation and controller synthesis steps, which is presented in the next section.

V-A Controller Refinement

The iterative algorithm to reduce the number of unwanted events via cause identification and controller synthesis is summarized in Alg. 3. In addition to the parameters of Alg. 1, Alg. 3 takes as input the system $S$ and a function over the state and control variables of the system to mark the unwanted events. Initially, the combined cause $\Psi$ is set to $false$ and a labeled dataset is generated by simulating the system in closed loop with a random control generator. Then, iteratively, a formula $\Phi$ is generated from the dataset $\mathcal{D}$ with Alg. 1, it is added to the previously identified causes $\Psi$ via disjunction, a controller $\mathcal{U}$ is synthesized from the new cause formula $\Psi$ with Alg. 2, and finally a new dataset is constructed by simulating the system in closed loop with the new controller $\mathcal{U}$. This iterative process continues until the rate of the unwanted events drops below a predefined limit $B$.

Example V.2

We run the iterative synthesis algorithm (Alg. 3) for the traffic system from Ex. II.1 with different values for $\underline{oc}$, $\overline{oc}$, $\overline{p}$, $\underline{val}$. In each experiment, the parameter domain given in Ex. IV.1 is used. In all of the experiments, we set $B$ to [math] so that the refinement loop terminates only when the congestion is avoided. The total number of labeled data points, $\mathcal{V}_{i}$, in dataset $\mathcal{D}$ for each iteration $i$ and the total computation time are reported in Table I. The parameters used in each experiment are shown in Table II. Each experiment is started with the same dataset that was used in the running example, e.g., $\mathcal{V}_{0}$ is the violation count in this dataset. In each case the proposed iterative controller synthesis algorithm is able to generate a control strategy that avoids the unwanted events.

*In the first two experiments, no limit is set for the number of operators and the number of causes as in Ex. IV.1. In the first experiment, due to the low valuation limit, detailed cause formulas with high operator counts are generated by Alg. 1. While a controller that avoids the congestion is synthesized in fewer iterations, due to the complexity of parameter synthesis, the computation takes longer. In the second experiment, the valuation limit is increased to $0.1$. As explained in Ex. IV.1, cause formulas with fewer number of operators are generated. The total computation time is reduced while the number of iterations is increased. The parameters used in the last experiment enforce formula synthesis algorithm to generate a single cause with operator count [math], the general formula $\phi_{i}$ is in the form of (12). Note that $\underline{val}$ is ineffective in this case. The refinement algorithm is able to reduce the violation count to [math] in seven iterations. The parameter optimization is performed for at most $3$ parameters ($oc=0$), which results in short computation time. *

VI Case Study

VI-A Congested Traffic System

In this case study, we increase the exogenous flow limit of link [math] to $10$ of the traffic system defined in Ex. II.1. All other parameters are kept the same. Due to the increase in the inflow, the average congestion is reached to $79\%$. In this example, we used the abstraction based synthesis approach [16] to generate a control strategy to avoid congestion (defined in (4)). The synthesis problem is infeasible even when the capacity of each link is partitioned into regions of length $1$ (i.e. the size of the abstraction is $40^{3}\times 20^{2}$).

We run Alg. 3 on this system with parameters $\overline{oc}=0$, $\underline{oc}=0$, $\overline{p}=1$, and $\underline{val}=0$. For each iteration, the total number of labeled data points $\mathcal{V}_{i}$, the formula $\Phi_{i}$ generated by Alg. 1 and its $tp$ and $fp$ count are shown in Table III.

The resulting formulas show that even though the valuation of the formula synthesized in Alg. 1 is high (see $tp$ and $fp$), the number of violations in the resulting system may not decrease ($\mathcal{V}_{i}$ in the next row). This is due to the formation of the new causes. For example, the controller that avoids $\Phi_{1}$ favors $u^{0}=0$, thus causes congestion on link $3$. $\Phi_{1}$ and $\Phi_{2}$ together can balance the control choice for the first signal $u^{0}$. The same situation occurs for the second signal $u^{1}$ with $\Phi_{3}$ and $\Phi_{4}$. In this example, the controller generated from $\Psi=\Phi_{1}\vee\ldots\vee\Phi_{4}$ reduces the total congestion count to $2$ ($0.05\%$), and subsequent iterations do not reduce it further.

This example shows that the proposed iterative controller synthesis algorithm is able to reduce the number of unwanted events significantly when a control strategy guaranteeing the avoidance of these events does not exist.

VI-B Region Avoidance

In this case study, we consider a basic region/obstacle avoidance scenario for a robot that can move in a planar arena. The arena is represented as a two-dimensional grid of size $M_{0}\times M_{1}$. The state of the robot is its location, i.e., $x_{k}\in[0,\ldots,M_{0}-1]\times[0,\ldots,M_{1}-1]$, and the control set is $\mathbb{U}=\{N,E,S,W\}$. The robot can move according to the control input, but it can not leave the arena:

[TABLE]

The dangerous regions are shown in gray in Fig. 3(a). The robot initially does not know the arena. It senses the dangerous region when it is in it (label 1). We run Alg. 3 on system (14) with parameters $\overline{oc}=1$, $\underline{oc}=1$, $\overline{p}=1$, ${\underline{val}}=0$, and the datasets include $20$ traces with length $100$. The algorithm terminates after 6 iterations. The total number of labeled data points, the formula generated by Alg. 1 and its $tp$ count are shown in Table IV.

For a trace of the robot controlled by Alg. 2 with formula $\Psi=\Phi_{1}\vee\Phi_{2}\vee\Phi_{3}\vee\Phi_{4}$, the number of visits of a cell over the length of the trace is shown in Fig. 3(b) with a heatmap. Due to the randomness in the controller (Alg. 2), the robot can explore the arena without going through the dangerous regions. This simple example shows that the proposed approach can be used to explore an arena and to learn a controller that avoids the bad areas.

VII Conclusions and Future Works

We presented a framework for synthesis of feedback controllers to avoid unwanted events. The main steps are the identification of the controllable causes as a ptSTL formula, and the synthesis of feedback controllers to avoid the satisfaction of the cause formula. The proposed method can be applied to any discrete-time dynamical system with a finite control set. We showed on two examples that the system reduces the number of the unwanted events. The reduction rate depends on the causality relation between the control inputs and the unwanted events, and the parameters of the formula synthesis algorithm. A stronger causality relation together with the suitable parameters yields a higher reduction rate. Future research will address verification of the resulting controlled system to guarantee correctness, and identifying other controllable cause structures.