Beyond Static Diagnosis: A Temporal ASP Framework for HVAC Fault Detection

One early example of declarative MBD is the work by Friedrich and Nejdl [14]. The authors introduce a direct diagnosis approach using hyperresolution in Prolog [5]. Unlike traditional MBD methods that first generate conflicts and then apply a hitting set algorithm to derive diagnoses, their approach obtains candidates directly as a subset of the consistent logical model encoded in Prolog.

Similarly, declarative MBD approaches using ASP define the system model directly in the formalism of the reasoning engine, avoiding an intermediate transformation into a separate logic or constraint representation. Wotawa [47] investigates ASP as an alternative reasoning mechanism for diagnosis of the well-known ISCAS85 circuits. In a consistency-based fashion, the ASP encoding describes the system as a composition of interconnected components, each defined by its nominal behavior. Observations are incorporated in the model as constraints, ensuring that any valid diagnosis must be consistent with the observed behavior. The empirical results indicate that while a traditional dedicated diagnosis algorithm is often faster, ASP is a stable and reliable approach. In an extension of this research, Wotawa and Kaufmann [48] present their direct $\mathrm{IDIAG}$ algorithm that iteratively generates all diagnoses with a cardinality of $0$ to $n$ based on a theorem prover. Their evaluation revealed that ASP-based diagnosis performance is comparable to specialized algorithms for digital circuits. However, for analog circuits, the required grounding process led to a significant increase in computation time.

Bayerkuhnlein and Wolter [4] propose an alternative ASP encoding for diagnosing faults in programming assignments within an intelligent tutoring system, incorporating intermediate values to enhance fault analysis. In addition, to their “traditional” ASP-based framework, they propose the use of Constraint Answer Set Programming, which enables reasoning over non-groundable domains, to deal with large or infinite domains in their application.

Prikler and Wotawa [34] introduce multi-shot solving, heuristics, and preference-based optimizations in ASP diagnosis and show that heuristic-based methods generally yield faster solutions. By incorporating incremental solving techniques, the authors improve the $\mathrm{IDIAG}$ diagnosis algorithm, making it more competitive with specialized diagnosis approaches. Experiments on the ISCAS85 circuits revealed that ASP-based diagnosis can match or outperform hitting-set-based methods when properly optimized.

The ability to reason about changing environments is fundamental to many AI applications, particularly in explaining observed phenomena and diagnosing unexpected system behaviors [7]. For instance, Raiman et al. [37] showed that even a single, weak temporal axiom – the non-intermittent-fault assumption – in combination with multiple snapshots allows to disregard explanations that would otherwise be candidates. McIlraith [28] applied Situation Calculus [27] to MBD to address temporal phenomena. By using Situation Calculus as the logical framework for diagnosing faults in dynamic systems, the approach can address fundamental challenges such as the ramification problem. In parallel, Thielscher [42] extended Fluent Calculus [43] to dynamic domains, enabling reasoning about system evolution and diagnosis using a constraint-based representation of healthy system behavior. Building on these foundations, Baral, McIlraith, and Son [3] use an action languages to provide a more compact and computationally efficient representation of diagnosis in dynamic systems. In the domain of robotics, Gspandl et al. [18] present a belief management system that embeds history-based diagnosis into the $\mathrm{IndiGolog}$ Situation-Calculus interpreter. Their method keeps a set of possible action histories and updates them after every step. It checks each history against the newest sensor readings, explains any inconsistencies by selecting the most plausible fault hypothesis, and retains only the best-supported histories to guide the robot’s next action.

Further advancing the field, Balduccini and Gelfond [2] exploit ASP in combination with the action language $𝒜ℒ$ to integrate diagnosis into an intelligent agent architecture. In their approach, $𝒜ℒ$ is used to formalize a high-level description of the system behavior, specifying actions, fluents, and causal laws. A-Prolog, logic programming under answer set semantics, serves as the computational framework for diagnosing faults. Their approach enables intelligent agents to perform diagnosis, testing, and repair within a unified framework of A-Prolog.

