# Pointwise-in-Time Explanation for Linear Temporal Logic Rules ††thanks: This
research was funded in part by a National Defense Science and Engineering
Graduate Fellowship.

Noel Brindise and Cédric Langbort N. Brindise and C. Langbort are with the
Department of Aerospace Engineering, Grainger College of Engineering,
University of Illinois Urbana-Champaign, 104 S Wright St, Urbana, IL 61801,
USA<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

The new field of Explainable Planning (XAIP) has produced a variety of
approaches to explain and describe the behavior of autonomous agents to human
observers. Many summarize agent behavior in terms of the constraints, or
“rules,” which the agent adheres to during its trajectories. In this work, we
narrow the focus from summary to specific moments in individual trajectories,
offering a “pointwise-in-time” view. Our novel framework, which we define on
Linear Temporal Logic (LTL) rules, assigns an intuitive status to any rule in
order to describe the trajectory progress at individual time steps; here, a
rule is classified as active, satisfied, inactive, or violated. Given a
trajectory, a user may query for status of specific LTL rules at individual
trajectory time steps.

In this paper, we present this novel framework, named Rule Status Assessment
(RSA), and provide an example of its implementation. We find that pointwise-
in-time status assessment is useful as a post-hoc diagnostic, enabling a user
to systematically track the agent’s behavior with respect to a set of rules.

##  I Introduction

Planning and performing on their own, autonomous agents are useful in a wide
variety of roles, from self-driving vehicles [1] and task-executing robots [2]
to decision-making software [3]. However, it can be challenging to understand
or characterize agent behavior. The emerging field of Explainable Planning
(XAIP), a subfield of Explainable AI (xAI), takes on this explanatory
challenge with mixed results [4, 5, 6]. Some approaches allow the user to
query hypotheticals (“What would [agent] do in [state]?”, etc.) [7]; others
generate domain alterations that would cause hypothetical route changes (“What
needs to change to make [plan] optimal instead?”) [8] or use visualizations to
help reconcile a human’s mental model with that of the agent (“Where does the
agent’s behavior differ from my expectations?”) [9].

A large body of work explains agent plans as a whole using rule inference, an
approach originating in formal methods and software model checking [10]. Here,
an agent is observed, and the explainer infers which “rules” or constraints
the agent tends to follow (“What does the agent usually, or never, do?”).
Rules may be expressed in signal temporal logic (STL) [11, 12] or, more
commonly, linear temporal logic (LTL) [13, 14]. Approaches have learned
contrasts between acceptable and unsatisfactory plans [15], inferred rules
from purely positive behavior [16] and noisy data [17]. In general, rule
inference provides global summaries of agent behavior by providing a set of
satisfied (or violated) rules.

For live assessment, the related field of LTL monitoring predicts the future
satisfaction of rules at a current point in a(n unfinished) trajectory [18];
similar methods have been used for STL rules in dynamic planning [19].

While global summaries produced by inference and monitoring are certainly
valuable, they do not address local behavior of the agent, which evokes other
questions (“Which rules is the agent following at time $t$? Which rules are
not relevant at $t$?”). We may ask, for example, whether a rule is still in
progress at $t$ or already completed. Moreover, implication-type
($x\rightarrow y$) rules require a consequence $y$ only after a triggering
condition $x$ occurs, making the rule trivially satisfied when $x$ does not
occur; we may want to know which rules are thus “triggered” at a given $t$.

In our work, we pursue an aspect of local, time step dependent diagnostics
which, to the best of the authors’ knowledge, remains unaddressed. We consider
trajectories of an arbitrary, black-box agent and define a notion of rule
status, which we use to assess when and how a system trajectory progresses
through each behavior (LTL rule) of interest. This is accomplished by defining
notions of active, inactive, satisfied, and violated rule status, such that
rules are uniquely assigned a status dependent on trajectory and time step. We
then introduce an algorithm to perform rule status assessment. We categorize
this novel time step-dependent analysis method as“pointwise-in-time”
explanation and demonstrate its potential applications on illustrative
examples.

##  II Background

We consider discrete-time, discrete-state systems, a common setting for
modeling autonomous agents. Such systems include Markov decision processes
(MDPs) and Kripke structures; we define the latter below. We then describe
Linear Temporal Logic (LTL), a temporal-logical language which can express
constraints (“rules”) on such systems.

Kripke Structures. We define a Kripke structure over a set of atomic
propositions, named labels, as in Definition 1.

######  Definition 1 (Kripke structure)

Given a set $P$ of labels, the Kripke structure $K$ over $P$ is a tuple

$K=(S,I,\mathcal{T},\mathcal{L}).$ (1)

where $S$ is a finite set of states, $I\subseteq S$ is the set of initial
states, and $\mathcal{T}\subseteq S\times S$ is a transition relation with
$(\sigma,\sigma^{\prime})\in\mathcal{T},$ $\sigma^{\prime}\in S$ for all
$\sigma\in S$. Finally, $\mathcal{L}:S\rightarrow 2^{P}$ is a labeling
function assigning a set $L\subseteq P$ to each state in $S$.

For clarity, we establish separate notation for a state variable $s_{t}$ and a
constant state $\sigma\in S$, i.e., the expression $s_{2}=\sigma_{1}$
signifies the state at time $t=2$ is $\sigma_{1}$. Each unique constant label
is denoted $\alpha\in P$.

We consider a finite discrete time interval $\\{t\ |\ T_{0}\leq t\leq
T_{f}\\}$, where $T_{0},t,T_{f}\in\mathbb{N}$. A run
$\kappa=s_{T_{0}},...,s_{T_{f}}$ of the system must satisfy $s_{T_{0}}\in I$
and $(s_{t},s_{t+1})\in R$ for all $t\in\\{T_{0},...,T_{f}\\}$. Importantly,
each $\kappa$ induces a trace $\rho$:

######  Definition 2 (Trace)

For any state $s_{t}\in S$, $T_{0}\leq t\leq T_{f}$, let
$\mathcal{L}(s_{t})=L_{t}$, where $L_{t}$ is a set of labels. A trace is the
sequence $\rho=(L_{T_{0}},...,L_{T_{f}})$ produced by system trajectory
$(s_{T_{0}},...,s_{T_{f}})$ from time step $T_{0}$ to $T_{f}$.

A trace suffix $\rho^{t_{0}...}=L_{t_{0}},...,L_{T_{f}}$ is the part of the
trace beginning at $t_{0}\geq T_{0}$ and ending at $T_{f}$.

Linear Temporal Logic. Linear temporal logic (LTL) is a human-intuitive way to
express time- and order-dependent specifications [20], [21]. An LTL formula
$\varphi$ may be evaluated on a trace $\rho$ provided $\varphi$ is defined on
labels in $P$.

######  Definition 3 (Linear Temporal Logic Formula)

For the set of LTL formulas over a finite set $P$ of labels,

  * •

if $\alpha\in\mathcal{T}$, then $\alpha$ is itself an LTL formula.

  * •

if $\varphi_{1}$ and $\varphi_{2}$ are LTL formulas, then $\neg\varphi_{1}$,
$\varphi_{1}\vee\varphi_{2}$, $\mathbf{X}\varphi_{1}$, and
$\varphi_{1}\mathbf{U}\varphi_{2}$ are LTL formulas.

######  Definition 4 (Formula Evaluation on Traces)

LTL formula $\varphi$ is true on trace $\rho$, denoted $\rho\models\varphi$,
in the following cases:

  * •

$\rho\models\alpha$ where $\alpha\in P\quad$ iff $\quad\alpha\in L_{0}$

  * •

$\rho\models\neg\varphi\quad$ iff $\quad\rho\not\models\varphi$

  * •

$\rho\models\varphi_{1}\vee\varphi_{2}\quad$ iff $\quad\rho\models\varphi_{1}$
or $\rho\models\varphi_{2}$

and for the temporal operators Next $\mathbf{X}$ and Until $\mathbf{U}$,

  * •

$\rho\models\mathbf{X}\varphi\quad$ iff $\quad\rho^{1...}\models\varphi$

  * •

$\rho\models\varphi_{1}\mathbf{U}\varphi_{2}\quad$ iff $\quad\exists i\geq 0$
s.t. $\rho^{i...}\models\varphi_{2}$ and
$\rho^{k...}\models\varphi_{1}$ for all $0\leq k<i$

Table I intuitively describes LTL operators. Note that all of the operators
listed can be constructed from $\mathbf{X,U},\vee,$ and $\neg$ [22]. Lastly,
we define formula arguments, so that we may decompose formulas into their
constituent parts.

######  Definition 5 (Arguments of an LTL formula)

Consider the LTL order of operations: (1) grouping symbols; (2)
$\neg,\mathbf{X}$, and other unary operators; (3) $\mathbf{U}$ and other
temporal binary operators; and (4) $\vee,\wedge,\rightarrow$. For LTL formula
$\varphi$, all $\varphi_{j}$ bound by the weakest operator are the arguments
of $\varphi$.

For example, $\varphi=\mathbf{G}\alpha_{1}\vee\alpha_{2}$ has arguments
$\varphi_{1}=\mathbf{G}\alpha_{1}$, $\varphi_{2}=\alpha_{2}$. For labels, the
argument is the formula itself ($\alpha$).

