Responsibility in Actor-Based Systems

Christel Baier; Johannes Lehmann; Sascha Kl\"uppelholz

REVIEW 3 major objections 3 minor 40 references

Responsibility in Actor-Based Systems

T0 review · 3 major / 3 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper shows how Shapley values can be used to assign responsibility for safety violations to the modules, variable values, or actions of a reactive program.

desk verdict A useful synthesis with two solid actor-extraction schemes and one flawed action-based scheme whose responsibility values depend on an arbitrary action ordering. read the letter →

arxiv 2412.05162 v1 pith:VCIGFQT3 submitted 2024-12-06 cs.FL

Christel Baier , Sascha Klüppelholz , Johannes Lehmann This is my paper · ORCID

classification cs.FL

keywords responsibilityShapleyvaluessafetypropertiestransitionsystemsreactivemodulesmodelcheckingcounterexamplesactorsets

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Modern reactive systems are often too complex for a counterexample alone to explain why a safety specification fails. This paper argues for a quantitative answer: assign each 'actor' of the system a number, a Shapley value, that measures how often that actor's choices are pivotal for whether the system can avoid a bad state. It unifies forward and backward responsibility in one framework and shows how to build actor sets directly from a reactive program's syntax, so actors can be modules, variable values, or actions. Two model transformations turn modules and actions into actors, and the paper proves both preserve which bad states are reachable, making the computed responsibility values meaningful for the original program. Initial experiments suggest the approach can rank suspects for debugging and scale to hundreds of thousands of states when the actor set is small.

What carries the argument

The load-bearing object is the Shapley value of a coalitional game defined by a safety game: for a coalition $C$ of actors, the game value $\gamma(C)$ is 1 if the coalition plus auxiliary states can force a run that never enters a bad state, and 0 otherwise, and $\mathrm{Shap}_\gamma(a)$ averages the marginal contributions $\gamma(C \cup \{a\}) - \gamma(C)$ over all coalitions not containing $a$. The two model transformations carry the argument: the scheduler construction splits states where several modules can act, and the action-separation construction splits each state's actions into auxiliary ?-states, !-states, and a demonic state. The soundness lemmas 4.3 and 4.10 connect the transformed games back to the original program by showing that bad-state reachability is preserved.

What would settle it

Take a program with a state that has at least two actions, reverse the ordering of those actions in Definition 4.9, recompute the action-based Shapley values for all actors, and compare; if any value changes, the responsibility score is an artifact of the ordering rather than a well-defined property of the program.

Watch

Extended reading notes

Core claim

The central claim is that Shapley-value responsibility, previously defined for arbitrary sets of states, can be attached to natural syntactic units of a reactive program without changing the safety semantics. For modules, the paper adds a scheduler module whose single variable records which module or synchronizing action is active, so each module becomes the set of states where it is active. For actions, it expands each state into a chain of auxiliary states that offer or skip each action, so each action becomes an actor that can be individually removed from a coalition. Lemmas 4.3 and 4.10 show both constructions preserve reachability of the bad states, and the reported case studies use the resulting values to identify the responsible module, time value, or action in a specification violation.

Load-bearing premise

The load-bearing premise is that the arbitrary ordering of a state's actions chosen in the action-separation construction does not affect the resulting responsibility values, and the paper does not prove this independence.

Editorial extensions

If this is right