Temporal logics are another formalism that has been used for diagnostic purposes, e.g., for behavioral diagnosis of Linear-Temporal Logic (LTL) specifications [33]. More recently, Feldman et al. [13] proposed Finite-Trace Next Logic (FTNL) and a SAT-based algorithm to diagnose synchronous sequential circuits. FTNL is a simpler temporal logic as it considers only finite traces and restricts temporal expressiveness to a single next operator. The FTNL formula is unrolled for a finite horizon before passing it to a SAT solver with a novel encoding that reduces the number of variables and clauses and has been shown to be efficient on the ISCAS89 circuits.

Our work is a natural extension of previous research as it combines declarative diagnostic modeling via ASP with FEC to capture behavior over time. Thus, we enable temporal reasoning that accounts for the progression of system behavior with the goal of efficient and effective FDD in the building heating domain.

In MBD [11, 38], we describe a system as a set of components, whose nominal behaviour can be formulated using some system of logics, e.g., first-order logic. A diagnosis problem occurs once we have gathered observations.

The diagnosis task, given a system description, components and observations as above, is to determine which components, if any, are faulty. The approach taken by MBD is based on consistency between the system description and observations: if the observations match the nominal behaviour of the system, no component needs to be marked as faulty. However, the system description may also formulate constraints based on the assumption that some $c\in \text{COMP}$ is healthy, typically written $\neg \text{ab}(c)$. If one assumes to the contrary $\text{ab}(c)$, said constraints are no longer enforced, allowing consistency once again if they were not to hold otherwise.

A diagnosis problem is ill-defined if $\mathrm{\Delta }=\text{COMP}$ is not a diagnosis. Loosely speaking, when all components of a system are found to be abnormal, there is no nominal behaviour to expect. On the other extreme, we expect $\mathrm{\Delta }=\mathrm{\varnothing }$ to be a diagnosis when the system behaves as intended.

More generally, we are interested in diagnoses that are in some sense minimal, that is diagnoses that do not mark components as faulty without reason.

ASP [6, 25] is a logic programming paradigm that allows for non-monotonic reasoning. An answer set program consists of rules of the shape

where $a$ and $b_i$ are atoms and not denotes default negation – that is $\text{not}x$ is assumed to hold unless $x$ is known to hold. The head of a rule $r$ is $h(r)=\{a\}$ and the body consists of positive atoms $b^{+}(r)=\{b_1,\mathrm{\dots },b_m\}$ and negative atoms $b^{-}(r)=\{b_{m+1},\mathrm{\dots },b_n\}$. Intuitively $h(r)$ follows if all atoms in $b^{+}(r)$ holds and no atom in $b^{-}(r)$ holds. A rule is called a fact, if $m=n=0$.

We call an answer set program ground if no variable occurs in any of its rules. The Gelfond-Lifschitz transformation [16] of a ground program $P$ with respect to a set of atoms (or model) $\tau$ is

By construction $P^{\tau }$ is a Horn formula and thus admits one unique minimal model. If this model is $\tau$, then $\tau$ is a stable model.

The rest of this section deals with non-ground programs, particularly Clingo extensions that we make use of. Non-ground answer set programs keep the basic shape of answer set programs, but use a wider set of literals than pure atoms and their default negations.

The first natural extension to ASP is the use of (implicitly quantified) variables. Consider for example the program

which is one way of formulating the “Tweety problem”. Given $\text{bird}(\text{tweety})$, we want to derive $\text{flies}(\text{tweety})$. Given $\text{penguin}(\text{tweety})$, we want to derive $\text{bird}(\text{tweety})$, but not $\text{flies}(\text{tweety})$, and so on.

To solve answer set programs with variables, we need to ensure that all replacements of variables with concrete (that is variable-free) terms are properly accounted for. To this end, we construct the Herbrand base of the program and then ground the program with respect to it.

Our definition of grounding is notably looser than the ones we find in literature, for reasons that will become apparent once we discuss extensions other than variables. However, even when dealing with variables, the traditional approach of replacing a variable with every possible term in $𝒰(P)$ one at a time is a wasteful over-approximation that modern solvers tend to avoid [31].

