Behavioral Diagnosis of LTL Specifications at Operator Level

1 Introduction

When a project's efficiency and the related return on investment are considered, rework efforts increasing consumed resources and time-to-market are a crucial factor. Industrial data show that about 50 percent of product defects result from flawed requirements and up to 80 percent of rework efforts can be traced back to requirement defects [Wiegers, 2001]. Surprisingly enough, traditionally, research has been focusing on using a (presumably correct) specification for design verification, and seldom aimed at assisting designers in their formulation or verifying their quality. However, and specifically for specification-driven development flows like proposed for Electronic Design Automation (EDA) by [PROSYD homepage, 2013], a specification's quality is crucial as design development/verification/synthesis depend on it.

Recently, specification development has been gaining specific attention in a formal context. Coverage and vacuity can pinpoint to specification issues [Fisman et al., 2009; Kupferman, 2006], and specification development tools like IBM's RuleBase PE [RuleBasePE homepage, 2013] or the academic tool RAT [Pill et al., 2006; Bloem et al., 2007] help by, for example, letting a designer explore a specification's semantics. RAT's property simulation (a similar feature was designed for RuleBase PE as well [Bloem et al., 2007]), for instance, lets a user explore a specification's evaluation along sample behavior (a trace). The temporal evolution for all subformulae is visualized via individual waveforms, presented according to a specification's parse tree. While industrial feedback was very good [Bloem et al., 2007], this still involves manual reasoning and intervention.

We aim to increase the level of automation via diagnostic reasoning that pinpoints to specification issues more directly. RuleBase PE offers a very interesting feature in this respect, explaining counterexamples using causality [Beer et al., 2009]. Reasoning about points in the trace where the prior stem's satisfiability status differs from its extension in distinctive ways, critical signals and related failure causes are identified and marked with red dots in the visualized waveform for this time-step. [Schuppan, 2012] offers unsatisfiable cores in the clauses he derives for specifications in the Linear Temporal Logic (LTL) [Pnueli, 1977].

In contrast to [Beer et al., 2009] we aim at the specification rather than the trace, and on a set of diagnoses instead of a flat list of affected components. That is, accommodating Reiter's theory of diagnosis in the context of formal specifications (in LTL as a first step), we derive diagnoses that describe viable combinations of operator occurrences (subformulae) whose concurrent incorrectness explains a trace's unexpected (un-)satisfiability, both in the context of weak and strong fault modes. Our diagnoses address operator occurrences rather than clauses (a diagnosis covers all unsat cores, and we can easily have 106 clauses even for small specifications), so that we effectively focus the search space to the items and granularity level the designer is working with.

Adopting the interface of the established property simulation idea, we consider specific scenarios in the form of infinite lasso-shaped traces a designer can define herself or retrieve, for example, by model-checking. We use a specifically tailored structure-preserving SAT encoding for our reasoning, exploiting known trace features and weak or strong fault models. For strong fault models that include descriptions of "alternative" behavior, our diagnoses directly suggest repairs like "there should come a weak instead of a strong until".

Extending [Pill and Quaritsch, 2012], our paper is structured as follows. We cover preliminaries in Section 2, and discuss our SAT-based diagnosis approach for LTL in Section 3. Following experimental results in Section 3.1, we draw conclusions and depict future work in Section 4. Related work is discussed throughout the paper where appropriate.

2 Preliminaries

