Trace Diagnostics Using Temporal Implicants

Abstract

Runtime verification and model checking are two important methods for assessing correctness of systems. In both techniques, detecting an error is witnessed by an execution that violates the system specification. However, a faulty execution on its own may not provide sufficiently precise insight to the causes of the reported violation. Additional, often manual effort is required to properly diagnose the system. In this paper we present a method for analyzing such causes. The specifications we consider are expressed in LTL (Linear Temporal Logic) and MTL (Metric Temporal Logic), and the execution models are taken as ultimately-periodic words, and finite variability continuous signals respectively. The diagnostics problem is defined for the propositional case as the search for a small implicant of a formula which is satisfied by a given valuation, or equivalently a subset of that valuation sufficient to render the formula true. We propose a suitable notion of implicants in the temporal case, that are semantically based on signal subsets, and guarantee the existence of prime implicants for arbitrary temporal properties. An inductive procedure for finding temporal implicants is obtained by the introduction of selection functions that appear in a process equivalent to Skolemization in first order logic. Through the model restrictions we impose for LTL and MTL we are able to generate concise implicants of a property, describing a small fragment of the input signal that causes violation of a formula.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Our work is concerned with the problem of temporal monitoring: given a single behavior w, either in discrete or dense time, and a temporal property $\varphi$ check whether $w\models \varphi$. This problem is known as runtime verification in software and assertion checking in hardware. In addition to the yes/no answer, we would like to produce an informative diagnostics, a small fragment of the behavior which provides a sufficient condition for the violation of $\varphi$ by w. This additional information helps localizing and explaining the causes of the fault. We solve the diagnostics problem for MTL [9], for which we assume that the input signal w has bounded variability. We further extend our results to LTL [15] under the assumption of an ultimately periodic input sequence. This makes our technique applicable to the analysis of counter-example executions as produced by a model checking procedure.

Consider the temporal logic formula $\square _{} ( p \rightarrow {{\mathrm{\lozenge }}}_{[1,2]} q)$. It requires that for any instant in time where p holds, there exists another instant within 1 to 2 time units where q holds. The behavior depicted in Fig. 1 violates this temporal property – the violation can be explained by the fact that p holds at time 1 and q does not hold throughout [2,3]. Such a concise piece of information, compared to w which can be a very long signal, will increase our confidence in monitoring and model-checking procedures, and promote their further acceptance in various application domains.

Fig. 1.

A behavior that violates $\square _{} ( p \rightarrow {{\mathrm{\lozenge }}}_{[1,2]} q)$. Grey-shaded area gives one possible explanation.

Finding an explanatory sub-model in the propositional case, is strongly related to the concept of prime implicants of a formula. The problem that we pose in this paper, finding explanatory temporal sub-models, is novel and in order to solve it we had to overcome numerous issues that come from the infinitude of the temporal models. Our main result is an inductive explanation generation scheme for MTL which produces focused dense time sub-signals sufficient to explain violation. A crucial ingredient of the procedure is the elimination of disjunctive operations by the introduction of selection functions similar in spirit to Skolem functions used to eliminate existential quantification. Under a finite variability assumption we can show that explanations can be taken as finitely variable. For LTL, we show similarly that infinite ultimately-periodic sequences admit ultimately-periodic explanatory sub-models.

Related Work. The problem of understanding a counter-example by finding the reason for the failure of a temporal logic formula in the trace itself was studied in [1]. This work differs from ours in several aspects. It adopts a different notion of failures based on Halpern and Pearl causality [6] and considers only LTL but not dense-time temporal logics. The explanations of ultimately periodic sequences are handled by unfolding the trace. Finally, the authors are interested in the detection of the first failure in a trace. In our work we provide more flexibility by means of selection functions, which allow to choose between several different failures. In [13], the authors propose a procedure that provides a minimal debugging window for traces that violate an MTL formula. The result can be seen as a coarse-grain diagnostic, providing a small segment of the input trace yet not discriminating signals and time intervals causing the violation.

There have been various studies on obtaining additional debugging information from counter-examples in LTL model checking. Tight automata [10] were introduced to find shortest finite counter-examples for safety properties, and extended in [17] to infinite words and full LTL. Comparing erroneous and correct traces with distance metrics in order to localize errors has been studied in the context of software checking in [5]. The problem of finding and repairing violations of LTL properties by sequential circuits was studied in [8], where a repair solution based on a game-oriented approach is proposed. A related problem is that of computing unsatisfiable cores for LTL, i.e. finding smaller unsatisfiable sub-formulas, as studied in [7, 14, 16]. At the syntactic level minimal unsatisfiable cores bear some similarity with prime implicants; they primarily address formal verification concerns.

2 Propositional Foundations

Consider the problem of explaining why a formula $\varphi$ is violated by a given execution w of some system, seen as finding the part of the execution w that causes $\varphi$ to be violated. Note that through negation this is equivalent to solving the dual problem of explaining why some formula is satisfied. We first introduce and study the problem in the simple setting of propositional logic.

2.1 Problem Statement

Let $\mathbb P$ be a finite set of propositional variables. A valuation w is taken to be a function $P \rightarrow \mathbb {B}$ with $P \subseteq \mathbb P$ its domain and $\mathbb {B}:= \{0,1\}$ the set of Boolean values. We define propositional formulas over $\mathbb P$ and the constant $\mathrm {true}$ the usual way. The set of models of a formula $\varphi$ is noted $[\![\varphi ]\!]$. For $\varphi$ and $\psi$ two formulas we write $\psi \Rightarrow \varphi$ when $[\![\psi ]\!]\subseteq [\![\varphi ]\!]$, and $\psi \Leftrightarrow \varphi$ when $[\![\psi ]\!]= [\![\varphi ]\!]$. Note that implication ($\Rightarrow$) induces a partial order over classes of equivalent ($\Leftrightarrow$) formulas.

Definition 1

(Terms, Implicants and Prime Implicants). A term $\gamma$ is defined as a conjunction of literals. If $\gamma \Rightarrow \varphi$ then the term $\gamma$ is an implicant of formula $\varphi$. If moreover $\gamma$ is maximal with respect to $\Rightarrow$ we talk of prime implicant.

We say that $\gamma$ explains the satisfaction of $\varphi$ by w, if $\gamma$ is an implicant of $\varphi$ and w is a model of $\gamma$. Note that the least general explanation of $\varphi$ relative to w is a term representing the truth status of every variable in w. It is intuitively clear, however that we opt for explanations that are smaller and more general, omitting “don’t care” variables. We aim at providing explanations that use small subsets of “do care” variables. The most general explanations are in particular the prime implicants of $\varphi$ satisfied by w.

Problem