In some places, where a domain is explicitly known, one can also use a pool as a notational shorthand rather than a variable. Pools are collections of terms separated by semicolons, i.e., written as $t_1;\mathrm{\dots };t_n$ with $t_i$ terms for $1\le i\le n$. Similar to variables, rules are instantiated with each possible replacement of the pool with one of its terms. As an illustrative example, the pooled “fact”

is a shorthand for the facts

Similar to variables, we might want to perform calculations on numbers, both concrete numbers and again variables. Let and $t_1,t_2$ terms, then $t_1\prec t_2$ is an arithmetic literal that the solver must evaluate numerically after having replaced all variables with concrete numbers.

We continue with conditional literals. Written $b:c_1,\mathrm{\dots },c_n$, conditional literals are grounded by replacing the symbolic or arithmetic literal $b$ with all replacements $b^{x=t}$, where $c_1^{x=t},\mathrm{\dots },c_n^{x=t}$ hold, where $l^{x=t}$ denotes the replacement of variables $x$ with concrete terms $t$ similar to how variables are handled in grounding.

Aggregate literals are written as $l\{b_1;\mathrm{\dots };b_n\}u$, where $l,u$ are integers and $b_1,\mathrm{\dots },b_n$ are literals²²2We only deal with a particular type of head aggregates here. Clingo also supports other aggregates, that are not needed within the scope of this paper., enforce a lower and upper bound respectively on the number of $b_1,\mathrm{\dots },b_n$ that may hold. Both $l$ and $u$ may be omitted; in this case no bound is enforced. As a special case, $\{a\}$ for a single literal $a$ is known as a choice expression and states that $a$ may or may not follow as the result of applying some rule.

For a more complete description of the syntax and semantics of Clingo, we refer the interested reader to [15].

The event calculus (EC) [23, 29] is a logical framework for representing and reasoning about actions (events) and their effects. FEC [26] extends this framework from the boolean domain to arbitrary domains.

The FEC has a sort $ℱ$ for fluents (variables $f,f^{\prime },f_1,f_2,\mathrm{\dots })$, a sort $𝒜$ for actions (variables $a,a^{\prime },a_1,a_2,\mathrm{\dots })$, a sort $𝒱$ for values (variables $v,v^{\prime },v_1,v_2,\mathrm{\dots })$, and a sort $𝒯$ for discrete points in time (variables $t,t^{\prime },t_1,t_2,\mathrm{\dots })$. For the scope of this paper, it suffices that $𝒯\subset \mathbb{N}$ and hence time is totally ordered under the comparison $\le$. Key predicates are $\text{happens}\subset 𝒜\times 𝒯$ and $\text{causes\_value}\subset 𝒜\times ℱ\times 𝒱\times 𝒯$. The function $\text{domain}:ℱ\to 2^{|𝒱|}$ assigns a domain to each fluent, while $\text{value\_of}:ℱ\times 𝒯\to 𝒱$ assigns a value to each fluent at each time step.

To describe the relationships between these predicates and functions, we first define the auxiliary predicates $\text{value\_caused}\subset ℱ\times 𝒱\times 𝒯$, $\text{value\_caused\_between}\subset ℱ\times 𝒱\times 𝒯\times 𝒯$ and $\text{other\_value\_caused\_between}\subset ℱ\times 𝒱\times 𝒯\times 𝒯$.

As can be seen from their definitions, value_caused posits that some action happens at the specified time, which gives cause for some fluent to take a certain value, whereas value_caused_between posits that such an action takes place within the interval $[t_1,t_2)$. Finally, other_value_caused_between posits that an action within the interval gives cause to some other value. In all of these, gives cause needs to be interpreted in a non-deterministic manner: a non-deterministic action, such as a dice roll, gives cause for any side of the dice to show up, but only one side will show up. Likewise, if two people try to respectively open and close a door, the door will not be open and close at the same time³³3It may however be “half open” if such a state is modeled..

