{"id":"cc26d5af-4caf-4d16-b473-a91bf4111d02","arxiv_id":"2412.05162","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper introduces three methods for deriving actor sets from reactive modules and shows how their Shapley-value based responsibility can be computed, with soundness proofs and a prototype implementation.","lead":"This paper adapts Shapley-value based responsibility measures from transition systems to programs written in a reactive module language, by extracting actors from modules, variable values, or actions. It shows how these responsibility values can point to the components or control points that matter most for a safety violation, with a prototype tool and initial experiments.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Action-based responsibility is not invariant under the arbitrary per-state action ordering in Definition 4.9; reversing the order changes Shapley values, so the central action-ranking claim is not well-defined as stated.","rationale":"The reader's weakest assumption is exactly the load-bearing point: Definition 4.9 fixes an arbitrary action order, and the paper does not prove the resulting responsibility values are independent of it. My hand-check shows the dependence is concrete, not hypothetical: the same transition system, with the same action set, gives Shapley values (1, 0) under one order and (1/2, 1/2) under the reversed order. This matters because action-based actors are one of the three headline actor-generation schemes, and the abstract credits them with identifying 'program instructions and control points that have the most influence on a specification violation.' With an unspecified ordering, the values are implementation-dependent and not a well-defined property of the program. Lemma 4.10 only proves that reachability of bad states is preserved under the transformation; it does not address invariance of Shapley values. The module-based sensitivity to syntactic details is acknowledged in Section 5.2, but no analogous caveat is provided for the action-based ordering sensitivity. I therefore keep the reader's conditional verdict: the issue is addressable in principle, but as written the central action-based claim is under-specified. A secondary technical gap is that Lemma 4.10's use of First(ρ_n) for an absorbing bad state with no outgoing actions is undefined in Definition 4.9, though that seems easier to repair than the order-dependence problem.","tokens_in":20573,"tokens_out":11622,"duration_ms":126940,"concrete_test":"Run the minimal two-action example above and compare forward Shapley values under the two orderings. If the values differ, the construction is order-dependent; the authors would then need to prove an alternative invariance or explicitly define and justify a canonical ordering before the action-based debugging claim can be accepted.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The action-separation construction (Definition 4.9) fixes an arbitrary ordering of Act(s) and routes non-enabling choices through First(s) and Next(s, α). The Shapley values of the action actors (Definition 4.11) depend on that ordering, and the paper gives no independence or canonicalization argument. Minimal counterexample: initial state s has two actions, α leading to a safe state and β leading to a bad state. Under order (α, β), the transformed safety game is winning exactly for coalitions containing a_α, so the forward Shapley values are (1, 0) for (a_α, a_β). Under order (β, α), the game is winning only for the coalition containing both actors, giving (1/2, 1/2). Thus the reported responsibility of action α changes from 1 to 1/2 solely by reordering the actions. Since Section 4.4 and Example 4.12 use action-based responsibility to identify the most influential program actions, the arbitrary ordering must either be shown irrelevant or be made an explicit, reproducible part of the definition.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":20833,"tokens_out":20284,"duration_ms":209139,"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":[{"comment":"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":"Section 4.4, Definition 4.9"},{"comment":"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":"Section 4.4, Definition 4.9"},{"comment":"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.","section":"Section 4.4, Definition 4.9"}],"minor_comments":[{"comment":"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), ϕ).","section":"Section 4.2, Definition 4.4"},{"comment":"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":"Lemma 4.10 proof"},{"comment":"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.","section":"Section 5.3"}],"recommendation":"major_revision","confidential_remarks":"The stress-test note's main counterexample about the action ordering does not hold as stated, because in the simple safe/bad two-action example the coalition containing the safe action wins in both orders. However, the manuscript has a more serious well-definedness problem in the arbitrary tie-breaking for duplicate transitions, and the formal definition of the action-separation transformation is not well-typed as written. These issues are fixable with a corrected definition and additional proofs, so I recommend major revision rather than rejection. The novelty beyond prior work [33, 2] is modest but real, consisting mainly of the actor-extraction schemes and the experimental study."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat 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.\n\nThe 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.\n\nWho 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.\n\nRecommendation: 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.","headline":"A useful synthesis with two solid actor-extraction schemes and one flawed action-based scheme whose responsibility values depend on an arbitrary action ordering.","tokens_in":21331,"tokens_out":5932,"would_cite":false,"duration_ms":57263,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["responsibility","Shapley values","safety properties","transition systems","reactive modules","model checking","counterexamples","actor sets"],"falsifier":"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.","tokens_in":20381,"feed_emoji":"🎯","tokens_out":8481,"duration_ms":76754,"temperature":0.7,"pith_summary":"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.","feed_headline":"Shapley values rank which program actors cause safety failures","feed_subtitle":"Module, value, and action actors get blame scores that carry through safety-preserving transformations.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the reactive modules formalism in which the programs and the three actor-set constructions are defined.","marker":"[1]"},{"why":"Defines forward responsibility via Shapley values in safety games and establishes the complexity results used in Section 3.","marker":"[33]"},{"why":"Defines backward (pessimistic) responsibility, provides the prototype implementation, and supplies the hardness results adapted here.","marker":"[2]"},{"why":"Provides the Shapley value formula that is the core of the responsibility measure.","marker":"[37]"},{"why":"The model checker used to build transition systems and generate counterexamples for the experiments.","marker":"[27]"},{"why":"Supplies the bounded retransmission protocol model used as the first case study.","marker":"[28]"}],"fun_headline_variants":["Shapley values rank which actors break safety properties","Blame scores for program actors via Shapley values","Shapley responsibility: pinpoint the module at fault","Which actor caused the safety failure? Shapley ranks them","Actor blame assignment via Shapley values in reactive systems"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Shapley values rank which actors break safety properties","Blame scores for program actors via Shapley values","Shapley responsibility: pinpoint the module at fault","Which actor caused the safety failure? Shapley ranks them","Actor blame assignment via Shapley values in reactive systems"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000143,"raw_usage":{"total_tokens":1126,"prompt_tokens":854,"completion_tokens":272,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":470,"completion_tokens_details":{"reasoning_tokens":192}},"tokens_in":470,"tokens_out":272,"duration_ms":3339,"temperature":1.0,"reasoning_tokens":192,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T20:51:20.800900+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Backward responsibility in transitio n systems using general power indices","cited_arxiv_id":null,"evidence_quote":"Defines backward (pessimistic) responsibility, provides the prototype implementation, and supplies the hardness results adapted here."},{"cited_title":"A value for n-person games","cited_arxiv_id":null,"evidence_quote":"Provides the Shapley value formula that is the core of the responsibility measure."}],"review_version":1}