If a safety invariant is violated, module-based responsibility values rank system components by how much influence they have on avoiding that violation.
Value-based actors group states by partial variable assignments, so their responsibility values identify which control points or variable values are most critical.
Action-based actors do the same for program instructions; the puzzle-box example shows that an unused action can receive responsibility zero.
The soundness of the scheduler and action-separation transformations means these rankings are not artifacts of the transformations, because bad states are reachable exactly when they were reachable in the original program.
Since computation is exponential in the number of actors but polynomial in model size, choosing a coarse actor signature makes the method feasible on models with hundreds of thousands of states.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The arbitrary ordering of actions fixed in Definition 4.9 is an implementation choice; until order-independence is proved or a canonical order is fixed, two tools using different orders could report different responsibility values for the same program.
The same machinery could be applied to per-state action actors rather than global action names, attaching responsibility to individual transitions and making the output closer to a line of code; the paper lists this as future work.
A responsibility value is an average over all coalitions, so it measures how often an actor is pivotal rather than whether it caused this particular violation; pairing forward and backward values could separate prevention ability from observed role.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this is a clear, well-written paper. The scheduler construction for module-based actors and the value-based grouping are new and their soundness proofs are correct. The action-separation construction, however, has a load-bearing flaw: Definition 4.9 fixes an arbitrary ordering of the actions per state, and the Shapley values of the action actors depend on that ordering. Reversing the order of two outgoing actions can change the forward responsibility of an action from 1 to 1/2, so the action-based notion is not a well-defined property of the program unless the ordering is made canonical or independence is proved. The paper does neither, and the issue is not mentioned anywhere. This undercuts Section 4.4's claim to identify the most influential program actions.

What is actually new and good: the paper gives a uniform presentation of forward/backward responsibility from [33, 2], which is genuinely useful. The module-based transformation (adding a scheduler) is clever and the soundness lemma is straightforward and correct. The value-based actors are simple but natural. The paper ships code and data, and the case studies give initial insight. The sensitivity of module-based responsibility to modelling style is acknowledged and documented in Section 5.2.

The main soft spot is the action-ordering dependence. A minimal example: a state with two actions, one leading safe and one bad. Under order (α, β), only coalition {α} wins, so α's responsibility is 1. Under (β, α), only {α, β} wins, giving both 1/2. The result changes without changing the program. The paper says "given an arbitrary ordering" but gives no argument that the choice is irrelevant. Other soft spots: the experiments are anecdotal and the performance study is small, but the paper does not overclaim. The complexity results are from prior work, correctly attributed.

Who this is for: people working on explainable verification or Shapley-based responsibility. The module and value actor parts are usable now. The action part needs a fix.

Recommendation: this paper deserves a serious referee. The flaw is real but repairable; a canonical ordering (e.g., lexicographic) would make the definition concrete, and then the results would be reproducible. I would accept it for review with a request for major revision.

Referee Report

3 major / 3 minor

Summary. The paper presents a uniform framework for forward and backward responsibility based on Shapley values in transition systems with safety properties, then proposes three schemes for deriving actors from reactive module programs: module-based actors via a scheduler transformation, value-based actors via partitioning by variable values, and action-based actors via an action-separation transformation. It proves soundness lemmas for the two transformations, states complexity results from prior work, and reports initial experiments with a prototypical implementation.

Significance. If the formalization is corrected, the paper provides a useful practical bridge between Shapley-based responsibility theory and program-level debugging, with concrete actor-extraction algorithms and an available implementation. The direct proofs of Lemmas 4.3 and 4.10 and the reproducible experimental setup are strengths. However, the novel action-separation construction currently has formal defects, and the paper does not fully establish that the proposed action-based values are well-defined properties of the program rather than artifacts of arbitrary choices.

major comments (3)

