Properties of finite state systems can be expressed using temporal languages; checking whether a given system satisfies the properties specified is an interesting verification problem. There are tools that provide estimations on how well the testing process covers the states of the system.

Chockler, Halpern, and Kupferman relate coverage to causality that is based on counterfactual dependence, and bring the notion of a degree of responsibility to the context of coverage, fault tolerance, and understanding error traces. The paper explains the concepts very well and provides a good review of the background material, making it easy to read.

However, computation of the degree of responsibility is hard and requires a separate computation for each of the variables of a given property. The paper provides a linear algorithm for the special case of read-once Boolean formulas, with the assumption that the formulas are expressed in positive normal form.

The concepts are explained using a detailed example. Although the finite state machine (FSM) for the example is clear, the design description in Figure 5 is not legal Verilog and needs to be corrected.

Adoption of these ideas into a tool can take significant implementation effort, and the integration of the computations for coverage and degree of responsibility into a single algorithm requires further research.