Networks and Distributed Systems
Research group of Prof. Peter Bernard Ladkin, Ph.D.
Some Dubious Theses in the Tense Logic of Accidents
Peter B. Ladkin
Research Report RVS-RR-96-14Abstract:
Some authors propose to use forms of linear time temporal logic
to describe and explain accidents. Common themes are:
(1) that the 'original causes' of an accident precede all other relevant
events;
(2) how to pick the temporal point of view from
which the accident can be explained;
(3) that it is a criterion of successful explanation that an assertion
of the accident event should be logically derivable from assertions of
preceding causally-relevant events;
(4) that the causal relation is expressed by the
tense-logical 'leads to' operator. Some authors have
suggested (5) that an accident is
explained by exhibiting the proof of the weak fairness of
the accident-action. I have explained elsewhere (ad 2) how to pick a
temporal point of view, and (ad 4) that causality is not suitably
expressed by 'leads to'.
I show here that the other three theses are implausible; that (1)
may be rescued only at great cost to intuition and common practice;
that (3) may be modified in the direction of a deductive-nomological model
of explanation; and that (5), if at all worthy, has a much simpler equivalent.
Explaining accidents is a goal of accident reports. Accidents require explanation so that one understands the causal factors involved and takes steps to reduce their occurrence in the future. I asserted in (1) that
- Explanation concerns causes, human intentions and purposes
- Causality involves determining how events unfolded in time
I noted that, according to the second theme above, determining which events are causally significant and determining the progression of these events in time is an important part of explaining causality. Some recent studies have claimed that the causal conditions relevant for accident reports can be defined purely in a formal logic of time. The temporal logic of intervals of Moffett et al. (2) was considered in (3). Johnson and Telford (4) use the language of a specific linear-time tense logic developed for formal reasoning about systems by Lamport: the Temporal Logic of Actions, TLA (5).
Johnson and Telford propose to define causality and write full explanations of accidents entirely within TLA, and propose as their main theses
- 1: that the fundamental causes of accidents temporally precede all derivative causes;
- 2: that accidents can best be described from the temporal point of view of the initial causal events leading to the accident;
- 3: that a criterion of successful explanation is that an assertion of the accident action should be logically derivable from assertions of preceding causally significant events using TLA rules of inference;
- 4: that the 'leads to' operator of temporal logic implements causality;
- 5: that the explanation of the accident is given by exhibiting a proof of the weak fairness of the accident action.
I have discussed in (1) why it may not be possible to explain all the relevant features of an accident sequence entirely within a standard tense logic; namely, features such as tight coupling and interactive complexity (or 'Vernetzheit') of systems (7) (8) are hard to express in the object language of such logics. However, there are some purely logical reasons to doubt these particular five theses. First, some comments on their interrelation.
Thesis 2 seems intuitively to obtain some plausibility from Thesis 1. However, they are independent. The temporal point of view as defined in (1) is the 'now' at which one expresses and interprets all events. Suppose I am running down the road, turn a corner, see another pedestrian, don't manage to avoid her and run right into her. One could describe the sequence of events from the time I turn the corner, in which case the failure to avoid and the ensuing collision are all in the (indeterminate) future; or one could describe it from the time of collision, in which case all the causal events lie in the past, and 'now' is the start of a beautiful friendship. These are two of the choices of the 'temporal point of view'. I argued in (1) for taking the temporal point of view to be contemporaneous with the postcondition of the accident event (events relate two states - a description of the second and how it is related to the first is the postcondition), in which case all the causally relevant events happened in the past of the temporal point of view. Thesis 1 is an assertion of causal origins, and must be substantiated (or not) by metaphysical arguments. The example does not talk about the causal origins of the sequence of events, therefore takes no position on Thesis 1. It also makes clear that Thesis 2 is concerned purely with descriptions of accidents, and is thus purely formal, in contrast to Thesis 1. One may choose a position on Thesis 2 for purely formal reasons. It could simply be mathematically easier to use another temporal point of view other than that proposed by Thesis 2. Such a view was argued in (1), which took no position on Thesis 1.
In the form in which it is expressed, Thesis 3 depends on Thesis 2. TLA contains only the tense-logic 'future' operators [] and <> ('always now and in the future' and 'sometime either now or in the future') and thus cannot refer to the past. For certain choices of temporal point of view, for example, that advocated in (1), one needs past-time tense-logical operators to express the causally-relevant events. I also showed that, for the standard models of temporal logics of action, the past is not a simple mirror of the future, and gave a valid rule of inference for past-time whose counterparts for future-time are not valid - indeed, this was part of my argument for taking the temporal point of view to be the accident occurrence and looking into the past for explanation. I shall not repeat in detail the arguments against Thesis 2.
Deductive-Nomological Explanations Versus Individual Causal Assertions
Despite its seeming dependence on Thesis 2, Thesis 3 may gain independent plausibility when expressed in a more general form. In discussing Thesis 3, I shall restrict myself to so-called 'physical' laws, nomological laws, and not consider human intentions, purposes and actions. This will suffice for the (mostly negative) point I wish to make.There is a tradition in which a goal of explanation is to enumerate collections of facts, premises, laws - the explanans - from which the explanandum follows logically. After Hempel (9), these are called Deductive-Nomological (D-N) models of explanation, to be distinguished from Inductive-Statistical (I-S) models. The theses I am considering fall centrally within a deductive model, and it could be argued that accident reports follow the D-N rather than the I-S model. In a D-N type of explanation, 'follows from' means 'so that it is seen as inevitable'. The aim of a D-N model of explanation is to reduce the concept of (physical) inevitability to that of 'is a logical consequence of'. It follows that the relevant scientific 'laws', embodying physical but (apparently) non-logical 'inevitability', must be explicitly stated as premises of the explanation.
Were a D-N model to succeed, it would follow that logical inevitability is a stronger notion than physical inevitability; that is, if B is logically inevitable given A, then B is physically inevitable given A, but the converse doesn't hold. The argument is as follows. Under a D-N model, B is physically inevitable given A if and only if B is logically inevitable given A together with relevant nomological laws. If B is logically inevitable given A, then any hypotheses whatever may be added to A, and B still logically follows. Thus, by adding any relevant physical laws (however 'relevance' might be determined), if B logically follows from A, then B logically follows from A and these laws, and therefore B is physically inevitable given A.
What relevance do D-N models have to explaining an accident? Mostly, one doesn't quote scientific 'laws' in the premises explaining an accident. Therefore, it seems one is not attempting to give a D-N explanation. But since a D-N model of explanation follows from the requirement to use logical inevitability as the only sort of inevitability, it seems from the discussion above that it would be implausible to insist on explanation as logical inevitability in accident reports while maintaining the heretofore preferred form of explanation of accidents, which doesn't invoke general physical laws. So much the worse for our hopes of saving Thesis 3.
However, it remains a criterion of success for physical theories that they turn physical inevitability into axioms, physical 'laws', plus logical inevitability. The D-N model thus has much to recommend it, were it to be achievable. Similarly, it is worthy as a goal to insist that an accident explanation is complete only when the sequence of behavior is sufficiently well described that the accident event follows as a logical consequence from the premises. But then, one must hope that axioms can be found which, so to speak, 'cut through' the physics of the situation, and enable the accident event to be logically derived, without us having to axiomatise general laws of physics and engineering. This is presumably the motivation behind Thesis 1. However, Thesis 1 cannot substantiate any faith that such axioms exist, because it is implausible, as I shall show below.
Other approaches besides Thesis 1 should be used to attain D-N standards of explanation, if this is desired. But one must beware of simplistic strategies. For example, Thesis 3 could simply be resurrected by fiat: one simply adds enough axioms to enable derivation of the accident event logically from the axioms. As a strategy for explaining an accident, this would be facile, and subject to the accusation of begging the question. If one could suitably restrict the search for such axioms, and motivate the constraint, such a strategy may be more appealing. An example. One could attempt to find key events, such that the accident event could be derived as a logical consequence of these key events plus some laws asserting the inevitable succession of these events. Such key events could be called 'fundamental causes' (as in Thesis 1) or 'root causes'. With a general law of the form that 'all events of type X are followed inevitably by events of type Y', one may derive the future occurrence of an event of type Y from an assertion of the occurrence of an event of type X. And so forth. Thereby may Thesis 3 be resurrected. Under this idea, an accident explanation would enumerate such laws, and assert the occurrence of the 'fundamental' events (logically, it suffices to find a subset of the set of all events sufficient to infer the occurrence of all events, including the accident event - there many be many such subsets), and show that the accident event logically follows.
Specifically, this yields the following strategy: enumerate all the events that are thought to be significant, X.1, X.2, ..... and so forth; elaborate the causal relations between them: All events of type X.1 are caused by occurrences of events of type X.2 along with events of type X.3; add these as general axioms to the 'explanation' , assert the occurrence of the earlier events, and derive logically the occurrence of the later events. This seems to be the sort of strategy envisaged by Johnson and Telford. Let's call it a 'General Causal Law' (GCL) approach. An objection to a GCL strategy would be that the addition of the 'causal laws' is gratuitous without some independent justification. Such a strategy could be simplified by eliminating the 'causal laws'. The simplified strategy would be: enumerate all the events that are thought to be significant, X.1, X.2, ..... and so forth; elaborate the causal relations between them: X.1 was caused by event X.2 along with event X.3; add these as axioms, then check for consistency (no contradictions; and that the causality relation actually satisfies the conditions of such a relation, see (3)) and completeness (that one has all the assertions of causality between the critical events, obtained through why?....because.... questions). Let's call this an Individual Causal Assertion (ICA) strategy.
An ICA strategy is pragmatic, and does not aim to be a complete D-N explanation. I would also argue that pragmatics is of the essence in accident explanations. The object of such explanations is to provide an understanding, relative to engineering considerations, of the accident, and to identify events whose occurrences could be alleviated in the future. These are pragmatic considerations. Providing a full D-N scientific theory which explains how the accident occurs is not purely pragmatic. Neither an engineer nor an accident investigator would take kindly to having to elaborate that because parts x and y were no longer connected (the bolt holding them together had sheared) that due to Newton's laws of motion plus forces acting on the parts derived from the fundamental equations of aerodynamics, the mutual acceleration of the parts relative to each other was positive and thus the distance between them over time increased. One wants to assert simply that the bolt sheared and the engine fell off, and take most of the physics as given. That is an ICA strategy. Some physics will likely be involved in figuring out how to modify the bolt to prevent a recurrence, but much will still be assumed. The GCL strategy lies somewhere in between an ICA strategy and a full D-N explanation. I see no method of refuting the criticism that the causal generalisations of a GCL strategy are gratuitous, except by grounding those generalisations in physical law, which means providing a D-N explanation or at least the possibility of one. This entails that I see no explanatorily-useful intermediate stage between a pragmatic ICA strategy and a full D-N model. I have argued for and applied an ICA strategy to actual accident reports in (11)(12).
Maybe a ICA strategy could use a GCL strategy, not as a justifiable explanatory model itself, but as a technical step on the way to a D-N model. The idea is a hierarchy of levels on the way to a full explanation (such an idea may have been implicitly suggested by Johnson and Telford). This may allow the investigator to terminate an inquiry at a level she deems appropriate, without having to descend to the baroque rigor of a full D-N model. Indeed, if one accepts the general validity of D-N models of explanation, one may expect such a hierarchy to lie behind any successful explanation of the accident. If we assert that the engine fell off because the retaining bolt sheared, then it is because we believe that generally engines fall off when their retaining bolts shear, and in turn this generalisation must be justified by an explanation based on the fundamental physics behind such a causal connection. Conversely, if we are wrong about the existence of such a potential explanation, then that is evidence that we are wrong about the causality.
The basic insight behind D-N explanations is the justifiable belief that formal-logical laws embody all and only valid reasoning. Valid reasoning reasons from premises to conclusion, and satisfies certain properties. We have seen that explaining accidents may involve statements of causality between events, in order to derive the conclusion that the accident was a causal consequence of certain events. Such statements of causality may appear in the premises; if they do so, they are assumptions of causality. They may be irreducible, or we may attempt to explain them away.
Causality is Not 'Leads To'
If statements of causality must appear irreducibly in the premises of a causal argument, then reasoning to the inevitability of the accident from its causes will involve reasoning using properties of the causal relation, and by hypothesis this reasoning is not purely logical, therefore must be axiomatised. Thesis 3 makes no allowance for such axioms. Thesis 4 attempts to explain away causal statements by reduced them to purely logical formulas, in which case valid inferences amongst causal statements would need no axioms, but be derivable purely from the logic inference rules, as Thesis 3 requires.
Thesis 4 claims that all that is relevant for explanation using the concept of causality can be embodied in the tense-logical 'leads-to' operator. This would reduce the concept of causal explanation to that of logical consequence. `B leads to A' is written B ~> A and is defined using [] and <> as [](B => <>A). It thus means that in all subsequent future states, whenever condition B holds then at the same or some later time condition A will also hold.
However, Thesis 4 seems simply to be mistaken, as argued in (1) and (3), and there is no other obvious candidate for reduction. There are simple logical puzzles which must somehow be explained away for any claim for Thesis 4 to be taken seriously. It might be suggested that 'leads to' includes part of the concept of causal dependence, but it has been argued coherently that the concept of causal dependence is related to the concept of counterfactual dependence (3), and there are some essential properties which counterfactual dependence does not share with 'leads to'. There are many puzzles to solve for those who claim that causal dependence can usefully be expressed by 'leads to'. Thesis 4 is unlikely to help resurrect Thesis 3, but maybe a weaker form may help?
Expressing Sufficient Causality in Simple Tense Logic
Even though it is strained to believe that assertions of causality are not equivalent to 'leads-to' assertions, it may be true that a causal relation between two events implies a 'leads to' relation between assertions of those events, without the converse being true. In this case, we could introduce axioms of the form (A is-caused-by B) => (B ~> A). It should be clear that this can be done only if B is a sufficient cause of A, because the 'leads-to' assertion says that A necessarily follows B sometime. Any given event A might have many necessary but individually insufficient causes. Let us assume sufficient logical power that we may conjoin them in tense logic to form one assertion of jointly-sufficient-and necessary-causes that may be written B. Call it an assertion of sufficient cause. We may indeed write an assertion of causality then as a binary relation A is-caused-by B, where B is an assertion of sufficient cause.
An assertion of sufficient causality between two events is an assertion of a binary causal dependence between binary relations on states (events are actions, and actions are binary relations on states, defined through their pre- and post-conditions). This is prima facie a second-order operation, since formulas defining actions are not themselves terms of the object language of simple temporal logic (as in TLA - for an explanation of the ontology of TLA, see (1). This is not to say that first-order tense logics may not be defined which have events as terms). Following the suggestion above, we have weakened an assertion of causality to one of temporal dependence: E ¹ ~> E ², where E ¹ and E ² are events, say expressed as TLA actions. However, such a formula is not a well-formed TLA formula. In TLA, an action formula may not involve the temporal operators of simple temporal logic. This helps to keep the inference rules simple. Such an action formula with temporal operators is a formula of 'Raw-TLA', RTLA. A complete set of inference rules for RTLA is not known. This suggests that the class of valid inferences between formulas of the form E ¹ ~> E ² may not be easy to determine.
This has consequences for the complexity of the formal theory in which we are proposing to formulate accident explanations. I propose we take the complexity warning seriously, and show how to reduce a statement of the form E ¹ ~> E ² to a statement of simple temporal logic, while attempting to preserve its overall meaning.
A short informal explanation should suffice to show how to perform the conversion. I define the postcondition of an action A in tense logic, say in TLA. The precondition of A in TLA has the definition Enabled(A), where Enabled(A) is that formula obtained from A by replacing each primed variable by a state variable not occurring in the formula, and existentially quantifying over that variable (5). (The order in which the variables are replaced and quantified does not matter, by a theorem of first-order logic). Similarly, define post-condition(A) to be that formula obtained from A by replacing each unprimed variable by a state variable not occurring in the formula, and existentially quantifying over that variable; and then replacing each primed variable by its unprimed correlate. Let B also be an action. Then we may formulate axioms of the form
| A is-caused-by B => |
| ((Enabled(B) /\ <>post-condition(B)) ~> (Enabled(A) /\ <>post-condition(A))). |
Not All Fundamental Causes Are Temporally Precedent
I turn now to Thesis 1. The `initial conditions' of a tense-logical specification of a class of behaviors are given by an assertion constraining the values of the state variables in the initial state of the behaviors. For example, suppose that the tense-logical specification describes the behaviors of a machine with variables x, y, z and the four possible actions X, Y, Z, N defined as:
| X: | x'=x+1 | /\ y'=y | /\ z'=z |
| Y: | x'=x | /\ y'=y+1 | /\ z'=z |
| Z: | x'=x | /\ y'=y | /\ z'=z+1 |
| N: | x'=x | /\ y'=y | /\ z'=z |
The first three actions describe incrementation by 1 of x, respectively, y and z, and the last is do nothing. One could partly describe the machine by saying that it always takes one of the above actions. Described from the temporal point of view of the initial conditions, this is expressed as
One would like to know what the machine can be relied upon to do, but there are no guarantees unless one knows what the values of the state variables are to start with - in other words, the initial condition. A reasonable initial condition would be x = y = z = 0. Then one would hope to prove the invariant [](x >= 0 /\ y >= 0 /\ z >= 0) from the specification. Without the initial condition, one could not even say whether actions X, Y or Z can happen: if x were not to start out as a number, it might make no sense to add 1 to it.
We have not yet ruled out that the machine never does anything: that every action is an N. A way of ensuring that the machine stirs from its slumber is by requiring some kind of liveness of the non-trivial actions X, Y, Z. We have no need to discuss liveness here, but we shall discuss one common liveness assertion, the Weak Fairness of an action, in the context of an accident event, below.
This small machine example helps to show why the initial condition is important (and why the temporal point of view is the initial state). Similarly, the analogy with an sequence of events describing an accident is that one may only prove that the accident inevitably follows the other events if at some point one can describe the state that the system is in (call this the initial state), and from which it follows, given the occurrence of the causally-relevant events, that the accident occurred. At some point in time, the initial state, the history of the accident must start, and this point, so goes the intuition, is best chosen as the point at which something `starts to go wrong'.
The analogy of accidents with machines only goes so far. I am sceptical of identifying any `initial conditions' of a temporal explanation with an `original cause'. For example, consider the following chain of events. Initially, and continually, there is bad rainy weather with poor visibility; a short grass runway with mountains at both ends; the aircraft requires maximum rate of descent to get in, and doesn't have a high-enough rate of climb to get out. The pilot tries anyway, and overshoots the runway. The cause: gross misjudgement, aggravated by personality features of the pilot. (U.S. light-plane pilots may recognise this sort of example.)
It does not suffice to consider the pilot's misjudgement only a temporally-initial condition. Although misjudgement may have been initially present, reversion to a correct assessment of the situation in time (a `go/no-go' decision at an advanced point in the procedure) would have avoided the incident and therefore earlier judgements cannot be considered to be causally determinate. It is generally regarded as appropriate to `look-and-see' provided one makes a 'go/no-go' decision at a suitable time. A continual failure to perceive a bad situation could be considered a continued state of misjudgement. The causally-relevant factor is this continued state, not the misjudgement in one state such as the initial state. Similarly, if one were to describe continued-misjudgement as an action for example, crudely, via a 'state-of-the-brain' variable x:
then it is the continual execution of this action which is causally relevant. Let us call such a continued state or continued action a continual event. No matter whether rendered as state-predicate or action, as argued in (1) the fact of this continual event's causal relevance to an accident is most easily expressed using the 'until' operator U, which is not part of TLA:
Rather than regard the continual misjudgement as the causal factor, some pilots might prefer to regard the fact that 'an appropriate go/no-go decision was not made at an appropriate decision point', or 'a go decision was made at the decision point at which a no-go decision was the appropriate choice' as causally determining. These describe, respectively, the absence of a desired event, and the occurrence of an undesired event. Let us call this a missed-event and a mistaken event respectively. Neither of these happens at a time prior to an initial state from which the accident would be described in an accident report.
So either a continual event (expressed most easily using until, which does not occur in TLA or other simple tense logics), or a missed event or mistaken event at a later decision point is the determining causal factor in this explanation. (Since I have given no grounds to distinguish 'determining' causal factors from other causal factors, let us just consider these simply causal factors.) Any of these views are not consistent with Thesis 1, which therefore does not appear to be consistent with actual practice.
We could attempt to resurrect the thesis by fiat, in the following way. It asserts that the causal conditions that really matter are those that lie at the start of a causal chain; and that causal chains begin at the `initial state'. Therefore the `initial conditions' occur at the first occurrence of a determining factor. Since the landing was abortable up to the go/no-go point t.1, and a competent pilot behaving appropriately could have flown the same profile up to t.1, but then made the decision to go around, one could take t.1 to constitute the time of `initial conditions', and the causal chain leading to the accident proceeds from t.1 onwards.
This is plausible with the current example, but with a slight modification to the example, it is no longer so. Say that as our pilot began the approach, he had chosen a go/no-go point appropriately (say, t.1) but the weather worsened in such a way (at, say, t.0) that would force a change in the go/no-go point to an earlier time (to, say, t.2 < t.1), but that the pilot did not modify his behavior to decide at t.2 rather than at t.1. The initial conditions must somehow include t.0, since at this time the causal sequence was affected: before, a decision at t.1 would have been appropriate, and after, a decision at t.1 is too late, but a decision at t.2 is appropriate: and the pilot makes his decision at t.1. The events at t.0 changed a behavior in which there would have been a success event at t.1 and no missed event at t.2 into a behavior in which there is a missed event at t.2 and a mistaken event at t.1. Therefore the event at t.0 is causally relevant, and the 'initial conditions' of the accident occur at a time at or before t.0. However, the missed event at t.2 > t.0 is now causally important, but it does not appear that previous events have caused this non-decision. The pilot, of his own free-will and (mis-)judgement, made no decision.
So the missed event at t.2 is a causal factor: had it happened differently (a go-around decision had been taken), the accident would not have happened. It is preceded by no other (important) factors on which it is causally dependent: the (lack of) decision proceeded under free will. And it is not initial. So much the worse, once again, for Thesis 1.
But, one could argue, this lack of decision does have preceding factors on which it is causally dependent. Strictly speaking, the pilot's lack of decision is causally dependent on, for example, his being born. I would respond that this is not an significant causal factor from the point of view of accident reports; and there are no significant causal factors of this sort preceding it. The rescue of the thesis thus hangs on what one considers significant. One could take as significant simply those factors which have historically been considered significant in actual accident reports. But it could be retorted that the `folk-theory' in actual accident reports is what we're trying to improve upon: one cannot take it as norm at the same time as improving on it.
For example, Thesis 1 is logically rescuable by adhering to strict determinism. A strict determinist believes that the state of the world at any time enables complete prediction of its state at any future time. To a strict determinist, the pilot's lack of decision at t.2 is a causal consequence of the state of the world at all preceding times: there is no free will. However, a strict determinist also cannot explain accidents the way in which we try to do so. To a strict determinist, the accident was preordained by the state of the world 100 years ago, or at any other time, and therefore in particular at the time of the `initial conditions'. Therefore under strict determinism it no longer makes sense to try to explain an accident the way which we are trying to explain it. To adhere to strict determinism requires huge distortions of discourse, but it does appear to be a logically coherent position. What one considers a significant cause does depend on one's metaphysical theory of causality.
We have considered two examples: one in which it was logically plausible, although contrary to current practice, to maintain Thesis 1, and a slight modification with which it would be hard to maintain Thesis 1 without considerable alteration in what one considered to be causally significant factors in the accident. Any thesis which responds to an intuitively small change in situation with a large change in the set of factors considered causally important loses its pragmatic value. Since pragmatic value is our main concern, we may reject Thesis 1 for this reason.
There is a deeper point to the example I just considered. The `causal chain' in accident analyses often involves people, yet people's decisions and intentions do not `cause' their actions in any well-understood sense of `cause' (it's perfectly possible to decide to do something, and then for no clear reason, just not carry it through; it's also possible to decide and intend and try to do something, and then fail, say, by lack of skill). It's not always clear how human processes merge with and into a `causal chain', and thus it is not clear what `root causes' might be, when human decision and action is involved.
Consider another situation. Suppose an accident contains a causal chain in which humans acted according to procedure, but had they done something completely and startlingly different, the accident would not have happened. For example, suppose the operators at the Three Mile Island nuclear plant had gone on strike and didn't turn up for work the week before the accident, so the operator had no recourse but to shut down the plant. The accident would not have happened. Thus, the accident is counterfactually dependent on the fact that the operators turned up for work and kept the plant running. On many accounts of causality, this could make it feature in the causal chain. But it's not in any accident report on TMI, and neither would we intuitively expect it to be. So it's not a 'root cause' in the sense in which we understand this term in accident reports, and it's not even a contributory factor (although other actions of the operators are). But nevertheless it fulfils some formal criteria -- the accident is couterfactually dependent on it. (It also `leads to' the accident in the temporal sense.) So why isn't it a cause? Such puzzles with human agency and counterfactuals render somewhat murky the whole business of identifying logically some causes to be `root' causes.
Finally, to drive these points home, I consider an example of an explanation which involves tightly-coupled design with operator actions and maintenance procedures. NTSB report NTSB-AAR-79-17 (13) concerned the 1979 Chicago DC-10 crash, and the McDonnell Douglas Corporation produced a report (14) arguing their position on the accident. The accident report was analysed in (12). A DC-10 lost an engine on take-off from Chicago O'Hare airport - and I do mean `lost an engine' - it fell off, unfortunately taking some hydraulics with it and causing certain high-lift devices on that wing to stow themselves. The wing stalled, and the airplane flipped over and flew into the ground. The entire incident was captured on video by an unfortunate onlooker whose relatives were on the plane. There ensued many public discussions about the safety of the DC-10.
The terminology of the report is curt but expressive. It asserts that the events happened at a `critical point' during takeoff. The point is 'critical' because the pilots were more preoccupied than they would have been in, say, cruise, and therefore their ability to diagnose the failure was impaired. McD says, and the NTSB agrees, that the airplane was in principle controllable. However, because the crew were occupied with the takeoff, one of the most intense phases of flight for the crew, they may have had less opportunity to devote immediate and undivided attention to diagnosing the failure, because they had to ensure all other factors remained under control as well. They continued flying the airplane 'by the book speeds' because they didn't know that the left wing slat had retracted (the failure also took out certain warning signals in the cockpit). Had they known the slat was retracted, they would have realised that the stall speed of the left wing was now higher than the 'book speed' that they were flying at, and (so we suppose) would have lowered the nose and flown faster, keeping the aircraft under complete control. They didn't know, neither does anyone suppose they would really have had time to find out, given the configuration of the aircraft and events at that time.
The crews' implicit choice to keep flying by the book speeds is, first, a continual decision, not an action. Therefore it is a continual event. Second, the accident is causally and counterfactually dependent on it, as discussed in the report (but not using these terms). Third, the start of this continual event happened after the main trigger event (the engine falling off), which was itself caused by improper maintenance procedures quite a time previously (improper handling of the engine when being refitted to the aircraft). Fourth, causal precedents to this continual event would be the pilots' training. None of the events intuitively 'comprising the accident' as discussed in the report are causally precedent to this continual event. This event is thus causally original, as far as the accident report is concerned, but temporally succeeds other necessary causes of the accident such as the event of the engine falling off.
I conclude that the argument for Thesis 1 is pragmatically weak to the point of counterintuitive. Although as far as I can tell the thesis could be logically rescued, any such rescue would render the form of the formal explanation unduly sensitive to intuitively minor changes in the situation surrounding the accident. Specifically, many preceding events which are not 'important' become causally relevant under minor changes in circumstances. Such unintuitive consequences of holding to Thesis 1 argue strongly against trying to rescue it.
Completeness
I come to my argument against Thesis 5. First, we must see why some thesis such as Thesis 5 is important. Such a thesis provides a goal for formal explanations of an accident. Formal explanations involve reasoning from assertions to other assertions, and the goal tells us what we are reasoning towards. We aim (in the general D-N framework within which we are working) formally to deduce the goal assertion from other assertions which we have found to be true in the course of the accident investigation. Attaining the goal as the conclusion of a chain of formal reasoning is one of the five criteria of Parsons (16, p171) for a piece of reasoning to be successful.The intuitive argument for identifying weak fairness as the sentence, the proof of which explains the accident, is as follows. Suppose we denote the undesired happening, the accident event, by Accident-action. Asserting weak fairness of this action, WF(Accident-action), is by definition to assert that either at some time in the future the accident action becomes forever impossible, or at some time in the future the accident action must happen. Since in the flow of things the action did not become forever impossible - after all, it really occurred! - formally proving weak fairness of the accident action will entail that the action became inevitable, given the hypotheses of the proof, and therefore these hypotheses explain the accident, since that is what 'explaining' is.
Thesis 5 was proposed by Johnson and Telford under the assumption of Theses 1-4 for which they had already argued. Under this view, to generate an explanation, we set up the initial conditions; construct the causal chains by positing basic causality in `leads to' statements and proving others; finally, we prove WF(Accident-action) from all these statements. Our initial attempts may fail, but we modify the assertions put in the initial condition, and add or alter `leads to' assertions, until we succeed. We shall then, according to this thesis, have a formal explanation of the accident: how it started, and how it progressed until disaster occurred. Note that none of these theses explain how we identify the crucial events and conditions that led to the acccident. So the proposal is reconstructive - we have first somehow to identify the causally relevant events. But from manipulating the formal statements, in particular from attempting and failing to construct a proof, we should learn whether or not our `ingredients list' suffices, whether we have identified all the factors. I call this property completeness of an explanation. Thesis 5 tells us when an explanation is complete. Thus does the formality act as a check whether we have done the background work properly.
So Thesis 5 is a criterion for completeness of an explanation. We have already seen that an account of the system properties of tight-coupling and interactive complexity is lacking in tense logic. If these properties of a system become essential to explain why an accident occurs, then we shall not be able to reason to the goal without including them, therefore a formalisation of this reasoning in tense logic will not yield the goal. Thus will our reasoning appear to be incomplete, whereas in reality it may not be - we are just excluding some necessary factors which we cannot express within the formalism. This shows that using tense logic to construct accident reasoning under a D-N model errs on the side of conservatism - it may sometimes fail to attain a goal that reasoning about tight-coupling and interactive complexity will succeed in attaining.
A useful formalisation of the accident reasoning would enable us, for example,
- to conclude that a certain set of causes is sufficient to cause the accident (completeness), and in the case of overdetermination, to determine which causes were sufficient by themselves to have caused it (sufficient completeness);
- that a certain sequence of actions, if followed, would have avoided a necessary cause of the accident (and thus that the `operating procedures' that this sequence represents were violated);
- that certain sets of causes are necessary.
Proving Weak Fairness Does Not Explain Accidents
I shall show that an assertion of weak fairness of an accident action doesn't seem to add much other than asserting that an accident is inevitable, which can be expressed much more simply in temporal logic.Weak Fairness of the accident action is a statement of the form
I shall show that
where Init is a conjunction of 'initial conditions', including some domain axioms. The reasoning depends essentially on the form of the assertion Accident-happens. The equivalence is most definitely not true in general.
Johnson and Telford claim a statement of weak fairness of the accident event "precisely characterises the aim of accident reports". If so, then it follows that so does a simple assertion that the accident happened, since the two are equivalent under the initial conditions. The statement that the accident eventually happened, given the initial conditions, hardly seems to be useful information, let alone a goal of accident reports.
Let us suppose that they misspoke, and meant to say that obtaining a logical proof of weak fairness of the accident events, from the causally-relevant facts, is the goal of accident reports. Then, rather than proving weak fairness, a somewhat tense-logically complicated formula, one could choose more simply to prove that the accident happened sometime, given the same causally-relevant facts. I conclude that Weak Fairness is certainly a weak, and definitely not a fair, goal of accident reports.
I take the definition of `accident' used in the US Federal Aviation Regulations, formalise it in TLA, and provide an argument that an assertion of Weak Fairness concerning accident behavior is logically equivalent to asserting simply that an accident happened sometime. In formulae,
Furthermore, I show that Init must include `domain axioms' in order to identify the right set of behaviors for analysis.
The US Federal Aviation Regulations define an accident as `an occurrence ... in which any person suffers death or serious injury, or in which the aircraft receives substantial damage'. In state-machine terms, one might formalise this in the following way. Let S be some set of persons and A be an aircraft. We can imagine that the set S of people includes passengers and people on the ground in the likely trajectory of (bits of) airplane A if it were to crash. As the aircraft is flying around in different places, the set S of people who are passengers or exposed to A's potential crashing pieces will change. Thus S is a variable parameter (in TLA terminology). More interestingly, it makes sense to regard airplane A as a variable parameter also. Here's why.
Airplane A has properties. Suppose `A is flying over London' is true now. Shortly afterwards, this sentence is false and `A is on the ground at Heathrow airport' becomes true. Now, a constant parameter in TLA satisfies the same state predicates from beginning to end of a behavior (infinite sequence of states). The reason is that a unary predicate whose satidfying instances form a set may be identified in set theory with this set of all the things which satisfy it (i.e., set theory is extensional). Showing that two satisfying sets are different thus suffices to show the related predicates are different. If A satisfies predicate P in one state in a behavior, but not in some other, then either P (considered as a set) must be a variable parameter of the behavior, or A must be. We can consider A a constant parameter, in which case most of the relations in which A partakes, including properties of A, must be variable parameters; alternatively, if we consider A to be a variable parameter, then maybe we can take the predicates for the most part to be constant parameters, and that's combinatorially more viable, since there are fewer variable parameters and therefore potentially fewer whose changes need to be regulated through TLA action definitions. Furthermore, Quine has argued that there is logically little to choose between language which talks of rabbits, and language which talks of successions of rabbit-time-and-space-slices (19). So it seems that we are moderately free to make the choice, and it's combinatorially more reasonable to consider A a variable parameter (aka `flexible variable'). So we'll take A to be a flexible variable.
We may think of variable A as an airplane-state-sequence (a sequence of `airplane-slices'), with varying values satisfying constant predicates (mostly). The predicate we care about most is that of being substantially damaged, which is a state predicate, therefore holds of airplane-slices. Similarly, we may also think of persons as person-state-sequences. The predicates we care about on persons are are those of being dead or being seriously injured. Similarly, they're both state predicates of persons, that is they hold of person-slices. So I only need an ontology of person-slices and set S, rather than one of person-slices, persons, and set S.
Let's call a potential value of A in any state an A-slice. Since airplane A is to be represented by a variable parameter, we have to put something in the state to ensure that all A-slices are somehow connected with the airplane A and not with some other airplane or object. One way is as follows (a Quinean `unique name'). Let's say airplane A has tail number G-AAAAA. We introduce the state predicate has-tail-number-`G-AAAAA' with the intended interpretation that any value which satisfies this predicate must be an A-slice. Thus all A-slices satisfy this predicate, and everything which satisfies this predicate must be an A-slice. It's thus one of the `invariants' of any state-machine which purports to describe any behavior involving A that
is true in the initial state.
Another problem mentioned earlier, that of how to deal with behaviors which do not continue to infinity, has a simple solution here. We need to add the following as axioms
| (A substantially-damaged) | => | [](A substantially-damaged) |
| (x dead-by-A) | => | [](x dead-by-A) |
| (x seriously-injured-by-A) | => | [](x seriously-injured-by-A) |
which together imply that when a state occurs which is the result of an accident, that state persists to infinity. But notice a technical difference between the formulae: A is a flexible variable, and x is a person-slice. Person-slices are values, and their properties are mathematical, thus independent of time, thus persist from one state to the next. So if formula F involves no flexible variables, and F is true in some state, then F is true in any state. In particular, this means that F => []F is true for any formula involving no flexible variables. However, what's true of flexible variable A in one state may not be true in the next, if A has a different value. To add these three formulae above as axioms, I need to assert that they're true in every state. For sentences involving flexible variables, this requires prepending [], and for statements involving rigid variables (person-slices), they're simply true or not true, independent of state. This means that I add as axiom only
Notice that if I had persons in my ontology, rather than just person-slices, I would have to add similar axioms for persons with dead-by-A, and for persons with seriously-injured-by-A.
I also add as axioms the following `type constraints' on the predicates:
| []((A substantially-damaged) | => | (A has-tail-number-`G-AAAAA')) |
| (x dead-by-A) | => | (x is-a-person-slice) |
| (x seriously-injured-by-A) | => | (x is-a-person-slice) |
Again, the first must be prepended by [] because A is flexible.
I also want to ensure the type constraints for A and S: that all values of A are A-slices and all values of elements of S are person-slices, and also that S consists of only person-slices that are `under influence' of A (whatever that means - this axiom should maybe be an equivalence, but I posit only an implication). They are:
| [] (A has-tail-number-`G-AAAAA') |
| [] (\forall x \in S : x is-a-person-slice) |
| [] (\forall x \in S : x is-under-influence-of A) |
Assuming these axioms, and using Lamport's `bulleted list' notation for /\ and \/, and the TLA ' operator, I can define an `accident to A' as:
| Accident-to-A == | /\ | \forall x \in S : ( ¬(x dead-by-A) /\ ¬(x seriously-injured-by-A)) |
| /\ | ¬(A substantially-damaged) | |
| /\ | \/ \exists x \in S' : ( (x dead-by-A)' \/ (x seriously-injured-by-A)' ) | |
| \/ (A substantially-damaged)' |
Notice that the post-condition of Accident-to-A is just the negation of the pre-condition. The definition of Enabled<Accident-to-A>_{S,A} just follows now by the usual TLA definition of Enabled:
Enabled<Accident-to-A>_{S,A} ==
| /\ | \forall x \in S : ((¬ (x dead-by-A) /\ ¬ (x seriously-injured-by-A)) |
| /\ | ¬ (A substantially-damaged) |
| /\ | \/ \exists T : \exists x \in T : ((x dead-by-A) \/ (x seriously-injured-by-A)) |
| \/ \exists B: (B substantially-damaged) |
Observe that T doesn't really matter in the third clause: if some person-slice x is dead-by-A or seriously-injured-by-A, T = { x }. But these values exist in the TLA universe for ever -- all values are sets and all individual sets are all there in all states. There is no notion of values being created and disappearing. So the \exists is to be interpreted as `potential value', not as `actual value'. If there are no such A-slices which are substantially-damaged, it means that A can never take such an A-slice as value and therefore that it is impossible for the airplane ever to become substantially-damaged: all sequences of A-slices contain only A-slices which are not substantially-damaged. Similarly with dead-by-A or seriously-injured-by-A person-slices. So, assuming that it's always possible somehow for airplane A to become damaged (its pilots can always fly it intentionally into the ground) and it's always possible somehow for a passenger on A to die or become seriously injured (for example, when the pilots fly the plane intentionally into the ground), the clause
| \/ \exists T : \exists x \in T : ((x dead-by-A) \/ (x seriously-injured-by-A)) |
| \/ \exists B: (B substantially-damaged) |
is true in any initial state which could represent any situation we care about. So let's add this to the axioms -- but replacing the redundant `\exists T : \exists x \in T :' by simply `\exists x :'. The formal parameter x will still be bounded in the TLA sense, since the two asserted predicates both imply (x is-a-person). So I add the axiom:
| \/ \exists x : ( (x dead-by-A) \/ (x seriously-injured-by-A)) |
| \/ \exists B: (B substantially-damaged) |
Since this is an axiom, and it contains no flexible variables, it is simply true in every state in every behavior. But again, since I'm introducing the predicates dead-by-A, etc, without saying exactly which property interprets them, it's semantically more flexible, and may serve our eventual purposes better, to assert it prepended by []. Note that it follows from this that
Enabled<Accident-to-A>_{S,A} <=>
| /\ \forall x \in S : (¬ (x dead-by-A) /\ ¬ (x seriously-injured-by-A) ) |
| /\ ¬ (A substantially-damaged) |
Let's call any person-slice satisfying ((x dead-by-A) \/ (x seriously-injured-by-A)) or A-slice satisfying (B substantially-damaged) an accident-value. A behavior may contain an accident-value in some state, or may not. But any behavior which does, and whose initial state contains no such values, represents an accident sequence. So let's add as axiom that the airplane starts in a no-accident-has-happened state:
| /\ \forall x \in S : ( ¬ (x dead-by-A) /\ ¬ (x seriously-injured-by-A) ) |
| /\ ¬ (A substantially-damaged) |
Note that this axiom, unlike the others, is only intended to be true in the initial state (the others are intended to be true in all states, i.e. invariants). It will become false after an Accident-to-A action.
We have now ensured in a manner consistent with TLA semantics that any behavior interpreting this specification will start out with A in an accident-free state and will either continue that way, or there will occur an accident with A. The part of this mathematical structure of interest to accident reports is the initial segment from initial state to the post-state of Accident-to-A. The initial condition is
Init ==
| /\ | [](A substantially-damaged) => [](A substantially-damaged) |
| /\ | [](A substantially-damaged) => (A has-tail-number-`G-AAAAA'), |
| /\ | \forall x : (x dead-by-A) => (x is-a-person-slice) |
| /\ | \forall x : (x seriously-injured-by-A) => (x is-a-person-slice) |
| /\ | [] (A has-tail-number-`G-AAAAA') |
| /\ | [] (\forall x \in S : x is-a-person-slice) |
| /\ | [] (\forall x \in S : x is-under-influence-of A) |
| /\ | \/ \exists x : ((x dead-by-A) \/ (x seriously-injured-by-A)) |
| \/ \exists B: (B substantially-damaged) | |
| /\ | (more-axioms) |
more-axioms is the catch-all phrase for axiomatising other aspects of the environment. It will presumably include things such as what is considered to be a normal structural description and normal behavior of an airplane, and maybe also `normal' pilot behavior.
Observe that Init includes, and must include, substantial information (more than what Johnson and Telford seem to claim as Opconds). The first four clauses are domain information (written as invariants, as justified above). Had we `persons' and not just `person-slices', we would have to add the persistence information about dead-by-A and seriously-injured-by-A, just as we did for substantially-damaged. The fifth and sixth are `type clauses', here written as []-statements to ensure they remain true in all states of a behavior. The seventh is the initial-state condition, which is simply that the initial state should be accident-free.
Consider any behavior starting in this initial state. Observe that if S and A never ever change, there's not been an accident to A, since there's not been one in the initial state (as entailed by Init) and for there to be an accident, the state of either S or A must change (in the way determined by Accident-to-A). If nothing ever happens, there's been no accident.
Observe now that the following is a TLA theorem:
I'd also like to be able to say that the occurrence of an accident disables the future occurrence of all accidents, because the postcondition of Accident-to-A is simply the negation of the precondition (== Enabled<Accident-to-A>_{S,A}) and this postcondition, if ever true, persists (by the domain axioms):
But this is simply not provable, because it is logically equivalent (by propositional logic) to
whose antecedent contains no primed flexible variables and whose consequent contains only primed flexible variables and so cannot be a TLA theorem unless the consequent itself alone is a TLA theorem, which it is not. However, the following should be valid:
because if Accident-to-A occurs once, it follows from Init that it is permanently disabled and thus cannot occur again. It now follows that
| Init => | |
| ( []<><Accident-to-A>_{S,A} \/ []<>¬Enabled<Accident-to-A>_{S,A} | |
| <=> []<> ¬ Enabled<Accident-to-A>_{S,A} ) |
since it follows from Init that the first disjunct is false. Also
A semantic argument for this follows from the following observations: Accident-to-A starts out Enabled, and the Enabled condition is precisely accident-freeness at the current state; any state in which ¬ Enabled<Accident-to-A>_{S,A} is true is a state in which an accident has at some time in the past occurred (which may be seen by passing the negation through to the atomic formulae), and Init is an accident-free state; further, when an Accident-to-A postcondition occurs, it remains true for ever.
Let WF_{S,a}(Accident-to-A) be the formula
as in the usual TLA notation. It follows from the two formulas above that
Thus showing that, under the domain axioms, Weak Fairness is equivalent to asserting simply that the accident eventually happens, as I needed to show.
This process of translation into TLA of a widely-used definition of accident has shown that:
- under the domain conditions, assertion of weak fairness is simply equivalent to saying that an accident actually occurs in the behavior;
- that the Init condition must include `domain axioms', which are invariant over the behavior, and various other components.
Even the formulation of the concept of accident encapsulated in the Accident-to-A action could not be appropriate for all situations. For some accidents, a pre-/post-condition formulation of the FAR definition would not allow us to focus on everything pertinent to an analysis. For example, in the Warsaw A320 accident, the aircraft was substantially damaged, and one pilot died from a trauma injury caused by impact. However, following the impact with the earth bank, the aircraft leaked fuel and began to burn, and a second passenger died from asphyxiation when he was unable to evacuate and not noticed by the cabin crew presumably because his body was obscured by smoke. In such cases, an accident is more to be thought of as a process which itself has a causal analysis (damage caused fuel leakage which with hot engine parts caused fire which caused smoke which obscured the cabin which was a factor in unconscious passenger not being noticed by others, etc). A similar situation occurred in the Manchester B737 fire-on-takeoff accident. The triggering event, an engine fire, counts as substantial damage and therefore an accident by itself according to the FAR definition, but passengers died as the pilot turned off the runway and brought the aircraft to a stop with the prevailing wind blowing smoke and flames towards the fuselage, which filled with smoke and soon caught fire.
Conclusions
I have considered five theses regarding the construction of formal explanations of accidents. I conclude that
- ad 1: root causes of accidents can succeed other necessary causes; they do not all occur in the `initial conditions' for an accident when temporally understood;
- ad 2: (as justified elsewhere) taking the temporal point of view to be temporally precedent to all the causally relevant events is not as reasonable as other choices;
- ad 3: although a D-N model is a worthy goal, there is doubt whether this can be achieved within the framework of tense logic without causal axioms; the inference rules of TLA are unlikely to suffice, and if the temporal point of view is not the `initial' state, they certainly do not;
- ad 4: (as justified elsewhere) 'leads to' is not equivalent to a statement of causal dependence, although it might be implied by such a statement;
- ad 5: if the goal of an accident report could be taken to be weak fairness of the accident action, then it might as well be taken to be the simpler formula expressing merely that the accident happens sometime.
References
References link back to the first mention.
Back to top
(1): Peter Ladkin,
Explaining Failure With Tense Logic.
Back
(2): Jonathan Moffett, Jon Hall, Andrew Coombes and
John McDermid, A Model for a Causal Logic for Requirements Engineering,
Journal of Requirements Engineering 1(1):27-46, March 1996.
Also in
ftp://ftp.cs.york.ac.uk/hise_reports/req_capture/causal.ps.Z.
Back
(3): Peter Ladkin,
Reasons and Causes.
Back
(4):C. W. Johnson and A. J. Telford,
Extending
the Application of Formal Methods to Analyse Human Error and
System Failure During Accident Investigations.
Back
(5): Leslie Lamport, The Temporal Logic of Actions,
ACM Transactions on Programming Languages and Systems 16(3):872-923,
May 1994. Also in (6).
Back
(6): Leslie Lamport,
The TLA Home Page.
Back
(7): Charles Perrow, Normal Accidents. Living With
High-Risk Technologies, Basic Books, 1984. Back
(8): Dietrich Dörner,
Die Logik des Misslingens: Strategisches Denken in
komplexen Situationen, Rowohlt Verlag 1989, Rohwohlt Taschenbuch Verlag
1992, translated in English as The Logic of Failure,
Metropolitan Books (Henry Holt), New York, 1996.
Back
(9): Carl G. Hempel, Explanation in Science and in History, in R. G. Colodny, ed., Frontiers of Science and Philosophy, Allen and Unwin/University of Pittsburgh Press, 1962, pp 7-33. Also in (10). Back
(10): David-Hillel Rubin, ed., Explanation, Oxford Readings in Philosophy series, Oxford University Press, 1993.
(11): Peter Ladkin,
The X-31 and A320 Warsaw Crashes: Whodunnit?.
Back
(12): Peter Ladkin,
Formalism Helps in Describing Accidents.
Back
(13): National Transportation Safety Board,
Aircraft Accident Report, American Airlines, Inc.
DC-10-10, N110AA, Chicago-O'Hare International Airport, Chicago, Illinois,
May 25, 1979., Report NTSB-AAR-79-17, NTSB, Washington, DC, 1979.
Also in (15).
Back
(14): McDonnell Douglas Corporation The DC-10: A Special
Report, McDonnell Douglas Corp., 1979.
Also in (15).
Back
(15): John H. Fielder and Douglas Birch, eds.,
The DC-10 Case, State University of New York Press, 1992.
(16): Terence Parsons, What is an Argument?, Journal of Philosophy XCIII(4):164-185, 1996. Back
(17): C. W. Johnson,
The Application of Petri Nets to
Represent and Reason About Human Factors Problems During Accident Analysis
,
in P. Palanque and R. Bastide, eds., The Design, Specification and
Verification of Interactive Systems, Springer-Verlag, 1995.
Back
(18): C. W. Johnson, J. C. McCarthy and P. C. Wright,
Using Petri Nets to Support Natural Language in Accident Reports,
Ergonomics 38(6):1264-1283, 1995. Back
(19): W. V. O. Quine, Word and Object, M.I.T. Press, 1960. Back