Causality for General LTL-definable Properties

TL;DR

This paper extends causality analysis to infinite counterexamples in LTL properties, enabling better understanding of violations in complex temporal logic specifications.

Contribution

It introduces a causality notion for infinite LTL counterexamples, building on previous finite-trace approaches, and aims for implementation in a causality checking tool.

Findings

Causality for infinite LTL counterexamples is characterized.

Loop unfolding in lasso-shaped traces reveals causal event sequences.

Framework is designed for integration with LTL model checking tools.

Abstract

In this paper we provide a notion of causality for the violation of general Linear Temporal Logic (LTL) properties. The current work is a natural extension of the previously proposed approach handling causality in the context of LTL-definable safety properties. The major difference is that now, counterexamples of general LTL properties are not merely finite traces, but infinite lasso-shaped traces. We analyze such infinite counterexamples and identify the relevant ordered occurrences of causal events, obtained by unfolding the looping part of the lasso shaped counterexample sufficiently many times. The focus is on LTL properties from practical considerations: the current results are to be implemented in QuantUM, a tool for causality checking, that exploits explicit state LTL model checking.

Equations

$$\varphi ,{\varphi }_1,{\varphi }_2::=true\mid a\mid {\varphi }_1\mid {\varphi }_2\mid {\varphi }_1\&{\varphi }_2\mid \sim \varphi \mid X\varphi \mid {\varphi }_{1}U{\varphi }_2\mid ◊\varphi \mid \square \varphi (a\in AP)$$

$$\varphi ,{\varphi }_1,{\varphi }_2::=\top \mid a_{\alpha }\mid \neg \varphi \mid {\varphi }_1\wedge {\varphi }_2\mid {\varphi }_1\vee {\varphi }_2(a_{\alpha }\in \mathcal{A}).$$

$$\psi ,{\psi }_1,{\psi }_2::=\varphi \mid {\psi }_1\text{wedgedot}{\psi }_2\mid {\psi }_1{\text{wedgedot}}_{\text{less}}\varphi {\text{wedgedot}}_{\text{gtr}}{\psi }_2\mid {\psi }_1\wedge {\psi }_2\mid {\psi }_1\vee {\psi }_2$$

$$\theta ::=\psi \mid \varphi {\text{wedgedot}}_{]}\theta \mid \theta {\text{wedgedot}}_{[}\varphi$$

$$\xi ::=\theta {\text{wedgedot}}^{\omega }\psi$$

$$\sigma =s_0\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\xi =a_{{\alpha }_1}{\text{wedgedot}}^{\omega }(a_{{\alpha }_2}\text{wedgedot}{a}_{{\alpha }_3})$$

$${\sigma }_1=s_0\stackrel{{\alpha }_1}{\to }{s}_1\stackrel{{\alpha }_2}{\to }{s}_2\stackrel{{\alpha }_3}{\to }{s}_1$$

$${\sigma }_2=s_1\stackrel{{\alpha }_2}{\to }{s}_2\stackrel{{\alpha }_3}{\to }{s}_1\stackrel{{\alpha }_2}{\to }{s}_2\stackrel{{\alpha }_3}{\to }{s}_1$$

$${\xi }^{\prime \prime }=a_{{\alpha }_1}\text{wedgedot}{a}_{{\alpha }_3}\text{wedgedot}{a}_{{\alpha }_2}\text{wedgedot}{a}_{{\alpha }_3}\text{wedgedot}{a}_{{\alpha }_2}{\text{wedgedot}}^{\omega }(a_{{\alpha }_2}\text{wedgedot}{a}_{{\alpha }_3}\text{wedgedot}{a}_{{\alpha }_2}\text{wedgedot}{a}_{{\alpha }_2}\text{wedgedot}{a}_{{\alpha }_2}).$$

$$\begin{array}[]{rcl}\sigma_{1}&=&s_{0}\xrightarrow{\alpha_{1}}s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}\\ \sigma_{2}&=&s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}\end{array}$$

$$\sigma =E_0{B}_2(B_1{E}_1{B}_0{E}_0{)}^{\omega }$$

$${\sigma }^{\prime }=E_0{B}_2(B_1{E}_1{E}_2{B}_0{E}_0{)}^{\omega }$$

$$va{l}_{\mathcal{M}}(\sigma ):=\{a_{\alpha }\in \mathcal{M}:\sigma {\models }_e{a}_{\alpha }\}.$$