Operator |  Meaning
---|---
G$\varphi_{1}$ |  Global: $\varphi_{1}$ is always true.
F$\varphi_{1}$ |  Eventual: $\varphi_{1}$ eventually occurs.
X$\varphi_{1}$ |  Next: $\varphi_{1}$ must occur at the next time step.
$\varphi_{1}$U$\varphi_{2}$ |  Until: $\varphi_{1}$ remains true until $\varphi_{2}$ occurs (and $\varphi_{2}$ must occur)
$\varphi_{1}$W$\varphi_{2}$ |  Weak until: $\varphi_{1}$ must remain true (1) always, or (2) until $\varphi_{2}$ becomes true.
$\varphi_{1}$R$\varphi_{2}$ |  Release: $\varphi_{1}$ must remain true (1) always, or (2) until (and including) the time step when $\varphi_{2}$ becomes true.
$\varphi_{1}$M$\varphi_{2}$ |  Strong release: True only if Condition (2) for Release is met.
$\varphi_{1}\wedge\varphi_{2}$ |  Conjunction: both $\varphi_{1}$ and $\varphi_{2}$ must be true
$\varphi_{1}\vee\varphi_{2}$ |  Disjunction: $\varphi_{1}$ or $\varphi_{2}$ or both must be true
$\varphi_{1}\rightarrow\varphi_{2}$ |  Implication: if $\varphi_{1}$ is true, $\varphi_{2}$ must also be true
TABLE I:  Selected LTL operators.

##  III Problem Statement

We consider a scenario in which an agent with unknown policy (a “black box”
agent) is observed by a human. We suppose the human wishes to characterize the
agent’s behavior in terms of a set of rules; these rules may represent tasks
or safety constraints, for example. A priori, an agent trajectory may or may
not follow any of the rules.

We suppose the human would like to know (1) which rules a trajectory follows,
as well as (2) when and how the trajectory progresses through each rule. For
example, (2) is relevant when a rule has subtasks (“do this, then that”) or
multiple fulfillment conditions (“do this or that”). The second question
requires diagnostics which check for specific conditions at each time step in
the trace; here, rule inference, which examines entire traces at once, is
insufficient.

Formal Problem Setting. We consider agents whose dynamics are expressible as a
Kripke structure, as well as a set of LTL rules over $P$ which describe
behaviors of interest. Given an observed trace $\rho$, our goal is to assess
the progress of rules at any time step; we propose the assignment of a status
to each rule and its arguments at query points $t^{*}\in\\{T_{0},...,T_{f}\\}$
for all trace suffixes $\rho^{t^{*}_{0}...}$ where $t^{*}_{0}\leq t^{*}$.

Moving towards a notion of rule status, we begin with two observations.
Firstly, consider a trace $\rho$ and rule $\varphi$. Suppose some $t_{0}$
exists such that $\varphi$ is true on $\rho^{t_{0}...}$ no matter which labels
are contained in any $L_{t\geq t_{0}}$. In this case, the trace beyond $t_{0}$
appears to be arbitrary with respect to $\varphi$:

######  Definition 6 (Arbitrariness of suffix)

For LTL formula $\varphi$, its argument(s) $\varphi_{j}$, trace
$\rho^{T_{0}...}$, and associated suffix $\rho^{t_{0}...}$ where $T_{0}\leq
t_{0}\leq T_{f}$, we say that $\rho^{t...}$ is arbitrary with respect to
$\varphi$ if $\rho^{t_{0}...}\models\varphi$ regardless of the truth of
$\rho^{t...}\models\varphi_{j}$ for all $t$ where $t_{0}\leq t\leq T_{f}$.

Secondly, we consider implication rules
$\varphi=\varphi_{1}\rightarrow\varphi_{2}$. When $\varphi$ is true on $\rho$,
there are two very distinct possibilities: either $\varphi_{1}$ has occurred
in $\rho$, in which case $\varphi_{2}$ must be made true; or $\varphi_{1}$ did
not occur, in which case $\varphi_{2}$ plays no role. We call such a
$\varphi_{1}$ a precondition:

######  Definition 7 (Precondition)

The precondition of an LTL formula $\varphi$ is defined as

  1. 1.

$\varphi_{1}$ if $\varphi$ has the form $\varphi_{1}\rightarrow\varphi_{2}$

  2. 2.

$\top$ otherwise

Motivated by these observations, we characterize the roles of rules at time
steps by defining a novel LTL rule status.

######  Definition 8 (Status of LTL rule)

For LTL formula $\varphi$, trace $\rho^{T_{0}...}$ and times
$t_{0},t\in\\{T_{0},...,T_{f}\\}$, $t_{0}\leq t$:

  * •

$\varphi$ is active (a) at $t$ iff (1) $\rho^{t_{0}...}\models\varphi$, (2)
$\rho^{t_{0}...}\models\psi$ for precondition $\psi$ of $\varphi$, and (3)
$\rho^{t...}$ is not arbitrary.

  * •

$\varphi$ is satisfied (s) at $t$ iff (1) $\varphi$ active at $t$ and (2)
$t=T_{f}$ or $\varphi$ not active at $t+1$.

  * •

$\varphi$ is inactive (i) at $t$ iff (1) $\rho^{t_{0}...}\models\varphi$ and
(2) $\varphi$ is neither active nor satisfied at $t$.

  * •

$\varphi$ is violated (v) at $t$ iff $\rho^{t_{0}...}\not\models\varphi$.

We briefly illustrate the status notions in simple examples, expressing rules
in words for clarity.

######  Example 1 (Status)

Consider trace $\rho=(L_{T_{0}},...,L_{T_{f}})$ produced by a sample
collection robot. Suppose we select a suffix $\rho^{t_{0}...}$ to analyze,
where $T_{0}\leq t_{0}\leq T_{f}$. Then we have the following status examples:

Active: Let $\varphi=\textup{``Headlight always on at night''}$ and suppose
${\textup{``night'', ``light on''}\in L_{t}}$ for all $t\geq t_{0}$. Then
$\varphi$ is active at all $t\geq t_{0}$.

Satisfied: Let ${\varphi=\textup{``Eventually deposit sample''}}$. Suppose
${\textup{``sample deposited''}\in L_{t}}$, ${\textup{``sample
deposited''}\not\in L_{t^{\prime}}}$ for all $t^{\prime}<t$. Then $\varphi$ is
satisfied at $t$.

Inactive (done): Let ${\varphi=\textup{``Eventually deposit sample''}}$ and
suppose ${\textup{``sample deposited''}\in L_{t^{\prime}}}$ for some
$t^{\prime}<t$. Then $\varphi$ is inactive at $t$, since $\varphi$ was already
satisfied.

Inactive (not triggered): Let ${\varphi=\textup{``If raining, stop''}}$ and
suppose ${\textup{``rain''}\not\in L_{t}}$. Then $\varphi$ is inactive at $t$,
since precondition “rain” is not occurring and stopping is not necessary.

Violated: Let ${\varphi=\textup{``Battery always above 10\%''}}$ and suppose
${\textup{``battery empty''}\in L_{t}}$. Then $\varphi$ is violated at all
$t$.

Finally, we can express the set of all times in $\\{t_{0},...,T_{f}\\}$ for
which $\varphi$ has status $q$ on $\rho^{t_{0}...}$ as a timeset

$\tau^{q}=\\{t\in\\{t_{0},...,T_{f}\\}\ |\ t\text{ has status }q\\}.$ (2)

If we recover such time sets for a rule $\varphi$, it is possible to check its
status at any moment in an agent trajectory; moreover, time sets for each
argument of $\varphi$ may help to track progress “through” the rule, such as
completion of subtasks.

Formal Problem Statement. For an LTL formula $\varphi$ and a plan trace
$\rho^{T_{0}...T_{f}}$, an explainer must be able to provide:

  * •

Status of $\varphi$ at $t$ on $\rho^{t_{0}...}$ for all
${\\{t_{0},t\in\\{T_{0},...,T_{f}\\}\ |\ t_{0}\leq t\\}}$

  * •

Status timesets $\tau^{a},\tau^{s},\tau^{i},\tau^{v}$ of $\varphi$ for each
${t_{0}\in\\{T_{0},...,T_{f}\\}}$

  * •

Both of the above for any argument $\varphi_{j}$ of $\varphi$.

In this paper, we propose an algorithm that returns this information on demand
and begin to explore its applications.

##  IV Rule Status Assessment

We wish to evaluate rule status for all arguments of a formula. To accomplish
this in a structured manner, formulas are first decomposed into a tree
structure as follows.

Tree Structure. LTL formulas $\varphi$ are commonly structured as trees with
$\varphi$ as the base node [13] [15]. Here, the children of a parent node are
the arguments of the parent formula, until each branch terminates in a leaf
containing only a label. We additionally store the type of the weakest
operator in $\varphi_{j}$ for each node, denoted $\theta_{j}$; in the case
where $\varphi_{j}=\alpha$, we assign type $\theta_{j}=AP$ (“atomic
proposition”) to denote that the node contains a label. An example is given in
Figure 1.

Figure 1: Example formula tree for
$\varphi=\alpha_{1}\mathbf{U}(\mathbf{G}\alpha_{2})$.

