PaperlayerView exact revision on arXiv

Source-linked AI summary

Sufficient Reasons and Explanations for Reactive Systems

Hadar Frenkel, Nadav Rutman Moshe

arXiv:2610.02184v1cs.FL

TL;DR

Reactive systems can be checked against temporal specifications, but a correctness result does not necessarily explain why they satisfy or falsify them. The paper formalizes sufficient reasons and contrastive explanations, including temporal variants, and analyzes their complexity. It reports representation results for minimal sufficient reasons and PSPACE-completeness for verification problems.

  • Problem

    Correctness checks for reactive systems do not always explain why a system satisfies or falsifies its temporal specification.

    Source: §1 · p. 1

  • Method

    The paper defines event-based and temporal sufficient reasons and contrastive explanations for reactive systems and provides algorithms and complexity analyses for their verification and synthesis.

    Source: §1 · p. 2, §10 · p. 18

  • Results

    Minimal event-set sufficient reasons always have an ultimately periodic representation, minimal temporal sufficient reasons have a unique ω-regular form, and verification problems are PSPACE-complete.

    Source: §1 · p. 3

  • Takeaways & Limitations

    For violating traces, sufficient reasons can identify behavior that would still violate a specification, while contrastive explanations identify minimal changes that would avoid the violation.

    Source: §1 · p. 2

    The prototype is not yet a fully automated tool; the authors plan to develop it for automatic computation of the explanation types.

    Source: §10 · p. 19

Abstract

from arXiv · show

We address the problem of temporal causality and explainability for reactive systems, and, in this setting, study sufficient reasons and contrastive explanations. These two notions are well-known explainability measures in the context of neural networks. In this work, we unify these notions for reactive systems and formal specifications given in temporal logic, providing dedicated definitions for sufficient reasons and contrastive explanations. We then lift these definitions to \emph{temporal} sufficient reasons and contrastive explanations, providing more general and symbolic representations of explainability. We analyze the complexity of both verifying and finding explanations of the different types, and we demonstrate our approach using a prototype implementation.

1 Introduction

The paper studies why reactive systems satisfy or violate temporal specifications, a question not answered by correctness checks alone. It formalizes sufficient reasons and contrastive explanations for these systems, including temporal variants, and analyzes their complexity.

1 Introduction

  • Reactive systems interact indefinitely with their environment, and LTL can verify specification correctness without necessarily explaining why a system satisfies or falsifies it.The paper places its work alongside prior research on temporal actual causality in reactive systems.Source: §1 · p. 1
  • Sufficient reasons describe actions that preserve an outcome, whereas contrastive explanations describe minimal changes that avoid it.The paper adapts these explainability notions, already used for neural-network outputs, to reactive systems and temporal logic.Source: §1 · p. 2
  • On a violating trace, sufficient reasons identify behavior that would still violate the specification, while contrastive explanations identify changes that could avoid violation.The analogous analysis of satisfying traces identifies actions that maintain satisfaction or changes that could lead to violation.Source: §1 · p. 2
  • The paper defines sufficient reasons and contrastive explanations for reactive systems as event sets and as temporal properties.It also presents algorithms for verifying and finding these explanations, complexity analyses, and a prototype implementation.Source: §1 · p. 2
  • Temporal sufficient reasons can have a unique ω-regular minimal form, while minimal event-set reasons always have an ultimately periodic representation.The event-set representation can be found by solving a model-checking instance.Source: §1 · p. 3
  • Verification of minimal and temporal sufficient reasons and contrastive explanations is PSPACE-complete, stemming from the underlying LTL model-checking problem.The paper focuses mainly on sufficient reasons; contrastive explanations receive briefer treatment.Source: §1 · p. 3

2 Preliminaries

The preliminaries define reactive-system traces, the automata and temporal logics used to reason about them, and the explanation concepts that the paper adapts. HyperLTL serves as a meta-logic for expressing reasons and explanations.

2 Preliminaries

  • A reactive system is modeled as an input-deterministic Mealy machine whose transition function maps a state and input set to a next state and output set.A path induces an infinite trace of input-output valuations.Source: Transition Systems and Temporal Logic · p. 3
  • A Büchi automaton accepts an infinite word when some run visits accepting states infinitely often; the paper represents transition systems as such automata for operations including intersection.Every LTL formula can also be translated into a Büchi automaton.Source: Transition Systems and Temporal Logic · pp. 3–4
  • LTL expresses properties of individual infinite traces, while HyperLTL adds trace variables and quantifiers and is used here as a meta-logic for explanations.A system satisfies an LTL formula when all its traces satisfy that formula.Source: Transition Systems and Temporal Logic · p. 4
  • An ultimately periodic event set repeats with a fixed period after a finite prefix, giving even an infinite set a finite representation.The preliminaries also define trace projection and pointwise trace union.Source: Transition Systems and Temporal Logic · pp. 3, 5
  • A sufficient reason fixes components of an input so the function's output remains unchanged; a minimal sufficient reason has no proper-subset sufficient reason.A contrastive explanation changes the output, and a minimal one minimizes distance from the original input.Source: Explanations · pp. 5–6