With these auxiliary definitions, we can define notions of cause, effect and inertia. Axiom FEC3 deals with inertia: a fluent which takes on a certain value at some time and has no action changing that value, will still take on that value in the future. Axiom FEC4 deals with cause and effect in a roundabout way: a fluent can not take on a value without cause if another value has been caused in some interval.⁴⁴4The original formalization [26] uses a slightly different variant of FEC3 that also takes into account values caused at $t_1$. This is redundant as per FEC4. Note that our FEC4 is functionally identically to the original formalization, but makes use of the additional auxiliary axiom FEC2a. Calling back to our earlier examples of non-deterministic outcomes, the consequent discards any value that has been given cause within the interval, leaving only values that were given cause to be potential effects.

Finally, we constrain fluents to only take values from their assigned domains.

The axioms FEC1, FEC2a, FEC2b, FEC3, FEC4, and FEC5 define the functional event calculus.

We assume, that the health state of a component may vary over time and thus model it as a fluent, i.e., $ℱ\supset \{\text{health}(c)|c\in \text{COMP}\}$. The health state of a component is composed of the good state ok and at least one abnormal state. The domain of this health state can be modeled as $\text{domain}(\text{health}(c))=\{\text{ok},\text{ab}\}$ in a weak fault model, whereas in a strong fault model we have $\text{domain}(\text{health}(c))=\{\text{ok},{\text{ab}}_1,\mathrm{\dots }{\text{ab}}_n\}$ for some $n$.

In order to allow for the health state of a component to switch from ok to ab (or ${\text{ab}}_i$ for some $i$), we allow unknown actions to occur. Likewise, to model repair, we add a dedicated repair action for each component. Formally, we have $𝒜\supset \{\text{unknown}\}\cup \{\text{repair}(c)|c\in \text{COMP}\}$. The singular unknown action acts as a stand-in for any number of actions that are all unknown.

The effects of unknown and repair actions are captured by $\text{causes\_value}\supset U\cup R$ with $U\subset \{(\text{unknown},\text{health}(c),v,t)|c\in \text{COMP},v\in \text{domain}(c)\setminus \{\text{ok}\},t\in 𝒯\}$ modeling the unknown action and $R=\{(\text{repair}(c),\text{health}(c),\text{ok},t)|c\in \text{COMP},t\in 𝒯\}$ modeling repair. Semantically, the repair actions always give reason for a component to become healthy (but they do not always happen), whereas unknown actions are free to give cause for some, but not all health states to change.

In ASP, we implement unknown actions using Listing 1. This implementation adds two further constraints: first $\text{happens}(\text{unknown},t)\leftarrow \exists f,v[\text{causes\_value}(\text{unknown},f,v,t)]$ ensures that the unknown action happens (and thus takes effect) when it is supposed to cause a value. Second, the unknown action only causes a healthy state to become abnormal, i.e., $\text{causes\_value}(\text{unknown},f,v,t)\to \text{value\_of}(f,t)=\text{ok}$. By not allowing the unknown action to transition between faulty state, we prevent the health state from alternating between to values that have (near-)identical symptoms attached to them.

We imagine idealized components to have three kinds of fluents attached to them: inputs, outputs and internal controls. Most components will have at least one input and an output, as well as a nominal relation between them.

In FEC, we need to represent this nominal relation using actions. For example, an analog adder has two numeric inputs $i_1,i_2$, one numeric output $o$ and the nominal relation $o=i_1+i_2$. This nominal relation is upheld by the adder adding its inputs; hence adding is an action (performed by the adder).

In ASP, we may describe adders as a generalized component as in Listing 2. The first line communicates that numbers are defined outside of the current scope – typically in the place where an adder is used. The second line states that adders are a component. A fluent for its health state is automatically created by code that implements Section 4.1. The third and fourth line define the fluents related to an adder and their domains respectively. Finally, the rule for inferring causes_value establishes the semantics of adding.

In addition to nominal behavior, abnormal behavior must also be described via actions. While all behavior is at the end implemented using mere logic rules, it makes sense to conceptually distinguish between

• $\mathrm{■}$

  abnormal behavior that causes no change in any fluent,

• $\mathrm{■}$

  abnormal behavior that modifies existing actions, and