Modules and Algorithm. Each node of a tree contains a formula consisting of
one or more arguments bound by an operator. The operator type determines how
the argument truth values map to a status; for instance, consider a trace
$\rho$ where a formula $\varphi_{j}$ is true at a single time step
$t^{\prime}$. Here, a node with $\varphi=\mathbf{G}\varphi_{j}$ (type
$\mathbf{G}$) is violated at all $t$; a node $\varphi=\mathbf{F}\varphi_{j}$
(type $\mathbf{F}$) is active until satisfaction at $t^{\prime}$. Thus, we
establish separate modules for every type, each with inputs $\varphi$,
$t_{0}$, $\rho^{t_{0}...}$ and outputs $\tau^{a},\tau^{s},\tau^{i},\tau^{v}$
to satisfy Definition 8.

Our proposed algorithm works node-by-node, beginning with all leaf nodes and
working up each branch until $\tau$ has been calculated for the entire tree
(child nodes are always instantiated before their parents). The algorithm then
accepts queries and returns status at the desired time steps:

Rule Status Assessment Algorithm

  1. 1.

Construct tree for LTL rule $\varphi$.

  2. 2.

Find $\tau^{a},\tau^{s},\tau^{i},\tau^{v}$ of each node for all
$\rho^{t_{0}...}$, ${t_{0}\in\\{T_{0},...,T_{f}\\}}$:

    1. (a)

For each distinct label $\alpha$ appearing in any leaf, pass
$\rho^{t_{0}...}$, ${\varphi=\alpha}$ into the $AP$ module for all
$t_{0}\in\\{T_{0},...,T_{f}\\}$. Store outputs $\tau$ for all leaves
containing this $\alpha$.

    2. (b)

For leaf $\varphi_{...x.y}$, check parent $\varphi_{...x}$. If $\tau$ is
already stored for all children of $\varphi_{...x}$, proceed to (c);
otherwise, move to next leaf and repeat (b).

    3. (c)

Identify $\theta$ of $\varphi_{...x}$. Pass $\varphi_{...x}$,
$\rho^{t_{0}...}$ into $\theta$ module for all
$t_{0}\in\\{T_{0},...,T_{f}\\}$; store output $\tau$ for $\varphi_{...x}$.

    4. (d)

Check parent of $\varphi_{...x}$. If it exists and all its children are
instantiated, repeat step c) for this parent. Otherwise, move to next leaf and
begin again from step (b).

  3. 3.

Answer status queries:

    1. (a)

Accept $t^{*},t^{*}_{0}$ and a node (e.g., $\varphi_{x.y}$) as input.

    2. (b)

Return status $q$ if $t^{*}\in\tau^{q}$ for $\rho^{t_{0}^{*}...}$.

The temporal and logical operator modules are defined in Tables III and II,
respectively. For proof that the modules satisfy Definition 8, see the
Appendix.

Not $(neg)$ |  LTL: $\varphi=\neg\varphi_{1}$
---|---
Initialize: |  Load all $\tau_{1}^{q}$ of child node $\varphi_{1}$ at $t_{0}$.
If $\tau^{v}_{1}=\emptyset:$ |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
Else: |  Set $\tau^{a},\tau^{s}=\\{t_{0}\\},\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$. Set $\tau^{v}=\emptyset$.
Or $(or)$ |  LTL: $\varphi=\varphi_{1}\vee\varphi_{2}$
Initialize: |  Load all $\tau_{1}^{q},\tau_{2}^{q}$ of child nodes $\varphi_{1},\varphi_{2}$ at $t_{0}$.
∗If $\tau^{v}_{1},\tau^{v}_{2}\neq\emptyset$: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
Else: |  Set $\tau^{a},\tau^{s}=\\{t_{0}\\},\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$. Set $\tau^{v}=\emptyset$.
And $(and)$ |  LTL: $\varphi=\varphi_{1}\wedge\varphi_{2}$
|  Same as $\vee$ with ∗ replaced by:
|  If $\tau^{v}_{1}$ or $\tau^{v}_{2}\neq\emptyset$: (…)
Implication $(\rightarrow)$ |  LTL: $\varphi=\varphi_{1}\rightarrow\varphi_{2}$
Initialize: |  Load all $\tau_{1}^{q}$ of child node $\varphi_{1}$ at $t_{0}$.
If $\tau^{v}_{1}\neq\emptyset$: |  Set $\tau^{a},\tau^{s},\tau^{v}=\emptyset$; $\tau^{i}=\\{t_{0},...,T\\}\setminus\tau^{a}.$ Exit the current module.
Else: |  Load all $\tau_{2}^{q}$ of child node $\varphi_{2}$ at $t_{0}$.
If $\tau^{v}_{2}\neq\emptyset$: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
Else: |  Set $\tau^{a},\tau^{s}=\\{t_{0}\\};\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$. Set $\tau^{v}=\emptyset$.
TABLE II:  Logical operator module definitions. Atomic $(AP)$ |  LTL: $\varphi=\alpha$
---|---
If $\alpha\in L_{t_{0}}$: |  Set $\tau^{a}$, $\tau^{s}=\\{t_{0}\\}$, $\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$. Set $\tau^{v}=\emptyset$.
Else: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
Next $(X)$ |  LTL: $\varphi=\mathbf{X}\varphi_{1}$
Initialize: |  Load all $\tau_{1}^{q}$ of child node $\varphi_{1}$ at $t_{0}^{1}=t_{1}$.
If $\tau_{1}^{v}=\emptyset$: |  Set $\tau^{a}=\\{t_{0},t_{1}\\}$; $\tau^{s}=\\{t_{1}\\}$, $\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$. Set $\tau^{v}=\emptyset$.
Else: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
Eventual $(F)$ |  LTL: $\varphi=\mathbf{F}\varphi_{1}$
For $t_{0}^{1}=t_{0}...T_{f}$: |  Load all $\tau_{1}^{q}$ of child node $\varphi_{1}$ at $t_{0}^{1}$. Continue until $t_{0}^{1}=T_{f}$ or $\tau^{v}_{1}=\emptyset$.
If $\tau_{1}^{v}=\emptyset$: |  Set $\tau^{a}=\\{t_{0},...,t_{0}^{1}\\}$; $\tau^{s}=\\{t_{0}^{1}\\}$; $\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$. Set $\tau^{v}=\emptyset$. Exit the current module.
Else: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
Global $(G)$ |  LTL: $\varphi=\mathbf{G}\varphi_{1}$
For $t_{0}^{1}=t_{0}...T_{f}$: |  Load all $\tau^{q}_{1}$ of child node $\varphi_{1}$ at $t_{0}^{1}$.
|  Continue until $t_{0}^{1}=T_{f}$ or $\tau_{1}^{v}\neq\emptyset$.
If $\tau_{1}^{v}\neq\emptyset$: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$. Exit the current module.
Else: |  Set $\tau^{a}=\\{t_{0},...,T_{f}\\};\tau^{s}=\\{T_{f}\\};\tau^{i},\tau^{v}=\emptyset$.
Until $(U)$ |  LTL: $\varphi=\varphi_{1}\mathbf{U}\varphi_{2}$
For $t_{0}^{\prime}=t_{0}...T_{f}$: |  Load all $\tau_{1}^{q},\tau_{2}^{q}$ of child nodes $\varphi_{1}$ and $\varphi_{2}$ at $t^{\prime}_{0}$. Continue until $\tau^{v}_{1}\neq\emptyset$ or $\tau_{2}^{v}=\emptyset$ or $t_{0}^{2}=T_{f}$.
†If $\tau_{2}^{v}=\emptyset$: |  Set $\tau^{a}=\\{t_{0},...,t^{\prime}_{0}\\};\tau^{s}=\\{t^{\prime}_{0}\\};\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$. Set $\tau^{v}=\emptyset$.
Else if $\tau^{v}_{1}\neq\emptyset$: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
∗Else: |  Set $\tau^{v}=\\{t_{0},...,T_{f}\\}$; $\tau^{a},\tau^{s},\tau^{i}=\emptyset$.
W. until $(W)$ |  LTL: $\varphi=\varphi_{1}\mathbf{W}\varphi_{2}$
|  Same as $\mathbf{U}$ with ∗ replaced by:
|  Else: Set
$\tau^{a}=\\{t_{0},...,T_{f}\\};\tau^{s}=\\{T_{f}\\},\tau^{i}=\emptyset$. Set
$\tau^{v}=\emptyset$.
S. release $(M)$ |  LTL: $\varphi=\varphi_{1}\mathbf{M}\varphi_{2}$
|  Same as $\mathbf{U}$ with † replaced by:
|  If $\tau_{2}^{v}=\emptyset$ and $\tau_{1}^{v}=\emptyset$: (…)
Release $(R)$ |  LTL: $\varphi=\varphi_{1}\mathbf{R}\varphi_{2}$
|  Same as $\mathbf{U}$ plus changes in $\mathbf{W}$ & $\mathbf{M}$.
TABLE III:  Temporal operator module definitions.

Algorithm Complexity. An upper bound on complexity may be established from the
modules. For each node $\varphi_{...x}$ in a tree, the corresponding module is
called once; this module produces $\tau$ for every $t_{0}$ in
$\\{T_{0},...,T_{f}\\}$, resulting in $\leq|\rho|$ iterations. At each
$t_{0}$, the module performs up to $T_{f}-t_{0}\leq|\rho|$ evaluations per
argument $\varphi_{...x.y}$. Thus, any node with a binary operator (two
arguments) performs $n\leq 2|\rho|^{2}$ computations.