[Section 4.4, Definition 4.9] The definition of S' as S? ∪ S! ∪ SX omits the original state set S, yet the transition relation is defined by clauses 's_α → t' and 's_X → t' with t ∈ S. Since t is not an element of S', these clauses do not define a transition system. The proof of Lemma 4.10 uses the intended transitions from s_α and s_X to First(t) (for example, 'By construction, there exists a transition to First(ρ_{i+1})'), so the corrected definition should replace t by First(t). This is a load-bearing formal error that must be fixed.
[Section 4.4, Definition 4.9] The sentence 'If there are multiple actions that produce the same transition, we arbitrarily choose one of them' introduces an arbitrary tie-break that changes the responsibility values. For example, let s have transitions s→t via both α and β, and a transition s→bad via γ, with t safe and bad absorbing. If the duplicate transition is assigned to α, then Act(s)={α,γ}; for coalition C={β}, no action in C is available at s, and the transformed game is losing because Reach proceeds to s_X and chooses bad. If the duplicate transition is assigned to β, then Act(s)={β,γ}; C controls s_β? and can move to s_β! and then to First(t), winning. Hence the Shapley value of β is 0 in the first case and positive in the second, purely from the arbitrary tie-break. The paper must provide a canonical treatment (for example, giving each action's !-state all successors produced by that action) or prove invariance.
[Section 4.4, Definition 4.9] The action-based responsibility values are defined relative to an arbitrary ordering of the actions per state, but the paper gives no proof that they are independent of this ordering. The simple two-action counterexample that one might construct with one safe and one bad successor does not actually demonstrate a dependence, since in both orders the coalition containing the action leading to the safe successor wins and the other coalition loses; nevertheless, the general question of order-independence is left open. The paper should either prove that the values are order-independent or fix a canonical order so that the values are a well-defined property of the program.

minor comments (3)

[Section 4.2, Definition 4.4] The definition says 'let S be the state space of T(P, ϕ)' and then defines module-based actors by the value of the variable 'active', but T(P, ϕ) does not contain the variable 'active'. The state space should be that of T(WithSched(P), ϕ).
[Lemma 4.10 proof] The expression 'Next(ρ'_last, α)' is formally undefined because Next is defined on pairs (s, α) for original states s and actions α, not on ?-states; it should be Next(ρ_i, α). With the corrected transition relation from Definition 4.9, the run construction should also explicitly state that the transition from ρ_{i,α(i)} goes to First(ρ_{i+1}).
[Section 5.3] The sentence 'we investigate the time taken to actually compute responsibility only 3' contains a dangling footnote marker '3' with no corresponding footnote text; it should be removed or the footnote should be supplied.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the actor-set transformations and their soundness lemmas are self-contained, and cited prior work is independent background rather than load-bearing input.

full rationale

The paper's central new content is the extraction of module-, value-, and action-based actor sets and the two model transformations that support them. Lemma 4.3 and Lemma 4.10 prove reachability equivalence between the original transition system and the transformed systems by direct run-projection arguments; neither proof assumes the Shapley-based responsibility values it is meant to support. The forward and backward responsibility notions in Section 3 are definitions built on standard Shapley values and safety games, not quantities fitted to data or predicted from hidden parameters. The complexity statements are attributed to the prior papers [33] and [2], which are separate published works with their own proofs; the present paper adapts those results rather than using them as an unverified premise for a circular conclusion. The self-citations are therefore not load-bearing in a way that makes the derivation equivalent to its inputs. One non-circular concern deserves explicit note: Definition 4.9 fixes an arbitrary ordering of the actions of each state when constructing the action-separated system, and the paper does not show that the resulting action-based Shapley values are independent of that ordering. This is a well-definedness and correctness question about the proposed notion, not a circularity: the responsibility values are still computed from the constructed game rather than being assumed or fitted. Overall, the derivation chain is self-contained for the claims it proves, and no step reduces to its own input by construction.

Assumptions & free parameters 0 free parameters · 3 assumptions · 2 invented entities

The paper introduces no fitted numerical parameters; the central definitions are deterministic. The unproven order-independence of Definition 4.9 is the main free choice that affects results. The scheduler and action-separation states are new formal objects introduced by the paper, justified only by reachability preservation, not by independent evidence that they capture intuitive responsibility.

assumptions (3)

standard math Safety games are determined and winning regions can be computed in linear time
Invoked in Section 3.1 for the complexity of the positivity and threshold problems; standard result cited as [18, Theorem 12].
domain assumption The operational semantics of the reactive modules language in Section 4.1 correctly captures the behavior of the program
The paper defines the semantics itself, so this is a modeling assumption that the transition system T(P, phi) is the right representation.
ad hoc to paper The arbitrary ordering of actions in Definition 4.9 does not affect the resulting responsibility values
The construction depends on First(s) and Next(s, alpha) for an arbitrary ordering, but no independence proof is provided; this is a load-bearing unproven assumption for action-based actors.

invented entities (2)