• $\mathrm{■}$

  abnormal behavior that causes new actions to occur.

The first kind of abnormal behavior is already implemented without any additional rules, as axioms FEC3 and FEC4 uphold that nothing happens without an action.

For abnormal behaviour that modifies existing actions, alternative rules with causes_value in their head need to be written. Just like the rules for the nominal behavior, these depend on the value of the health state. A typical assumption in a weak fault model would be “anything goes”, i.e., the action may give cause for affected fluents (when in doubt: all output fluents) to take any value from its domain. A strong fault model could instead assume that the outcome differs only slightly from the one that is expected.

For abnormal behavior that causes new actions to occur, we also need to write rules with happens in their head, which again depend on the health state of a component.

As an alternative to the above, a generic rule could encode all possible behaviour, with constraints restricting the possible actions and caused values in the nominal state. An example of this is shown in Listing 3.

Having modeled individual components, it is now time to model the connections between them. As in traditional model-based diagnosis, we assume that the values at either end of a connection is always the same as the other – if this is not the case, we can always add components that introduce the necessary delays.

Similar to the approach used by Wotawa and Kaufmann [48], we can establish connections with an auxiliary predicate $\text{bound}\subset ℱ\times ℱ$ and the rule

To make the relation symmetrical, one can write $\text{bound}(f_1,f_2)\wedge \text{bound}(f_2,f_1)$. Note that this rule does not yet propagate values caused from one fluent to another. To this end, the rule

can be used.

Apart from fluents that are unconditionally bound, our system also supports conditionally bound fluents. We write these as

where $f_2$ typically refers to a fluent that may have its value changed by an action of the component $c$.

Alternatively, one could model connections by using the same fluent as the input/output of the affected components, i.e., using shared fluents. This incurs a level of indirection, as a mapping of fluents to component inputs/outputs needs to be established and consistently used.

The axioms FEC3 and FEC4 make it so that one unit of time passes between cause and effect of a change and thus assume a passage of time between them. Modeling time this closely requires sampling at the speed of change, which is wasteful, as often small changes accumulate over time to make large changes. Instead, we may wish to establish effects that become visible “immediately”, that is in the same time step as they occur.

To this end, we introduce the predicates $\text{causes\_value\_immediately}\subset \text{causes\_value}$ and $\text{value\_caused\_immediately}\subset \text{value\_caused}$. The semantics of these “immediate” predicates is similar to their non-immediate counterparts, except that they cause a value change to be observed in the same time step rather than the next.

To make axioms FEC3 and FEC4 respect immediate changes, we replace FEC2a with FECi2. Intuitively, this version of value_caused_between allows “between” to mean at the end of the interval, or $t=t_2$, when a value is caused immediately, while preserving $t_1\ne t_2$.

Lastly, a value caused immediately must have its change actually happen in the same time step. This is enforced by FECi3. Without this axiom, two “immediate” changes happening at times $t$ and $t+1$ would trigger non-determinism in FEC4, allowing either value to be taken.

This set of axioms allows us to model sensors that are polled at regular intervals as well as components that merely propagate changes (e.g., idealized non-sequential components of sequential circuits).

The heat distribution line is hydraulically designed as an injection circuit with a globe valve. Figure 1 depicts its schematics. When the heating system is switched on, the central flow pipe transports hot water to the flow pipe ($FP$) of the heat distribution line. The central return pipe is connected to the return pipe ($RP$) of the heat distribution line and transports the cooled water back to the transfer station. The heat output in the zone is regulated by controlling the temperature of the water in the flow pipe. This control is based on the outdoor temperature and is adjusted through a motorized valve. The room temperature is regulated directly at the radiators within the zone.

The relationship between the outdoor temperature and the room temperature is represented by the heating curve, which determines the setpoint for the flow pipe temperature. The lower the outdoor temperature, the higher the supply temperature must be to ensure the desired room temperature.

The heat distribution line consists of the following components:

• $\mathrm{■}$

  Heat Exchanger ($H$): $H$ transfers heat from the hot water in the flow pipe to the indoor air within the zone.