Now, for a tree with depth L, with base node at level $l=0$ and maximum 2
children per node, the number of nodes at level $L$, $n_{L}$, satisfies
$n_{L}\leq 2^{L}$. Maximum complexity is thus order $2^{l}(2|\rho|^{2})$, or

$\mathcal{O}(2^{l+1}|\rho|^{2}).$ (3)

Logical operators with more than 2 arguments (e.g.
$\varphi_{1}\vee\varphi_{2}\vee\varphi_{3}$) can be rewritten as a tree of
their groupings (e.g., $\varphi_{1}\vee(\varphi_{2}\vee\varphi_{3})$), with
$L$ adjusted appropriately.

##  V Application

In this section, we apply status assessment on hypothetical runs of two agents
using the rule status assessment algorithm located at
https://github.com/n-brindise/live_expl. We also suggest a basic heuristic to
identify times $t^{*},t^{*}_{0}$ of potential interest in a trace.

Query Heuristics. Status assessment allows for a large number of queries
$(\mathcal{O}(2^{l+1}|\rho|^{2}))$; thus, identification of informative
queries from this large set is desirable. A first-order approach simply
monitors the $\tau$ values as the algorithm iterates over
$t_{0}\in\\{T_{0},...,T_{f}\\}$ and stores any $t_{0}$ where $\rho$ changes
status to active or violated from the preceding $t_{0}$. We denote the set of
all $t^{*}_{0}$ of interest by $\tau^{*}$.

Muddy Yard Example. The real world-inspired “muddy yard” scenario (Fig. 2)
features an “outdoor” area with two “muddy” sections and an outdoor “mat,” as
well as an “indoor” area with a “sink.” The two areas are separated by a
“wall” with a “door.” We formulate the domain as a Kripke structure with set
$S$ of states and set $P$ of labels:

$\displaystyle S=\\{\sigma_{1}$
$\displaystyle=\text{grass}\quad\sigma_{2}=\text{mud}\quad\sigma_{3}=\text{mat}\quad\sigma_{4}=\text{floor}$
$\displaystyle\quad\sigma_{5}$
$\displaystyle=\text{sink}\quad\sigma_{6}=\text{wall}\quad\sigma_{7}=\text{door}\\}$
$\displaystyle P=\\{\alpha_{1}$
$\displaystyle=\text{outside}\quad\alpha_{2}=\text{inside}\quad\alpha_{3}=\text{muddy}$
$\displaystyle\alpha_{4}$
$\displaystyle=\text{wiped}\quad\alpha_{5}=\text{washed}\quad\alpha_{6}=\text{impassable}\\}$

where $I=S$. The transition relation $\mathcal{T}$ exclusively allows the
agent to transition between adjacent states (e.g.,
$(\sigma_{1},\sigma_{2})\in\mathcal{T}$, but
$(\sigma_{1},\sigma_{5})\not\in\mathcal{T}$). Finally, the labeling function
$\mathcal{L}$ is

$\displaystyle\mathcal{L}(\sigma_{1})$
$\displaystyle=\\{\alpha_{1}\\}\quad\mathcal{L}(\sigma_{2})=\\{\alpha_{1},\alpha_{3}\\}\quad\mathcal{L}(\sigma_{3})=\\{\alpha_{1},\alpha_{4}\\}$
$\displaystyle\mathcal{L}(\sigma_{4})$
$\displaystyle=\\{\alpha_{2}\\}\quad\mathcal{L}(\sigma_{5})=\\{\alpha_{2},\alpha_{5}\\}\quad\mathcal{L}(\sigma_{6})=\\{\alpha_{6}\\}$
$\displaystyle\mathcal{L}(\sigma_{7})$
$\displaystyle=\\{\alpha_{1},\alpha_{2}\\}.$

We wish to analyze the agent run in Figure 3 subject to the following LTL
rules:

  1. 1.

$\varphi=\mathbf{F}\alpha_{1}$ “Eventually be outside”

  2. 2.

$\varphi=\mathbf{F}\alpha_{2}\rightarrow\mathbf{F}\alpha_{5}$ “If eventually
inside, eventually wash up”

  3. 3.

$\varphi=\mathbf{G}(\alpha_{3}\rightarrow(\neg\alpha_{2}\mathbf{W}\alpha_{4}))$
“Always, if muddy, do not go inside until wiping off”

  4. 4.

$\varphi=\mathbf{G}(\neg\alpha_{6})$ “Never enter an impassable place”

Figure 2: “Muddy yard” example domain, representing a yard (“outside”) with
two muddy patches and a mat, as well as a home interior (“inside”) with a
sink. Outside and Inside are separated by an untraversable wall. Figure 3:
Example path over the muddy yard domain. Each triangle represents the agent
position and direction of travel at a single time step.

From Figure 3, the system run is

$\kappa=\sigma_{1},\sigma_{1},\sigma_{2},\sigma_{1},\sigma_{1},\sigma_{3},\sigma_{1},\sigma_{1},\sigma_{7},\sigma_{4},\sigma_{4},\sigma_{5},$

which produces the trace

$\displaystyle\rho=$
$\displaystyle\\{\alpha_{1}\\}_{0},\\{\alpha_{1}\\}_{1},\\{\alpha_{1},\alpha_{3}\\}_{2},\\{\alpha_{1}\\}_{3},\\{\alpha_{1}\\}_{4},\\{\alpha_{1},\alpha_{4}\\}_{5},$
$\displaystyle\\{\alpha_{1}\\}_{6},\\{\alpha_{1}\\}_{7},\\{\alpha_{1},\alpha_{2}\\}_{8},\\{\alpha_{2}\\}_{9},\\{\alpha_{2}\\}_{10},\\{\alpha_{2},\alpha_{5}\\}_{11}.$

We now use status assessment to answer a series of questions. (When listing
timeset outputs, we omit any $\tau=\emptyset$ for clarity.)

Question: “Which rules are active at time $t^{*}$?”

For $t_{0}=T_{0}$, Rules 1-4 have (nonempty) timesets

  1. 1.

$\tau^{a}=\\{0\\},\tau^{s}=\\{0\\},\tau^{i}=\\{1,...,11\\}$

  2. 2.

$\tau^{a}=\\{0\\},\tau^{s}=\\{0\\},\tau^{i}=\\{1,...,11\\}$

  3. 3.

$\tau^{a}=\\{0,...,11\\},\tau^{s}=\\{11\\}$

  4. 4.

$\tau^{a}=\\{0,...,11\\},\tau^{s}=\\{11\\}$

At $t^{*}=3$, output is:

  * •

“Rules 1 and 2 are inactive”

  * •

“Rules 3 and 4 are active”

Intuitively, Rule 1 requires that the agent goes outside; this occurred
already at $t=0$, hence the inactivity by $t=3$. Rule 2 requires that, if the
agent will eventually go inside, it must also eventually wash up; both of
these conditions are already true on $\rho^{0...}$, and thus inactive for
$t^{*}>0$. This output is less intuitive, as it is not clear when the agent
will go inside or wash up. Finally, Rules 3 and 4 are global and must be
active at every time step. For 2, 3, and 4, elaboration is likely necessary,
prompting another question.

Question:  “Which arguments of rules are active at $t^{*}$?”

We first query Rule 3 at node $\varphi_{1}$. From heuristics,
${\tau^{*}=\\{2\\}}$, so we query $\varphi_{1}$ at ${t^{*},t^{*}_{0}=2}$,
which yields

  * •

$\tau^{a}_{1}=\\{2\\},\tau^{s}_{1}=\\{2\\},\tau^{i}_{1}=\\{0,1,3,...,11\\}$

  * •

“Rule 3.1 is active and satisfied (at $t^{*}=2$)”

This suggests that $\alpha_{3}\rightarrow(\neg\alpha_{2}\mathbf{W}\alpha_{4})$
is active on $\rho^{2...}$. Indeed, $\alpha_{3}$ (“muddy”) occurs at $t=2$,
triggering the implication. Querying $\varphi_{1.2}$ at
${t_{0}^{*}=2,t^{*}=5}$,

  * •

${\tau^{a}_{1.2}=\\{2,...,5\\}},{\tau^{s}_{1.2}=\\{5\\}},{\tau^{i}_{1.2}=\\{6,...,11\\}}$

  * •

“Rule 3.1.2 is active and satisfied (at $t^{*}=5$)”

Intuitively, though Rule 3 always holds, it only takes direct effect starting
at 2 (when the agent becomes muddy) and releases this effect at 5 (when the
agent wipes itself off).

Moving on to Rule 2, we perform queries for $\varphi_{1}=\mathbf{F}\alpha_{2}$
and $\varphi_{2}=\mathbf{F}\alpha_{5}$, and we find that both are active at
$t_{0}^{*}=0,t^{*}=3$. This makes sense, as the agent has neither gone inside
nor washed up by step $3$. At $t^{*}_{0},t^{*}=9$, $\varphi_{1}$ is now
inactive, since the agent has been inside for several steps, but $\varphi_{2}$
remains active, since it has yet to wash up. Finally, the agent washes up at
$11$, and $t^{*}=11$ gives $\varphi_{2}$ satisfied.