Scheduler module (Definition 4.2)
purpose: Adds an active variable and scheduler commands to split state ownership among modules and synchronising actions.
The scheduler is a syntactic construction whose soundness is only proven for safety reachability (Lemma 4.3); whether it yields a meaningful notion of module responsibility is not independently validated.
Action-separation states s_alpha?, s_alpha, s_X (Definition 4.9)
purpose: Separate the enabling of an action from its execution so that each action can be an actor.
The classification of ?-states as actors, !-states as auxiliary cooperative, and X-states as adversarial is a modeling choice without outside evidence; the responsibility values depend on this choice.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Responsibility in Actor-Based Systems." pith.science (2026). https://pith.science/paper/VCIGFQT3

@misc{pith2026241205162,
  author       = {Pith},
  title        = {Pith review of: Responsibility in Actor-Based Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VCIGFQT3}},
  note         = {Machine review of arXiv:2412.05162}
}

read the original abstract

The enormous growth of the complexity of modern computer systems leads to an increasing demand for techniques that support the comprehensibility of systems. This has motivated the very active research field of formal methods that enhance the understanding of why systems behave the way they do. One important line of research within the verification community relies on formal notions that measure the degree of responsibility of different actors. In this paper, we first provide a uniform presentation of recent work on responsibility notions based on Shapley values for reactive systems modeled by transition systems and considering safety properties. The paper then discusses how to use these formal responsibility notions and corresponding algorithms for three different types of actor sets: the module-based notion serves to reason about the impact of system components on the satisfaction or violation of a safety property. Responsibility values for value-based actor sets and action-based actors allow for the identification of program instructions and control points that have the most influence on a specification violation. Beyond the theoretical considerations, this paper reports on experimental results that provide initial insights into applicability and scalability.

Figures

Figures reproduced from arXiv: 2412.05162 by the authors.