((Minimal) Diagnostics). Given a valuation w and a formula $\varphi$, find a (prime) implicant $\gamma$ of $\varphi$ such that $w \models \gamma$.

2.2 Syntactic and Semantic Formulations

Take $\varphi$ a formula, w a model of $\varphi$ and $\gamma$ a solution to the corresponding diagnostics problem. As $\gamma \Rightarrow \varphi$, there exists a proof of $\varphi$ under hypothesis $\gamma$; a correct algorithm producing the diagnostics is implicitly constructing that proof. The more general the implicant is, the more complex the associated proof can be.

Example 1

Take formula $\varphi := (p \wedge q) \vee (p \wedge \lnot q)$ and valuation $w := \{ p\mapsto 1, q \mapsto 0, r \mapsto 0\}$. The formulas $\alpha := p$ and $\beta := p \wedge \lnot q$ are both implicants of $\varphi$, and satisfied by w with $\alpha$ a prime implicant of $\varphi$. In sequent calculus the proof $\beta \vdash \varphi$ is direct through a right disjunction rule, while the proof $\alpha \vdash \varphi$ requires the application of several rules, and uses non-intuitionistic reasoning.

We now sketch the semantic counter-parts of implicants, beginning with a refinement relation $\sqsubseteq$ between valuations.

Definition 2

For two valuations $u : P \rightarrow \mathbb {B}$ and $v : Q \rightarrow \mathbb {B}$ we have $u \sqsubseteq v$ if and only if $P \subseteq Q$ and $u(p) = v(p)$ for all $p \in P$.

The space of valuations is a semi-lattice with respect to $\sqsubseteq$ with meet operation $\sqcap$ and least element $\bot$. Let u and v be some valuations with domain P and Q respectively. The valuation $u \sqcap v$ has domain $\{ p \in P \cap Q ~:~u(p) = v(p) \}$ and value $u\sqcap v\,(p) = u(p)$ where defined. The least element $\bot$ is the nowhere-defined valuation with domain $\emptyset$.

One can think of a valuation v over $P \subseteq \mathbb P$ as a compact representation for all valuations w over $\mathbb P$ such that $v \sqsubseteq w$. A valuation v corresponds to a term $\gamma _v$, the conjunction of literals true according to v, and reciprocally any satisfiable term $\gamma$ corresponds to a valuation $v_\gamma$, that assigns a value to variables according to the literals in $\gamma$.

Definition 3

(Sub-Model). A valuation v is a sub-model of $\varphi$ if for all valuations w over $\mathbb P$ such that $v \sqsubseteq w$ we have $w \models \varphi$; if moreover v is minimal with respect to $\sqsubseteq$ we talk of minimal sub-model.

A valuation v is a sub-model of $\varphi$ if and only if $\gamma _v$ is an implicant of $\varphi$. The (minimal) diagnostics problem for $\varphi$ relative to w can thus be formulated equivalently as the problem of finding a (minimal) sub-model of $\varphi$ contained in w.

2.3 Practical Solution

Note that the minimal diagnostics problem is at least as hard as a satisfiability query, since tautologies can be recognized by their unique prime implicant, the empty term $\mathrm {true}$. However by relaxing the minimality assumption, knowing the truth value of each sub-formula of $\varphi$ on w allows to construct implicants $\gamma$ such that $w \models \gamma$ in a simple, top-down fashion. For every formula we take for implicant a combination of implicants for its sub-formulas that are satisfied by w, or violated by w when in the context of a negation. Accordingly we define an operator E (and its dual F) that for a given formula $\varphi$ returns an implicant of $\varphi$ (respectively of $\lnot \varphi$) which under suitable assumptions is satisfied by w. The explanation of $\varphi$ is then defined as