Autonomous Vehicle Example. Autonomous vehicles must comply to safety
guidelines, operational limits, and traffic laws, all of which are typically
expressible via temporal logics [23]. This example considers a hypothetical
setting in which an autonomous vehicle completes three distinct trips,
producing 3 traces over a large vocabulary ($|\mathcal{P}|=54$) and 90 time
steps. 21 LTL formulas describe various rules for safety, legal, and trip
requirements, such as “reduce speed in construction zones” and “activate
wipers if rain hazard present.” The traces and list of rules are available in
the Appendix.

Notably, the raw traces are visually difficult to parse. Single time steps
contain lengthy sets of labels, for example {leftmost, doors-closed, driver-
awake, clear-ahead, want-turn-left, clear-right, lane-to-right, gas-low,
intersection-ahead, green-ahead, reduced-speed, safe-stop} at $\rho_{1},t=36$.

Figure 4: Vehicle observed changing lanes and reducing speed at
$t=t^{\prime}$.

To motivate our example, suppose we observe the vehicle changes lanes to the
left and reduces speed at time $t^{\prime}$ in all three trips, as shown in
Figure 4. We wish to investigate what has occurred in each trace that may
explain this behavior.

As the traces are dense and the list of rules is long, we use status
assessment. We place queries at $t_{0}^{*},t^{*}=t^{\prime}$ for the first
argument of all 20 global rules $\mathbf{G}(...)$.

For $\rho_{1}$, we find (1) satisfied $\text{gas-
low}\rightarrow\neg(\text{goal})\mathbf{U}\text{gas-station}$, (2) satisfied
$\text{want-left-turn}\wedge\text{near-intersection}\wedge\text{clear-
left}\wedge\text{lane-to-left}\rightarrow\text{change-left}$ and (3) satisfied
$\text{want-turn}\wedge\text{near-intersection}\rightarrow\text{reduced-
speed}$. In words, the vehicle is heading to a gas station, approaching an
intersection, and planning to turn left.

For $\rho_{2}$, we find (1) satisfied $\text{merge-left}\wedge\text{clear-
left}\wedge\text{lane-to-left}\rightarrow\text{change-left}$ and (2) satisfied
$\text{construction-zone}\rightarrow\text{reduced-speed}\mathbf{U}\text{leave-
zone}$. Here, the vehicle has entered a construction zone and must merge.

Finally, for $\rho_{3}$, we have (1) satisfied $\text{short-follow-
distance}\rightarrow\text{reduced-speed}$. We place an additional query at
$t^{*}_{0},t^{*}=t^{\prime}-1$, which returns (2) satisfied $\text{short-
follow-distance}\wedge(\text{clear-left}\wedge\text{lane-to-
left})\rightarrow\mathbf{X}\text{change-left}$. Thus, the vehicle encountered
another vehicle which had dangerously reduced the following distance.

In all, status assessment processed a large set of rules and dense traces to
produce brief diagnostic statements which highlighted the specific
circumstances of each left-lane change, a promising aid to understand the
situation.

##  VI Discussion and Conclusion

In this work, we introduce rule status assessment (RSA), a method for
explanatory diagnostics for generic autonomous agent trajectories. RSA is
applicable to any system expressible via Kripke structure, providing a novel
framework to classify LTL rules of interest as active, satisfied, inactive, or
violated at individual trajectory time steps. This makes it possible to track
an agent’s progress through subtasks and more; it also provides insight into
the applicability of individual rules and reduces the total number of rules a
human must consider at once.

Multiple directions exist for future work. Firstly, the broader application of
RSA is a critical next step to demonstrate effectiveness for practical
purposes, particularly in common settings such as Machine Learning (ML).
Further application also calls for additional query heuristics; it is a
challenge to identify useful queries to achieve insightful RSA diagnostics.
Finally, the existing framework is entirely post-hoc; for certain families of
systems, such as Reinforcement Learning agents, use of agent internals (i.e.,
Q function) could incorporate agent intentionality.

##  VII Appendix

###  VII-A Algorithm Soundness by Module

Here we prove the soundness of module $\tau$-assignments subject to Definition
8. We first establish a set of basic principles that apply to all modules.
Consider the following statements:

$\displaystyle(\tau^{v}=\emptyset)$
$\displaystyle\iff(\rho^{t_{0}...}\models\varphi)$ (4)
$\displaystyle(\tau^{v}\neq\emptyset)$
$\displaystyle\Rightarrow(\tau^{a},\tau^{s},\tau^{i}=\emptyset;\tau^{v}=\\{t_{0},...,T_{f}\\})$
(5) $\displaystyle(\tau^{v}=\emptyset)$
$\displaystyle\Rightarrow\tau^{i}=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}$ (6)

We begin with 4. By Definition 8, $\varphi$ is violated at $t$ iff
$\rho^{t_{0}...}\not\models\varphi$. This means that when
$\rho^{t_{0}...}\not\models\varphi$, $\varphi$ is violated for all
$t\in\\{t_{0},...,T_{f}\\}$. Since

$t\text{ violated }\Rightarrow t\in\tau^{v}$ (7)

by 2, all $t\in\\{t_{0},...,T_{f}\\}$ must then appear in $\tau^{v}$. Thus,
for the nontrivial case, $\tau^{v}\neq\emptyset$. Meanwhile, if
$\rho^{t_{0}...}\models\varphi$, $\varphi$ must not be violated at any
$t\in\\{t_{0},...,T_{f}\\}$; thus $\tau_{v}=\emptyset$ in this case.
Therefore, 4 meets Definition 8.

Assume going forward that 4 holds. Statement 5 requires that $\tau^{v}$
nonempty implies $\tau^{a},\tau^{s},\tau^{i}$ empty. This is clearly true from
Definition 8, since a requirement for all active, inactive, and satisfied $t$
is that $\rho^{t_{0}...}\models\varphi$, which is never true when
$\tau^{v}\neq\emptyset$. Therefore, $\tau^{v}\neq\emptyset$ implies that no
$t$ exists at which $\varphi$ is active, inactive, or satisfied. Instead, all
$t$ must be such that $\varphi$ violated at $t$, implying that
$\tau^{v}=\\{t_{0},...,T_{f}\\}$.

Finally, 6 requires that $\tau^{v}=\emptyset$ implies $\tau^{i}$ contains all
times but those in $\tau^{a}$. By Definition 8, $t\in\tau^{i}$ iff
$\rho^{t_{0}...}\models\varphi$ and $t\not\in\tau^{a}\cup\tau^{s}$. If
$t\in\tau^{s}$, then $t\in\tau^{a}$, and thus $\tau^{s}\subseteq\tau^{a}$.
This yields $\tau^{a}\cup\tau^{s}=\tau^{a}$, meaning that
$\\{t_{0},...,T_{f}\\}\setminus(\tau^{a}\cup\tau^{s})=\\{t_{0},...,T_{f}\\}\setminus\tau^{a}=\tau^{i}$
when $\rho^{t_{0}...}\models\varphi$; $\tau^{i}$ is set to $\emptyset$
otherwise. Thus, such a formulation of $\tau^{i}$ will always satisfy
Definition 8 (given that $\tau^{a},\tau^{s}$ are sound).

We note that every module in Tables II and III makes assignments satisfying 5
and 6. This means we have shown the following:

| if $\mathbf{\tau^{v}=\emptyset}$ | if $\mathbf{\tau^{v}\neq\emptyset}$
---|---|---
$\tau^{v}$ | sound | sound
$\tau^{i}$ | sound | sound
$\tau^{a}$ | ? | sound
$\tau^{s}$ | ? | sound

We need only show three remaining conditions to prove soundness of the
modules:

  1. 1.

$\tau^{v}=^{?}\emptyset$ is soundly assessed

  2. 2.

$\tau^{a}$ is sound when $\tau^{v}=\emptyset$

  3. 3.

$\tau^{s}$ is sound when $\tau^{v}=\emptyset$

Here, item (1) true means that the conditions $\tau^{v}=^{?}\emptyset$ soundly
correspond to $\rho^{t_{0}...}\models^{?}\varphi$ as prescribed by 4. Item (2)
and (3) mean that $\tau^{a},\tau^{s}$ are properly assigned when
$\rho^{t_{0}...}\models\varphi$. We must show these three items are true for
each individual module.

In order to simplify proofs and conserve space, we write $(qp)$ to mean
Condition $p$, introduced in Definition 8, is satisfied for Status $q$. For
example, “$(a3)$ for $t_{1}$” means $\rho^{t_{1}...}$ not arbitrary.
Corresponding to the three items above, for every module we must show

  1. 1.

$\rho^{t_{0}...}\models\varphi$ by Definition 3,

  2. 2.

(a1), (a2), (a3) true for all $t\in\\{t_{0},...,T_{f}\\}$,

  3. 3.

(s1), (s2) true for all $t\in\\{t_{0},...,T_{f}\\}$.

We check these conditions for each, beginning with $AP$. For every module with
assignments depending on input from other modules, we assume the outputs from
these other modules meet soundness criteria.

Atomic proposition ($AP$):

  1. 1.