**Figure 2.** Example program in the reactive modules language [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗

**Figure 3.** Model of Ada and Julia throwing rocks at a potentially rock-pr [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗

Figures from the paper (5 more)

**Figure 4.** Figure 4: Model of Ada and Rebeca’s drive from Malm¨o to V¨aster˚as. [PITH_FULL_IMAGE:figures/full_fig_p014_4.png]

**Figure 5.** Figure 5: Action-separation transformation applied to a state with th [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]

**Figure 6.** Figure 6: Model of Rebeca’s puzzle box. For the sake of simplicity, over [PITH_FULL_IMAGE:figures/full_fig_p018_6.png]

**Figure 7.** Figure 7: Distribution of module-based responsibility among the schedu [PITH_FULL_IMAGE:figures/full_fig_p020_7.png]

**Figure 8.** Figure 8: Runtimes for the computing responsibility values for the thre [PITH_FULL_IMAGE:figures/full_fig_p022_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 22 canonical work pages

[1]

Reactive modules

Rajeev Alur and Thomas A Henzinger. “Reactive modules”. In: Formal methods in system design 15 (1999), pp. 7–48. doi: 10.1023/A:1008739929481. url: https://doi.org/10.1023/A:1008739929481

doi:10.1023/a:1008739929481 1999
[2]

Backward responsibility in transitio n systems using general power indices

Christel Baier, Roxane van den Bossche, Sascha Kl¨ uppelholz, Johannes Lehmann, and Jakob Piribauer. “Backward responsibility in transitio n systems using general power indices”. In: Proceedings of the AAAI Con- ference on Artiﬁcial Intelligence . Vol. 38. 18. 2024, pp. 20320–20327. doi: 10.1609/aaai.v38i18.30013. url: https://doi.org/10.1609/aaai. v38i18.30013

work page doi:10.1609/aaai.v38i18.30013 2024
[3]

From Veriﬁcation to Causality-Based Explications (Invited Talk)

Christel Baier, Clemens Dubslaﬀ, Florian Funke, Simon Jantsch, R upak Majumdar, Jakob Piribauer, and Robin Ziemek. “From Veriﬁcation to Causality-Based Explications (Invited Talk)”. In: 48th International Col- loquium on Automata, Languages, and Programming (ICALP) . Vol. 198. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2021, 1:1–1:20. do...

work page doi:10.4230/lipics.icalp.2021.1 2021
[4]

A Game-Th eoretic Account of Responsibility Allocation

Christel Baier, Florian Funke, and Rupak Majumdar. “A Game-Th eoretic Account of Responsibility Allocation”. In: Proceedings of the Thirti- eth International Joint Conference on Artiﬁcial Intellige nce, IJCAI-21 . Ed. by Zhi-Hua Zhou. Main Track. International Joint Conference s on Artiﬁcial Intelligence Organization, Aug. 2021, pp. 1773–1779. doi: 10.249...

work page doi:10.24963/ijcai.2021/244 2021
[5]

Responsib il- ity Attribution in Parameterized Markovian Models

Christel Baier, Florian Funke, and Rupak Majumdar. “Responsib il- ity Attribution in Parameterized Markovian Models”. In: Thirty-Fifth AAAI Conference on Artiﬁcial Intelligence (AAAI) . AAAI Press, 2021, pp. 11734–11743. doi: 10.1609/AAAI.V35I13.17395. url: https://doi. org/10.1609/aaai.v35i13.17395

work page doi:10.1609/aaai.v35i13.17395 2021
[6]

Principles of model checking

Christel Baier and Joost-Pieter Katoen. Principles of model checking . MIT Press, 2008. isbn: 978-0-262-02649-9

work page 2008
[7]

From symptom to cause: localizing errors in counterexample traces

Thomas Ball, Mayur Naik, and Sriram K. Rajamani. “From symptom to cause: localizing errors in counterexample traces”. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Prog ram- ming Languages . POPL ’03. New Orleans, Louisiana, USA: Association for Computing Machinery, 2003, pp. 97–105. isbn: 1581136285. doi: 10.1145/604131.604140...

arXiv 2003
[8]

Explaining counterexamples using causality

Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, and Ric hard J. Treﬂer. “Explaining counterexamples using causality”. In: Formal Meth- ods Syst. Des. 40.1 (2012), pp. 20–40. doi: 10.1007/S10703-011-0132-2 . url: https://doi.org/10.1007/s10703-011-0132-2

doi:10.1007/s10703-011-0132-2 2012

Show all 40 references

[9]

On correctness, precision, and performance in quantitative veriﬁca tion: QComp 2020 competition report

Carlos E Budde, Arnd Hartmanns, Michaela Klauck, Jan Kˇ ret ´ ıns k´ y, David Parker, Tim Quatmann, Andrea Turrini, and Zhen Zhang. “On correctness, precision, and performance in quantitative veriﬁca tion: QComp 2020 competition report”. In: International symposium on lever- a...

2020 doi
[10]

A Fr ame- work for Certiﬁed Program Analysis and Its Applications to Mobile-Co de Safety

Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula. “A Fr ame- work for Certiﬁed Program Analysis and Its Applications to Mobile-Co de Safety”. In: Veriﬁcation, Model Checking, and Abstract Interpretation , 7th International Conference, VMCAI 2006, Charleston, SC, USA , J...

2006 doi
[11]

Causality and Responsibility for Formal Veriﬁca tion and Beyond

Hana Chockler. “Causality and Responsibility for Formal Veriﬁca tion and Beyond”. In: First Workshop on Causal Reasoning for Embed- ded and safety-critical Systems Technologies (CREST) . Ed. by Gregor G¨ ossler and Oleg Sokolsky. Vol. 224. EPTCS. 2016, pp. 1–8. doi: 10.4204/EP...

2016 doi
[12]

Eﬃcient Aut omatic STE Reﬁnement Using Responsibility

Hana Chockler, Orna Grumberg, and Avi Yadgar. “Eﬃcient Aut omatic STE Reﬁnement Using Responsibility”. In: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Vol. 4963. Lecture Notes in Computer Science. Springer, 2008, ...

2008 doi
[13]

Responsibility and Blame: A Structural-Model Approach

Hana Chockler and Joseph Y. Halpern. “Responsibility and Blame: A Structural-Model Approach”. In: J. Artif. Intell. Res. 22 (2004), pp. 93–

2004
[14]

Wha t causes a system to satisfy a speciﬁcation?

Hana Chockler, Joseph Y. Halpern, and Orna Kupferman. “Wha t causes a system to satisfy a speciﬁcation?” In: ACM Trans. Comput. Log. 9.3 (2008), 20:1–20:26. doi: 10.1145/1352582.1352588. url: https://doi. org/10.1145/1352582.1352588

2008
[15]

Clarke, Orna Grumberg, and Doron A

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model check- ing, 1st Edition . MIT Press, 2001. isbn: 978-0-262-03270-4. url: http:// books.google.de/books?id=Nmc4wEaLXFEC

2001
[16]

Clarke, Thomas A

Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Rode rick Bloem, eds. Handbook of Model Checking . Springer, 2018. isbn: 978-3-319- 10574-1. doi: 10.1007/978-3-319-10575-8 . url: https://doi.org/10. 1007/978-3-319-10575-8

2018 doi
[17]

Responsibility of AI Sy stems

Mehdi Dastani and Vahid Yazdanpanah. “Responsibility of AI Sy stems”. In: AI Soc. 38.2 (2023), pp. 843–852. doi: 10.1007/S00146-022-01481-4 . url: https://doi.org/10.1007/s00146-022-01481-4

2023 doi
[18]

Games on Graphs

Nathana¨ el Fijalkow, Nathalie Bertrand, Patricia Bouyer-Dec itre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian H orn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr N ovotn´ y, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre...

2023 doi arXiv
[19]

Automata, Logics, and Inﬁnite Games: A Guide to Current Research [outc ome of a Dagstuhl seminar, February 2001]

Erich Gr¨ adel, Wolfgang Thomas, and Thomas Wilke, eds. Automata, Logics, and Inﬁnite Games: A Guide to Current Research [outc ome of a Dagstuhl seminar, February 2001] . Vol. 2500. Lecture Notes in Computer Science. Springer, 2002. isbn: 3-540-00388-6. doi: 10.1007/3-540-3638...

2001 doi
[20]

Error explanation with distance metrics

Alex Groce, Sagar Chaki, Daniel Kroening, and Ofer Strichman. “Error explanation with distance metrics”. In: International Jour- nal on Software Tools for Technology Transfer 8 (2006), pp. 229–247. doi: 10.1007/s10009-005-0202-0 . url: https://doi.org/10.1007/ s10009-005-0202-0

2006 doi
[21]

What went wrong: Explaining counte rex- amples

Alex Groce and Willem Visser. “What went wrong: Explaining counte rex- amples”. In: International SPIN Workshop on Model Checking of Soft- ware. Springer. 2003, pp. 121–136. doi: 10.1007/3-540-44829-2_8 . url: https://doi.org/10.1007/3-540-44829-2_8

2003 doi
[22]

Causes and explanations: A structural-model approach. Part I: Causes

Joseph Y Halpern and Judea Pearl. “Causes and explanations: A structural-model approach. Part I: Causes”. In: The British journal for the philosophy of science (2005)

2005
[23]

Causes and explanations: A structural-model approach. Part II: Explanations

Joseph Y Halpern and Judea Pearl. “Causes and explanations: A structural-model approach. Part II: Explanations”. In: The British journal for the philosophy of science (2005)

2005
[24]

A Modiﬁcation of the Halpern-Pearl Deﬁnit ion of Causality

Joseph Y. Halpern. “A Modiﬁcation of the Halpern-Pearl Deﬁnit ion of Causality”. In: IJCAI. AAAI Press, 2015, pp. 3022–3033

2015
[25]

Temporal-Safety Proofs for Systems Code

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C . Necula, Gr´ egoire Sutre, and Westley Weimer. “Temporal-Safety Proofs for Systems Code”. In: 14th International Conference on Computer Aided Veriﬁcati on (CAV). Vol. 2404. Lecture Notes in Computer Science. Springer...

2002 doi
[26]

Cert i- ﬁcation for µ-Calculus with Winning Strategies

Martin Hofmann, Christian Neukirchen, and Harald Rueß. “Cert i- ﬁcation for µ-Calculus with Winning Strategies”. In: 23rd Interna- tional Symposium on Model Checking Software (SPIN) . Vol. 9641. Lecture Notes in Computer Science. Springer, 2016, pp. 111–128 . doi: 10.1007/978-...

2016 doi
[27]

PRISM 4.0: Veriﬁc ation of Probabilistic Real-time Systems

M. Kwiatkowska, G. Norman, and D. Parker. “PRISM 4.0: Veriﬁc ation of Probabilistic Real-time Systems”. In: Proc. 23rd International Conference on Computer Aided Veriﬁcation (CAV’11) . Ed. by G. Gopalakrishnan and S. Qadeer. Vol. 6806. LNCS. Springer, 2011, pp. 585–591. doi: 1...

2011 doi
[28]

The PR ISM benchmark suite

Marta Kwiatkowska, Gethin Norman, and David Parker. “The PR ISM benchmark suite”. In: 9th International Conference on Quantita- tive Evaluation of SysTems . IEEE CS press. 2012, pp. 203–204. doi: 10.1109/QEST.2012.14. url: https://doi.org/10.1109/QEST.2012. 14

2012 doi
[29]

Evaluation of Measures for Statistical Fault Localisation and an Op - timising Scheme

David Landsberg, Hana Chockler, Daniel Kroening, and Matt Le wis. “Evaluation of Measures for Statistical Fault Localisation and an Op - timising Scheme”. In: 18th International Conference on Fundamental Approaches to Software Engineering (F ASE) . Ed. by Alexander Egyed and I...

2015 doi
[30]

Tool to compute actor-based responsibility

Johannes Lehmann. Tool to compute actor-based responsibility . Sept
[31]

SpinCause: a tool f or causality checking

Florian Leitner-Fischer and Stefan Leue. “SpinCause: a tool f or causality checking”. In: International Symposium on Model Checking of Software (SPIN). ACM, 2014, pp. 117–120. doi: 10.1145/2632362.2632371. url: https://doi.org/10.1145/2632362.2632371

2014
[32]

A formally veriﬁed compiler back-end

Xavier Leroy. “A formally veriﬁed compiler back-end”. In: Journal of Auto- mated Reasoning 43.4 (2009), pp. 363–446. doi: 10.1007/s10817-009-9155-4 . url: http://xavierleroy.org/publi/compcert-backend.pdf

2009 doi
[33]

Responsibility and veriﬁcation: Importance value in tempor al log- ics

Corto Mascle, Christel Baier, Florian Funke, Simon Jantsch, an d Stefan Kiefer. “Responsibility and veriﬁcation: Importance value in tempor al log- ics”. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE. 2021, pp. 1–14. doi: 10.1109/LICS52264.2...

2021
[34]

Certifying Model Checkers

Kedar S. Namjoshi. “Certifying Model Checkers”. In: 13th Interna- tional Conference on Computer Aided Veriﬁcation (CAV) . Vol. 2102. Lecture Notes in Computer Science. Springer, 2001, pp. 2–13. doi: 10.1007/3-540-44585-4\_2 . url: https://doi.org/10.1007/3-540- 44585-4%5C_2

2001 doi
[35]

Proof-Carrying Code

George C. Necula. “Proof-Carrying Code”. In: Encyclopedia of Cryptogra- phy and Security, 2nd Ed . Ed. by Henk C. A. van Tilborg and Sushil Jajo- dia. Springer, 2011, pp. 984–986. doi: 10.1007/978-1-4419-5906-5\_864 . url: https://doi.org/10.1007/978-1-4419-5906-5%5C_864

2011 doi
[36]

The Relation Between Forward-Looking and Ba ckward- Looking Responsibility

Ibo van de Poel. “The Relation Between Forward-Looking and Ba ckward- Looking Responsibility”. In: Moral Responsibility: Beyond Free Will and Determinism. Ed. by Nicole A. Vincent, Ibo van de Poel, and Jeroen van den Hoven. Dordrecht: Springer Netherlands, 2011, pp. 37–52. isb...

2011 doi
[37]

A value for n-person games

Lloyd S Shapley. “A value for n-person games”. In: Contributions to the Theory of Games 2 (1953)

1953
[38]

Strategic Responsibility Under Imper- fect Information

Vahid Yazdanpanah, Mehdi Dastani, Wojciech Jamroga, Natas ha Alechina, and Brian Logan. “Strategic Responsibility Under Imper- fect Information”. In: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’19, Montr eal, QC, Canada,...

2019
[115]

url: https://doi.org/10.1613/jair

doi: 10.1613/JAIR.1391. url: https://doi.org/10.1613/jair. 1391

doi
[2024]

url: https://doi.org/10

doi: 10.5281/zenodo.13738447. url: https://doi.org/10. 5281/zenodo.13738447

doi

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [1]

Reactive modules

Rajeev Alur and Thomas A Henzinger. “Reactive modules”. In: Formal methods in system design 15 (1999), pp. 7–48. doi: 10.1023/A:1008739929481. url: https://doi.org/10.1023/A:1008739929481

doi:10.1023/a:1008739929481 1999

[2] [2]

Backward responsibility in transitio n systems using general power indices

Christel Baier, Roxane van den Bossche, Sascha Kl¨ uppelholz, Johannes Lehmann, and Jakob Piribauer. “Backward responsibility in transitio n systems using general power indices”. In: Proceedings of the AAAI Con- ference on Artiﬁcial Intelligence . Vol. 38. 18. 2024, pp. 20320–20327. doi: 10.1609/aaai.v38i18.30013. url: https://doi.org/10.1609/aaai. v38i18.30013

work page doi:10.1609/aaai.v38i18.30013 2024

[3] [3]

From Veriﬁcation to Causality-Based Explications (Invited Talk)

Christel Baier, Clemens Dubslaﬀ, Florian Funke, Simon Jantsch, R upak Majumdar, Jakob Piribauer, and Robin Ziemek. “From Veriﬁcation to Causality-Based Explications (Invited Talk)”. In: 48th International Col- loquium on Automata, Languages, and Programming (ICALP) . Vol. 198. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2021, 1:1–1:20. do...

work page doi:10.4230/lipics.icalp.2021.1 2021

[4] [4]

A Game-Th eoretic Account of Responsibility Allocation

Christel Baier, Florian Funke, and Rupak Majumdar. “A Game-Th eoretic Account of Responsibility Allocation”. In: Proceedings of the Thirti- eth International Joint Conference on Artiﬁcial Intellige nce, IJCAI-21 . Ed. by Zhi-Hua Zhou. Main Track. International Joint Conference s on Artiﬁcial Intelligence Organization, Aug. 2021, pp. 1773–1779. doi: 10.249...

work page doi:10.24963/ijcai.2021/244 2021

[5] [5]

Responsib il- ity Attribution in Parameterized Markovian Models

Christel Baier, Florian Funke, and Rupak Majumdar. “Responsib il- ity Attribution in Parameterized Markovian Models”. In: Thirty-Fifth AAAI Conference on Artiﬁcial Intelligence (AAAI) . AAAI Press, 2021, pp. 11734–11743. doi: 10.1609/AAAI.V35I13.17395. url: https://doi. org/10.1609/aaai.v35i13.17395

work page doi:10.1609/aaai.v35i13.17395 2021

[6] [6]

Principles of model checking

Christel Baier and Joost-Pieter Katoen. Principles of model checking . MIT Press, 2008. isbn: 978-0-262-02649-9

work page 2008

[7] [7]

From symptom to cause: localizing errors in counterexample traces

Thomas Ball, Mayur Naik, and Sriram K. Rajamani. “From symptom to cause: localizing errors in counterexample traces”. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Prog ram- ming Languages . POPL ’03. New Orleans, Louisiana, USA: Association for Computing Machinery, 2003, pp. 97–105. isbn: 1581136285. doi: 10.1145/604131.604140...

arXiv 2003

[8] [8]

Explaining counterexamples using causality

Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, and Ric hard J. Treﬂer. “Explaining counterexamples using causality”. In: Formal Meth- ods Syst. Des. 40.1 (2012), pp. 20–40. doi: 10.1007/S10703-011-0132-2 . url: https://doi.org/10.1007/s10703-011-0132-2

doi:10.1007/s10703-011-0132-2 2012