• $\mathrm{■}$

  Temperature Sensors ($T_1,T_2$): $T_1$ measures the temperature of the water in the flow pipe and serves as a reference for control, while $T_2$ monitors the return water temperature.

• $\mathrm{■}$

  Pumps ($P_1,P_2$): The pumps circulate water within the heating circuit and maintain constant pressure. $P_1$ and $P_2$ operate alternately or remain simultaneously switched off. As soon as one pump is running, there is a flow.

• $\mathrm{■}$

  Valve ($V$): The motorized globe valve regulates the mixing ratio of flow and return water by modifying its position. It serves as the control element, adjusting the proportion of hot flow water entering the heating zone based on its position (0–100%). At 0%, no hot heating water is injected, meaning the flow temperature equals the return temperature. At 100%, the maximum amount is injected, and the flow temperature corresponds to the district heating supply temperature.

• $\mathrm{■}$

  Check valve ($CV$): $CV$ prevents direct bypassing of hot water from the flow pipe to the return pipe, ensuring proper circulation within the heating system.

• $\mathrm{■}$

  Outdoor Temperature Sensor: Although not depicted in Figure 1, this sensor provides an essential input for the control system.

Additionally, we have preconfigured value ranges to verify the plausibility of the measured values, along with supplemental constraints that further define the system:

• $\mathrm{■}$

  The measured flow temperature must always be higher than the measured return temperature.

• $\mathrm{■}$

  The measured flow temperature may be up to a maximum of 2 K lower than the setpoint temperature.

• $\mathrm{■}$

  The measured flow temperature may exceed the setpoint temperature by a maximum of 1 K.

We simplify our model as outlined in Figure 2:

• $\mathrm{■}$

  Mixing valve ($MV$): The check valve $CV$ and motorized globe valve $V$ from Figure 1 are simplified into a singular mixing valve $MV$.

• $\mathrm{■}$

  Mixing valve ($IV$): A second mixing valve $IV$ is added. This mixing valve is controlled by the answer set program to always use the active pump.

• $\mathrm{■}$

  Temperature Sensors ($T_1,T_2$): The temperature sensors $T_1$ and $T_2$ are “loosely” attached to the system – they only measure the temperature, but do not influence it.

• $\mathrm{■}$

  Main Pump ($MP$): A “main pump” $MP$ abstracts the link to the district heating transfer station.

Each component type has a set of fluents associated with its instances. For example, pumps have the fluents $\{\text{<object type="image/svg+xml" data="dagpub-standalone-dagpub-svg-2026-01-26-16-43-16.pdf2svg.svg" id="S5.SS2.p2.m1.g1nest" class="ltx\_graphics ltx\_img\_square" width="10" height="10" style="width: 20px; height: unset; max-width: 100\%"></object>},F^{\leftarrow },F^{\to },T^{\leftarrow },T^{\to }\}$ indicating their power status (“on” or “of”), inflow, outflow, inflow temperature and outflow temperature respectively. In ASP, we model these fluents and their domains as in Listing 4.

We model pumps so that they allow for temperature to change in the direction of their input – that is, if the input is warmer than the current output, the next output is allowed to be warmer, and likewise for colder inputs. To model this behavior, we introduce two actions – heating and cooling respectively. The heating action is shown in Listing 5.

Mixing valves can either immediately forward temperatures and flows from one of their inputs or mix them, allowing for any temperature between the warmer and the colder side to be achieved at their output. Finally, the heat exchanger allows for any output strictly below its input.

The preconfigured value ranges form the domains of fluents within our model. In particular, we discretize them, so that any integer temperature value within the known range is a temperature, power and flow are binary (“on” or “off” and “flowing” or “not flowing” respectively), and the mixing valves have positions 1, 2, and mix. The constraints regarding the flow temperature are implemented by additional rules for components and groups of components. The adjustment of setpoints and valve positions is unchecked, as is the condition that both pumps must operate alternately.