$$\begin{aligned} {\text {Exp}}(\varphi )=\left\{ \begin{array}{ll} E(\varphi ) &{} \text { if } w\,\models \,\varphi \\ F(\varphi ) &{} \text { otherwise}\end{array}\right. \end{aligned}$$

with

$$\begin{aligned} E(p)&= p&F(p)&= \lnot p \\ E(\lnot \varphi )&= F(\varphi )&F(\lnot \varphi )&= E(\varphi ) \\ E(\varphi _1 \vee \varphi _2)&= E(\xi (\varphi _1 \vee \varphi _2))&F(\varphi _1 \vee \varphi _2)&= F(\varphi _1) \wedge F(\varphi _2) \end{aligned}$$

where $\xi$ is a selection function satisfying $\xi (\varphi _1 \vee \varphi _2) \in \{\varphi _1, \varphi _2\}$. When for any formula $\varphi _1 \vee \varphi _2$ such that $w \models \varphi _1 \vee \varphi _2$ it holds $w \models \xi (\varphi _1 \vee \varphi _2)$, we say that $\xi$ is correct with respect to w. We can take for example

$$\xi : \varphi _1 \vee \varphi _2 \mapsto \left\{ \begin{array}{ll} \varphi _1 &{} \text { if } w\,\models \,\varphi _1 \\ \varphi _2 &{} \text { otherwise}\end{array}\right. $$

This gives priority to the left disjunct. Under the assumption that $\xi$ is correct with respect to w, the formula Exp$(\varphi )$ is a solution to the diagnostics problem associated to $\varphi$ and w. In the case of Example 1, applying the procedure on $\varphi$ and w yields the explanation $\beta$.

3 Temporal Issues

We introduce the temporal logics LTL [15] and MTL [9] in a unified framework. Temporal formulas will be given by the grammar

$$\begin{aligned} \varphi {:}{=} p ~|~ \lnot \varphi ~|~ \varphi \vee \varphi ~|~ \varphi \,\mathcal {U}_{I} \varphi \end{aligned}$$

where I is a real interval with integer endpoints. Other temporal connectives are introduced through the abbreviations $\varphi _1 \,\mathcal {U}_{} \varphi _2 := \varphi _1 \,\mathcal {U}_{(0,+\infty )} \varphi _2$ for strict until, ${{\mathrm{\bigcirc }}}\varphi := \mathrm {false}{{\mathrm{\mathcal {U}}}}\varphi$ for next, $\varphi _1 {{\mathrm{\mathcal {\tilde{U}}}}}{} \varphi _2 := \varphi _2 \vee (\varphi _1 \wedge \varphi _1 \,\mathcal {U}_{} \varphi _2)$ for non-strict until, $\lozenge _{} \varphi := \mathrm {true}{{\mathrm{\mathcal {\tilde{U}}}}}\varphi$ for eventually, $\square _{} \varphi := \lnot (\lozenge _{} \lnot \varphi )$ for always and $\lozenge _{I} \varphi := \mathrm {true}\,\mathcal {U}_{I} \varphi$, $\square _{I} \varphi := \lnot \lozenge _{I} \lnot \varphi$ for their timed versions. LTL formulas are then constructed using temporal connectives ${{\mathrm{\bigcirc }}}$ and ${{\mathrm{\mathcal {\tilde{U}}}}}$, while MTL formulas are constructed using temporal connectives $\lozenge _{I}$ and ${{\mathrm{\mathcal {U}}}}$.

A temporal behavior is defined as a function $\mathbb {T}\times P \rightarrow \mathbb {B}$, for $P \subseteq \mathbb P$ a set of propositional variables and $\mathbb {T}$ a linearly-ordered time domain. Given a behavior w we note w[t] its value at time $t \in \mathbb {T}$ taken to be a vector of Boolean values, and $w_p$ the behavior $\mathbb {T}\rightarrow \mathbb {B}$ that is the projection of w on the component $p \in \mathbb P$. The models for both logics are defined over infinite time domains, $\mathbb {N}$ and [0, d) respectively. In the following, we use the term signal to refer both to discrete continuous time behaviors.

We write $I \oplus J = \{ t+t' \in \mathbb {T}~:~t\in I \; \text {and} \; t' \in J\}$ and $I \ominus J = \{ t-t' \in \mathbb {T}~:~t\in I \; \text {and} \; t' \in J\}$ the Minkowski sum and difference of two intervals I and J, that we may simply note $t \oplus J$ and $t \ominus J$ when $I=[t,t]$. The semantics of a temporal logic formula $\varphi$ with respect to a signal $w: \mathbb {T}\times \mathbb P\rightarrow \mathbb {B}$ and time $t\in \mathbb {T}$ are given as follows:

$$\begin{aligned} (w,t)&\models p&\leftrightarrow&w_{p}[t] = 1\\ (w,t)&\models \lnot \varphi&\leftrightarrow&(w,t) \not \models \varphi \\ (w,t)&\models \varphi _1 \vee \varphi _2&\leftrightarrow&(w,t) \models \varphi _1 \text { or } (w,t) \models \varphi _2\\ (w,t)&\models \varphi _1 \,\mathcal {U}_{I} \varphi _2&\leftrightarrow&\exists t' \in t \oplus I ,\ (w,t') \models \varphi _2 \text { and } \forall t'' \in (t,t') ,\, (w,t'') \models \varphi _1 \end{aligned}$$

We say that w is a model of $\varphi$ and write $w \models \varphi$ when $(w,0) \models \varphi$. A signal can be “projected” for any formula $\varphi$ to its satisfaction signal $w_\varphi : \mathbb {T}\rightarrow \mathbb {B}$ such that $w_{\varphi }[t] = 1$ if and only if $(w,t) \models \varphi$. We extend the notion of satisfaction signal $w_\varphi$ to sets of formulas $\varPsi$ by letting $w_{\varPsi } : \mathbb {T}\times \varPsi \rightarrow \mathbb {B}$ be a multi-dimensional signal featuring the corresponding $|\varPsi |$ satisfaction signals $w_\psi$ for $\psi \in \varPsi$. The satisfaction signals of $\varphi$ and of all its sub-formulas $\psi$ are given as the result of applying a monitoring procedure such as the one from [11] to w and $\varphi$.

3.1 Syntactic Rewritings

The fragment of temporal logic based on operators $\lnot , \vee , \lozenge _{I}$ and $\mathcal U$ as introduced, has the same expressiveness as the fragment $\lnot , \vee$ and $\mathcal U_I$, often taken as primitive MTL operators. This equivalence is based on the observation that the timed until operator admits a decomposition into a timing part, and a sequential part [4]. For instance we have $\varphi \,\mathcal {U}_{(a,b)}\psi \Leftrightarrow \Box _{[0,a]}(\varphi \,\mathcal {U}_{} \psi ) \wedge \Diamond _{(a,b)} \psi$, and similar decompositions in the case of semi-opened and closed timing intervals.

For the purpose of handling the negation of an until formula we introduce its dual operation release, with non-strict and strict versions as follows.

$$\begin{aligned} \varphi {{\mathrm{\mathcal {\tilde{R}}}}}\psi&:= \psi {{\mathrm{\mathcal {\tilde{U}}}}}(\psi \wedge \varphi ) \ \vee \ {{\mathrm{\square }}}\psi \\ \varphi \,\mathcal R\, \psi&:= \varphi {{\mathrm{\mathcal {U}}}}\mathrm {true}\ \vee \ \psi {{\mathrm{\mathcal {U}}}}(\psi \wedge \varphi ) \ \vee \ \psi {{\mathrm{\mathcal {U}}}}(\psi \wedge \varphi {{\mathrm{\mathcal {U}}}}\mathrm {true}) \ \vee \ \square _{(0,\infty )} \psi \end{aligned}$$

In discrete time $\lnot (\varphi {{\mathrm{\mathcal {\tilde{U}}}}}\psi ) \Leftrightarrow \lnot \varphi {{\mathrm{\mathcal {\tilde{R}}}}}\lnot \psi$, while in continuous time $\lnot ( \varphi \,\mathcal {U}_{} \psi ) \Leftrightarrow \lnot \varphi \,\mathcal R\, \lnot \psi$. We explain the MTL negation of an until as follows: $\varphi \,\mathcal {U}_{} \psi$ does not hold if $\varphi$ is immediately false, or if $\varphi$ becomes false before (or immediately when) $\psi$ becomes true, or if $\psi$ never holds in the future.

3.2 Semantic Restrictions

We now introduce some definitions allowing us to place restrictions on the kind of signals we consider. Given a some constant in $\mathbb {T}$ we note $w^{a..}$ the shifted sequence such that $w^{a..}[t] = w[t+a]$ for all $t \in \mathbb {T}$. For a and b constants in $\mathbb {T}$ we say that some sequence w is ultimately periodic with period a and prefix b if $w^{a+b..} = w^{b..}$ holds. Some real interval I is said to be uniform with respect to signal w when $w[t]=w[t']$ for all t and $t'$ in I; if moreover I is maximal with respect to $\subseteq$ we talk of a maximally uniform interval. The variability of a signal is taken to be the largest number of maximally uniform intervals in any unit length segment of that signal.

In what follows on one hand we assume that all continuous signals have finite variability, that is MTL finite variability semantics. On the other hand we consider arbitrary discrete signals, that is LTL unrestricted semantics. However we will always assume that the input signal to the LTL diagnostic is ultimately-periodic.

3.3 Sub-models of a Formula

We define, similarly to the propositional case, sub-signals with domain $T \subseteq \mathbb {T}\times \mathbb P$ and partially ordered $\sqsubseteq$. Sub-signals u and v with respective domains R and S verify $u \sqsubseteq v$ if and only if $R \subseteq S$ and $u_{p}[t] = v_{p}[t]$ for all $(t,p) \in R$. Given formula $\varphi$ and sub-signal v, we say that v is a sub-model of $\varphi$ if $w\models \varphi$ for all signals $w \sqsupseteq v$.

To ensure finite representation we introduce corresponding semantic restrictions (ultimate periodicity, finite variability) on sub-signals. The notions of uniform segment and shifting operation extend to sub-signals in a natural way. A finite variability sub-signal has a domain $\bigcup _{p \in P} T_p \times \{p\}$, where $T_p \subseteq \mathbb {T}$ is the domain of p, such that the number of intervals in the intersection of each $T_p$ with a unit interval admits a maximum. An ultimately-periodic signal v with period a and prefix b has a domain T such that $(t+b, p) \in T$ if and only if $(t+b+a, p) \in T$.

In the discrete case, a relative ultimate-periodicity hypothesis does not guarantee the existence of a minimal sub-model.

Example 2

(LTL). The formula $\varphi := {{\mathrm{\lozenge }}}{{\mathrm{\square }}}p$ has no minimal ultimately-periodic sub-model over the discrete time domain $\mathbb {N}$. Consider the monotone sequence $(v_i)$ of ultimately-periodic sub-models of $\varphi$ with period 1 and prefix i, and domain $[i, \infty ) \times \{p\}$. The sub-signal $\sqcap _{i \in \mathbb {N}} v_i = \bot$ is not a sub-model of $\varphi$.

We thus fix the period a and prefix b as given by the input signal, and restrict our analysis to sub-models with corresponding ultimate periodicity. For representation convenience we define the domain $\mathbb {T}_{a,b} = \{0,1, \ldots , b-1, b^\infty , (b+1)^\infty ,\ldots , (a+b-1)^\infty \}$ featuring recurrent time symbols $t^\infty$ for $t=b, b+1, \ldots ,a+b-1$. For an arbitrary signal w and element $t^\infty \in \mathbb {T}_{a,b}$, we define $w[t^\infty ]$ with $w[t^\infty ] = 1$ iff $w[t + a\, n] = 1$ for all $n\in \mathbb {N}$. Any ultimately-periodic signal over $\mathbb {T}=\mathbb {N}$ with corresponding period and prefix may be seen without loss of generality as a signal over $\mathbb {T}_{a,b}$.

In the continuous case, uniformly bounding the variability does not even guarantee the existence of a minimal sub-model.

Example 3

(MTL). The formula $\varphi =p {{\mathrm{\mathcal {U}}}}\mathrm {true}$ has no minimal sub-model over the dense time domain [0, 1). Consider the monotone sequence $(v_i)$ of sub-models of $\varphi$ with variability 1, and domain $(0, \frac{1}{i+1}] \times \{p\}$. The sub-signal $\sqcap _{i \in \mathbb {N}} v_i = \bot$ is not a sub-model of $\varphi$.

To overcome limit problems we extend the temporal domain $\mathbb {T}= [0,d)$ to non-standard reals taken in $\mathbb {T}^+=\{ t^+ ~:~t \in \mathbb {T}\}$ and $\mathbb {T}^- = \{t^- ~:~t \in (0,d] \}$, with $\mathbb {T}^*=\mathbb {T}\cup \mathbb {T}^+ \cup \mathbb {T}^-$. We note $w[t^+]$ the right limit of some signal w at time t and $w[t^-]$ its left limit. Any finite variability signal over $\mathbb {T}=[0,d)$ may be extended this way to a signal over $\mathbb {T}^*$.

3.4 Temporal Implicants

We now introduce sentences based on (possibly infinite) conjunctions of unary predicates p[t] and their negation $\lnot p[t]$ for t in some domain $\mathbb {D}$, that we will take to be $\mathbb {T}_{a,b}$ or $\mathbb {T}^*$.

Definition 4

(Terms, Implicants and Prime Implicants). Temporal terms are are defined using the grammar

$$\begin{aligned} \gamma :=p[t] ~|~ \lnot p[t] ~|~ \gamma \wedge \gamma ~|~ \bigwedge _{t\in D} \theta [t] \end{aligned}$$

where $p \in \mathbb P$ is a propositional variable, t is a time in $\mathbb {D}$, D is a subset of $\mathbb {D}$, and $\theta$ a function from $\mathbb {D}$ to temporal terms. The semantics $\models$ of temporal terms relative to a signal w are as expected for predicates and binary conjunctions, and for the case of general conjunctions are given by

$$\begin{aligned} w \models \bigwedge _{t\in D} \theta [t] \ \leftrightarrow \ \forall t \in D,\, w\,\models \,\theta [t] \end{aligned}$$

An implicant of some temporal formula $\varphi$ is a temporal term $\gamma$ such that $\gamma \Rightarrow \varphi$. We talk of prime implicant when $\gamma$ is maximal with respect to $\Rightarrow$.

The above definition of temporal terms is very general, allowing arbitrary functions $\theta$ under infinite conjunctions. However temporal terms can always be written in a simpler normal form as follows, which is straightforward to prove by structural induction.

Proposition 1

(Normal Form). For every temporal term there exists an equivalent temporal term of the form $\bigwedge _{\ell \in L} \bigwedge _{t \in T_\ell } \ell [t]$, where L is the set of propositional literals over $\mathbb P$. Assuming L is ordered this normal form is unique.

For any term $\gamma$ we will write $\bigwedge _{\ell \in L} \bigwedge _{t \in V^\gamma _\ell } \ell [t]$ its normal form. Then given arbitrary terms $\alpha$ and $\beta$, it holds $\alpha \Rightarrow \beta$ if and only if $V^\beta _\ell \subseteq V^\alpha _\ell$ for all $\ell \in L$. Notably $\Rightarrow$ defines a partial order over normal form terms.

It is clear that normal form temporal terms are analogous to sub-signals over $\mathbb {D}$. By considering such terms over domains $\mathbb {D}= \mathbb {T}_{a,b}$ and $\mathbb {D}= \mathbb {T}^*$ we obtain the existence of at least one prime implicant for every satisfiable LTL and MTL formula respectively. Recall that we use full discrete semantics over $\mathbb {T}= \mathbb {N}$, and finite variability continuous semantics over $\mathbb {T}= [0,d)$.

Proposition 2

(Existence of Prime Implicants). For any LTL formula $\varphi$ and sequence w with period a and prefix b such that $w \models \varphi$ there exists a prime implicant $\gamma$ of $\varphi$ over $\mathbb {T}_{a,b}$ such that $w \models \gamma$. For any MTL formula $\varphi$ and signal w such that $w \models \varphi$ there exists a prime implicant $\gamma$ of $\varphi$ over $\mathbb {T}^*$ such that $w \models \gamma$.

Proof

Let us note $\varGamma$ the set of implicants $\gamma$ of $\varphi$ such that $w \models \gamma$, that we may assume in normal form. In both discrete and continuous cases, w seen as a temporal term is itself an implicant of $\varphi$. This gives us $\varGamma \ne \emptyset$.

• In the discrete case $\varGamma$ is finite, so that there exists of a maximal element of $\varGamma$ relative to $\Rightarrow$, which proves our proposition.

• In the continuous case, we demonstrate the existence of a maximal element of $\varGamma$ relative to $\Rightarrow$ by direct application of Zorn’s Lemma as follows.

Consider $\varDelta$ an arbitrary totally ordered subset of $\varGamma$. First we can see that $\varDelta$ is bounded by the temporal term $\alpha = \bigwedge _{\ell \in L} \bigwedge _{t \in U_\ell } \ell [t]$, where each $U_\ell = \bigcap _{\gamma \in \varDelta } \overline{V^\gamma _\ell }$ is the intersection over all $\gamma \in \varDelta$ of the closure of $V^\gamma _\ell$ in $\mathbb {T}^*$. This does not pose any difficulty. We then show that moreover $\alpha \in \varGamma$ so that $\gamma$ is indeed an upper bound of $\varDelta$ in $\varGamma$. For that we need to show $w \models \alpha$ which is trivial, and to show $\alpha \Rightarrow \varphi$. To demonstrate the latter fact we take $w'$ an arbitrary model of $\alpha$ and prove the existence of some $\gamma \in \varDelta$ such that $w' \models \gamma$. As $\varDelta \subseteq \varGamma$ we will then have $w' \models \varphi$ by definition of $\varGamma$.

Assume, in search of a contradiction that $w' \not \models \gamma$ for all $\gamma \in \varDelta$. For each $\gamma \in \varDelta$ there exists $\ell \in L$ and $t \in V_\ell ^\gamma$ such that $w'_\ell [t] = 0$. We may construct a sequence $(\gamma _i, \ell _i, t_i)$ of $\varDelta \times L \times \mathbb {T}^*$ such that $t_i \in V^\gamma _{\ell _i}$ and $w'_{\ell _i}[t_i] = 0$ for all $i \in \mathbb {N}$, and such that $(\gamma _i)$ is monotone and diverging, that is $\gamma _i \Rightarrow \gamma _j$ if $i \le j$, and for all $\gamma \in \varDelta$ there exists $i \in \mathbb {N}$ such that $\gamma \Rightarrow \gamma _i$. We take $s_i \in \mathbb {T}$ the standard part of $t_i$, that is $t_i \in \{s_i^+, s_i^-, s_i\}$. As L is finite, we can safely assume that the sequence $(\ell _i)$ is constant. As $\mathbb {T}$ is bounded, by Bolzano-Weierstrass Theorem we may in turn assume that the sequence $(s_i)$ is monotone and convergent, an assumption that we extend to $(t_i)$. Let us note $\ell$ the value of $(\ell _i)$, and t the limit of $(t_i)$. As $(\gamma _i)$ is monotone, the subsequence of times $(t_j)_{j \ge i}$ has all its values in $V_\ell ^{\gamma _i}$, so that $t \in \overline{V_\ell ^{\gamma _i}}$. In particular $t \in \bigcap _{i \in \mathbb {N}} \overline{V^{\gamma _i}_\ell } = \bigcap _{\gamma \in \varDelta } \overline{V_\ell ^\gamma } = U_\ell$ given that $(\gamma _i)$ is diverging. Then $t \in U_\ell$ yields $w'_\ell [t] = 1$. By finite variability of $w'$, as $(t_i)$ converges to t there exists i such that $w'_\ell [t_i]= 1$. Yet $w'[t_i] = 0$ by hypothesis. Contradiction! Therefore there exists $\gamma \in \varDelta$ such that $w' \models \gamma$.

4 MTL Diagnostics

In this section, we propose an effective procedure to compute implicants of an MTL formula $\varphi$ relative to a multi-dimensional signal $w : [0,d) \times \mathbb P\rightarrow \mathbb {B}$ of length d. First, note that the satisfaction signal $w_\varphi$ of a given formula $\varphi$ relative to a finite variability signals w has itself finite variability, the variability of satisfaction signals growing at most quadratically with the size of the formula. Like satisfaction, an explanation for a temporal formula is time dependent and should be a function from the time domain to formulas that explain satisfaction or violation at some time t. Analogously to the notion of satisfaction signal $w_\varphi : \mathbb {T}\rightarrow \mathbb {B}$ we define the notion of explanation signal noted $E(\varphi )$ such that $E(\varphi )[t]$ explains the satisfaction of $\varphi$ by w at time $t \in \mathbb {T}$. We then construct explanations through definitions of $E(\varphi )[t]$ and its dual $F(\varphi )[t]$, which are inductive on the structure of formula $\varphi$, and on the times t at which explanations of its sub-formulas are required. We are able to guarantee finite representation by producing finite variability explanation signals. We use selection functions $\xi _\varphi$ to relate the truth of some formula $\varphi$ at time t with the truth of its sub-formulas at some time $\xi _\varphi [t]$. Arbitrary selection functions may yet lead to explanations which are almost as large as the signal itself, however we can find selection functions that allow best “explanation sharing”. For instance given a non-singular interval I the same $t'$ may belong to $t \oplus I$ for every t in some interval T. Hence a selection function satisfying $\xi _\varphi [t]=t'$ for every $t\in T$ will use only one point to witness the satisfaction of $\varphi =\lozenge _{I} \psi$ throughout T.

4.1 Non-Standard MTL Semantics

The relation $<$ over the reals of $\mathbb {T}$ naturally extends to $\mathbb {T}^*$ with $t^- < t < t^+$. We then define over $\mathbb {T}^*$ the relation $\ll$ with $t \ll t'$ if and only if $t < t'$ or $t = t' \notin \mathbb {R}$. Interval notations using angled parentheses are introduced with $\langle t, t'\rangle = \{ t'' ~:~t \ll t'' \ll t' \}$ and $[t,t'\rangle = \{ t'' ~:~t \le t'' \ll t' \}$. The sum of symbolic limit $t^+$, respectively $t^-$, and a real number a is taken as $(t + a)^+$, respectively $(t + a)^-$. The sum $t \boxplus I$ of some $t \in \mathbb {T}^*$ and a real interval I is then defined as the closure in $\mathbb {T}^*$ of $t \oplus I$, and the difference $t \boxminus I$ is defined similarly.

We extend the satisfaction relation for temporal formulas to non-standard reals by writing $(w,t) \models \varphi$ if $w_\varphi [t] = 1$. Now conditions induced by timed eventually, and until operators can be expressed in terms of closed intervals of $\mathbb {T}^*$.

Lemma 1

For any formula $\varphi$, $\psi$, (finite variability) signal w, and time or symbolic limit $t \in \mathbb {T}^*$ we have

• $(w,t) \models \lozenge _{I} \varphi$ if and only if there exists $t'$ in $t \boxplus I$ such that $(w,t') \models \varphi$;

• $(w,t) \models \varphi {{\mathrm{\mathcal {U}}}}\psi$ if and only if there exists $t' \gg t$ such that $(w,t') \models \psi$ and for all $t'' \in \langle t,t' \rangle$ it holds $(w,t'') \models \varphi$.

4.2 Explanation Operators

We may now formally define operators $E(\varphi )[t]$ and $F(\varphi )[t]$ providing explanations of $\varphi$, or $\lnot \varphi$ relative to signal w at time $t \in \mathbb {T}^*$ in the form of temporal terms. The explanation of a formula $\varphi$ relative to a signal w is then given by the application of E or F at time 0 as follows. We let

$$\begin{aligned} {\text {Exp}}(\varphi ) = \left\{ \begin{array}{l l} E(\varphi )[0] &{} \quad \text {if } (w,0)\,\models \,\varphi \\ F(\varphi )[0] &{} \quad \text {otherwise} \end{array} \right. \end{aligned}$$

with

where $\xi _{\varphi \vee \psi }$ from $\mathbb {T}^*$ to formulas, $\xi _{\lozenge _{I} \varphi }$ and $\xi _{\varphi {{\mathrm{\mathcal {U}}}}\psi }$ from $\mathbb {T}^*$ to $\mathbb {T}^*$ are selection functions such that for all $t \in \mathbb {T}^*$, it holds $\xi _{\varphi \vee \psi }[t] \in \{ \varphi , \psi \}$, $\xi _{\lozenge _{I} \varphi }[t] \in t \boxplus I$ and $\xi _{\varphi {{\mathrm{\mathcal {U}}}}\psi }[t] \gg t$.

We say that a selection function $\xi _{\varphi }$ is correct with respect to w if for all $t \in \mathbb {T}^*$ such that $(w,t) \models \varphi$ we have

• $(w,t) \models \xi _{\varphi }[t]$ when $\varphi$ is of the form $\varphi _1 \vee \varphi _2$;

• $(w, \xi _\varphi [t]) \models \psi$ when $\varphi$ is of the form $\lozenge _{I} \psi$;

• $(w, \xi _\varphi [t]) \models \varphi _2$ and $\forall t' \in \langle t,\xi [t] \rangle ,\ (w,t') \models \varphi _1$ when $\varphi$ is of the form $\varphi _1 {{\mathrm{\mathcal {U}}}}\varphi _2$.

The following result is straightforward to prove from Lemma 1.

Theorem 1

(Soundness). A term Exp$(\varphi )$, correct with respect to signal w is a solution to the diagnostics problem of $\varphi$ with respect to w.

Moreover, given finite variability selection functions our explanations can be effectively represented.

Proposition 3

(Finite Representation). Assuming all selection functions are finitely variable, the term Exp$(\varphi )$ has a normal form $\bigwedge _{\ell \in L} \bigwedge _{t' \in T_\ell } \ell [t']$ such that each $T_\ell$ is a finite union of intervals of $\mathbb {T}^*$.

4.3 Computation of Selection Functions

We describe procedures that define explicit instances of selection functions, and satisfying the correctness and finite variability criteria. The explanation operators can be made constructive when the normalization of the terms they produce is interleaved with the instantiation of selection functions over intervals appearing in the normalization process. It is indeed sufficient to define selection functions piecewise on closed intervals T of $\mathbb {T}^*$. Furthermore we can assume that for such intervals T, formula $\varphi$ holds for all $t \in T$ as the correctness assumption is void outside such intervals, with the finite variability assumption then trivial to match.

Disjunction. Consider the formula $\varphi \vee \psi$ and the signal w. A finitely variable selection function $\xi _{\varphi \vee \psi }$ and correct with respect to w can be constructed as follows. By finite variability hypothesis on w, the satisfaction signal $w_{\varphi , \psi }: \mathbb {T}\rightarrow \mathbb {B}$ has finite variability over any interval T where $\varphi \vee \psi$ holds. We partition T in k maximally uniform intervals $T_i$, and take $\xi _{\varphi \vee \psi }[t] = \varphi$ over intervals $T_i$ where $(w,t) \models \varphi$, and $\xi _{\varphi \vee \psi }[t] = \psi$ over other intervals. The function $\xi _{\varphi \vee \psi }$ is uniform over all $T_i$, so has finite variability.

Timed Eventually. Now consider the formula $\lozenge _{I} \varphi$ for I non-singular and the signal w, and assume that the formula is satisfied over some interval T. We build a procedure that generates a small set of witnesses of $\varphi$ accounting for the satisfaction of $\lozenge _{I} \varphi$ by w over T. The satisfaction of $\lozenge _{I} \varphi$ over T can be explained by the satisfaction of $\varphi$ at some time points within the interval $T \boxplus I = \bigcup _{t \in T} t\boxplus I$, and in particular the satisfaction of $\varphi$ at some $s \in T \boxplus I$ provides a sufficient explanation for the satisfaction of $\lozenge _{I} \varphi$ for all $t \in (s \boxminus I) \cap T$. We use these two observations to generate a piecewise constant selection function $\xi _{\lozenge _{I} \varphi }$ defined over T and correct relative to a signal w.

Fig. 2.

(a) Algorithm to find a correct instance of $\xi _{\lozenge _{I} \varphi }$ over T relative to signal w; (b) Example of R and s computation for $\lozenge _{I} \varphi$.

We present the procedure in Fig. 2-(a); it works as follows. The selection function is initialized (line 1) as nowhere defined. In every iteration of the main while loop (line 2), we find a time domain $S = (t \boxplus I) \cap \{ t' ~:~(w,t') \models \varphi \}$ such that $\varphi$ is satisfied inside S and any point in S provides a sufficient (Lemma 1) explanation for the satisfaction of $\lozenge _{I} \varphi$ at t taken as the earliest time of T. Such set S is obtained directly from the satisfaction signal $w_\varphi$, that we suppose already computed by the monitoring procedure. We then take s the latest time of S, which constitutes a minimal subset of S sufficient to explain the satisfaction of $\lozenge _{I} \varphi$ throughout the domain $s \boxminus I$; when intersected with T it gives R, a prefix of T. At the end of the iteration, the definition of $\xi _{\lozenge _{I} \varphi }$ over the interval R is taken as s, which we may write $R \times \{s\}$ identifying selection functions with subsets of $\mathbb {T}^* \times \mathbb {T}^*$ (line 7). The covered prefix R can be removed from T (line 8). The procedure terminates when T the domain remaining to cover becomes empty.

Untimed Until. Consider the formula $\varphi {{\mathrm{\mathcal {U}}}}\psi$ and the signal w and assume that the formula is satisfied over T, taken without loss of generality to be a closed interval of $\mathbb {T}^*$. For $t\in \mathbb {T}^*$, similarly to the case of timed eventually a single witness $t'\gg t$ of $\psi$ along with a uniform interval $\langle t,t' \rangle$ where $\varphi$ holds is sufficient to explain the satisfaction of $\varphi {{\mathrm{\mathcal {U}}}}\psi$ over the whole interval $[t,t'\rangle$. With such observations we generate a piecewise constant selection function $\xi _{\varphi {{\mathrm{\mathcal {U}}}}\psi }$ correct with respect to some signal w and defined over T. We make use of a subroutine $W(\varphi , \psi , t)$ that returns the set of witnesses of $\psi$ in signal w that are sufficient to explain $\varphi {{\mathrm{\mathcal {U}}}}\psi$ at time $t \in \mathbb {T}^*$ where $\varphi {{\mathrm{\mathcal {U}}}}\psi$ holds. Thanks to Lemma 1 we have $W(\varphi , \psi , t) = \{ t' \gg t ~:~(w,t') \models \psi \ \text { and } \forall t'' \in \langle t,t' \rangle ,\, (w,t'') \models \varphi \}$. Assuming the satisfaction signals $w_\varphi$ and $w_\psi$ given by the monitoring algorithm, the procedure $W(\varphi , \psi , t)$ can be realized as follows. First decompose the domain $\{ t' \in \mathbb {T}^* ~:~t' \gg t \}$ as a finite partition into uniform intervals of $\mathbb {T}^*$ with respect to $w_{\varphi , \psi }$ that we can assume of the form $[t_i, t_i]$ and $(t_i, t_{i+1})$ with $(t_i)_{i \le n}$ an ordered sequence of times. Start from the interval containing $t_0 = t$ and iterate through intervals, accumulating intervals where $\psi$ holds, until $\varphi$ stops holding at $[t_i,t_i]$ or $(t_{i},t_{i+1})$, or we reach the interval containing $t_n=d^-$ marking the end of the time domain.

Fig. 3.

(a) Algorithm to find a correct instance of $\xi _{\varphi {{\mathrm{\mathcal {U}}}}\psi }$ over T relative to signal w; (b) Example of R and s computation for $\varphi {{\mathrm{\mathcal {U}}}}\psi$.

We present the main procedure to compute the selection function in Fig. 3-(a). The procedure first assigns $\xi _{\varphi {{\mathrm{\mathcal {U}}}}\psi }$ the empty function $\emptyset$ (line 1). In every iteration of the while loop, we compute an interval S whose elements s are witnesses of $\psi$ providing sufficient explanation for the satisfaction of the $\varphi {{\mathrm{\mathcal {U}}}}\psi$ throughout $[t,s\rangle$. When S lies entirely outside T we take s to be the earliest suitable witness of $\psi$, so as not to impose a condition on $\varphi$ beyond it (line 5). When S intersects with T on the contrary we look for the latest suitable witness of $\psi$ in their intersection (line 6). As a direct corollary of Lemma 1 the interval $R = [t,s\rangle \cap T$ is now accounted for, hence we define $\xi _{\varphi {{\mathrm{\mathcal {U}}}}\psi }$ as taking the value s over interval R (line 8). Eventually R can be removed from T for the next iteration (line 9), and the procedure terminates when T becomes empty.

4.4 Discussion

Our procedure does not guarantee minimality, with for instance propositional tautologies not being recognized. However we obtain some form of temporal minimality through the proposed construction for selection functions. Intuitively each time a witness is required we select the furthest away, which maximizes the interval over which that witness is valid. Let $\varphi$ be an eventually or until formula, w a trace such that $\varphi$ holds for w on some domain T. We claim that selection functions $\xi _\varphi$ constructed by our algorithms choose a set of witnesses $\xi _\varphi [T] = \{ \xi _\varphi [t] ~:~t \in T \}$ that is minimal relative to w.

The main advantage of our explanation principle is its hierarchical character: every sub-formula has its own explanation, which is then used in turn to account for the satisfaction or violation of its super-formulas. This makes the process of fault-finding transparent: if the fault lies in the specification then it can be localized syntactically, otherwise it lies in the system in which case the explanation of each sub-formula provides important insight on what went wrong. This also allows to solve the diagnostics problem efficiently. Under a uniform bounded variability assumption, computing Exp$(\varphi )$ with our algorithms takes time quadratic in the size of the formula, linear in the size of the input signal. The minimal diagnostics problem has a higher complexity. By reduction to the satisfiability of Bounded-MTL [3], minimal diagnostics is EXPSPACE-hard in the combined input size.

Let us now illustrate the overall process of deriving an explanation.

Example 4

We take $\varphi$ the formula $\lozenge _{[1,2]} {{\mathrm{\square }}}(p \rightarrow \lnot (q {{\mathrm{\mathcal {U}}}}r))$, and $w: [0,6) \rightarrow \mathbb {B}^{3}$ the right-continuous signal illustrated in Fig. 4. The top-down computation of Exp$(\varphi )$ is shown in terms of sub-signals, inductively extracted from satisfaction signals. We found the diagnostics Exp$(\varphi ) \Leftrightarrow \bigwedge _{t \in (2,3]} \lnot r[t] \wedge \bigwedge _{t \in [3,3]} \lnot q[t] \wedge \bigwedge _{t \in [3,6)} \lnot p[t]$. It reads as follows: r is false between 2 and 3, q is false at time 3 and p is false from 3 onwards.

Fig. 4.

Computing Exp$(\varphi )$, for $\varphi = \lozenge _{[1,2]} {{\mathrm{\square }}}(p \rightarrow \lnot (q {{\mathrm{\mathcal {U}}}}r))$.

5 LTL Ultimately-Periodic Diagnostics

Our explanation scheme for LTL formulas solves the diagnostics problem with respect to an ultimately-periodic sequence w with period a and prefix b. The first remark we make is that the satisfaction sequence $w_\varphi$ of any LTL formula $\varphi$ is then also ultimately-periodic. Let us say that a property $\varphi$ is future if for any sequence w and time constant a it holds $(w,a) \models \varphi$ iff $w^{a..} \models \varphi$. It is trivial to check that given an ultimately periodic sequence, future properties have a satisfaction sequence that preserves the prefix and period. Following this remark we may assume that we dispose of the satisfaction sequences for each sub-formula. We refer the reader to [12] for the monitoring of ultimately-periodic sequences.

5.1 Recurrent LTL Semantics

We equip $\mathbb {T}_{a,b}$ with a pseudo-successor function ${{\mathrm{\widetilde{+}}}}1$ that we define by

$$\begin{aligned} t {{\mathrm{\widetilde{+}}}}1&= t + 1&\text { for } t < b-1\\ t^\infty {{\mathrm{\widetilde{+}}}}1&= (t + 1)^\infty&\text { for } b \le t < a+b-1\\ (b-1) {{\mathrm{\widetilde{+}}}}1&= (a+b-1)^\infty {{\mathrm{\widetilde{+}}}}1 =b^\infty&\end{aligned}$$

The $n^\text {th}$ successor of a symbolic time $t \in \mathbb {T}_{a,b}$ is then given by

$$\begin{aligned} t {{\mathrm{\widetilde{+}}}}0&= t&\\ t {{\mathrm{\widetilde{+}}}}n&= (t {{\mathrm{\widetilde{+}}}}1) {{\mathrm{\widetilde{+}}}}(n-1)&\text { for } n \ge 1 \end{aligned}$$

We further define on $\mathbb {T}_{a,b}$ a preorder relation $\preceq$ such that $t \preceq t'$ if and only if there exists $n \ge 0$ such that $t'=t {{\mathrm{\widetilde{+}}}}n$. The usual interval notations $[t,t')$ are extend to arbitrary $t,t' \in \mathbb {T}_{a,b}$ by letting $[t,t') = \{ t'' ~:~\exists n \ge 0,\, t''=t {{\mathrm{\widetilde{+}}}}n \text { and } \forall k \le n,\, t {{\mathrm{\widetilde{+}}}}k \ne t' \}$. The semantics of LTL are extended to recurrent times by writing $(w,t^\infty ) \models \varphi$ if $(w, t + a\,n) \models \varphi$ for all $n \in \mathbb {N}$. We then have the following implications.

Lemma 2

For any formula $\varphi$, $\psi$, sequence w, and symbolic time $t \in \mathbb {T}_{a,b}$ we have

• $(w,t) \models {{\mathrm{\bigcirc }}}\varphi$ if $(w, t {{\mathrm{\widetilde{+}}}}1) \models \varphi$;

• $(w,t) \models \varphi {{\mathrm{\mathcal {U}}}}\psi$ if there exists $t' \succeq t$ such that $(w,t') \models \psi$ and $(w,t'') \models \varphi$ for all $t'' \in [t,t')$.

Note that when w is ultimately-periodic with period a and prefix b, the preceding formulas are satisfied if and only if the corresponding conditions hold.

5.2 Explanation Operators

The explanation scheme for LTL is also derived from the propositional one by making operators E and F time dependent. Such operators take a formula $\varphi$ and a symbolic time $t \in \mathbb {T}_{a,b}$, and return propositional terms over unary predicates $p[t']$ with $p \in \mathbb P$ and $t' \in \mathbb {T}_{a,b}$. The explanation Exp is then given by E or F at time 0 as follows. We let

$$\begin{aligned} {\text {Exp}}(\varphi ) = \left\{ \begin{array}{ll}E(\varphi )[0] &{}\text { if } w\,\models \,\varphi \\ F(\varphi )[0] &{} \text { otherwise}\end{array}\right. \end{aligned}$$

with

where $\xi _{\varphi \vee \psi }$ from $\mathbb {T}_{a,b}$ to formulas, and $\xi _{\varphi {{\mathrm{\mathcal {\tilde{U}}}}}\psi }$ from $\mathbb {T}_{a,b}$ to $\mathbb {T}_{a,b}$ are selection functions such that for all $t \in \mathbb {T}_{a,b}$, it holds $\xi _{\varphi \vee \psi }[t] \in \{ \varphi , \psi \}$ and $\xi _{\varphi {{\mathrm{\mathcal {\tilde{U}}}}}\psi }[t] \succeq t$.

We say that a selection function $\xi _{\varphi }$ is correct with respect to w if for all $t \in \mathbb {T}_{a,b}$ such that $(w,t) \models \varphi$ we have

• $(w,t) \models \xi _{\varphi }[t]$ when $\varphi$ is of the form $\varphi _1 \vee \varphi _2$,

• $(w, \xi _\varphi [t]) \models \varphi _2$ and $\forall t' \in [t,\xi [t]),\ (w,t') \models \varphi _1$ when $\varphi$ is of the form $\varphi _1 {{\mathrm{\mathcal {\tilde{U}}}}}\varphi _2$.

Correct selection functions can easily be constructed, knowing that the domain $\mathbb {T}_{a,b}$ is finite. The following result is straightforward to prove from Lemma 2.

Theorem 2

(Soundness). Under the assumption that selection functions are correct with respect to w, Exp$(\varphi )$ is a solution to the diagnostic problem of $\varphi$ and w.

We now give an example of diagnostic produced by our explanation principle.

Example 5

Let $\varphi$ be the formula $r \rightarrow {{\mathrm{\bigcirc }}}{{\mathrm{\square }}}(p {{\mathrm{\mathcal {\tilde{U}}}}}\lnot q)$ and $w: \mathbb {N}\rightarrow \mathbb {B}^3$ be the sequence with period 4 and prefix 2 defined by the following $\omega$-regular expression:

$$\begin{aligned}p\, q\, r \cdot p\, q\, r \cdot ( \overline{p}\, \overline{q}\, \overline{r} \cdot p\, q\, \overline{r} \cdot \overline{p}\, \overline{q}\, r \cdot p\, q\, r )^\omega \end{aligned}$$

We find Exp$(\varphi ) = p[1] \wedge \lnot q[2^\infty ] \wedge p[3^\infty ] \wedge \lnot q[4^\infty ] \wedge p[5^\infty ]$, which may be written as the $\omega$-regular language $\mathrm {true}\cdot p \cdot (\overline{q} \cdot p \cdot \overline{q} \cdot p)^\omega$.

6 Conclusion and Perspectives

We have enriched MTL monitoring, and LTL model checking techniques with a focused analysis of the causes of satisfaction/violation of such a specification by a given temporal behavior. For monitoring applications we plan to develop an online version of our algorithms, which may then be integrated in the monitoring procedure to allow fault analysis on a simulation, or even a real execution without having to save all of the monitored signals. Looking more generally at temporal implicants it would be interesting to study alternative formulations, based on the desiderata of [2] that list atomicity of literals, closure under intersection, duality with implicates, etc. Our approach to diagnosis may then transfer to other problems, such as fault localization where a system model is assumed to be available.