3 Running Example

The running example uses a biased arbiter to illustrate event-based and temporal sufficient reasons, alongside contrastive explanations. In each case, the explanation describes what evidence or change bears on the specified outcome.

3 Running Example

  • In the arbiter, after user1 requests access, user2 can never receive a grant; user1's requests are granted, and user2's requests are granted only before user1 requests.Source: §3 · p. 6
  • For the trace that repeatedly contains both requests and user1's grant, the event r1 at time 0 is a minimal sufficient reason for the violation of eventual g2.Any superset of that event is also a sufficient reason for the violation.Source: §3 · p. 6
  • For the same trace and effect g1, the paper gives temporal sufficient reasons including r1, and identifies r1 as the minimal temporal sufficient reason.The reason is a temporal property satisfied by the trace and sufficient to observe g1.Source: §3 · p. 6
  • A closest contrastive trace for g1 is the repeated trace containing r2 and g2, which avoids g1 by avoiding every occurrence of r1.Source: §3 · p. 6

4 Definitions

The definitions set up event-set reasons and their trace representations, then formulate verification and synthesis for reasons drawn from a system trace. An augmented system and automata operations support the formal constructions.

4 Definitions

  • An event set of input propositions and time points is represented by an infinite trace that marks each time with r and includes the selected inputs.Ultimately periodic event sets have ultimately periodic trace representations.Source: §4 · p. 7
  • The augmented transition system preserves original system behavior and adds traces that can represent event sets.Its number of transitions can grow exponentially with the input-proposition set, while its size remains linear in the original system size.Source: §4 · p. 7
  • Projection removes propositions from an automaton's alphabet, while extension adds propositions without changing its original transitions.Source: §4 · p. 7
  • The problem considers an LTL effect and a trace of the transition system satisfying that effect, and asks about reasons represented as event sets or trace properties.For each reason type, it distinguishes verifying a proposed reason from synthesizing a minimal one.Source: Problem Definition · p. 7

5 Non-Temporal Sufficient Reasons

The section defines sufficient reasons as input events on a trace that guarantee an LTL effect across matching system traces, then encodes their verification and synthesis using HyperLTL. It establishes finite-representation results and complexity bounds, while showing that minimal event-based reasons need not always exist.

5 Non-Temporal Sufficient Reasons

  • An event set is a sufficient reason when every system trace matching the original trace on those inputs at those times satisfies the effect; it is minimal if no strict subset also suffices.Reasons range over input propositions, while the effect may involve all atomic propositions.Source: §5 · p. 8
  • All input events on a satisfying trace always form a sufficient reason, with a finite trace representation.This universal reason does not guarantee a minimal one exists.Source: §5 · p. 8
  • Countable event reasons can lack a minimal member when they form an infinite strictly descending chain, as in the recurring-g1 example.The example gives a chain of reasons that successively omits earlier inputs, with no minimal sufficient reason.Source: §5 · p. 8

5.1 Logical Encoding of Sufficient Reasons

  • For ultimately periodic traces, a reason exists iff an ultimately periodic reason exists, enabling finite HyperLTL-based verification and synthesis.The paper encodes reasons with trace representations and reduces their verification or synthesis to HyperLTL model checking.Source: §5.1 · pp. 8–9, §5.1.1 · p. 9

5.2.1 Verification of Sufficient Reasons

  • PSPACE-complete SR verification uses ultimately periodic reasons and traces, with the system and LTL property as inputs.The stated bound applies to verifying whether a given reason is sufficient.Source: §5.2.1 · p. 10

5.2 Complexities and Algorithms of SRs Verification and Synthesis

  • MSR verification is PSPACE-hard with an at most double-exponential upper bound, while MSR synthesis is at most 3EXPTIME in the size of φ.Synthesizing an arbitrary SR is trivial because the all-input reason always works; the paper reports finding MSRs in reasonable time in its prototype.Source: §5.2.1 · p. 11, §5.2.2 · p. 11

6 Temporal Sufficient Reasons

Temporal sufficient reasons extend event-based reasons to temporal properties, including cases where useful event-set reasons are unavailable. The section defines these reasons and presents verification and synthesis results.