By Definition 3, $\alpha\in L_{t_{0}}$ iff $\rho^{t_{0}...}\models\varphi$.
Thus, the condition $\alpha\in L_{t_{0}}$ correctly assigns
$\tau^{v}=\emptyset$, and the Else correctly assigns $\tau_{v}\neq\emptyset$.

  2. 2.

Again by Definition 3, $\alpha\in L_{t_{0}}$ iff
$\rho^{t_{0}...}\models\varphi$, meaning condition $\alpha\in L_{t_{0}}$
implies (a1). Additionally, $\psi=\top$ for $\varphi=\alpha$ (a2). Finally,
since other $L_{t^{\prime}}$ do not affect whether $\alpha\in L_{t_{0}}$, all
$\rho^{t^{\prime}...},t^{\prime}\neq t_{0}$ are arbitrary (a3). Thus,
$\tau^{a}={t_{0}}$ is properly assigned.

  3. 3.

When $\tau^{a}=\emptyset$, the module sets $\tau^{s}=\emptyset$ (s1, s2).
Otherwise $\tau^{a}=\\{t_{0}\\}$; here, the module sets
$\tau^{s}=\\{t_{0}\\}$. We have $t_{0}\in\tau^{a}$ (s1). We also see that
$t_{0}+1\not\in\tau^{a}$ (s2).

Next ($\mathbf{X}\varphi_{1}$):

  1. 1.

By Definition 3, $\rho^{t_{0}...}\models\mathbf{X}\varphi_{1}$ iff
$\rho^{t_{1}...}\models\varphi_{1}$. We have
$\rho^{t_{1}...}\models\varphi_{1}$ iff $\tau^{v}_{1}=\emptyset$ for
$t_{1},...,T_{f}$ by 4. Thus, $\tau^{v}_{1}=\emptyset$ iff
$\rho^{t_{0}...}\models\mathbf{X}\varphi_{1}$.

  2. 2.