Reiter's theory of diagnosis [Reiter, 1987] defines the consistency-oriented model-based diagnosis [Reiter, 1987; de Kleer and Williams, 1987] of a system as follows: A system description SD describes the behavior of a set of interacting components COMP. SD contains sentences ¬AB(ci) ⇒ NominalBehavior(ci) encoding a component's behavior under the assumption that it is not operating abnormally (the assumption predicate AB(ci) triggers a component ci's abnormal behavior, and NominalBehavior defines correct behavior in first order logic). As there are no definitions regarding abnormal behavior, the approach is considered to use a weak fault model (WFM). Given some actually observed system behavior OBS, a system is recognized to be faulty, iff SD ∪ OBS ∪ {¬AB(ci)|ci ∈ COMP} is inconsistent. A minimal diagnosis explaining the issue is defined as follows.

Definition 1. A minimal diagnosis for (SD, COMP, OBS) is a subset-minimal set ∆ ⊆ COMP such that SD ∪ OBS ∪ {¬AB(ci)|ci ∈ COMP \ ∆} is consistent.

Reiter proposes to compute all the minimal diagnoses as the minimal hitting sets of the set of not necessarily minimal conflict sets for (SD, COMP, OBS).

Definition 2. A conflict set CS for (SD, COMP, OBS) is a set CS ⊆ COMP such that SD∪OBS∪{¬AB(ci)|ci ∈ CS} is inconsistent. If no proper subset of CS is a conflict set, CS is a minimal conflict set.

Using a theorem prover capable of returning conflicts, Reiter's algorithm [Reiter, 1987] is able to obtain the sets of conflict sets and minimal diagnoses on-the-fly, where appropriate consistency checks verify a diagnosis ∆'s validity, and a set of pruning rules ensures their minimality. [Greiner et al., 1989] presented an improved version, HS-DAG, that uses a directed acyclic graph (DAG) instead of a tree and addresses some minor but serious flaws in Reiter's original publication.

For a strong fault model (SFM) approach, also abnormal behavior is defined [de Kleer and Williams, 1989], which has the advantage that diagnoses become more specific. On the downside, with n the number of assumptions and m the maximum number of modes for any assumption, the search space grows significantly from 2n to O(mn ).

For our definitions of an infinite trace and the Linear Temporal Logic (LTL) [Pnueli, 1977], we assume a finite set of atomic propositions AP that induces alphabet Σ = 2AP . Complementing the in- and output signals, we add further propositions for the subformulae to encode their evaluation. It will be evident from the context when we refer with a trace to the signals only. LTL is defined in the context of infinite traces, which we define as sequence as is usual. A sequence of letters with finite space (of finite length k) can describe an infinite computation only in the form of a lasso-shaped trace (with a cycle looping back from k to 0 ≤ l ≤ k) as follows (or it could describe all traces that have the sequence as prefix):

Definition 3. An infinite trace τ is an infinite sequence over letters from some alphabet Σ of the form τ = (τ0τ1 . . . τl-1)(τlτl+1 . . . τk)ω with l, k ∈ N, l ≤ k, τi ∈ Σ for any 0 ≤ i ≤ k, (...)ω denoting infinite repetition of the corresponding (sub-)sequence, (τ0τ1 . . . τl-1) referring to τ's finite stem, l to the loop-back time step, and (τlτl+1 . . . τk) representing the trace's (k,l)-loop [Biere et al., 1999]. We denote the infinite suffix starting at i as τ i , and τi refers to τ's element at time step i, where for any i > k we have τi = τl+(i-l)%(k-l+1).

Definition 4. Assuming a finite set of atomic propositions AP, and δ to be an LTL formula, an LTL formula ϕ is defined inductively as follows [Pnueli, 1977]:

• for any p ∈ AP, p is an LTL formula
• ¬ϕ, ϕ ∧ δ, ϕ ∨ δ, Xϕ, and ϕU δ are LTL formulae

Note that the popular operators δ Rσ, Fϕ, Gϕ, and δWσ not mentioned in Def. 4 are syntactic sugar for common formulae ¬((¬δ) U (¬σ)), ⊤ U ϕ, ⊥ R ϕ, and δ U σ ∨G δ respectively. Their semantics are thus defined only due to their use in the arbiter example depicted later on:

Similar to τi and a trace, we denote with ϕi a formula's evaluation at time step i. We use the usual abbreviations δ → σ and δ ↔ σ for ¬δ ∨ σ and (δ → σ) ∧ (σ → δ) respectively. For brevity, we will also use p to denote the negation of some atomic proposition p ∈ AP , as well as ⊤/⊥ for p∨¬p/p∧¬p.

Definition 5. Given a trace τ and an LTL formula ϕ, τ(=τ 0 ) satisfies ϕ, denoted as τ |= ϕ, under the following conditions

3 Model-Based Diagnosis at the Operator Level for LTL Specifications

Explanations why things went wrong are always welcome when facing unexpected and surprising situations, for example, when a supposed witness contradicts a specification as in the following example taken from [Pill et al., 2006]: Assume a two line arbiter with two request lines r1 and r2 and the corresponding grant lines g1 and g2. Its specification consists of the following four requirements: R1 demanding that requests on both lines must be granted eventually, R2 ensuring that no simultaneous grants are given, R3 ruling out any initial grant before a request, and finally R4 preventing additional grants until new incoming requests. Testing her specification, a designer defines a supposed witness τ (i.e. a trace that should satisfy the specification) featuring a simultaneous initial request and grant for line 1 (line 2 is omitted for clarity).

As pointed out by RAT's authors, using a tool like RAT, the designer would recognize that, unexpectedly, her trace contradicts the specification. However, diagnostic reasoning offering explanations why this is the case, would obviously be a valuable asset for debugging, which is exactly our challenge.

The specific problem in the scenario above is the until operator ¬gi Uri in R4 that should be replaced by its weak version ¬gi Wri: While the idea of both operators is that ¬gi should hold until ri holds, the weak version does not require ri to hold eventually, while the "strong" one does. Thus, R4 in its current form repeatedly requires further requests that are not provided by τ, and which is presumably not in the designer's intent. Evidently, the effectiveness of a diagnostic reasoning approach depends on whether a diagnosis' impact on a specification is easy to grasp, and can pinpoint the designer intuitively to issues like the one in our example.

Before describing our diagnosis approach for LTL specifications, we now introduce our general temporal reasoning principles for LTL, which we are going to adapt accordingly.

For an LTL formula ϕ, we can reason about its satisfaction by a trace τ via recursively considering τ's current and next time step in the scope of ϕ and its subformulae. While this is obvious for the Boolean connectives and the next operator X, the until operator is more complex. The well known expansion rules as immanently present also in LTL tableaus and automata constructions [Clarke et al., 1994; Somenzi and Bloem, 2000] capture this line of reasoning. We can unfold δ Uσ to σ ∨ δ ∧ X(δ Uσ), which basically encodes the options of how to satisfy ϕ in the current time step (considering Def. 5 this is the case where j = i) and the option of pushing the obligation (possibly iteratively) to the next time step (j > i). Considering acceptance, we have to verify whether the obligation would be pushed infinitely in time. Like [Biere et al., 1999] suggested for LTL model-checking, we use a SAT solver for our reasoning, with the advantage that k is known. Similar to their encoding or [Heljanko et al., 2005], we encode our questions into a satisfiability problem, where, as in our case also the loop-back time step l is given, we can check for pushed obligations very efficiently in our structure-preserving variant.

In Table 1, column 2 lists our unfolding rationales that connect ϕi to the evaluations of ϕ's subformulae and signals in the current and next time step. A checkmark in the third column indicates whether a rationale is to be instantiated for all time steps (remember that τk+1 = τl due to Def. 3, so with our encoding ϕk+1 = ϕl), whereas in the last column we list the corresponding clauses as added to our conjunctive normal form (CNF) encoding. In the clauses, ϕi represents the corresponding time-instantiated variable that we add for each subformula in order to derive a structure-preserving encoding. Given these clauses, we can directly obtain a SAT problem for τ |= ϕ in CNF from ϕ's parse tree and τ as follows.

Definition 6. In the context of a given infinite trace with length k and loop-back time-step l, E1(ψ) encodes an LTL formula ψ using the clauses presented in Table 1, where we instantiate for each subformula ϕ a new variable over time, denoted ϕi for time instance i. Please note that we assume that k and l are known inside E1 and R.

with ◦1 ∈ {∧, ∨,U}, ◦2 ∈ {¬, X} and R(ϕ) defined as the conjunction of the corresponding clauses in Table 1.

Definition 7. For a given infinite trace τ (with given k), E2(τ ) = ∧0≤i≤k [∧pi∈τi pi ∧ ∧pi∈AP\τi ¬pi ] encodes the signal values as specified by τ .

Theorem 1. An encoding E(ϕ, τ) = E1(ϕ) ∧ E2(τ) of an LTL formula ϕ and a trace τ as of Definitions 6 and 7 is satisfiable, SAT(E(ϕ, τ)), iff τ |= ϕ.

Proof. (Sketch). The correctness regarding the Boolean operators and the temporal operator next (X(δ)) is trivial, so that we concentrate on the operator until (δ Uσ).

We will start with the direction (τ i |= ϕ) → ϕi: According to Def. 5, τ i |= ϕ implies that there exists some j ≥ i, such that τ j |= σ, and for the time steps i ≤ m < j we have τ m |= δ. Clause (g) then requires ϕj to become ⊤, and Clause (h) propagates that backward to ϕi. For the direction ϕi → (τ i |= ϕ) Clauses (f1) and (f2) require either the immediate satisfaction by σi or postpone (possibly iteratively) the occurrence of σ in time (in the latter case requiring ϕi+1 and δi). According to Def. 5, the first option obviously implies τ i |= ϕ, while for the second one it is necessary to show that the obligation is not postponed infinitely such that the existential quantifier (see Def. 5) would not be fulfilled. This is ensured by Clause (i), that, if the satisfaction of σ is postponed until k, requires there to be some σm, with m in the infinite k, l loop, such that τ m |= σ. Thus we have that ϕi implies τ i |= ϕ, and in turn (τ i |= ϕ) ↔ϕi.

Via Theorem 1, we can verify whether an infinite signal trace τ is contained in a specification ϕ or not. Our encoding E(ϕ, τ) forms a SAT problem in CNF that is satisfiable iff τ |= ϕ. An affirmative answer is accompanied by a complete evaluation of all subformulae along the trace. For counterexamples, we obtain such an evaluation by encoding the negated specification. Via E(ϕ, τ) we can also derive (or complete) k, l witnesses (by encoding ϕ) and counterexamples (encoding ¬ϕ), due to the fact that concerning Theorem 1 we only weaken the restrictions regarding signal values for this task.

As today's SAT solvers are able to compute (minimal) unsatisfiable cores [Lynce and Silva, 2004] (MUCs) in the CNF clauses, we could implement a diagnosis approach at clause level adopting Reiter's theory. Scalability would however be a severe issue: The diagnosis space would be exponential in the number of clauses, where we can easily have 106 clauses for |τ| = |ϕ| = 200 (see Table 3). We thus introduce for any subformula ψ of ϕ an assumption opψ encoding whether the correct operator was used for ψ. Focusing on these assumptions, the diagnosis space is exponential in the length of ϕ, and furthermore, we argue that the smaller diagnosis set at operator level (at which a designer works) is more intuitive.

For a WFM diagnosis we extend our encoding as follows:

Theorem 2. Assume an updated Table 1, where each clause c is extended to opϕ ∨ c, and an assignment op to all assumptions opψ on ϕ's various subformulae ψ's correctness. An encoding EWFM(ϕ, τ) = E1(ϕ) ∧ E2(τ) of an LTL formula ϕ and a trace τ as of Definitions 6 and 7 is satisfiable, SAT(EWFM(ϕ, τ)), iff τ |= ϕ under assumptions op.

For an SFM diagnosis, each operator assumption toggles between various behavioral (sub-)modes ∈ {nominal ,mode1, . . . ,moden-1}, where, like for the nominal one, the actual behavior has to be defined for any mode via modei ⇒ clause. A good example for an effective fault mode for the strong until operator (U) is suggested by our running example; use a weak until (W) instead. We extend Theorem 2 as follows, where we introduce for any subformula ψ with n modes ld(n) assumption bits opψ,j :

Theorem 3. Assume for a formula ϕ with n modes ld(n) variables opϕ,j , and for a mode 0 ≤ m ≤ n the corresponding mintermM(m) in these variables. Furthermore assume an updated Table 1 where each clause c describing the behavior of mode m for ϕ is extended to ¬M(m) ∨ c, an assignment op to all assumptions opψ on ϕ's various subformulae ψ's modes, and a CNF formula E3 consisting of the conjunction of all negated minterms in the operator mode variables that don't refer to a behavioral mode (for all ψ). Then, an encoding ESFM (ϕ, τ ) = E1(ϕ) ∧ E2(τ ) ∧ E3 of an LTL formula ϕ and a trace τ as of Definitions 6 and 7 is satisfiable, SAT(ESFM(ϕ, τ)), iff τ |= ϕ under assumptions op.

The correctness of both extensions to Theorem 1 follows from that for Theorem 1 and the constructions.

Table 2: The nine SFM diagnoses for the arbiter.

With m the number of signals, n the size of ϕ, o the maximum number of modes for any operator, and p the maximum number of clauses for any operator mode, upper bounds for the number of variables and clauses for EWFM(ϕ, τ) and ESFM(ϕ, τ ) can be estimated as O((m+n)k +n · ld(o)) and O((m · k + n · ld(o) + p · o · k · n) respectively. While the terms can obviously be simplified, they illustrate the origins of the variables and clauses.

Using our encodings, and varying the assumptions on the operators' correctness, we can obviously compute LTL specification diagnoses that have the desired focus on operator occurrences using various diagnosis algorithms, i.e., based on hitting conflicts like Reiter's approach or computing diagnoses directly as, e.g., suggested by [Metodi et al., 2012].

For our proof-of-concept tests, we used HS-DAG which has several interesting features for our setting. Besides being complete, due to its support of on-the-fly computations (including the conflict sets themselves), it is very efficient when limiting the desired diagnosis size. Furthermore, as diagnoses are continually found during computation, they can be reported to the user instantly, which is an attractive feature for interactive tools. For SFM models, we made HS-DAG aware of strong fault modes adopting a notion of conflicts similar to [Nyberg, 2011]. We implemented basic fault models like confusion of Boolean operators, confusion of unary temporal operators, confusion of binary temporal operators, twisted operands for binary temporal operators and "use variable vj instead of vi". Using a SAT solver that is able to return MUCs, we extract those unit clauses from the returned core that assign operator assumptions. Those sets represent our (not necessarily minimal) conflict sets on the operators.

For the arbiter, our WFM approach results in five single fault diagnoses. All five concern (faulty) R4 for line 1, and when rewriting the implication, they are the bold-faced operators in G(¬¬¬g1 ∨∨∨ X(¬gi U ri)). Intuitively, when considering the parse tree, those diagnoses farthest from the root should be prioritized during debugging, which would be the incorrect until for our arbiter example. Our SFM approach derived the nine diagnoses listed in Table 2, where the first one "replace ¬g1 Ur1 by ¬g1 Wr1" catches the actual fault.

While we considered operators F, G, W, and R as (easily rewritable) syntactic sugar for the Theorems, we actually translate these operators directly, reducing the number of variables and clauses, and without rewriting, our diagnoses directly address the operators as originally specified by the designer. Due to lack of space we do not report the corresponding clauses (see [Pill and Quaritsch, 2012]), which however can be easily constructed (with further optimization potential) from those for the until operator via the correspond-

4

(b) Run-time and memory scalability.

Figure 1: Diagnosis performance for random samples.

ing rewrite rules. For the weak until operator, e.g., clause (i) is replaced by ϕk ∨ ∨l≤i≤k δi.

Sharing/reusing subformulae in an encoding (for example if the subformula aUb occurs twice in a specification) could save variables and entail speedups for satisfiability checks. However, this would be counterproductive in a diagnostic context due to situations when only one instance is at fault.

Similarly to instrumenting the specification, we could take the specification as granted (with no instrumenting assumptions) and ask what is wrong with the trace. Via filtering those unit clauses in E2(τ) from the unsat core defining the signals in τ , there is even no need for any instrumentation when considering the weak fault model (which is a strong model in the sense that then the value should be flipped).

3.1 Experimental Results

While the exemplary diagnoses for the arbiter illustrate the viability of our approach, in the following we discuss results for larger samples. We implemented our specification diagnosis approach using Python (CPython 2.7.1) for both the encoding and the HS-DAG algorithm. As SAT solver, we used the most recent minimal unsat core-capable PicoSAT [Biere, 2008] version 936. We ran our tests on an early 2011-generation MacBook Pro (Intel Core i5 2.3GHz, 4GiB RAM, SSD) with an up-to-date version of Mac OS X 10.6, the GUI and swapping disabled, and using a RAM-drive for the file system.

As already mentioned, the on-the-fly nature of HS-DAG allows us to report diagnoses to the user as soon as their validity has been verified. In this context, we investigated the temporal distribution of solutions for both WFM and SFM diagnosis runs. Figure 1(a) shows the number of diagnoses found for any fraction of the total computation time of a single run with a random formula of length 100, derived as suggested in [Daniele et al., 1999] with N = ⌊|ϕ|/3⌋ variables and a uniform distribution of LTL operators. We introduced a single fault in order to derive ϕm from ϕ, and using our encoding we derived an assignment for τ ∧ϕ∧¬ϕm that defines τ for k = 200 and l = 100. We then solved the diagnosis problem E(ϕm, τ). For a WFM, the computation finished in 3.3 seconds discovering 7 single fault diagnoses (note that the xaxis is given in logarithmic scale). For an SFM, we stopped HS-DAG after 10 hours, with 118 diagnoses computed with a memory footprint of 1 GiB. It is important to note, however, that within one minute, all 40 single fault diagnoses were found, more than can be presumably investigated by a user in this time. All the 63 double fault diagnoses were identified after 9 minutes, and thus the majority of the 10 hours were spent for another 15 diagnoses with cardinality 3 or 4.

In Figure 1(b) we show some results regarding diagnosis scalability for random samples with varying sizes. For any |ϕ| in {50, 100, . . . , 300} we generated 10 random formulae as above, and restricted the search to single fault diagnoses. Restricting the cardinality of desired solutions is common practice in model-based diagnosis, and as can be seen from the last column in Table 3, we still get a considerable amount of diagnoses. In Figure 1(b), we report the average total run-time, as well as the maximum resident set size (RSS) of our whole approach and the part for PicoSAT (PS). The performance using a WFM is very attractive, with average run-times below 50 seconds and a memory footprint of approx. 100 MiB (1 MiB = 220 bytes vs. 1 MB = 106 bytes) even for samples with |ϕ| = 300. As expected, the performance disadvantage for SFM against WFM is huge; up to two orders of magnitude for the run-time and up to one for memory (maximum resident size). Identifying an effective modeset, and tool options to focus the diagnosis on certain operators/subformulae (avoiding the instrumentation of all others) seem crucial steps to retain resources for large samples.

Table 3 offers run-time (total and those parts for the SAT solver and creating the encoding), memory and encoding details for WFM and SFM single fault diagnosis of three samples with |ϕ| = |τ| = 200. Apparently the majority of computation time is spent in the SAT solver tackling a multitude of encoding instances, and most of the memory footprint is related to the diagnosis part (the DAG). Thus we report also results for solving a single encoding instance in the following.

Figure 2 shows the run-times for a set of 27 formulae taken from [Somenzi and Bloem, 2000] for 100 random traces with k = 100 and l = 50. These traces were generated such that each signal is true at a certain time step with a probability of 0.5. The graph compares different variants of our encoding and the effects of enabling MUC computation, where Table 4 reports variable and clause numbers when scaling |ϕ| and |τ |.

Compared to an uninstrumented encoding, a WFM one is only slightly slower and an SFM variant experiences a penalty of about factor 5. Apparently, the computation of unsat cores is very cheap, making the "+C" lines nearly indistinguishable from the standard ones. Lacking the space to report corresponding numbers, we experimented also with other SAT solvers (MiniSAT 2.2 [E´en and S¨orensson, 2003] and Z3 4.1 [de Moura and Bjørner, 2008]), comparing LTL-SAT to encoding LTL semantics as an SMT problem with quantifiers over uninterpreted functions in Z3. Regardless of the SATsolver, LTL-SAT outperformed the "na¨ıve" SMT approach, with Z3 in the lead. Presumably due to the returned cores, Z3 proved to be significantly slower than PicoSAT in the diagnosis case, so that we chose the latter for our diagnosis runs.

4 Summary and FutureWork

In this paper, we proposed a novel diagnostic reasoning approach that assists designers in tackling LTL specification development situations where, unexpectedly, a presumed witness fails or a presumed counterexample satisfies a given formal specification. For such scenarios, we provide designers with complete (with respect to the model) sets of diagnoses explaining possible issues. Using the computationally cheaper weak fault model (there are no obligations on faulty operators), a diagnosis defines (a set of) operator occurrences, whose simultaneous incorrectness explains the issue. Defining also abnormal behavior variants in a strong fault model makes computation harder, but diagnoses become more precise in delivering also specific repairs (e.g., "for that occurrence of the release operator flip the operands").

Our implementation for the Linear Temporal Logic, which is a core of more elaborate industrial-strength logics such as PSL and is used also outside EDA, e.g. in the context of Service Oriented Architectures [Garc´ıa-Fanjul et al., 2006], showed the viability of our approach. In contrast to Schuppan's approach [Schuppan, 2012], a designer can define scenarios and ask concrete questions (via the trace), and is supplied with (multi-fault) diagnoses addressing a specification's operator occurrences, rather than unsatisfiable cores of derived clauses. Compared to RuleBase PE's trace explanations via causality reasoning [Beer et al., 2009], we address the specification rather than the trace and provide more detail compared to the set of "red dots" on the trace.

Based on Reiter's diagnosis theory, we use a structurepreserving SAT encoding for our reasoning about a presumed witness' or counterexample's relation to a specification, exploiting the knowledge about a trace's description length k and loop-back time step l. While we used HS-DAG for our tests, our WFM or SFM enhanced encoding obviously supports also newer algorithms like [Stern et al., 2012], and can also be used in approaches computing diagnoses directly [Metodi et al., 2012].

Extending our implementation optimizations, the latter also suggests directions for future encoding optimizations, like transferring the concept of dominating gates to specifications. Exploring incremental SAT approaches [Shtrichman, 2001] will also provide interesting results.

Compared with synthesizing a fix for an operator by solving a game, (our) individual strong fault model variants precisely define the corresponding search space. While this is good in a computational sense, it could lead to missed options, where an elaborate evaluation of fault mode-sets will be interesting future work.

Future research will aim also at accommodating multiple traces in a single diagnosis DAG, while our main objective is supporting constructs from more elaborate languages, like regular expressions (SEREs in PSL) and related operators, i.e., suffix implication and conjunction.

Acknowledgments

Our work has been funded by the Austrian Science Fund (FWF): P22959-N23. We would like to thank the reviewers for their comments and Franz Wotawa for fruitful discussions.