We assess our model on three real-world traces, one containing data from operation under nominal conditions, and two where the valve was leaking and stuck respectively. We prepare those traces so that initial values for all fluents of interest – particularly, the states of the pumps and valve as well as all measured temperatures – are available, but encode later changes of the state only via actions. This means that in order to arrive at the correct diagnoses, the solver can not simply rely on the input providing the state directly, but has to actually reason about the actions and retain information.⁵⁵5It should be noted that in continuous monitoring scenarios, residual-based and data-driven approaches also require updates of internal variables when they start diverging.

We consider two scenarios for our evaluation: first, we apply a naïve approach using a single solver call to diagnose $n$ time steps at once. As we will see, this approach is quite effective for small $n$, but does not scale well as the number of time steps and thus the solution space increases. Next, we integrate multiple solver calls over a rolling window to achieve more efficient diagnosis over a larger number of time steps. In both scenarios, we use a domain-specific heuristic to ensure trace-minimal diagnoses. A diagnosis $\mathrm{\Delta }$ is trace-minimal if $\mathrm{\nexists }{\mathrm{\Delta }}^{\prime }\forall t:{\mathrm{\Delta }}_t^{\prime }\subseteq {\mathrm{\Delta }}_t$, that is there is no other diagnosis that reports a subset of components as broken in each time step $t$. A stricter heuristic would consider subset-minimal diagnoses in the final time step.

Table 1 shows the diagnoses eventually yielded after 8, 16, and 64 time steps. For the nominal trace, there is a false positive at a certain time step, where in our discretization $T_1$ and $T_2$ report the same temperature despite $T_1$ still being larger. This issue could be solved by increasing the precision, e.g., by premultiplying with 10, 100, or 1000, which however also leads to larger domains for the fluents, and thus a significantly larger solution space.

For the faulty traces, the correct diagnosis is always among the diagnoses in the leaking case, but curiously absent in the stuck case when only a smaller part of the input is considered. In fact, with just one more time step, that is $n=9$, we get the same diagnoses as for $n=16$. More generally, without repair actions, which are absent from our inputs, diagnoses only grow larger. For most traces, this means that eventually a fixed point will be reached, where no more information is gained by considering future time steps – especially if $\mathrm{\Delta }=COMP$. Practical applications should however consider repair sooner.

We also see an interesting behaviour with $n=64$ by choice of our heuristic, as we compute the minimal diagnoses w.r.t. all time steps, but only report the last. In this data set, we encounter multiple steps where components supposedly break. The first yields the diagnoses $\{\{H\},\{T_1\},\{T_2\}\}$ – the second component, i.e., $T_1$, $T_2$ or $MV$, only breaks later and thus there are different explanations. If instead one were to compute the minimal diagnosis for the last time step only, these gratuitous diagnoses would vanish.

In terms of performance, we find that a naïve approach of using ASP to diagnose $n$ time steps does not scale for increasingly large $n$. The performance limitations can be seen in Figure 3: while the total diagnosis time for 8 time steps is just three times that of 2 time steps – and thus scales sublinearly up to this point – diagnosis times for 16 time steps are more than twice as large. For even larger window sizes, e.g., $w=32$ or $w=64$, performance is worse still, if such window sizes are even feasible – in our experiments, we found $w=64$ to be infeasible and thus used a rolling window for Table 1. A window size of $4\le w\le 8$ appears optimal from our observations. The overhead of preserving fluents seems negligible.

The rolling window, however, introduces soundness problems to the diagnosis, as information is lost between subsequent invocations of the solver. It is both possible to be too strict and not strict enough about the fluent values to remember. Table 2 shows a few examples of different configurations – varying the window size $w$, the number $n$ of time steps considered, and the set $K$ of fluents, whose value is carried over to the next window (not including the ab health states, i.e., the previous diagnoses, which are always kept) – leading to different results.

It is well possible, that in the general case, this inconsistency can – or must be – resolved by means of another answer set program and solver call. Particularly, cautious consequences (cf., e.g., [1]) would indicate which fluents must take a certain value in any answer set that assumes a particular diagnosis, but may not be enough to also model which fluents may not ever take a certain value while assuming a particular diagnosis. We leave this gap to future work.