$\varphi$ is not arbitrary at $t_{1}$ since
$\rho^{t_{1}...}\models^{?}\varphi_{1}$ determines
$\rho^{t_{0}...}\models^{?}\varphi$ (it is also trivially not arbitrary at
$t_{0}$, since $\rho^{t_{0}...}$ contains nonarbitrary $\rho^{t_{1}...}$.
However, $\rho^{t_{1}...}\models\varphi_{1}$ alone implies
$\rho^{t_{0}...}\models\varphi$, rendering all
$\rho^{t^{\prime}...},t^{\prime}>1$ irrelevant to
$\rho^{t_{0}...}\models^{?}\varphi$ (a1, a3). (a2) is trivially true. Thus,
$\tau^{a}=\\{t_{0},t_{1}\\}$ is correct.

  3. 3.

When $\tau^{a}=\emptyset$, the module sets $\tau^{s}=\emptyset$ as well
(s1,s2). Otherwise, we have $\tau^{s}=\\{t_{1}\\}$ sound since
$\\{t_{1}\\}\subseteq\\{t_{0},t_{1}\\}$ (s1) and
$t_{0}+1\in\tau^{a},t_{1}+1\not\in\tau^{a}$ (s2).

Eventual ($\mathbf{F}\varphi_{1}$):

  1. 1.

From Definition 3, $\mathbf{F}\varphi_{1}\equiv\top\ \mathbf{U}\varphi_{1}$.
Thus, by the definition of $\varphi^{\prime}\mathbf{U}\varphi^{\prime\prime}$,
$\rho^{t_{0}...}\models\varphi$ iff $\rho^{t^{1}_{0}...}\models\varphi_{1}$
(i.e., $\tau^{v}_{1}=\emptyset$) for some $t^{1}_{0}\in\\{t_{0},...,T_{f}\\}$.
Accordingly, the module assigns $\tau^{v}\neq\emptyset$ iff $t_{0}^{1}=T_{f}$
is reached without $\tau^{v}_{1}=\emptyset$ for any
$t_{0}^{1}\in\\{t_{0},...,T_{f}\\}$.

  2. 2.

The module iterates upward from $t^{1}_{0}=t_{0}$ until
$\tau^{v}_{1}=\emptyset$ or $t^{1}_{0}=T_{f}$. As soon as
$\tau^{v}_{1}\neq\emptyset$ on $\rho^{t^{1}_{0}}$ (if this occurs), we have
(a1) for all $t$ from Definition 3. We have (a2) trivially. Finally, we note
that the module sets $\tau^{a}=\\{t_{0},...,t^{1}_{0}\\}$ for $t^{1}_{0}$
meeting the conditions above. Clearly $\rho^{t^{\prime}...}$ is not arbitrary
for $t^{\prime}<t^{1}_{0}$, as the iteration condition guarantees
$\rho^{t^{\prime}}\not\models\varphi_{1}$ until $t^{\prime}=t^{1}_{0}$.
Meanwhile, since $\rho^{t^{1}_{0}...}\models\varphi_{1}$ implies
$\rho^{t_{0}...}\models\varphi$, we have $\rho^{t^{\prime}...}$ arbitrary for
all $t^{\prime}>t^{1}_{0}$ (a3).

  3. 3.

The module sets $\tau^{s}=\emptyset$ when $\tau^{a}=\emptyset$, which is sound
by (s1, s2); when $\tau^{a}=\\{t_{0},...,t^{1}_{0}\\}$, the module sets
$\tau^{s}=\\{t^{1}_{0}\\}$. We have
$\\{t^{1}_{0}\\}\subseteq\\{t_{0},...,t^{1}_{0}\\}$ (s1), and $t^{1}_{0}$ is
the only $t\in\\{t_{0},...,t^{1}_{0}\\}$ such that $t+1\not\in\tau^{a}$ (s2).

Global ($\mathbf{G}\varphi_{1}$):

  1. 1.

By Definition 3, we have
$\mathbf{G}\varphi_{1}\equiv\neg\mathbf{F}(\neg\varphi_{1})\equiv\neg(\top\mathbf{U}(\neg\varphi_{1}))$.
By the definition of $\mathbf{U}$,
$\rho^{t_{0}...}\models\top\mathbf{U}(\neg\varphi_{1})$ iff
$\rho^{t^{\prime}...}\models\neg\varphi_{1}$ for some
$t^{\prime}\in\\{t_{0},...,T_{f}\\}$; thus,
$\rho^{t_{0}...}\models\mathbf{G}\varphi_{1}$ iff no such $t^{\prime}$ exists.
Accordingly, the module sets $\tau^{v}=\emptyset$ iff
$\tau^{v}_{1}\neq\emptyset$ for some $t_{0}^{1}\in\\{t_{0},...,T_{f}\\}$,
which occurs iff $\rho^{t^{\prime}...}\models\neg\varphi_{1}$.

  2. 2.

If no $t^{\prime}$ is reached such that $\tau^{v}_{1}\neq\emptyset$,
$\rho^{t^{\prime}...}\models\varphi_{1}$ for all $t^{\prime}$ (a1), and the
module sets $\tau^{a}=\\{t_{0},...,T_{f}\\}$. Since any
$\rho^{t^{\prime}...}\not\models\varphi_{1}$ implies
$\rho^{t_{0}...}\not\models\varphi_{1}$, no $\rho^{t^{\prime}...}$ is
arbitrary (a3); (a2) is satisfied trivially.

  3. 3.

If $\tau^{a}=\emptyset$, the module sets $\tau^{s}=\emptyset$ (s1, s2);
otherwise, $\tau^{a}=\\{t_{0},...,T_{f}\\}$, and the module sets
$\tau^{s}=\\{t_{0}^{1}\\}=\\{T_{f}\\}$. Clearly $T_{f}\in\tau^{a}$ (s1) and
$t^{1}_{0}=T_{f}$ (s2).

Until ($\varphi_{1}\mathbf{U}\varphi_{2}$):

  1. 1.

The module first iterates from $t_{0}$ to $T_{f}$, terminating iteration at
the first $t^{\prime}$ when $\tau^{v}_{1}\neq\emptyset$,
$\tau^{v}_{2}=\emptyset$, or $t^{\prime}=T_{f}$. Firstly, if
$\tau^{v}_{2}=\emptyset$, we have $\rho^{t^{\prime}...}\models\varphi_{2}$; we
also know that $\rho^{t...}\models\varphi_{1}$ for all $t<t^{\prime}$, since
$\tau^{v}_{1}\neq\emptyset$ would have halted iteration at any such previous
$t$. In this case, $\varphi_{1}$ was true on all $\varphi^{t...}$ until
$\rho^{t^{\prime}...}\models\varphi_{2}$ became true, meeting Definition 3. In
the next case, if $\tau^{v}_{1}\neq\emptyset,\tau^{v}_{2}\neq\emptyset$ at
iteration termination, the conditions for $\rho^{t_{0}...}\models\varphi$ are
violated, and $\tau^{v}\neq\emptyset$ accordingly. Finally, in the last case,
$T_{f}$ is reached with $\tau^{v}_{1}=\emptyset,\tau^{v}_{2}\neq\emptyset$ for
all $t$. This means that $\varphi_{2}$ was never true at any $t$, and thus
$\tau^{v}\neq\emptyset$ by Definition 3.

  2. 2.

When $\tau_{v}=\emptyset$ (a1), the module sets $\tau^{a}=\\{t_{0}\\}$ (if
$t^{\prime}=t_{0}$) or $\tau^{a}=\\{t_{0},...,t^{\prime}\\}$ (otherwise). We
note that $\rho^{t^{\prime}...}$ is clearly not arbitrary (i.e., it must
satisfy $\rho^{t^{\prime}...}\models\varphi_{2}$), and thus, no
$\rho^{t...},t\leq t^{\prime}$ is arbitrary. On the other hand,
$\rho^{t^{\prime}...}\models\varphi_{2}$ implies all
$\rho^{t...},t>t^{\prime}$ are arbitrary (a3). We have (a2) trivially.

  3. 3.

When $\tau^{a}=\emptyset$, $\tau^{s}=\emptyset$ (s1, s2). Otherwise,
$\tau^{s}$ is set to the largest member of $\tau^{a}$, satisfying both (s1,
s2).

Other temporal operator modules: The soundness of the remaining modules may be
proven similarly as for the preceding modules.

Implication ($\varphi=\varphi_{1}\rightarrow\varphi_{2}$):

  1. 1.

We have from Definition 3 that
$\varphi_{1}\rightarrow\varphi_{2}\equiv\neg\varphi_{1}\vee\varphi_{2}$. The
module first checks whether $\tau^{v}_{1}=\emptyset$ at $t_{0}$. If not, then
$\neg\varphi_{1}$ is true, implying $\rho^{t_{0}...}\models\varphi$.
Otherwise, $\rho^{t_{0}...}\models\varphi$ only if
$\rho^{t_{0}...}\models\varphi_{2}$ (i.e., if $\tau^{v}_{2}=\emptyset$ at
$t_{0}$). Thus, if $\tau^{v}_{1}=\emptyset$ and $\tau^{v}_{2}\neq\emptyset$,
the module sets $\tau^{v}=\\{t_{0},...,T_{f}\\}$ corresponding to
$\rho^{t_{0}...}\not\models\varphi$; otherwise, the module sets
$\tau^{v}=\emptyset$ for $\rho^{t_{0}...}\models\varphi$.

  2. 2.

When $\tau^{v}_{1}\neq\emptyset$, we have $\rho^{t_{0}...}\models\varphi_{1}$
(a1), but the precondition $\varphi_{1}$ of $\varphi$ is not met by Definition
7 (a2 violated for all $t$), so $\tau^{a}=\emptyset$ is correct. Otherwise
($\tau^{v}_{1}=\emptyset$), the precondition is met by Definition 7 (a2). The
module then checks whether $\rho^{t_{0}...}\models\varphi_{2}$, which is
clearly a requirement for
$\rho^{t_{0}...}\models\neg\varphi_{1}\vee\varphi_{2}$ true when
$\rho^{t_{0}...}\models\varphi_{1}$. If $\tau^{v}_{0}\neq\emptyset$, then
$\varphi_{2}$ is violated on $\rho^{t_{0}...}$, and thus
$\rho^{t_{0}...}\not\models\varphi$ (a1 violated); the module thus sets
$\tau_{a}=\emptyset$. Else ($\tau^{v}_{2}\neq\emptyset$), we have
$\rho^{t_{0}...}\models\varphi$ (a1). The module sets $\tau^{a}=\\{t_{0}\\}$,
since $\rho^{t_{0}...}\models\neg\varphi_{1}\vee\varphi_{2}$ is necessary (a3
at $t_{0}$), but is not dependent on whether
$\rho^{t^{\prime}...}\models\neg\varphi_{1}$ or
$\rho^{t^{\prime}...}\models\varphi_{2}$ for any $t^{\prime}>t_{0}$ (a3
violated for $t^{\prime}>t_{0}$).

  3. 3.

When $\tau^{a}=\emptyset$, the module sets $\tau^{s}=\emptyset$; this is sound
because $(\tau^{a}=\emptyset)\Rightarrow(\tau^{s}=\emptyset)$ by (s1). When
$\tau^{a}\neq\emptyset$, $\tau^{a}=\\{t_{0}\\}$, meaning that (s2) is violated
for all $t$ except $t_{0}$; thus, the module assignment $\tau^{s}=\\{t_{0}\\}$
in this case is also sound.

Other logical operator modules: The soundness of the remaining logical
operator modules are trivial to show, following the example for Implication.

###  VII-B Autonomous Driving Example

The rules for the autonomous driving example are:

  1. 1.

$\mathbf{G}(\text{want-left-turn}\wedge\text{near-
intersection}\wedge\text{clear-left}\wedge\text{lane-to-
left}\rightarrow\text{change-left})$

  2. 2.

$\mathbf{G}(\text{want-turn}\wedge\text{near-
intersection}\rightarrow\text{reduced-speed})$

  3. 3.

$\mathbf{G}(\text{gas-low}\rightarrow\neg(\text{goal})\mathbf{U}\text{gas-
station})$

  4. 4.

$\mathbf{F}\text{goal}$

  5. 5.

$\mathbf{G}(\text{merge-left}\wedge\text{clear-left}\wedge\text{lane-to-
left}\rightarrow\text{change-left})$

  6. 6.

$\mathbf{G}(\text{merge-right}\wedge\text{clear-right}\wedge\text{lane-to-
right}\rightarrow\text{change-right})$

  7. 7.

$\mathbf{G}(\text{construction-zone}\rightarrow\text{reduced-
speed}\mathbf{U}\text{leave-zone})$

  8. 8.

$\mathbf{G}(\text{short-follow-distance}\rightarrow\text{reduced-speed})$

  9. 9.

$\mathbf{G}(\text{short-follow-distance}\wedge\text{clear-
left}\wedge\text{lane-to-left}\rightarrow\mathbf{X}\text{change-left})$

  10. 10.

$\mathbf{G}(\text{want-pass}\wedge\text{clear-left}\wedge\text{lane-to-
left}\rightarrow\mathbf{X}\text{change-left})$

  11. 11.

$\mathbf{G}(\text{rain-hazard}\rightarrow\text{wipers-on})$

  12. 12.

$\mathbf{G}(\text{parking-brake}\rightarrow\text{stop})$

  13. 13.

$\mathbf{G}(\text{ice-hazard}\vee\text{wind-hazard}\rightarrow\text{reduced-
speed})$

  14. 14.

$\mathbf{G}(\text{want-right-turn}\wedge\text{no-right-on-
red}\rightarrow\text{stop}\mathbf{U}\text{green})$

  15. 15.

$\mathbf{G}(\text{want-right-turn}\wedge\neg\text{no-right-on-
red}\rightarrow\text{stop}\mathbf{U}((\text{red}\wedge\text{clear-
ahead})\vee\text{green}))$

  16. 16.

$\mathbf{G}(\text{problem-detected}\rightarrow\mathbf{X}\text{find-pullout})$

  17. 17.

$\mathbf{G}(\neg(\text{doors-closed}\wedge\text{driver-
awake})\rightarrow\text{stop})$

  18. 18.

$\mathbf{G}(\text{yellow-ahead}\wedge\text{safe-stop}\rightarrow(\text{reduce-
speed}\wedge\mathbf{X}\text{yellow}\rightarrow\text{stop}))$

  19. 19.

$\mathbf{G}(\text{red-ahead}\rightarrow(\text{reduce-
speed}\wedge\mathbf{X}\text{red}\rightarrow\text{stop}))$

  20. 20.

$\mathbf{G}(\text{want-left-
turn}\wedge\text{intersection}\wedge\neg\text{clear-
ahead}\rightarrow\text{stop}\mathbf{U}\text{clear-ahead})$

  21. 21.

$\mathbf{G}(\text{yieldsign-ahead}\wedge\neg\text{clear-
ahead}\rightarrow\text{reduce-
speed}\wedge(\mathbf{X}\text{yieldsign}\rightarrow\text{stop}))$

Full trace data and $AP$ are available at
https://github.com/n-brindise/pointwiseExpl-example.git. Samples of each trace
are provided here. Time step is given by $(t)$, followed by a list of the
labels in $L_{t}$. Query time $t^{\prime}$ is also shown.

Trace 1 $(\rho_{1})$

(1) origin

(…)

(11) doors-closed, driver-awake, clear-ahead, want-straight, pass-allowed,
rightmost, rain-hazard, wipers-on, lane-to-left

(12) doors-closed, driver-awake, clear-ahead, want-turn-right, pass-allowed,
rightmost, rain-hazard, wipers-on, yellow-ahead, intersection-ahead, safe-
stop, lane-to-left

(13) doors-closed, driver-awake, clear-ahead, want-turn-right, rightmost,
rain-hazard, wipers-on, yellow-ahead, intersection-ahead, safe-stop, lane-to-
left

(14) doors-closed, driver-awake, clear-ahead, want-turn-right, rightmost,
rain-hazard, wipers-on, red, intersection, stop, no-right-on-red, clear-right,
clear-left, lane-to-left

(15) doors-closed, driver-awake, clear-ahead, want-turn-right, rightmost,
rain-hazard, wipers-on, red, intersection, stop, no-right-on-red, clear-right,
lane-to-left

(16) doors-closed, driver-awake, clear-ahead, want-turn-right, rightmost,
rain-hazard, wipers-on, red, intersection, stop, no-right-on-red, clear-right,
lane-to-left

(17) doors-closed, driver-awake, clear-ahead, want-turn-right, rightmost,
rain-hazard, wipers-on, intersection, green, stop, no-right-on-red, clear-
right, lane-to-left

(18) doors-closed, driver-awake, clear-ahead, rightmost, intersection, green,
no-right-on-red, clear-right, turn-right

(19) rightmost, doors-closed, driver-awake, clear-ahead, want-straight, pass-
allowed, clear-left, lane-to-left

(…)

(32) rightmost, doors-closed, driver-awake, clear-ahead, want-straight, pass-
allowed, clear-left, gas-low, lane-to-left

(33) rightmost, doors-closed, driver-awake, clear-ahead, want-straight, pass-
allowed, clear-left, gas-low, lane-to-left

($\mathbf{t^{\prime}}$) rightmost, doors-closed, driver-awake, clear-ahead,
want-turn-left, pass-allowed, clear-left, lane-to-left, gas-low, intersection-
ahead, green-ahead, reduced-speed, change-left, safe-stop

(35) leftmost, doors-closed, driver-awake, clear-ahead, want-turn-left, pass-
allowed, clear-right, lane-to-right, gas-low, intersection-ahead, green-ahead,
reduced-speed, safe-stop

(36) leftmost, doors-closed, driver-awake, clear-ahead, want-turn-left, clear-
right, lane-to-right, gas-low, intersection-ahead, green-ahead, reduced-speed,
safe-stop

(37) leftmost, doors-closed, driver-awake, clear-ahead, want-turn-left, clear-
right, lane-to-right, gas-low, intersection, green, reduced-speed, turn-left

(38) leftmost, doors-closed, driver-awake, clear-ahead, pass-allowed, clear-
right, gas-low, lane-to-right

(…)

(44) gas-station, driver-awake, stop, clear-ahead

(…)

(90) goal

Trace 2 $(\rho_{2})$

(1) origin

(…)

(32) rightmost, doors-closed, driver-awake, clear-ahead, want-straight, clear-
left, lane-to-left

(33) rightmost, doors-closed, driver-awake, clear-ahead, want-straight, lane-
to-left, merge-left

($\mathbf{t^{\prime}}$) rightmost, doors-closed, driver-awake, clear-ahead,
want-straight, clear-left, lane-to-left, merge-left, reduced-speed, change-
left, construction-zone

(35) leftmost, doors-closed, driver-awake, clear-ahead, want-straight,
reduced-speed, construction-zone, merge-left, lane-to-right

(36) leftmost, rightmost, doors-closed, driver-awake, clear-ahead, want-
straight, reduced-speed, construction-zone

(37) leftmost, rightmost, doors-closed, driver-awake, clear-ahead, want-
straight, reduced-speed, construction-zone (…)

(45) leftmost, rightmost, doors-closed, driver-awake, clear-ahead, want-
straight, reduced-speed, leave-zone

(46) leftmost, doors-closed, driver-awake, clear-ahead, clear-right, lane-to-
right, want-straight

(…)

(90) goal

Trace 3 $(\rho_{3})$

(1) origin

(…)

(32) rightmost, doors-closed, driver-awake, clear-ahead, want-straight, clear-
left, lane-to-left

(33) rightmost, doors-closed, driver-awake, want-straight, short-follow-
distance, clear-left, lane-to-left, reduced-speed

($\mathbf{t^{\prime}}$) rightmost, doors-closed, driver-awake, want-straight,
short-follow-distance, clear-left, lane-to-left, reduced-speed, change-left

(35) leftmost, doors-closed, driver-awake, lane-to-right

(36) leftmost, doors-closed, driver-awake, clear-ahead, want-straight, lane-
to-right

(37) leftmost, doors-closed, driver-awake, clear-ahead, want-straight, lane-
to-right, clear-right

(…)

(90) goal

## References

  * [1] Y. Xing, C. Lv, D. Cao, and P. Hang, “Toward human-vehicle collaboration: Review and perspectives on human-centered collaborative automated driving,” _Transportation research part C: emerging technologies_ , vol. 128, p. 103199, 2021.
  * [2] I. Seeber, L. Waizenegger, S. Seidel, S. Morana, I. Benbasat, and P. B. Lowry, “Collaborating with technology-based autonomous agents: Issues and research opportunities,” _Internet Research_ , 2020.
  * [3] S. Franklin and A. Graesser, “Is it an agent, or just a program?: A taxonomy for autonomous agents,” in _Intelligent Agents III Agent Theories, Architectures, and Languages: ECAI’96 Workshop (ATAL) Budapest, Hungary, August 12–13, 1996 Proceedings 3_. Springer, 1997, pp. 21–35.
  * [4] S. Sreedharan, A. Kulkarni, and S. Kambhampati, “Explainable human–ai interaction: A planning perspective,” _Synthesis Lectures on Artificial Intelligence and Machine Learning_ , vol. 16, no. 1, pp. 1–184, 2022.
  * [5] A. Lindsay, “Using generic subproblems for understanding and answering queries in xaip,” _Proceedings of KEPS_ , 2020.
  * [6] T. Chakraborti, S. Sreedharan, and S. Kambhampati, “The emerging landscape of explainable automated planning and decision making,” in _Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20_ , C. Bessiere, Ed. International Joint Conferences on Artificial Intelligence Organization, 7 2020, pp. 4803–4811, survey track. [Online]. Available: https://doi.org/10.24963/ijcai.2020/669
  * [7] K. Boggess, S. Kraus, and L. Feng, “Toward policy explanations for multi-agent reinforcement learning,” _arXiv preprint arXiv:2204.12568_ , 2022.
  * [8] M. Brandão and Y. Setiawan, “’why not this mapf plan instead?’contrastive map-based explanations for optimal mapf,” in _ICAPS 2022 Workshop on Explainable AI Planning_ , 2022.
  * [9] A. Kumar, S. L. Vasileiou, M. Bancilhon, A. Ottley, and W. Yeoh, “Vizxp: A visualization framework for conveying explanations to users in model reconciliation problems,” in _Proceedings of the International Conference on Automated Planning and Scheduling_ , vol. 32, 2022, pp. 701–709.
  * [10] D. Neider and I. Gavran, “Learning linear temporal properties,” in _2018 Formal Methods in Computer Aided Design (FMCAD)_. IEEE, 2018, pp. 1–10.
  * [11] G. Bombara, C.-I. Vasile, F. Penedo, H. Yasuoka, and C. Belta, “A decision tree approach to data classification using signal temporal logic,” in _Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control_ , 2016, pp. 1–10.
  * [12] G. Bombara and C. Belta, “Offline and online learning of signal temporal logic formulae using decision trees,” _ACM Trans. Cyber-Phys. Syst._ , vol. 5, no. 3, mar 2021. [Online]. Available: https://doi.org/10.1145/3433994
  * [13] C. Lemieux, D. Park, and I. Beschastnikh, “General ltl specification mining (t),” in _2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE)_. IEEE, 2015, pp. 81–92.
  * [14] G. Chou, N. Ozay, and D. Berenson, “Explaining multi-stage tasks by learning temporal logic formulas from suboptimal demonstrations,” _arXiv preprint arXiv:2006.02411_ , 2020.
  * [15] J. Kim, C. Muise, A. J. Shah, S. Agarwal, and J. A. Shah, “Bayesian inference of linear temporal logic specifications for contrastive explanations,” _IJCAI International Joint Conference on Artificial Intelligence_ , 2019.
  * [16] R. Roy, J.-R. Gaglione, N. Baharisangari, D. Neider, Z. Xu, and U. Topcu, “Learning interpretable temporal properties from positive examples only,” in _Proceedings of the AAAI Conference on Artificial Intelligence_ , vol. 37, no. 5, 2023, pp. 6507–6515.
  * [17] J.-R. Gaglione, D. Neider, R. Roy, U. Topcu, and Z. Xu, “Learning linear temporal properties from noisy data: A maxsat-based approach,” in _Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings 19_. Springer, 2021, pp. 74–90.
  * [18] E. Bartocci, R. Bloem, D. Nickovic, and F. Röck, “A counting semantics for monitoring ltl specifications over finite traces,” in _International Conference on Computer Aided Verification_. Springer, 2018, pp. 547–564.
  * [19] E. Aasi, C. I. Vasile, M. Bahreinian, and C. Belta, “Inferring temporal logic properties from data using boosted decision trees,” _arXiv preprint arXiv:2105.11508_ , 2021.
  * [20] X. Ding, S. L. Smith, C. Belta, and D. Rus, “Optimal control of markov decision processes with linear temporal logic constraints,” _IEEE Transactions on Automatic Control_ , vol. 59, no. 5, pp. 1244–1257, 2014.
  * [21] A. Camacho and S. A. McIlraith, “Learning interpretable models expressed in linear temporal logic,” in _Proceedings of the International Conference on Automated Planning and Scheduling_ , vol. 29, 2019, pp. 621–630.
  * [22] A. Pnueli, “The temporal logic of programs,” in _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_. ieee, 1977, pp. 46–57.
  * [23] S. Maierhofer, P. Moosbrugger, and M. Althoff, “Formalization of intersection traffic rules in temporal logic,” in _2022 IEEE Intelligent Vehicles Symposium (IV)_ , 2022, pp. 1135–1144.