6 Temporal Sufficient Reasons

  • A TSR holds on the given trace and guarantees the effect on every system trace satisfying it; minimality excludes any strictly broader TSR.This seeks the weakest sufficient condition, rather than the strongest condition used by some temporal-causality approaches.Source: §6 · pp. 11–12

6.1 Verification of Temporal Sufficient Reasons

  • For LTL-formula reasons, verification checks φR → φ over the system’s traces, not over all possible traces.The verification approach encodes temporal reasons in HyperLTL and uses HyperLTL model checking.Source: §6.1 · p. 12
  • Verifying whether a trace property is a TSR is PSPACE-complete for NBA or LTL representations.The hardness proof reduces LTL model checking to TSR verification.Source: §6.1 · p. 12

6.2 Synthesis of Minimal Temporal Sufficient Reasons

  • In Example 5, the MTSR constrains inputs at even timesteps because odd-position inputs do not influence the output.This reason is not expressible in LTL, but has a simple NBA representation.Source: §6.2 · p. 13
  • The MTSR is the projection of the system traces satisfying the effect onto the input propositions, and it is unique and ω-regular.Its construction can require an NBA even when the effect is given as an LTL formula.Source: §6.2 · pp. 13–14
  • The MTSR depends on the effect and system, not on which satisfying trace is chosen; users can choose more concrete non-temporal reasons instead.The only constraint on the trace is that it satisfies the effect.Source: §6.2 · p. 14
  • Finding the MTSR is exponential in the size of the LTL effect.The bound follows from the automaton construction and the exponential size of the effect automaton.Source: §6.2 · p. 14

7 Contrastive Explanations

The section defines contrastive explanations as system traces that violate an effect satisfied by the reference trace, with minimality based on the changes from that trace. It presents HyperLTL-based verification and synthesis, extends the notion to temporal sets of explanations, and relates minimal contrastive explanations to sufficient reasons.

7 Contrastive Explanations

  • A minimal contrastive explanation is a violating system trace for which no violating trace has a strictly smaller set of changes from the reference trace.The distance records the inputs and timesteps at which traces disagree.Source: §7 · p. 14

7.1.1 Verification of Minimal Contrastive Explanations

  • HyperLTL encodes the minimality condition: every system trace agreeing with the reference wherever the candidate agrees must satisfy the effect.A fixed candidate can be checked using the encoding; verifying an ultimately periodic candidate is PSPACE-complete.Source: §7.1 · p. 15, §7.1.1 · p. 15

7.1 Verification and Synthesis of CEs using HyperLTL Encoding

  • MCE synthesis existentially quantifies over candidate traces in the HyperLTL encoding, with complexity at most double-exponential in the effect formula.A witness is an MCE; its projection over input propositions gives an input-only contrastive explanation.Source: §7.1.1 · p. 15

7.2 Temporal Contrastive Explanations

  • A minimal temporal contrastive explanation is the set of all MCEs projected over input propositions, and verifying one is PSPACE-complete.The verification approach represents the set as an omega-regular language and modifies the MCE formula.Source: §7.2 · p. 16, §7.2.1 · p. 16

7.3 Between Sufficient Reasons and Contrastive Explanations

  • Minimal sufficient reasons and MCEs are related but not dual: every MCE differs from at least one event in each minimal sufficient reason.The system constrains which traces are available, so negating sufficient-reason events does not directly derive contrastive explanations.Source: §7.3 · p. 16

8 Evaluation

The evaluation uses a preliminary prototype to illustrate the approach and compare it with existing temporal-causality tools. The reported comparisons are intended to provide intuition, not to rank different explanation notions.

8 Evaluation

  • The prototype evaluation is preliminary rather than an automated tool, with transition systems, input traces, and effects hard-coded in each test.The causal analysis using HyperLTL model checking remains general.Source: §8 · p. 17
  • The TSR verification approach runs faster than CATS on its benchmarks because TSRs are easier to verify than temporal actual causes.The authors caution that the approaches address different notions of causality, so the comparison is not intended to determine which is better.Source: §8 · p. 17
  • The paper compares MTSR synthesis with CORP and illustrates MSR synthesis, while describing its approach as incomparable with because of differing effects and reason representations.The approach handles LTL effects and can represent infinite event sets; handles HyperLTL effects and provides finite event sets.Source: §8 · p. 17

9 Related Work

The related-work section positions sufficient reasons and contrastive explanations as explainability notions adapted from AI, distinct from prior temporal-causality work. It also situates the paper's comparisons with existing tools and its ability to represent infinite event sets.