$$\begin{array}[]{rr@{}c@{}l}\sigma^{\prime\prime}=E_{0}B_{2}E_{2}(B_{1}E_{1}B_{0}E_{0})^{\omega}&\xi_{\sigma}=(E0\wedgedot B2\wedgedot_{[}\lnot E2)&\,\,{\wedgedot}^{\omega}&(B1\wedgedot E1\wedgedot B0\wedgedot E0)\\ \sigma^{\prime\prime}=E_{0}B_{2}(B_{1}E_{1}E_{2}B_{0}E_{0})^{\omega}&\xi_{\sigma}=(E0\wedgedot B2\wedgedot_{[}\lnot E2)&\,\,{\wedgedot}^{\omega}&(B1\wedgedot E1{\wedgedot_{\less}\,}{\lnot E2}{\,\wedgedot_{\gtr}}B0\wedgedot E0)\\ \sigma^{\prime\prime}=E_{0}B_{2}(B_{1}E_{1}B_{0}E_{2}E_{0})^{\omega}&\xi_{\sigma}=(E0\wedgedot B2\wedgedot_{[}\lnot E2)&\,\,{\wedgedot}^{\omega}&(B1{\wedgedot_{\less}\,}{\lnot E2}{\,\wedgedot_{\gtr}}E1{\wedgedot_{\less}\,}{\lnot E2}{\,\wedgedot_{\gtr}}B0\wedgedot E0)\\ \sigma^{\prime\prime}=E_{0}B_{2}(B_{1}E_{1}E_{2}B_{0}E_{0})^{\omega}&\xi_{\sigma}=(E0\wedgedot B2\wedgedot_{[}\lnot E2)&\,\,{\wedgedot}^{\omega}&(B1{\wedgedot_{\less}\,}{\lnot E2}{\,\wedgedot_{\gtr}}E1{\wedgedot_{\less}\,}{\lnot E2}{\,\wedgedot_{\gtr}}B0{\wedgedot_{\less}\,}{\lnot E2}{\,\wedgedot_{\gtr}}E0)\\ \ldots\end{array}$$

$${\xi }_{\sigma }=(B2{\text{wedgedot}}_{[}\neg E2){\text{wedgedot}}^{\omega }(\neg E2)$$

$$\{(a_{{\alpha }_i},a_{{\alpha }_j})\mid a_{{\alpha }_i}\text{wedgedot}{a}_{{\alpha }_j}\text{ occurs in }\xi \}.$$

Full text

1 Introduction

The importance and complexity of software driven systems is steadily increasing. Software plays a central rôle in daily used objects, such as computers and mobile phones, but also in other areas, for example medical systems, aircraft and automobiles. Particularly in these latter areas, software failures may entail major environmental harm and/or serious injuries of humans. Software systems whose malfunction has such serious consequences are also called safety-critical systems. This paper addresses methods to analyze models of such systems for the detection of ordered sequences of events that can be considered causal for the malfunctioning of such a system. Of particular importance in this setting is the identification of actual causes, i.e., sequences of events that are indispensable for the malfunctioning to occur and not just mere “noise” in the system execution.

Model-checking [2] is a formal verification technique for systematically checking whether certain temporal requirements are satisfied by a system model. Given a state-based model $M$ of the considered system and a property specification $\varphi$, model checkers return a counterexample if $\varphi$ is not satisfied by $M$. This counterexample typically is an execution trace that includes a violation of the property $\varphi$ and can be used to understand the cause of the property violation and to fix the problem. However, counterexamples can be very long and often contain numerous events that are of no relevance to the violation of $\varphi$. Furthermore, there can be a very large number of counterexample traces in $M$ that all lead to the violation of $\varphi$.

In precursory work [21, 20], model checking of reachability properties has been extended to causality checking by considering all traces in a model that violate a system safety property expressed by a reachability property $\varphi$. Inspired by the actual cause conditions defined in the Structural Equation Model (SEM) for causality in systems [16, 15] the work in [21, 20] defines actual cause conditions on ordered sequences of events that correspond to computations in a Transition System model.

In this paper we provide a notion of causality for the violation of general Linear Temporal Logic (LTL) properties. Counterexamples of such properties can always be represented by $\omega$-regular expressions of the form $uv^{\omega}$, where $u$ and $v$ are regular expressions [23]. Counterexamples of this type are also often referred to as “lasso-shaped”. They consist of an initial path fragment that can witness the violation of a “something bad never happens”-kind of property (i.e., a safety property) followed by a loop that can witness the violation of a “something good eventually happens”-kind of property (i.e., a liveness property). In particular, for the case of “pure” safety properties, the lasso ends in a self-loop state where the property is violated.

Consider, for an example, the behaviour of an elevator system as follows:

Example 1** (Elevator).**

The elevator can commute between three floors (0,1,2). On each floor there is a button that can be pressed in order to call the elevator. Whenever a button on some floor is pressed, the elevator will try to go to that floor immediately. If two buttons are pressed, the elevator will go to the lower floor first. We use the identifier $E_{i}$ to denote the event “elevator is on floor $i$”, and $B_{i}$ to denote “button on floor $i$ is pressed”, for $i\in\{0,1,2\}$.

A liveness property is, for example, that whenever a button on the second floor is pressed, the elevator will go there eventually. Assume we are interested in finding those sequences of events that lead to a hazard in which the button on the second floor is pressed, but the elevator never arrives at the second floor. A corresponding counterexample is a lasso-shaped execution in which $B2$ can be observed, whereas $E2$ occurs neither along the initial path fragment after $B2$, nor in the loop.

In this paper, causality checking for general definable LTL properties is done by identifying the counterexample of a temporal property with a so-called Event Order Logic formula. This formula encodes the relevant ordered occurrences of causal events, and is obtained by unfolding the loop-counterexample “sufficiently many times”.

Related work.

The idea of exploiting counterexamples as a debugging aid, in order to understand what determined a certain system failure, has been addressed by other works as well. We refer, for instance, to the results in [3] that uses the notion of causality in [16, 15] and provides the user a visual explanation of the failure by marking causes as red dots along the counterexample trace. In [3], causes for the violation of an LTL property are computed via an over-approximation algorithm. For another example, we refer to the work in [18], where errors in system models are elicited from similar counterexamples witnessing the violation of liveness properties.

It is certain that imposing minimality conditions on the size of causal explanations is desirable. In our work, we adapt the approach from [16, 15], and formalise a notion of causality that is minimal with respect to the number of events (i.e., system actions) it encompasses. In a similar spirit, [24] proposes a methodology for computing shortest counterexamples for symbolic model checking of so-called LTL with past formulae. Other “nice to have” properties of causality such as, compositionality, for instance, were addressed in [11, 10, 12, 13, 6].

For a more comprehensive survey on principles, algorithms and applications of counterexample analysis, we refer to [7].

Contributions.

In this paper we introduce a notion of causality with respect to the violation of general LTL properties. This is an extension of the work in [20], where causality was handled in the context of safety LTL properties. Our main contributions include an adaptation of the so-called Event Order Logic (EOL) in [20] in order to enable compact (finite) descriptions of what caused the violation of a system failure. The proposed notion of causality incorporates a series of properties to be satisfied by the EOL formulae characterising property violations. A notion of soundness and completeness depending on a complete enumeration of all bad traces (i.e., counterexamples) and good traces is also established. We show that causality in the sense of [20] is equivalent with causality in the current paper, for the case of safety LTL properties.

Structure of paper.

Section 2 briefly introduces the formal framework for analysing counterexamples witnessing the violation of LTL system properties in the context of transition system models. The corresponding extension of EOL to describe such counterexamples is provided in Section 3. Section 4 introduces the proposed notion of causality. In Section 5 we discuss soundness and completeness of our approach. Section 6 draws the conclusions and provides pointers to future work.

2 Preliminaries

In this section we introduce the formal framework for analysing counterexamples witnessing he violation of Linear Temporal Logic [17] system properties in the context of transition systems.

Definition 1** (Transition Systems (TS’s)).**

A TS is a tuple $T=(S,Act,\rightarrow,I,AP,L)$, where $S$ is a finite set of states, $Act$ is a set of actions, $\rightarrow\subseteq S\times Act\times S$ is a transition relation, $I\subseteq S$ is a set of initial states, $AP$ is a set of atomic propositions, and $L:S\rightarrow\mathcal{P}(AP)$ is a function associating to states in $S$ a set of atomic propositions in $AP$.

For $(s,\alpha,s^{\prime})\in~{}\rightarrow$ we also write $s\xrightarrow{\alpha}s^{\prime}$. In the remainder of this paper, for each $\alpha\in Act$, we consider an atomic proposition or event variable $a_{\alpha}\in AP$ such that: given $s^{\prime}\in S$, it holds that $a_{\alpha}\in L(s^{\prime})$ whenever there exists $s\in S$ with $s\xrightarrow{\alpha}s^{\prime}$.

We define an execution, or execution trace of $T$, as a possibly infinite sequence $\sigma=s_{0}\alpha_{1}s_{1}\alpha_{2}s_{2}\ldots$ with $s_{0}\in I$ and $s_{i}\xrightarrow{\alpha_{i+1}}s_{i+1}$ for all $i\geq 0$. Moreover, for all $i\geq 0$ we write $\sigma[i\ldots]$ to represent the execution $s_{i}\alpha_{i+1}s_{i+1}\ldots~{}$. Additionally, for all $0\leq i<j$ we write $\sigma[i..j]$ to represent the finite execution $s_{i}\alpha_{i+1}\ldots\alpha_{j}s_{j}$.

Given an execution trace $\sigma^{\prime}=s_{0}^{\prime}\alpha_{1}^{\prime}s_{1}^{\prime}\alpha_{2}^{\prime}\ldots$, we write $s_{0}\alpha_{1}:\sigma^{\prime}$ as a shorthand for the execution trace $\sigma=s_{0}\alpha_{1}s_{0}^{\prime}\alpha_{1}^{\prime}s_{1}^{\prime}\alpha_{2}^{\prime}\ldots$. For simplicity of notation, we sometimes write $\alpha^{\prime}_{1}\alpha^{\prime}_{2}\ldots$, or $a_{\alpha^{\prime}_{1}}a_{\alpha^{\prime}_{2}}\ldots$ to equivalently represent $\sigma^{\prime}$.

Remark 1**.**

*In this paper, we consider TS’s without terminal states, i.e., TS’s for which all executions are infinite. Observe that this is not a limitation. Finite executions ending in a terminal state $s$ can be straightforwardly extended to infinite executions via a transition $s\xrightarrow{\lambda}s_{\lambda}$ such that $s_{\lambda}$ has a self-loop labelled $\lambda$, i.e., $s_{\lambda}\xrightarrow{\lambda}s_{\lambda}$. *

We further focus on formalising properties of TS’s. A safety property can be seen as a requirement that some bad event never happens. More formally, a property $P_{\textnormal{\it{safe}}}$ is a safety property if and only if every path, or execution that violates $P_{\textnormal{\it{safe}}}$ has a finite prefix that can not be extended to a path satisfying $P_{\textnormal{\it{safe}}}$. Intuitively, this means that if a safety property is violated, this violation already happens after the model has passed a finite sequence of states and after this finite sequence the violation is unrecoverable. Consequently, if we want to check whether a safety property is satisfied or not, it suffices to only look at finite paths of the system. A well known approach for reasoning on the violation of safety properties is model-checking implemented via simple depth first search (DFS) algorithms [2]. These algorithms check whether starting from an initial state we can find a path to some state of the model where the bad event specified by the safety property happens. If such a path can be found, the property is violated.

A liveness property requires that some good event eventually happens. It follows that when checking whether a liveness property is satisfied or not it does not suffice to only look at finite execution fragments of the system. Orthogonally to the model-checking of safety properties, reasoning on the violation of liveness properties is performed via nested depth first search (NDFS) [8]. This algorithm searches for an infinite path in the model, such that the good event described by the liveness property does not hold along that path. If such a path can be found, the property is violated.

Linear time (LT) properties can be expressed in terms of a safety and a liveness property, based on the Decomposition Theorem $3.37$ in [2]. Consequently, reasoning on the violation of LT properties requires an NDFS-based approach.

We further provide a brief overview on Linear Temporal Logic (LTL) [17] – a formalism to describe system properties. Intuitively, LTL formulae range over the atomic proposition $\mathit{true}$, that holds in any state of a transition system and, respectively, over atomic propositions $a$ satisfied within a state $s$ whenever the labelling function indicates so. Recursively, LTL formulae are defined as disjunctions ($\,\,\!\!\!\shortmid\!\!\!\,\,$), conjunctions ($\&$) and negations ($\sim$) of formulae. The next ($X$) operator indicates the satisfiability of a property starting with the “next” state, whereas the until ($U$) operator indicates the satisfiability of a formula $\phi_{1}$ all the time until a formula $\phi_{2}$ is finally satisfied. The eventually ($\Diamond$) and generally ($\square$) operators indicate the satisfiability of a formula “at some point” in the future and, respectively, “all the time”.

Definition 2** (Linear Temporal Logic (LTL)).**

LTL formulae over the set $AP$ of atomic propositions are built according to the following grammar:

[TABLE]

LTL formulae are interpreted over transition systems without terminal states $T=(S,Act,\rightarrow,I,AP,L)$. Let $\sigma=s_{0}\alpha_{1}s_{1}\alpha_{2}s_{2}\ldots$ be an execution trace in $T$. The following hold:

• •

$\sigma\vDash{\mathit{t}rue}$**

• •

$\sigma\vDash a$* iff $a\in L(s_{0})$*

• •

$\sigma\vDash\sim\phi$* iff not $\sigma\vDash\phi$*

• •

$\sigma\vDash\phi_{1}\!\!\!\shortmid\!\!\!\phi_{2}$* iff $\sigma\vDash\phi_{1}$ or $\sigma\vDash\phi_{2}$*

• •

$\sigma\vDash\phi_{1}~{}\&~{}\phi_{2}$* iff $\sigma\vDash\phi_{1}$ and $\sigma\vDash\phi_{2}$*

• •

$\sigma\vDash X\phi$* iff $\sigma[1..]\vDash\phi$*

• •

$\sigma\vDash\phi_{1}~{}U~{}\phi_{2}$* iff $\exists k\geq 0:\sigma[k..]\vDash\phi_{2}$ and $\forall 0\leq i<k:\sigma[i..]\vDash\phi_{1}$*

• •

$\sigma\vDash\Diamond\phi$* iff $\exists k\geq 0:\sigma[k..]\vDash\phi$*

• •

$\sigma\vDash\square\phi$* iff $\forall k\geq 0:\sigma[k..]\vDash\phi$*

We write $(\varphi_{1}\rightarrow\varphi_{2})$ as a syntactic sugar for $(\sim\varphi_{1}\!\!\!\shortmid\!\!\!\varphi_{2})$, and $(\varphi_{1}\leftrightarrow\varphi_{2})$ as a syntactic sugar for $((\sim\varphi_{1}\rightarrow\varphi_{2})\&(\sim\varphi_{2}\rightarrow\varphi_{1}))$.

We say that a transition system $T$ satisfies a LTL formula $\phi$, written as $T\vDash\phi$, if and only if for all executions $\sigma$ of $T$ it holds that $\sigma\vDash\phi$.

If a system model, or TS in our setting, does not satisfy some given LTL-definable property $P$, there must be an execution witnessing the violation of the property. Such executions are called counterexamples. For safety properties, counterexamples are finite execution fragments that start in an initial state of the system and lead to an undesired state where “something bad” actually happens. For liveness properties, counterexamples must be infinite executions, because every finite path can still be extended to a path satisfying the liveness property and does, therefore, not suffice as an example for the violation of the property. An infinite path that violates a liveness property is lasso-shaped.

3 Event Order Logic

The work in [20] introduces the so-called Event Order Logic (EOL). Intuitively, formulae in EOL are used to express causality classes for counterexamples. Causality classes can be seen as generalized counterexamples. A causality class represents several counterexamples, all leading to the property violation in the “same way”. Such counterexamples may only differ in some other events that are not essential for the property violation.

In the case of liveness properties, our counterexamples must be lasso shaped, that is, they contain a loop at the end. The sequence “$E0,B2,(B1,E1,B0,E0)^{\omega}$”  is a counterexample of $\varphi:=\square(B2\rightarrow\Diamond E2)$ in the elevator model. In words, the elevator is stuck between the ground floor and the first floor, as $(B1,E1,B0,E0)^{\omega}$ indicates that the sequence $(B1,E1,B0,E0)$ keeps repeating forever. We can say that the cause of the property violation is that the buttons on the ground floor and the first floor are pressed repeatedly and between that, the elevator never has the chance to go to the second floor.

We see that the cause of a liveness property violation must consist of some events happening at the beginning and then some other events happening again and again (in the loop). Hence, in what follows, we propose an extension of EOL in [20] with so-called infinite formulae to express infinite causal behaviours.

The work in [20] introduces two kinds of EOL formulae: simple and complex. Intuitively, simple EOL formulae, usually denoted by $\phi$, are built over event variables $a_{\alpha}$ that are atomic propositions witnessing the execution of actions $\alpha$ at some point in the future. The satisfiability of atomic propositions is different within the frameworks of EOL and LTL: the latter assumes satisfiability with respect to the initial state of a trace, whereas the former has an “eventually” component. This difference is formalized in Definition 4 providing the semantics of EOL.

Similarly to the case of LTL, simple EOL formulae are inductively defined using negation ($\neg$), conjunction ($\land$) and disjunction ($\lor$). As a consequence of the observation above, formulae of shape $\phi_{1}\land\phi_{2}$ (respectively, $\phi_{1}\lor\phi_{2}$) read as: eventually $\phi_{1}$ will hold and (respectively, or) eventually $\phi_{2}$ will hold.

For technical reasons related to the semantics of the aforementioned infinite EOL formulae, we split the complex EOL formulae in [20] into: I-complex and G-complex, respectively. We refer to Remark 2 for a more detailed explanation.

I-complex formulae, usually denoted by $\psi$, include simple EOL formulae, conjunctions ($\land$) and disjunctions ($\lor$) of I-complex formulae. An I-complex formula $\psi_{1}\wedgedot\psi_{2}$ has an “ordered-and”-like semantics and reads: first $\psi_{1}$ holds and then $\psi_{2}$. Last, but not least, an I-complex formula $\psi_{1}{\wedgedot_{\less}\,}{\phi}{\,\wedgedot_{\gtr}}\psi_{2}$ reads: first $\psi_{1}$ holds, then $\psi_{2}$ holds and in between the “interval” determined by the satisfiability of $\psi_{1}$ and $\psi_{2}$ the simple EOL formula $\phi$ holds all the time.

G-complex formulae, usually denoted by $\theta$, range over I-complex formulae and encompass two more temporal operators: $\wedgedot_{]}$ that has an “until”-like semantics, and $\wedgedot_{[}$ that has an “after”-like semantics. More precisely, $\phi\wedgedot_{]}\theta$ reads: $\theta$ will hold at some point in the future and until then, the simple EOL formula $\phi$ holds all the time. Orthogonally, $\theta\wedgedot_{[}\phi$ reads: at some point $\theta$ holds, and after that, $\phi$ holds all the time.

Observe that the simple and, respectively, G-complex formulae in this paper have the same expressive power as the simple and, respectively, complex EOL formulae originally proposed in [20].

To express infinite causal behaviour, we extend the EOL in [20] with the so-called infinite formulae, usually denoted by $\xi$. These are formulae built over the new logical symbol ${\wedgedot}^{\omega}$. For a G-complex formula $\theta$ and an I-complex formula $\psi$ we write $\theta{\wedgedot}^{\omega}\psi$ to express that first $\theta$ holds and then $\psi$ happens infinitely many times.

Formally, as the new EOL we obtain the following:

Definition 3** (Extended Event Order Logic (EOL) – Syntax).**

Simple EOL formulae* over a set $\mathcal{A}$ of event variables are formed according to the following grammar:*

[TABLE]

Complex EOL formulae* are of two kinds:*

• •

I-complex EOL formulae*, formed according to the following grammar:*

[TABLE]

where $\phi$ is a simple EOL formula.

• •

G-complex EOL formulae*, formed according to the following grammar:*

[TABLE]

where $\phi$ is a simple EOL formula and $\psi$ an I-complex EOL formula.

Infinite EOL formulae* are formed according to the following grammar:*

[TABLE]

where $\theta$ is a G-complex EOL formula and $\psi$ is an I-complex formula.

We want an infinite execution $\sigma$ to satisfy an infinite EOL formula $\xi=\theta{\,\,{\wedgedot}^{\omega}}\psi$ if and only if (a) the events in $\theta$ occur in $\sigma$ in the order specified by $\theta$, and (b) the events of $\psi$ occur in $\sigma$ in the order specified by $\psi$, infinitely many times.

As an example, consider the following execution $\sigma$ in a TS:

[TABLE]

It is easy to see that $\sigma$ satisfies the formula

[TABLE]

where $a_{\alpha_{i}}$ is the event variable corresponding to $\alpha_{i}$ for $i\in\{1,2,3\}$. We see that $\sigma$ contains a finite part $\sigma_{1}=s_{0}\xrightarrow{\alpha_{1}}s_{1}$ determining the event variable $a_{\alpha_{1}}$ to occur, and a finite part in the loop $\sigma_{2}=s_{1}\xrightarrow{\alpha_{2}}s_{2}\xrightarrow{\alpha_{3}}s_{1}$ where $a_{\alpha_{2}}$ and $a_{\alpha_{3}}$ occur. Thus, an intuitive approach to decide whether an infinite execution trace satisfies an infinite EOL formula $\xi=\theta{\,\,{\wedgedot}^{\omega}}\psi$ is to split $\sigma$ into an initial final trace $\sigma_{1}$ and finite trace $\sigma_{2}$ inside of the loop, and check if $\sigma_{1}$ satisfies $\theta$ and if $\sigma_{2}$ satisfies $\psi$, respectively.

The following example shows that it is not enough to split the lasso shaped execution trace $\sigma$ into a first part $\sigma_{1}$ that contains all states up to the loop and a second part $\sigma_{2}$ that consists of the loop executed only once. Consider the execution $\sigma$ in (1) and the EOL formula $\xi^{\prime}=a_{\alpha_{1}}\wedgedot a_{\alpha_{3}}\,\,{\wedgedot}^{\omega}(a_{\alpha_{3}}\wedgedot a_{\alpha_{2}}).$ Our execution $\sigma$ also satisfies $\xi^{\prime}$ because in $\sigma$ the event $a_{\alpha_{1}}$ happens before $a_{\alpha_{3}}$ and after that, $a_{\alpha_{2}}$ happens after $a_{\alpha_{3}}$ infinitely many times. Hence, in this case, the finite traces guaranteeing the satisfiability of $\xi^{\prime}$ are as follows:

[TABLE]

is obtained by concatenating the sequence in $\sigma$ up to the loop, with one unfolding of the loop, whereas

[TABLE]

is the unfolding of the loop twice.

By following a similar pattern, consider $\sigma$ in (1) and the EOL formula

[TABLE]

We want $\sigma$ to satisfy this formula as well, but $\sigma_{1}$ in (2) and $\sigma_{2}$ in (3) do not satisfy their corresponding EOL formulae in $\xi^{\prime\prime}$. We have to extend $\sigma_{1}$ until the loop has been executed three times, while $\sigma_{2}$ is defined by unfolding the loop four times. Hence, we get:

[TABLE]

Intuitively, $\sigma$ satisfies an infinite EOL formula $\xi=\theta{\,\,{\wedgedot}^{\omega}}\psi$ whenever $\sigma$ can be split into two finite executions $\sigma_{1}$ and $\sigma_{2}$, “large enough” to satisfy $\theta$ and $\psi$, respectively.

Remark 2**.**

As can be seen in Definition 3, we choose to classify the complex EOL formulae in [20] into I-complex formulae $\psi$ and G-complex formulae $\theta$. This is because we want to allow only interval-like formulae $\psi$ as right-hand side of the $\,\,{\wedgedot}^{\omega}$ operator. The occurrence of $\phi\wedgedot_{]}\psi$ or $\psi\wedgedot_{[}\phi$ in a cycle does not make sense unless $\psi=\phi$, case in which the corresponding formulae $\xi$ can be equivalently expressed in terms of formulae $\theta\,\,{\wedgedot}^{\omega}(\phi\wedgedot..\wedgedot\phi)$, where $\phi\wedgedot..\wedgedot\phi$ stands for finite ordered conjunctions ($\wedgedot$) of simple formulae $\phi$.

The EOL semantics is translated to the setting of general LTL- properties and infinite loop-traces as follows:

Definition 4** (EOL – Semantics).**

Let $T=(S,Act,\rightarrow,I,AP,L)$ be a transition system without terminal states. Let $\phi,\phi_{1},\phi_{2}$ be simple EOL formulae, let $\psi,\psi_{1},\psi_{2}$ be complex EOL formulae, let $\theta$ be a G-complex EOL formula, and let $\xi$ be an infinite EOL formula. Let $\mathcal{A}$ be a set of event variables and let $a_{\alpha},a_{\alpha_{i}}$ range over arbitrary event variables in $\mathcal{A}$.

The satisfiability of EOL formulae ($\vDash_{e}$) is defined over execution traces $\sigma=s_{0}\alpha_{1}s_{1}\alpha_{2}\ldots$ in $T$.

For simple EOL formulae we define:

• •

$\sigma\vDash_{e}\top$, i.e., $\top$ (true) is trivially satisfied by all traces

• •

$\sigma\vDash_{e}a_{\alpha}$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}a_{\alpha}$ iff *$\exists 0<j\leq r:s_{j-1}\xrightarrow{\alpha}s_{j}$

• •

$\sigma\vDash_{e}\lnot\phi$* iff not $\sigma\vDash_{e}\phi$*

• •

$\sigma\vDash_{e}\phi_{1}\land\phi_{2}$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}\phi_{1}\land\phi_{2}$ iff $\exists 0<r:\sigma[0..r]\vDash_{e}\phi_{1}$ and $\sigma[0..r]\vDash_{e}\phi_{2}$*

• •

$\sigma\vDash_{e}\phi_{1}\lor\phi_{2}$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}\phi_{1}\lor\phi_{2}$ iff $\exists 0<r:\sigma[0..r]\vDash_{e}\phi_{1}$ or $\sigma[0..r]\vDash_{e}\phi_{2}$*

For I-complex EOL formulae we define:

• •

$\sigma\vDash_{e}\psi_{1}\ {\wedgedot}\ \psi_{2}$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}\psi_{1}\ {\wedgedot}\ \psi_{2}$ iff*

$\exists 0<j\leq k<r:\sigma[0..j]\vDash_{e}\psi_{1}$* and $\sigma[k..r]\vDash_{e}\psi_{2}$*

• •

$\sigma\vDash_{e}\psi_{1}\ {\wedgedot}_{<}\ \phi\ {\wedgedot}_{>}\ \psi_{2}$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}\psi_{1}\ {\wedgedot}_{<}\ \phi\ {\wedgedot}_{>}\ \psi_{2}$ iff*

$\exists 0<j\leq k<r:\sigma[0..j]\vDash_{e}\psi_{1}$* and $\sigma[k..r]\vDash_{e}\psi_{2}$ and $\forall l$ s.t. $j\leq l<k:\sigma[l..l+1]\vDash_{e}\phi$*

• •

$\sigma\vDash_{e}\psi_{1}\land\psi_{2}$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}\psi_{1}\land\psi_{2}$ iff $\exists 0<r:\sigma[0..r]\vDash_{e}\psi_{1}$ and $\sigma[0..r]\vDash_{e}\psi_{2}$*

• •

$\sigma\vDash_{e}\psi_{1}\lor\psi_{2}$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}\psi_{1}\lor\psi_{2}$ iff $\exists 0<r:\sigma[0..r]\vDash_{e}\psi_{1}$ or $\sigma[0..r]\vDash_{e}\psi_{2}$*

For G-complex EOL formulae we define:

• •

$\sigma[i..r]\vDash_{e}\phi\ {\wedgedot}_{]}\ \theta$* iff $\exists i\leq j<r:\sigma[j..r]\vDash_{e}\theta$ and $\forall k$ s.t. $i\leq k<j:\sigma[k..k+1]\vDash_{e}\phi$*

• •

$\sigma[i..r]\vDash_{e}\theta\ {\wedgedot}_{[}\phi$* iff $\exists i<j\leq r:\sigma[i..j]\vDash_{e}\theta$ and $\forall k$ s.t. $j\leq k<r:\sigma[k..k+1]\vDash_{e}\phi$*

• •

$\sigma\vDash_{e}\phi\ {\wedgedot}_{]}\ \theta$* iff $\exists 0\leq r:\sigma[r..]\vDash_{e}\theta$ and $\forall j$ s.t. $0\leq j<r:\sigma[j..j+1]\vDash_{e}\phi$*