9 Related Work

  • Sufficient reasons and contrastive explanations were defined for k-nearest-neighbor classification, and this paper lifts them to temporal explanations for formal verification.Other AI works also treat these notions as formal explanations.Source: §9 · pp. 17–18
  • Table 1 compares TSR verification with CATS actual-causality judgments, while Table 2 compares MTSR synthesis with CORP.The Table 1 caption notes that the tools may judge a formula differently because they address different explanation notions.Source: Table 1 · p. 18, Table 2 · p. 18
  • Prior work addresses temporal effects and explanations, but the paper defines contrastive explanations over infinite traces and general LTL effects, unlike work limited to finite traces or restricted effects.Counterfactual theory in is described as orthogonal because it uses a new temporal logic for counterfactual worlds.Source: §9 · p. 18
  • Earlier temporal actual-causality work includes definitions, tools, synthesis, and complexity analysis; this paper develops corresponding aspects for sufficient reasons and contrastive explanations.Unlike, which finds finite event sets, this approach can find infinite sets using an ultimately periodic representation.Source: §9 · p. 18

10 Conclusions

The paper concludes that it formalizes sufficient reasons and contrastive explanations for reactive systems with LTL effects, including temporal variants, algorithms, and complexity analyses. Its appendix supplies background definitions for LTL and HyperLTL, while future work targets an automated prototype and relations among explanation notions.

10 Conclusions

  • The paper provides formal definitions, algorithms, and complexity analyses for verification and synthesis of non-temporal and temporal sufficient reasons and contrastive explanations for reactive systems with LTL effects.The authors present sufficient reasons as another view of explainability and identify further formalization of explainability notions as future work for understanding systems and behavior.Source: §10 · pp. 18–19
  • The authors plan to develop the prototype into a fully automated tool and study relations and derivations among causality and explainability notions.The planned automation covers minimal and temporal sufficient reasons and contrastive explanations.Source: §10 · p. 19

A LTL and HyperLTL

  • The appendix defines LTL satisfaction over infinite words and states that a system satisfies an LTL formula when all its traces satisfy it.It also describes HyperLTL as extending LTL with trace quantification and relational properties over infinite executions.Source: A LTL and HyperLTL · p. 23

B Full Proofs

The proofs connect reason verification to LTL model checking and establish PSPACE-completeness for temporal sufficient reasons. They also characterize how minimal contrastive explanations intersect minimal sufficient reasons.

B Full Proofs

  • Lemma 1 equates the event-set reason condition f[R, π] with ψ_sr on the augmented system, whose relevant traces recover those of the original system..Source: B Full Proofs · p. 24
  • Verifying a temporal sufficient reason is PSPACE-complete when the reason is given as a Büchi automaton or an LTL formula.The proof handles both encodings through model-checking procedures and reduces LTL model checking for hardness.Source: B Full Proofs · p. 24
  • The hardness reduction adds a fresh trace and modifies the effect so that true is a temporal sufficient reason exactly when the original system satisfies the original effect.The construction is polynomial in the transition system and formula.Source: B Full Proofs · p. 25
  • Every minimal contrastive explanation differs from each minimal sufficient reason on at least one event.Theorem 9 states that their event-difference set has nonempty intersection with every minimal sufficient reason.Source: B Full Proofs · p. 25

C Additional Tables for Experimental Evaluation

The additional evaluation tables describe verification judgments and synthesized reason or explanation representations, along with how their outputs should be interpreted.

C Additional Tables for Experimental Evaluation

  • Table 3 marks whether each tool accepts a formula as a cause or reason, but CATS and TSR assess different notions.CATS considers actual causality, whereas TSR considers sufficient reasons.Source: Table 3 · p. 26
  • Table 4 reports the effect being explained and the state counts of generated MTSR and CORP witness automata.|A| and |B| denote the respective automaton state counts.Source: Table 4 · p. 27
  • Table 5 compares logical formulas derived from the synthesized automata, with some causes representable only as NBAs and not equivalent LTL formulas.The MTSR and CORP implementations output explicit NBAs; LTL formulas were derived manually for semantic comparison.Source: Table 5 · p. 27
  • Table 6 lists the original trace and synthesized minimal counterfactual trace, using a dash when no counterfactual exists.Figure 4 presents minimal contrastive explanation synthesis, and its caption says the results align with the definitions.Source: Figure 4 · p. 26, Table 6 · p. 28
  • Table 7 reports each minimal sufficient reason as an event set over input propositions and time steps, with infinity marking a reason that repeats on the loop.Source: Table 7 · p. 28
Loading 2610.02184v1…