• •

$\sigma\vDash_{e}\theta\ {\wedgedot}_{[}\phi$* iff $\exists 0<r:\sigma[0..r]\vDash_{e}\theta$ and $\forall j$ s.t. $j\geq r:\sigma[j..j+1]\vDash_{e}\phi$*

Let $\sigma=s_{0}\alpha_{1}s_{1}\alpha_{2}\ldots s_{l}\alpha_{l+1}s_{l+1}\ldots\alpha_{l+m}s_{l+m}\alpha_{l+m+1}s_{l+1}\alpha_{l+2}\ldots$ be an infinite execution trace of $T$ with a loop consisting of $m$ states and starting with $s_{l+1}$. Let $\sigma_{2}^{j}=\sigma[l..l+j*m-1]$ be the unfolding of the loop for $j$ times.

For infinite EOL formulae $\xi=\theta\,\,{\wedgedot}^{\omega}\psi$ we define:

• •

$\sigma\vDash_{e}\xi$* iff $\exists i\geq 0,j\geq 0:\sigma_{1}=\sigma[0..i]$ and $\sigma_{2}^{j}=\sigma[l..l+j*m-1]$ and $\sigma_{1}\vDash_{e}\theta$ and $\sigma_{2}^{j}\vDash_{e}\psi$.*

Definition 5** (EOL Formulae over Executions).**

Let $\sigma=s_{0}\alpha_{1}s_{1}\alpha_{2}\ldots s_{l}\alpha_{l+1}\ldots s_{l+m-1}\alpha_{l+m}s_{l}\alpha_{l+1}\ldots$ be an infinite execution trace of $T$ with a loop consisting of $m$ states and starting with $s_{l}$. The EOL formula over $\sigma$ is defined as: $\xi_{\sigma}:=a_{\alpha_{1}}\wedgedot\ldots\wedgedot a_{\alpha_{l}}\,\,{\wedgedot}^{\omega}(a_{\alpha_{l+1}}\wedgedot\ldots\wedgedot a_{\alpha_{l+m}}).$

The following definition will give us a possibility of comparing two EOL formulae. Whenever we have an EOL formula $\xi_{1}$ and extend it to an EOL formula $\xi_{2}$ by adding some events to the formula, the set of executions that satisfy the EOL formula $\xi_{2}$ will be a subset of those executions that satisfy the EOL formula $\xi_{1}$. Intuitively, this holds as in $\xi_{2}$ we have more constraints on the represented execution traces. Therefore, for two infinite EOL formulae $\xi_{1}$ and $\xi_{2}$ we will use the notation $\xi_{1}\subseteq\xi_{2}$ to express that every execution $\sigma$ that satisfies $\xi_{2}$ also satisfies $\xi_{1}$. In that case, $\xi_{1}$ can be seen as a generalized form of $\xi_{2}$.

Definition 6** (EOL Formulae Subset Relationship).**

Let $\xi_{1}and\xi_{2}$ be infinite EOL formulae.

• •

$\subseteq:\xi_{1}\subseteq\xi_{2}$* iff every execution $\sigma$ that satisfies $\xi_{2}$ also satisfies $\xi_{1}$. Intuitively, this means that the set of events in $\xi_{1}$ is a subset of the events in $\xi_{2}$.*

• •

$\subset:\xi_{1}\subset\xi_{2}$* iff $\xi_{1}\subseteq\xi_{2}$ and $\xi_{1}\neq\xi_{2}$.*

As an example we consider the EOL formulae $\xi_{1}=E0\wedgedot B1\wedgedot E1$ and $\xi_{2}=E0\wedgedot B1\wedgedot B2\wedgedot E1$. In every execution $\sigma$ that satisfies $\xi_{2}$, the events $E0$, $B1$ and $E1$ will happen one after the other (but there can be other events happening between them). Therefore, every execution $\sigma$ that satisfies $\xi_{2}$ also satisfies $\xi_{1}$. Hence, it holds that $\xi_{1}\subseteq\xi_{2}$.

4 Causality for general LTL-definable properties

In this section, we formally define the notion of actual causality (AC) for general LTL-definable properties. The definition follows its counterpart in [20]. The latter is an adoption of the actual causality in [16], to the context of concurrent systems. Next, we provide a brief reminder of the causal setting in [16].

In [16], systems under analysis are formalized as structural equation models. Intuitively, structural equations are used to describe causal influence of variables in the system. The set of all variables is partitioned into the set $U$ of exogenous variables that are irrelevant with respect to the causal effect, and the set $V$ of endogenous variables that are considered to have a meaningful, potentially causal effect. The set $X\subseteq V$ contains all events that jointly might represent a cause. A signature $\cal{S}$ is defined as a tuple $\cal{(U,V,R)}$, where $\cal{U}$ is a finite set of exogenous variables, $\cal{V}$ is a finite set of endogenous variables, and $\cal{R}$ associates with every variable $Y\in\cal{U}\cup\cal{V}$ a nonempty set ${\cal{R}}(Y)$ of possible values for Y. A structural equation model over a signature $\cal{S}$ is defined in [16] as tuple $M=(\cal{S,F})$, where $\cal{F}$ associates with each variable $X\in\cal{V}$ a function denoted $F_{X}$ that defines the values of all variables in X given the values of all other variables in $\cal{U}\cup\cal{V}$. Consider a structural equation model $M=(\cal{S,F})$, a vector $\vec{X}$ of variables in $\cal{V}$, and vectors $\vec{x}$ and $\vec{u}$ of values for the variables in $\vec{X}$ and $\cal{U}$. $M_{\vec{X}\leftarrow\vec{x}}$ denotes the structural equation model for which variables in $\vec{X}$ are set to $\vec{x}$. Given a signature $\cal{S=(U,V,R)}$, a formula of the form $X=x$, for $X\in\cal{V}$ and $x\in{\cal{R}}(X)$, is called a primitive event. A basic causal formula over $\cal{S}$ is one of the form $[Y_{1}\leftarrow y_{1},...,Y_{k}\leftarrow y_{k},]\varphi$ where $\varphi$ stands for the effect, or hazard, and $Y_{1},...Y_{k}$ and X are variables in $\cal{V}$. The formula $[Y_{1}\leftarrow y_{1},...,Y_{k}\leftarrow y_{k},]\varphi$ is abbreviated as $[\vec{Y}\leftarrow\vec{y}]\varphi$. Intuitively, $[\vec{Y}\leftarrow\vec{y}]\varphi$ states that $\varphi$ holds in a setting in which the values of the variables in $\vec{Y}$ are set to the values in $\vec{y}$. A causal formula $\psi$ is a Boolean combination of basic causal formulae. We write $(M,\vec{u})\models_{SM}\psi$ whenever $\psi$ is true in the structural model $M$, given the context defined by $\vec{u}$. Additionally, $\vec{X}=\vec{x}$ stands for a conjunction of primitive events of the form $X_{1}=x_{1}\wedge....\wedge X_{k}=x_{k}$.

An actual cause with respect to the hazard, or effect $\varphi$ is defined in [16] as follows:

Definition 7** (Actual cause [16]).**

$\vec{X}=\vec{x}$* is an actual cause of $\varphi$ in $(M,\vec{u})$ if the following three actual cause conditions (AC) hold:*

AC1:

$(M,\vec{u})\models_{SM}(\vec{X}=\vec{x})\wedge\varphi$.

AC2:

There exists a partition $(\vec{Z},\vec{W})$ of $\cal{V}$ with $\vec{X}\subseteq\vec{Z}$ and some setting $(\vec{x},\vec{w})$ of the variable in $(\vec{X},\vec{W})$ such that:

1. 1.

$(M,\vec{u})\models_{SM}[\vec{X}\leftarrow\vec{x}^{\prime},\vec{W}\leftarrow\vec{w}^{\prime}]\neg\varphi$** 2. 2.

$(M,\vec{u})\models_{SM}[\vec{X}\leftarrow\vec{x},\vec{W}\leftarrow\vec{w}^{\prime},\vec{Z}^{\prime}\leftarrow\vec{z}^{*}]\varphi$* for all subsets $\vec{Z}^{\prime}$ of $\vec{Z}$*

AC3:

$\vec{X}$* is minimal, in the sense that no subset of $\vec{X}$ satisfies conditions AC1 and AC2. *

Intuitively, in [16], condition AC1 states that there is a setting in which both the cause and the effect occur. AC2(1) expresses a necessity condition. It says that for $\vec{X}=\vec{x}$ to be a cause of $\varphi$, there must be a setting $\vec{x^{\prime}}$ such that if $\vec{X}$ is set to $\vec{x}^{\prime}$, $\varphi$ would not have occurred. However, as stated in [16], AC2(1) might be too permissive as it allows to change the values of the variables in both $X$ and $W$. Hence, the change of $\varphi$ form true to false could be caused by a change of a variable in $X$ or $W$. The set $W$ enables expressing so-called “contingent dependencies”. For an intuition, consider two events “Alice presses button B2” and “Bob presses button B2” that enable the elevator to reach the second floor of a building. We say that the elevator reaching the second floor depends on Alice pressing the button, under the contingency that Bob did not press the button. AC2(2) constrains AC2(1) by keeping the values of the variables in $X$ at their original values and only changing the variables in $W$. AC2(2) corresponds to a sufficiency condition. Intuitively, setting $\vec{X}$ to $\vec{x}$, guarantees that $\varphi$ holds. The minimality condition in AC3 ensures that only those elements that are essential with respect to $\varphi$ are part of the cause.

Actual causality in the context of TS’s and LTL-definable properties is defined as an adoption of [16] to the setting of concurrent systems, in the spirit of [20]. In our setting, $\neg\varphi$ represents the hazard, or the effect.

Definition 8** (Causality for LTL).**

Let $T=(S,Act,\rightarrow,I,AP,L)$ be a transition system without terminal states. An EOL formula $\xi$ is considered a cause for the violation of the LTL specifiable property $\varphi$, if the following conditions are satisfied:

• •

AC1: There exists an infinite execution $\sigma$ in $T$ such that $\sigma\vDash_{e}\xi$ and $\sigma\nvDash\varphi$

• •

AC2(1): There exists an infinite execution $\sigma$ in $T$ such that $\sigma\nvDash_{e}\xi$ and $\sigma\vDash\varphi$

• •

AC2(2): For all infinite executions $\sigma^{\prime\prime}$ in $T$ with $\sigma^{\prime\prime}\vDash_{e}\xi$ it holds that $\sigma^{\prime\prime}\nvDash\varphi$.

• •

AC3: The EOL formula $\xi$ is minimal, i.e., there does not exist an EOL formula $\xi^{\prime}$ with $\xi^{\prime}\subset\xi$ that also satisfies conditions AC1 and AC2.

AC1 above resembles its counterpart in Definition 7 in the sense that it identifies a setting $\sigma$ that satisfies both the cause $\xi$ and the effect $\varphi$. AC2(1) entails a necessity condition that identifies a setting witnessed by $\neg\xi$ in which the violation of $\varphi$ would not occur. We fully formalise necessity as a completeness result in Theorem 1, Section 5. AC2(2) is a sufficiency result, stating that satisfying the cause $\xi$ is enough to guarantee the violation of $\varphi$. AC3 is the minimality condition which states that no true subset of $\xi$ satisfies conditions AC1 and AC2. Intuitively, $\xi$ is in the “most general form possible”. Moreover, note that our definition of causality does not employ a notion of “contingency”. This is because our approach to causality checking is based on a complete exploration of the traces within a TS model and enables the explicit identification of all potential causes.

Example 2**.**

If we want to show that $\xi=E_{0}\wedgedot B2\,\,{\wedgedot}^{\omega}(B1\wedgedot E1\wedgedot B0\wedgedot E0)$ is causal with respect to the violation of the LTL property $\varphi=\square(B2\rightarrow\Diamond E2)$, we need to show that AC1, AC2 and AC3 are fulfilled for $\xi$.

Consider the infinite execution:

[TABLE]

Informally, (5) states that when at floor $E_{0}$, after pressing button $B_{2}$, only alternations of actions press $B_{i}$ and reach $E_{i}$ are possible, where $i\in\{1,2\}$. Note that $E_{2}$ is never reached, even if $B_{2}$ was pressed.

Moreover, consider a behaviour in which the elevator stops at floor $E_{2}$ infinitely many times after $B_{2}$ being pressed once:

[TABLE]

At this point, we can infer the following:

• •

AC1 is satisfied as, for $\sigma$ in (5), $\sigma\vDash_{e}\xi$ and $\sigma\not\vDash\varphi$ hold.

• •

AC2(1) holds for $\sigma^{\prime\prime}=E_{0}(B_{2}E_{2}B_{1}E_{1})^{\omega}$, for instance.

• •

AC2(2) is not fulfilled as, for instance, for $\sigma^{\prime}$ in (6), $\sigma^{\prime}\vDash_{e}\xi$ and $\sigma^{\prime}\vDash\varphi$ hold.

Hence, $\xi$ is not causal, as it does not prohibit the occurrence of $E_{2}$.

We observe that in order to compute causes for a property violation according to Definition 8 it is not sufficient to start with an execution trace $\sigma$ that is a counterexample for the property $\varphi$, build the EOL formula $\xi_{\sigma}$ over $\sigma$ and generalize it (in the sense of Definition 6) until it satisfies conditions AC1-AC3. Example 2 shows that also the non-occurrence of events can be causal for the violation of a general LTL-property. We further introduce a method to compute the events over $\sigma$ whose non-occurrence is causal for the violation of $\varphi$, and encode this information within the cause $\xi$.

We proceed by first defining a valuation function with respect to a set of event variables $\mathcal{M}$. This function maps an execution trace $\sigma$ to the subset of event variables of $\mathcal{M}$ occurring in $\sigma$.

Definition 9** (Valuation Function).**

Given a transition system $T=(S,Act,\rightarrow,I,AP,L)$ and a finite set of event variables $\mathcal{M}=\{a_{\alpha_{1}},...,a_{\alpha_{n}}\}$, we define the valuation function $val_{\mathcal{M}}$ as a function on the set of execution traces of $T$ to the set $\mathcal{P(M)}$ – the powerset of $\mathcal{M}$. Let $\sigma$ be an execution trace of $T$. Then:

[TABLE]

Definition 10** (Non-Occurrence of Events).**

Let $T=(S,Act,\rightarrow,I,AP,L)$ be a transition system without terminal states, $\varphi$ an LTL-definable property, $\sigma$ an execution trace over $T$ with $\sigma\nvDash\varphi$ and $\xi_{\sigma}$ the EOL formula built over $\sigma$. Let $\mathcal{A}$ be the set of event variables, let $\mathcal{Z}$ be the set of event variables occurring in $\xi_{\sigma}$ and let $\mathcal{W}:=\mathcal{A}\backslash\mathcal{Z}$. We say that that $Q$ is the subset of event variables whose non-occurrence in $\sigma$ is causal for the property violation of $\varphi$, if

$\xi_{\sigma}$* satisfies AC1 and AC2(1).* 2. 2.

There exists an execution trace $\sigma^{\prime\prime}$ with $\sigma^{\prime\prime}\vDash_{e}\xi_{\sigma}$,

$val_{\mathcal{Z}}(\sigma)=val_{\mathcal{Z}}(\sigma^{\prime\prime})$, $val_{\mathcal{W}}(\sigma)\neq val_{\mathcal{W}}(\sigma^{\prime\prime})$ and $\sigma^{\prime\prime}\vDash\varphi$. 3. 3.

$Q\subseteq W$* is the smallest set s.t. for all execution traces $\sigma^{\prime\prime}$ with $\sigma^{\prime\prime}\vDash_{e}\xi_{\sigma}$ and $val_{\mathcal{Z}}(\sigma)=val_{\mathcal{Z}}(\sigma^{\prime\prime})$ and $val_{Q}(\sigma)=val_{Q}(\sigma^{\prime\prime})=\emptyset$ we have $\sigma^{\prime\prime}\nvDash\varphi$.*

As above, let $\sigma$ be a counterexample for the property $\varphi$, let $\xi_{\sigma}$ be the EOL formula built over $\sigma$ and assume $\xi_{\sigma}$ satisfies the first two conditions of the definition above.

We can now compute the subset $Q$ and determine the location of the event variables $a_{\alpha}\in Q$ in the EOL formula $\xi_{\sigma^{\prime\prime}}$ built over a $\sigma^{\prime\prime}$ which we choose as in condition 2 above. We then compare $\xi_{\sigma}$ to $\xi_{\sigma^{\prime\prime}}$ and prohibit the occurrence of $a_{\alpha}$ in $\xi_{\sigma}$ in the same locations as they occur in $\xi_{\sigma^{\prime\prime}}$. We repeat the procedure for all $\sigma^{\prime\prime}$ as in 2 above, and build $\xi_{\sigma}$ in an incremental fashion. This way we obtain a new EOL formula $\xi_{\sigma}$ that also satisfies condition AC2(2).

If, based on Definition 6, there is a generalization $\xi^{\prime}$ of $\xi_{\sigma}$ that also satisfies AC1 and AC2, we replace $\xi_{\sigma}$ by $\xi^{\prime}$. We repeat this procedure until $\xi_{\sigma}$ is in the most general form possible and, therefore, also satisfies AC3. Since $\xi_{\sigma}$ satisfies AC1-AC3 by construction, it is a cause for the violation of $\varphi$.

In the context of Example 2, from traces $\sigma^{\prime\prime}$ satisfying condition 2, we obtain intermediate formulae $\xi_{\sigma}$ of shape:

[TABLE]

On top of the formula incrementally derived as in (7), the repeated generalisation procedure entails the EOL formula:

[TABLE]

which is semantically equivalent with $B2\wedgedot\lnot E2$. Observe that $\xi_{\sigma}$ satisfies AC1 for $\sigma$ in (5) and AC2. $\xi_{\sigma}$ also satisfies AC3, because every superset of $\xi_{\sigma}$ will either violate AC1 or AC2. Thus, the EOL formula $\xi_{\sigma}$ satisfies AC1-AC3 .

Conditions AC1-AC3 do not imply that the order of the occurring events is causal. Whether the order of events occurring in an EOL formula $\xi$ that satisfies AC1-AC3 is causal or not, can be checked by the following Order Condition (OC). Note that $\xi$ can be causal even if the OC is not satisfied.

Definition 11** (Order Condition (OC)).**

Let $T=(S,\mathit{Act},$ $\rightarrow,$ $I,AP,L)$ be a transition system without terminal states. Let $\sigma$ be an infinite execution trace violating an LTL-definable property $\varphi$. Let $\xi$ be the EOL formula built over $\sigma$. Let $\mathcal{Z}$ be the set of event variables occurring in $\xi$ and let $\mathcal{W}:=\mathcal{A}\backslash\mathcal{Z}$. Consider a set of pairs of event variables over $Y\subseteq\cal{Z}$:

[TABLE]

Let $\xi_{\wedge}$ be the formula obtained by replacing the occurrences $a_{\alpha_{i}}\wedgedot a_{\alpha_{j}}$ in $\psi$ with $a_{\alpha_{i}}\land a_{\alpha_{j}}$.

The order condition (OC) states that the order of events $a_{\alpha_{i}}$ and $a_{\alpha_{j}}$ as above is not causal if the following holds: $\textnormal{exists }\sigma^{\prime}\textnormal{ such that }\sigma^{\prime}\not\vDash\varphi\textnormal{ and }val_{\cal A}(\sigma)=val_{\cal A}(\sigma^{\prime})\textnormal{ and }\sigma^{\prime}\not\vDash_{e}\xi\textnormal{ and }\sigma^{\prime}\vDash_{e}\xi_{\land}.$

Note that for the EOL formula $\xi_{\sigma}$ in (8) the following holds: $\xi_{\sigma}=\xi_{\sigma\land}$. As a consequence, the order of events in $\xi_{\sigma}$ is causal. We say that $\xi_{\sigma}$ satisfies OC.

The following result states the equivalence with the original notion of causality in [20], for the case of safety LTL properties.

Corollary 1**.**

Let $T=(S,\mathit{Act},$ $\rightarrow,$ $I,AP,L)$ be a transition system without terminal states. Let $\varphi$ be a safety LTL property. A G-complex EOL formula $\theta$ is a cause in the sense of Definition 8 if and only if it is a cause in the sense of [20].

Proof Sketch..

First, recall that counterexamples witnessing the violation of safety properties are finite. Hence, in [20], the satisfiability of EOL formulae (characterising such counterexamples) was established based on finite traces. Nevertheless, as can be seen from Definition 4, satisfiability of G-complex formulae can be defined via finite traces as well. In fact, the semantics of G-complex formulae and EOL formulae as in [20] coincide. These being said, the equivalence of the two notions of causality in the context of safety properties follows immediately by case analysis on AC1–AC3. AC1 and, respectively, AC3 in Definition 8 are identical to their counterparts in [20]. From AC2(1) and AC2(2) in Definition 8 we can infer AC2(1) in [20]. AC2(2) in Definition 8 implies AC2(2) in [20], whereas AC2(1) and AC2(2) in [20] imply their counterparts in Definition 8. ∎

We further introduce a definition of causality classes for general LTL-properties. Intuitively, causality classes can be interpreted as “generalized counterexamples”.

Definition 12** (Causality Class).**

Let $T=(S,Act,\rightarrow,I,AP,L)$ be a transition system without terminal states and let $\varphi$ be a general LTL formula. Every infinite EOL formula $\xi=\theta$ ${\wedgedot}^{\omega}$ $\psi$ that is considered a cause for the violation of $\varphi$, i.e., every infinite EOL formula $\xi$ that satisfies AC1-AC3 and OC, defines a causality class $CC_{\xi}.$ $CC_{\xi}$ is defined as the set of all valid execution traces in $T$ that satisfy $\xi$.

For example, the EOL formula $\xi_{\sigma}=(B2\wedgedot_{[}\lnot E2)\,\,{\wedgedot}^{\omega}(\lnot E2)$ in (8) satisfies AC1–AC3 and OC and, therefore, defines a causality class. Moreover, note that one execution can belong to more than one causality class.

5 Completeness and Soundness

We say that causality checking is complete whenever for each possible execution trace that violates an LTL property in the transition system under analysis, there exists a causality class representing this trace. Therefore, completeness can be seen as a necessity condition. The completeness of causality checking depends on a complete enumeration of all bad and good traces in the system.

Theorem 1** (Completeness).**

Let $T=(S,\mathit{Act},$ $\rightarrow,$ $I,AP,L)$ be a transition system without terminal states. Let $\sigma$ range over infinite execution traces in $T$ violating an LTL-definable property $\varphi$, i.e., $\sigma\nvDash\varphi$. For each such $\sigma$ there exists a causality class of $\varphi$ containing this trace.

Proof.

Let $\varphi$ be a general LTL property and let $\xi=\xi_{1}\lor...\lor\xi_{n}$ be the disjunction of all EOL formulae $\xi_{i}$ that satisfy AC1–AC3 and OC. Let $\sigma$ be a trace such that $\sigma\not\vDash\varphi$. We have to show that $\sigma\in CC_{\xi_{i}}$ for some $i\in 1,\ldots,n$. Assume that $\sigma$ is not contained in any causality class, that is $\sigma\nvDash_{e}\xi_{i}$ for all EOL formulae $\xi_{i}$ that satisfy the conditions AC1–AC3 and OC.

Let $\xi_{\sigma}$ be the EOL formula representing $\sigma$, and let $\mathcal{Z}$ and $\mathcal{W}$ be the corresponding event variable partitioning, with respect to $\mathit{Act}$. Since $\sigma\vDash_{e}\xi_{\sigma}$ it follows that $\xi_{\sigma}$ is excluded from $\xi$ by one of the AC1–AC3 tests. We will show that this is not the case for any of the conditions AC1–AC3 or OC.

• •

AC1 is satisfied because for $\sigma$ it holds that $\sigma\vDash_{e}\xi_{\sigma}$ and $\sigma\nvDash\varphi$.

• •

AC2(1) holds given the assumption that there exist $n$ EOL formulae in $\xi$ that satisfy AC1–AC3 and OC.

• •

If AC2(2) fails, then there exists an infinite execution $\sigma^{\prime\prime}$ with $\sigma^{\prime\prime}\vDash_{e}\xi_{\sigma}$ (and, hence, $val_{\mathcal{Z}}(\sigma)=val_{\mathcal{Z}}(\sigma^{\prime\prime})$) but $\sigma^{\prime\prime}\vDash\varphi$. Let $\xi_{\sigma^{\prime\prime}}$ be the EOL formula derived from $\sigma^{\prime\prime}$. We can now transform $\xi_{\sigma}$ to a new formula ${\xi^{\prime}_{\sigma}}$ by prohibiting the occurrence of $a_{\alpha}$ in $\xi_{\sigma}$, in the same locations as they occur in $\xi_{\sigma^{\prime\prime}}$. Consequently, we still have $\sigma\vDash_{e}{\xi^{\prime}_{\sigma}}$ and $\sigma\vDash{\xi^{\prime}_{\sigma}}$ but now, $\sigma^{\prime\prime}\nvDash_{e}{\xi^{\prime}_{\sigma}}$. Thus, $\sigma^{\prime\prime}$ does not influence the satisfaction of AC2(2) by ${\xi^{\prime}_{\sigma}}$. If ${\xi^{\prime}_{\sigma}}$ still doesn’t satisfy AC2(2), i.e., if there is another $\sigma^{\prime\prime\prime}$ with $\sigma^{\prime\prime\prime}\vDash_{e}\xi$ and $val_{\mathcal{Z}}(\sigma)=val_{\mathcal{Z}}(\sigma^{\prime\prime\prime})$ but $\sigma^{\prime\prime\prime}\vDash\varphi$, we repeat the procedure from above. Since the action alphabet is finite and the EOL formulae are finitely representable, this procedure will stop after finitely many steps. The resulted EOL formula ${\xi^{\prime}_{\sigma}}$ satisfies AC2(2).

• •

If AC3 excludes $\xi_{\sigma}$, then there must be some ${\xi^{\prime}_{\sigma}}\subset\xi_{\sigma}$ that satisfies AC1 and AC2. We still have $\sigma\vDash{\xi^{\prime}_{\sigma}}$ by Definition 8 .

In all cases we obtain an EOL formula ${\xi^{\prime}_{\sigma}}$ that satisfies AC1-AC3 and OC, such that $\sigma\vDash{\xi^{\prime}_{\sigma}}$. Thus, $\sigma$ is contained in the causality class $CC_{\xi^{\prime}_{\sigma}}.$ ∎

We define a causality checking result to be sound if whenever the events described by a causality class occur, the property violation occurs.

Theorem 2** (Soundness).**

Let $T=(S,\mathit{Act},$ $\rightarrow,$ $I,AP,L)$ be a transition system without terminal states. Each execution trace $\sigma$ of $T$ contained in a causality class of a general LTL property $\varphi$ is a bad trace, i.e. $\sigma\nvDash\varphi$.

Proof.

Let $\sigma$ be contained in the causality class $CC_{\xi}$ for some EOL formula $\xi$. Since $\xi$ defines a causality class, it must, by definition, satisfy AC1-AC3 and OC. In particular, $\xi$ must satisfy AC2(2). Since $\sigma\in CC_{\xi}$ we have $\sigma\vDash_{e}\xi$ by definition of causality classes. It follows from AC2(2) that $\sigma\nvDash\varphi$. ∎

6 Conclusions

We have presented an approach for extending causality checking towards general LTL-definable properties. To this end, we have reconsidered the actual cause conditions AC1-AC3 and OC, and adapted them to the lasso-shaped counterexamples that general LTL properties entail.

For practical reasons related to the implementation of the causality checking procedure, our current results are limited to LTL-definable properties. Nevertheless, in the future, we consider extending the formal framework of causality checking to the more general case of $\omega-$ regular linear-time properties [2]. It should be pointed out that the described adaption can be straightforwardly extend to general $\omega$-regular properties, corresponding to the expressiveness of Büchi automata, which are a strictly larger class of properties than LTL [26].

As already mentioned, we consider implementing the current causality checking approach in an automated tool. Of particular interest is QuantUM [19], a tool that enables the semi-formal specification of systems in terms of SysML [22] and applies LTL model-checking for determining what caused the violation of a safety LTL property. Recall that our notion of causality relies on the complete enumeration of system traces. Hence, the main challenge is to determine all (lasso-shaped) counterexamples in an efficient way (e.g., on-the-fly [9, 25, 4, 5]). Further future research comprises significant case studies in order to asses the scalability of our approach.

**Acknowledgements. **The authors are grateful for the useful comments received from the anonymous reviewers of CREST 2018.