Reasoning About Safety-Critical Information Flow Between Pilot and Computer

TL;DR

This paper introduces Dynamic Agent Safety Logic (DASL), a new formal framework based on DEL, to analyze safety-critical information flow between pilots and computers, with applications to real incidents and mechanization in Coq.

Contribution

The paper develops DASL, extending DEL to model safe actions, belief, and knowledge relationships, enabling analysis of information gaps in safety-critical scenarios.

Findings

DASL can identify missing safety-critical information in pilot actions.

Application to Air France 447 demonstrates practical utility.

Mechanization in Coq validates the logic's formal properties.

Abstract

This paper presents research results that develop a dynamic logic for reasoning about safety-critical information flow among humans and computers. The logic advances previous efforts to develop logics of agent knowledge, which make assumptions that are too strong for realistic human agents. We introduce Dynamic Agent Safety Logic (DASL), based on Dynamic Epistemic Logic (DEL), with extensions to account for safe actions, belief, and the logical relationships among knowledge, belief, and safe action. With this logic we can infer which safety-critical information a pilot is missing when executing an unsafe action. We apply the logic to the Air France 447 incident as a case study and provide a mechanization of the case study in the Coq proof assistant.

Equations

$$\phi ::=p|\neg \phi |\phi \wedge \phi |{\mathbf{K}}_{\mathbf{i}}\phi |{\mathbf{B}}_{\mathbf{i}}\phi |[\mathbf{i},(\mathbf{A},\mathbf{a})]\phi |[\mathbf{i},(\mathbf{A},\mathbf{a}),\mathbf{S}]\phi ,$$

$$post(A,p)=p\text{mbox}ifupdate(M,A,w,a,i)\models p,\text{mbox}else\neg p.$$

$$M,w\models p$$

$$M,w\models \neg \phi$$

$$M,w\models \phi \wedge \psi$$

$$M,w\models {\mathbf{K}}_{\mathbf{i}}\phi$$

$$M,w\models {\mathbf{B}}_{\mathbf{i}}\phi$$

$$M,w\models [\mathbf{i},(\mathbf{A},\mathbf{a})]\phi$$

$$\text{ implies }{M}^{\prime },w^{\prime }\models \phi$$

$$M,w\models [\mathbf{i},(\mathbf{A},\mathbf{a}),\mathbf{S}]\phi$$

$$\text{ implies }{M}^{\prime },w^{\prime }\models \phi$$

$$(M,w)[[i,(A,a)]](M^{\prime },w^{\prime })$$

$$\text{ and }update(M,A,w,a,i)=(M^{\prime },w^{\prime })$$

$$(M,w)[[i,(A,a),S]](M^{\prime },w^{\prime })$$

$$\text{ and }update(M,A,w,a,i)=(M^{\prime },w^{\prime })$$

$${\mathbf{B}}_{\mathbf{i}}\phi \Rightarrow \neg {\mathbf{K}}_{\mathbf{i}}\neg \phi .$$

$${\mathbf{B}}_{\mathbf{i}}\phi \Rightarrow ⟨{\mathbf{B}}_i⟩\phi ,$$

$${\mathbf{B}}_{\mathbf{i}}\phi \Rightarrow \neg {\mathbf{B}}_{\mathbf{i}}\neg \phi .$$

$${\mathbf{B}}_{\mathbf{i}}\phi \Rightarrow \neg {\mathbf{K}}_{\mathbf{i}}\neg \phi .$$

$$\neg pr{e}_s(a)\Rightarrow {\mathbf{K}}_{\mathbf{i}}\neg {\mathbf{K}}_{\mathbf{i}}pr{e}_s(a)$$

$$\neg pr{e}_s(a)\Rightarrow {\mathbf{K}}_{\mathbf{i}}\neg pr{e}_s(a)$$

$$⟨\mathbf{i},\mathbf{a}⟩true\wedge \neg pr{e}_s(a)\Rightarrow \neg {\mathbf{K}}_{\mathbf{i}}\neg {\mathbf{K}}_{\mathbf{i}}pr{e}_s(a)$$

$$⟨\mathbf{i},\mathbf{a}⟩true\wedge \neg pr{e}_s(a)\Rightarrow \neg {\mathbf{K}}_{\mathbf{i}}\neg pr{e}_s(a)$$

$${\mathbf{K}}_{\mathbf{i}}\neg pr{e}_s(a)\Rightarrow \neg ⟨\mathbf{i},\mathbf{a}⟩true\vee pr{e}_s(a)$$

$${\mathbf{K}}_{\mathbf{i}}\neg pr{e}_s(a)\Rightarrow \neg ⟨\mathbf{i},\mathbf{a}⟩true.$$

Full text

1 Introduction

A common theme for aviation mishaps attributed to human error is for a pilot to become overwhelmed by data, lose situational awareness, and provide unsafe inputs to the flight controls. As yet, little work has been done to leverage the power of formal methods to address this problem. This paper remedies that by defining a dynamic logic of belief, knowledge, and safe action. We use the logic to create an axiomatic model of agency suitable for reasoning about safety-critical information flow among pilots and the flight computer. We mechanize this model in the Coq Proof Assistant and apply it to the Air France 447 incident as a case study.111This is a pre-print of an article published in 9th International Symposium, NASA Formal Methods 17. The final authenticated version is available online at: https://doi.org/10.1007/978-3-319-57288-8_25.222Code: https://github.com/sethahrenbach/DASL/blob/master/DASL.v

The research contributions of this paper include the development of a dynamic logic that is suitable for reasoning about safety-critical information flow. The dynamic logic is extended beyond most dynamic logics’ treatment of action in that it treats both mere action and safe action, and captures the relationship between the two. The subsequent application and mechanization in Coq explore novel uses of formal methods in aviation safety, beyond mere verification of system component correctness. They introduce the idea of formally analyzing the human component of the safety-critical systems.

Dynamic Logic is a type of modal logic used for reasoning about state transition diagrams of programs [8, 3]. A diagram consists of nodes and edges, representing states of the system and labeled transitions between them, respectively. It is distinguished from other logics by the fact that truth is dynamic, rather than static, in its semantics. Thus, it is capable of representing the way actions change the truth of propositions. It serves as a foundation for a variety of logics similarly concerned with changes in some aspect of the truth as a result of actions. This family of logics has been described as logical dynamics, and includes Public Announcement Logic (PAL) and Dynamic Epistemic Logic (DEL) [5].

Logical dynamics allows researchers to model information flow, rationality, and action in multi-agent systems [5]. In Ahrenbach and Goodloe [1], the authors develop a static modal logic for knowledge, belief, and safety to analyze a family of aviation mishaps involving a type of reasoning error suffered by a single pilot. This paper extends that work by employing dynamic methodologies from logical dynamics to the analysis of mishaps. The use of a dynamic logic rather than a static logic connects safety-critical information and actions in a more natural way, and allows for easier inference from action to information. The application of these methods advances the discipline of logical dynamics by employing them in the real world, beyond toy examples and logic puzzles, and likewise improves the discipline of aviation safety by introducing a formal method suitable for analyzing safety-critical information flow between pilots and machine.

Recent work at the intersection of game theory and logical dynamics focuses on information flow during games. Van Ditmarsch identifies a class of games called knowledge games, in which players have diverging information[6]. This slightly relaxes the assumption of classical game theory that players have common knowledge about each other’s perfect information. This invites logicians to study the information conveyed by the fact that an action is executed. For example, if agent $1$ asks agent $2$ the question, “$p$?”, the information conveyed is that $1$ does not know whether $p$, believes that $2$ knows whether $p$, and after the action occurs, this information becomes publicly known. Many actions convey such information, beyond mere speech acts. For example, when a pilot provides flight control inputs, her action conveys information about what she believes about the aircraft’s state, namely that it is in a state that safely permits those inputs. Anyone observing her inputs, like the first officer or the flight computer, can make such inferences about her mental picture based on her actions.

This paper proceeds as follows. In Section 2 we define the formal model, which consists of a set of axioms in a dynamic modal logic for reasoning about pilot knowledge, belief, and safety. Section 3 mechanizes the model in the Coq Proof Assistant and applies it to case studies, illustrating the logic’s use as a formal method for aviation safety. We offer a brief discussion of future work in Section 5 and conclude in Section 6.

2 Dynamic Agent Safety Logic

The logic for reasoning about information flow in knowledge games is called Dynamic Epistemic Logic (DEL). As its name suggests, it combines elements of epistemic logic and dynamic logic. Epistemic logic is the static logic for reasoning about knowledge, and dynamic logic is used to reason about actions. In dynamic logic semantics, nodes are states of the system or the world, and relations on nodes are transitions via programs or actions from node to node. If we think of each node in dynamic logic as being a model of epistemic logic, then actions become relations on models, representing transitions from one multi-agent epistemic model to another. For example, if we have a static epistemic model $M1$ representing the knowledge states of agents $1$ and $2$ at a moment, then the action $``p?"$ is a relation between $M1$ and $M2$, a new static epistemic model of $1$’s and $2$’s knowledge after the question is asked. All of this is captured by DEL.

We are concerned with an additional element: the safety status of an action, and an agent’s knowledge and belief about that. To capture this, we extend DEL and call the new logic Dynamic Agent Safety Logic (DASL). The remainder of this section presents DASL’s syntax, semantics, and proves its soundness.

2.1 Syntax and Semantics

The Dynamic Agent Safety Logic (DASL) used in this paper has the following syntax.

$\varphi\ ::=\ \mathit{p}\ |\ {\neg}\varphi\ |\ \varphi{\ \wedge\ }\varphi\ |\ \mathbf{K}_{\mathbf{i}}\,\varphi\ |\ \mathbf{B}_{\mathbf{i}}\,\varphi\ |\ \mathbf{[{i,(A,a)}]}\varphi\ |\ \mathbf{[{i,(A,a),S}]}\varphi,$

where $\mathit{p}\in AtProp$ is an atomic proposition, $\mathbf{i}$ refers to $i\in Agents$, $\mathbf{a}$ is the name of an action, called an action token, belong to a set of such tokens, $Actions$, and $\mathbf{A}$ refers to an action structure. The knowledge operator $\mathbf{K}_{\mathbf{i}}\,$ indicates that “agent i knows that …” Similarly, the operator for belief, $\mathbf{B}_{\mathbf{i}}\,$ can be read, “agent i believes that…” The notion of action tokens and structures will be defined in the semantics. The operators $\mathbf{[{i,(A,a)}]}$ and $\mathbf{[{i,(A,a),S}]}$ are the dynamic operators for agent $i$ executing action token $a$ from action structure $A$ in the former case, and doing so safely in the latter case. Note that the $\mathbf{S}$ in $\mathbf{[{i,(A,a),S}]}$ stands for ‘safety’, and is not a variable, whereas the $\mathbf{i,(A,a)}$ are variables for agents, action structures, and action tokens, respectively. One can read the action operators as “after $i$ executes $a$ from $A$, $\varphi$ holds.’ We define the dual modal operators $\langle\mathbf{K}_{i}\rangle\,$, $\langle\mathbf{B}_{i}\rangle\,$, $\mathbf{\langle i,(A,a)\rangle}\,$, and $\mathbf{\langle i,(A,a),\mathbf{S}\rangle}\,$ in the usual way.

The semantics of DASL involve two structures that are defined simultaneously, one for epistemic models, and one for action structures capturing the transition relation among epistemic models. Additionally, we define numerous helper functions that straddle the division between metalanguage and object language.

2.1.1 Kripke Model

A Kripke model $M\in Model$ is a tuple $\langle W,\{R_{k}^{i}\},\{R_{b}^{i}\},w,V\rangle$. It is a set of worlds, sets of epistemic and doxastic relations on worlds for agents, a world denoting the actual world, and a valuation function V mapping atomic propositions to the set of worlds satisfying them. Most readers will be somewhat familiar with epistemic logic, the logic for reasoning about knowledge. Doxastic logic is a similar logic for reasoning about belief[9].

2.1.2 Action Structure

An action structure $A\in ActionStruct$ is a tuple $\langle Actions,\\ \{\chi_{k}^{i}\},\{\chi_{b}^{i}\},a\rangle$. It is a set of action tokens, sets of epistemic and doxastic relations on action tokens for agents, and an action token, $a$, denoting an actual action token executed.

An action structure captures the associated subjective events of an action occurring, including how it is observed by various agents, incorporating their uncertainty. The action tokens are the actual objective events that might occur. For example, if I am handed a piece of paper telling me who won the Oscar for Best Actress, and I read it, and you see me read it, then the action structure will include possible tokens in which I read that each nominee has won, and you will consider each of these tokens to be possible. When I read the paper, I consider only one action token to be the one executed. This action structure represents that transition from one epistemic model, in which both of us considers all nominees the potential winner, to an epistemic model in which I know the winner and you still do not know the winner. We can think of the action structure $A$ as the general action “Agent 1 reads the piece of paper” and the tokens as the specific actions “Agent 1 reads that nominee n has won the award.”

2.1.3 Model Relation

Just as $R_{k}^{i}$ denotes a relation on worlds, $\llbracket i,(A,a)\rrbracket$ denotes a relation on Kripke model-world pairs. It represents the relation that holds between $M,w$ and $M^{\prime},w^{\prime}$ when agent $i$ executes action $(A,a)$ at $M,w$ and causes the world to transition to $M^{\prime},w^{\prime}$.

2.1.4 Precondition Function

The Precondition function, $pre::Actions\mapsto\varphi$, maps an action to the formula capturing the conditions under which the action can occur. For example, if we assume agents tell the truth, then an announcement action has as a precondition that the announced proposition is true, as with regular Public Announcement Logic.

2.1.5 Postcondition Function

The Postcondition function, $post::A\times AtProp\mapsto AtProp$, takes an action structure and an atomic proposition, and maps to the corresponding atomic proposition after the action occurs.

[TABLE]

2.1.6 Update Function

The Update function, $update::(Model\times ActionStruct\times W\times Actions\times Agents)\mapsto(Model\times W)$, takes a Kripke model $M$, an action structure $A$, a world from the Kripke model, an action token from the Action structure, and an agent executing the action, and returns a new Kripke model-world pair. It represents the effect actions have on models, and is more complicated than other DEL semantics in that actions can change the facts on the ground in addition to the knowledge and belief relations. It is a partial function that is defined iff a model-world pair satisfies the action’s preconditions.

$update(M,A,w,a,i)=(M^{\prime},w^{\prime})\ where:\\$ $1.\ M=\langle W,\{R_{k}^{i}\},\{R_{b}^{i}\},w,V\rangle$

$2.\ A=\langle Actions,\{\chi_{k}^{i}\},\{\chi_{b}^{i}\},a,pre,post\rangle$

$3.\ M^{\prime}=\langle W^{\prime},\{R_{k}^{\prime i}\},\{R_{b}^{\prime i}\},w^{\prime},V^{\prime}\rangle$

$4.\ W^{\prime}=\{(w,a)|w\in W,a\in Actions,\ \textsf{\ and \ }\ w\models pre(a)\}$

$5.\ R_{k}^{\prime i}=\{((w,a),(v,b))|wR_{k}^{i}v\textsf{\ and \ }a\chi_{k}^{i}b\}$

$6.\ R_{b}^{\prime i}=\{((w,a),(v,b))|wR_{b}^{i}v\textsf{\ and \ }a\chi_{b}^{i}b\}$

$7.\ w^{\prime}=(w,a)$

$8.\ V^{\prime}(p)=post(A,p)$

2.1.7 Safety Precondition Function

The Safety Precondition Function, $pre_{s}::Actions\mapsto\varphi$, is a more restrictive function than $pre$. Where $pre$ returns the conditions that dictate whether the action is possible, $pre_{s}$ returns the conditions that dictate whether the action is safely permissible. This function is the key reason the dynamic approach allows for easy inference from action to safety-critical information.

The logic DASL has the following Kripke semantics.

$\displaystyle M,w\models p$ $\displaystyle\textsf{\ iff \ }w\in V(p)$

$\displaystyle M,w\models{\neg}\varphi$ $\displaystyle\textsf{\ iff \ }M,w\not\models\varphi$

$\displaystyle M,w\models\varphi{\ \wedge\ }\psi$ $\displaystyle\textsf{\ iff \ }M,w\models\varphi\textsf{\ and \ }M,w\models\psi$

$\displaystyle M,w\models\mathbf{K}_{\mathbf{i}}\,\varphi$ $\displaystyle\textsf{\ iff \ }\forall v,\ wR_{k}^{i}v\ \textsf{\ implies \ }\ M,v\models\varphi$

$\displaystyle M,w\models\mathbf{B}_{\mathbf{i}}\,\varphi$ $\displaystyle\textsf{\ iff \ }\forall v,\ wR_{b}^{i}v\ \textsf{\ implies \ }\ M,v\models\varphi$

$\displaystyle M,w\models\mathbf{[{i,(A,a)}]}\varphi$ \displaystyle\textsf{\ iff \ }\forall M^{\prime},w^{\prime},\ (M,w)\llbracket i,(A,a)\rrbracket(M^{\prime},w^{\prime})\

$\displaystyle\textsf{\ implies \ }\ M^{\prime},w^{\prime}\models\varphi$

$\displaystyle M,w\models\mathbf{[{i,(A,a),S}]}\varphi$ \displaystyle\textsf{\ iff \ }\forall M^{\prime},w^{\prime},\ (M,w)\llbracket i,(A,a),S\rrbracket(M^{\prime},w^{\prime})\

$\displaystyle\textsf{\ implies \ }\ M^{\prime},w^{\prime}\models\varphi$

The definitions of the dynamic modalities make use of a relation between two model-world pairs, which we now define.

$\displaystyle(M,w)\llbracket i,(A,a)\rrbracket(M^{\prime},w^{\prime})$ $\displaystyle\textsf{\ iff \ }M,w\models\mathit{pre}(a)$

$\displaystyle\textsf{\ and \ }update(M,A,w,a,i)=(M^{\prime},w^{\prime})$

$\displaystyle(M,w)\llbracket i,(A,a),S\rrbracket(M^{\prime},w^{\prime})$ $\displaystyle\textsf{\ iff \ }M,w\models pre_{s}(a)$

$\displaystyle\textsf{\ and \ }update(M,A,w,a,i)=(M^{\prime},w^{\prime})$

2.2 Hilbert System

DASL is axiomatized by the following Hilbert system.

All propositional tautologies are axioms.

$\mathbf{K}_{\mathbf{i}}\,$ is T (knowledge relation is reflexive)

$\mathbf{B}_{\mathbf{i}}\,$ is KD45 (belief relation is serial, transitive, and Euclidean)

EP1: $\mathbf{K}_{\mathbf{i}}\,\varphi{\ \Rightarrow\ }\mathbf{B}_{\mathbf{i}}\,\varphi$

EP2: $\mathbf{B}_{\mathbf{i}}\,\varphi{\ \Rightarrow\ }\mathbf{B}_{\mathbf{i}}\,\mathbf{K}_{\mathbf{i}}\,\varphi$

EP3: $\mathbf{B}_{\mathbf{i}}\,\varphi{\ \Rightarrow\ }\mathbf{K}_{\mathbf{i}}\,\mathbf{B}_{\mathbf{i}}\,\varphi$

SP: $\mathbf{[{i,(A,a)}]}\varphi{\ \Rightarrow\ }\mathbf{[{i,(A,a),S}]}\varphi$

PR: $\mathbf{\langle i,(A,a)\rangle}\,\varphi{\ \Rightarrow\ }\mathbf{B}_{\mathbf{i}}\,\mathbf{\langle i,(A,a),\mathbf{S}\rangle}\,\varphi$,

plus the inference rules Modus Ponens and Necessitation for $\mathbf{K}_{\mathbf{i}}\,$ and $\mathbf{B}_{\mathbf{i}}\,$.

Above are the axioms characterizing the logic. Knowledge is weaker here than in most epistemic logics, and belief is standard [7]. They are related logically by EP(1-3), which hold that knowledge entails belief, belief entails that one believes that one knows, and belief entails than one knows that one believes. Finally, actions and safe actions are logically related by SP and PR, which hold that necessary consequences of mere action are also necessary consequences of safe actions, and that a pilot can execute an action only if he believes that he is executing a safe action.

2.3 Soundness

Theorem 2.1 (Soundness)

*Dynamic Agent Safety Logic is sound for Kripke structures with

(1) reflexive $R_{k}^{i}$ relations,

(2) serial, transitive, Euclidean $R_{b}^{i}$ relations,

(3) which are partially ordered $(R_{k}^{i}\circ R_{b}^{i})\subseteq R_{b}^{i}$, $(R_{b}^{i}\circ R_{k}^{i})\subseteq R_{b}^{i}$, and $R_{b}^{i}\subseteq R_{k}^{i}$,

(4) $\llbracket i,(A,a),S\rrbracket\subseteq\llbracket i,(A,a)\rrbracket$and

(5) $(\llbracket i,(A,a),S\rrbracket\circ R_{b}^{i})\subseteq\llbracket i,(A,a)\rrbracket$.*

$\mathbf{Proof}.$ $(1)\ and\ (2)$ correspond to the axioms that $\mathbf{K}_{\mathbf{i}}\,$ is a T modality and $\mathbf{B}_{\mathbf{i}}\,$ is a KD45 modality in the usual way. $(3)$ corresponds to EP1, EP2, and EP3. Axioms AP through SB are reduction axioms. This leaves $(4)$, corresponding to SP, and $(5)$ which corresponds to PR. Here we will prove $(5)$. Let $M$ be a Kripke structure satisfying the five conditions above. Let $A$ be an Action structure with $a$ and $i$ as its actual action token and agent.

We prove $(5)$ via the contrapositive of PR: $\langle\mathbf{B}_{i}\rangle\,\mathbf{[{i,(A,a),S}]}\varphi{\ \Rightarrow\ }\mathbf{[{i,(A,a)}]}\varphi$. Assume $M,w\models\langle\mathbf{B}_{i}\rangle\,\mathbf{[{i.(A,a),S}]}\varphi$. By the semantics of $\langle\mathbf{B}_{i}\rangle\,$, there exists a $v$, such that $wR_{b}^{i}v$ and $v\models\mathbf{[{i,(A,a),S}]}\varphi$. From the semantics, it follows that forall $M^{\prime},v^{\prime}$, if $(M,v)\llbracket i,(A,a),S\rrbracket(M^{\prime},v^{\prime})$ then $M^{\prime},v^{\prime}\models\varphi$. By slightly abusing the notation, and letting $(W,w)R_{b}^{i}(W,v)$ be equivalent to $wR_{b}^{i}v$, we can create the composed relation $(\llbracket i,(A,a),S\rrbracket\circ R_{b}^{i})$. It then holds, by condition $(5)$, that $(M,w)(\llbracket i,(A,a),S\rrbracket\circ R_{b}^{i})(M^{\prime},v^{\prime})$ implies $(M,w)\llbracket i,(A,a)\rrbracket(M^{\prime},v^{\prime})$. So, for all $M^{\prime},v^{\prime}$, if $(M,w)\llbracket i,(A,a)\rrbracket(M^{\prime},v^{\prime})$, then $M^{\prime},v^{\prime}\models\varphi$. So, $M,w\models\mathbf{[{i,(A,a)}]}\varphi$. $\Box$

3 Case Study and Mechanization

We apply the logic just developed to the formal analysis of the Air France 447 aviation incident. We also mechanize the formalization in the Coq Proof Assistant. Our mechanization follows similar work by Maliković and Čubrilo [12, 13], in which they mechanize an analysis of the game of Cluedo using Dynamic Epistemic Logic, based on van Ditmarsch’s formalization of the game [6]. It is commonly assumed that games must be adversarial, but this is not the case. Games need only involve situations in which players’ payoffs depend on the actions of other players. Similarly, knowledge games need not be adversarial, and must only involve diverging information. Thus, it is appropriate to model aviation incidents as knowledge games of sorts, where players’ payoffs depend on what others do, specifically the way the players communicate information with each other. The goal is to achieve an accurate situational awareness and provide flight control inputs appropriate for the situation. Failures to achieve this goal result in disaster, and often result from imperfect information flow. A formal model of information flow in these situations provides insight and allows for the application of formal methods to improve information flow during emergency situations.

3.1 Air France 447

This case study is based on the authoritative investigative report into Air France 447 performed and released by France’s Bureau d’Enquêtes et d’Analyses pour la Sécurité de l’Aviation Civile (BEA), responsible for investigating civil aviation incidents and issuing factual findings[4]. The case is mechanized by instantiating, in Coq, the above logic to reflect the facts of the case. One challenge associated with this is that the readings about inputs present in aviation are often real values on a continuum, whereas for our purposes we require discrete values. We accomplish this by dividing the continuum associated with inputs and readings into discrete chunks, similar to how fuzzy logic maps defines predicates with real values[10].

This paper will formalize an excerpted instance from the beginning of the case, involving an initial inconsistency among airspeed indicators, and the subsequent dangerous input provided by the pilot. Formalized in the logic, the facts of the case allow us to infer that the pilot lacked negative introspection about the safety-critical data required for his action. This demonstrates that the logic allows information about the pilot’s situational awareness to flow to the computer, via the pilot’s actions. It likewise establishes a safety property to be enforced by the computer, namely that a pilot should maintain negative introspection about safety-critical data, and if he fails to do so, it should be re-established as quickly as possible.

According to the official report, at 2 hours and 10 minutes into the flight, a Pitot probe likely became clogged by ice, resulting in an inconsistency between airspeed indicators, and the autopilot disconnecting. This resulted in a change of mode from Normal Law to Alternate Law 2, in which certain stall and control protections ceased to exist. The pilot then made inappropriate control inputs, namely aggressive nose up commands, the only explanation for which is that he mistakenly believed that the aircraft was in Normal Law mode with protections in place to prevent a stall. This situation, and the inference regarding the pilot’s mistaken belief, is modeled in the following application and mechanization of the logic.

3.2 Mechanization in Coq

The following mechanization demonstrates progress from the artificially simply toy examples normally analyzed in the literature to richer real-world examples. However, it does not represent the full richness of the approach. The actions and instrument readings mechanized in this paper are constrained to those most relevant to the case study. The approach is capable of capturing the full richness of all instrument reading configurations and actions available to a pilot. To do so, one needs to consult a flight safety manual and formally represent each action available to a pilot, and each potential instrument reading, according to the following scheme.

Before beginning, we note that our use of sets in the following Coq code requires the following argument passed to coqtop before executing: -impredicative-set. In CoqIDE, this can be done by selecting the ‘Tools’ dropdown, then ‘Coqtop arguments’. Type in -impredicative-set.

We first formalize the set of agents.

⬇ Inductive Agents: Set := Pilot | CoPilot | AutoPilot.

Next we formalize the set of available inputs. These themselves are not actions, but represent atomic propositions true or false of a configuration.

⬇ Inductive Inputs : Set :=

               HardThrustPlus  | ThrustPlus

             | HardNoseUp      | NoseUp

             | HardWingLeft    | WingLeft

             | HardThrustMinus | ThrustMinus

             | HardNoseDown    | NoseDown

             | HardWingRight   | WingRight.

We represent readings by indicating which side of the panel they are on. Typically, an instrument has a left-side version, a right-side version, and sometimes a middle version serving as backup. When one of these instruments conflicts with its siblings, the autopilot will disconnect and give control to the pilot.

⬇ Inductive Side : Set := Left | Middle | Right.

We divide the main instruments into chunks of values they can take, in order to provide them with a discrete representation in the logic. For example, the reading VertUp1 may represent a nose up reading between 0$\degree$ and 10$\degree$, while VertUp2 represents a reading between 11$\degree$ and 20$\degree$.

⬇ Inductive Readings (s : Side) : Set :=

      VertUp1 | VertUp2 | VertUp3 | VertUp4

    | VertDown1 | VertDown2 | VertDown3 | VertDown4

    | VertLevel | HorLeft1 | HorLeft2 | HorLeft3

    | HorRight1 | HorRight2 | HorRight3 | HorLevel

    | AirspeedFast1 | AirspeedFast2 | AirspeedFast3

    | AirspeedSlow1 | AirspeedSlow2 | AirspeedSlow3

    | AirspeedCruise| AltCruise | AltClimb | AltDesc | AltLand.

We define a set of potential modes the aircraft can be in.

⬇ Inductive Mode : Set := Normal | Alternate1 | Alternate2.

We define a set of global instrument readings representing the mode and all of the instrument readings, left, right, and middle, combined together. This represents the configuration of the instumentation.

⬇ Inductive GlobalReadings : Set := Global (m: Mode)

                                        (rl : Readings Left)

                                        (rm : Readings Middle)

                                        (rr : Readings Right).

The set of atomic propositions we are concerned with are those representing facts about the instrumentation.

⬇ Inductive Atoms : Set :=

     | M (m : Mode)

     | Input (a : Inputs)

     | InstrumentL (r : Readings Left)

     | InstrumentM (r : Readings Middle)

     | InstrumentR (r : Readings Right)

     | InstrumentsG (g : GlobalReadings).

Next we follow Maliković and Čubrilo [12, 13] in defining a set prop of propositions in predicate calculus, distinct from Coq’s built in type Prop. The definition provides constructors for atomic propositions consisting of particular instrument reading predicate statements, implications, propositions beginning with a knowledge modality, and those beginning with a belief modality. Interestingly, modal logic cannot be directly represented in Coq’s framework [11]. We first define propositions in first-order logic, which we then use to define DASL. This appears to be the standard technique for mechanizing modal logics in Coq.

⬇ Inductive prop : Set :=

| atm : Atoms $\rightarrow\;$ prop

| imp: prop $\rightarrow\;$ prop $\rightarrow\;$ prop

| Forall : forall (A : Set), (A $\rightarrow\;$ prop) $\rightarrow\;$ prop

| K : Agents $\rightarrow\;$ prop $\rightarrow\;$ prop

| B : Agents $\rightarrow\;$ prop $\rightarrow\;$ prop

| Ck : list Agents $\rightarrow\;$ prop $\rightarrow\;$ prop

| Cb : list Agents $\rightarrow\;$ prop $\rightarrow\;$ prop.

We use the following notation for implication and universal quantification.

⬇ Infix "$\Longrightarrow\;$" := imp (right associativity, at level 85).

Notation "-/ p" := (Forall _ p) (at level 70, right associativity).

We likewise follow Maliković and Čubrilo [12, 13] by defining an inductive type theorem representing a theorem of DASL. The constructors correspond to the Hilbert system, either as characteristic axioms, or inference rules. The first three represent axioms for propositional logic, then the rule Modus Ponens, then the axioms for the epistemic operator plus its Necessitation rule, then the doxastic operator and its Necessitation rule. Do not confuse the Necessitation rules with material implication in the object language. The final constructors capture the axioms relating belief and knowledge. The axioms for dynamic modal operators are defined separately, and are not included here.

⬇ Inductive theorem : prop $\rightarrow\;$ Prop :=

|Hilbert_K: forall p q : prop, theorem (p $\Longrightarrow\;$ q $\Longrightarrow\;$ p)

|Hilbert_S: forall p q r : prop,

            theorem ((p$\Longrightarrow\;$q$\Longrightarrow\;$r)$\Longrightarrow\;$(p$\Longrightarrow\;$q)$\Longrightarrow\;$(p$\Longrightarrow\;$r))

|Classic_NOTNOT : forall p : prop, theorem ((NOT (NOT p)) $\Longrightarrow\;$ p)

|MP : forall p q : prop, theorem (p $\Longrightarrow\;$ q) $\rightarrow\;$ theorem p $\rightarrow\;$ theorem q

|K_Nec : forall (a : Agents) (p : prop), theorem p $\rightarrow\;$ theorem (K a p)

|K_K : forall (a : Agents) (p q : prop),

      theorem (K a p $\Longrightarrow\;$ K a (p $\Longrightarrow\;$ q) $\Longrightarrow\;$ K a q)

|K_T : forall (a : Agents) (p : prop), theorem (K a p $\Longrightarrow\;$ p)

|B_Nec : forall (a : Agents) (p : prop), theorem p $\rightarrow\;$ theorem (B a p)

|B_K : forall (a : Agents) (p q : prop),

      theorem (B a p $\Longrightarrow\;$ B a (p $\Longrightarrow\;$ q) $\Longrightarrow\;$ B a q)

|B_Serial : forall (a : Agents) (p : prop),

           theorem (B a p $\Longrightarrow\;$ NOT (B a (NOT p)))

|B_4 : forall (a : Agents) (p : prop), theorem (B a p $\Longrightarrow\;$ B a (B a p))

|B_5 : forall (a : Agents) (p : prop),

      theorem (NOT (B a p) $\Longrightarrow\;$ B a (NOT (B a p)))

|K_B : forall (a : Agents) (p : prop), theorem (K a p $\Longrightarrow\;$ B a p)

|B_BK : forall (a : Agents) (p : prop), theorem (B a p $\Longrightarrow\;$ B a (K a p)).

We use the following notation for theorem:

⬇ Notation "|-- p" := (theorem p) (at level 80).

We encode actions as records in Coq, recording the acting pilot, the observability of the action (whether it is observed by other agents or not), the input provided by the pilot, and the preconditions for the action and the safety preconditions for the action, both represented as global atoms.

⬇ Record Action : Set := act {Ai : Agents; Aj : Agents; pi : PI;

                            input : Inputs; c : GlobalReadings;

                            c_s : GlobalReadings}.

The variable c holds the configuration representing the precondition for the action, while the variable c_s holds the configuration for the safety precondition.

We encode the precondition and safety precondition functions as follows.

⬇ Function pre (a:Action) : prop := atm (InstrumentsG (c a)).

Function pre_s (a : Action) : prop := atm (InstrumentsG (c_s a)).

In the object language, the dynamic modalities of action and safe action are encoded as follows.

⬇ Parameter aft_ex_act : Action $\rightarrow\;$ prop $\rightarrow\;$ prop.

Parameter aft_ex_act_s : Action $\rightarrow\;$ prop $\rightarrow\;$ prop.

Many standard properties of logic, like the simplification of conjunctions, hypothetical syllogism, and contraposition, are encoded as Coq axioms. As an example, here is how we encode simplifying a conjunction into just its left conjunct.

⬇ Axiom simplifyL : forall p1 p2,

   |– p1 & p2 $\rightarrow\;$ |– p1.

We formalize the configuration of the instruments at 2 hour 10 minutes into the flight as follows.

⬇ Definition Config_1 := (atm (M Alternate2)) &

                     (atm (InstrumentL (AirspeedSlow3 Left))) &

                     (atm (InstrumentM (AirspeedSlow3 Middle))) &

                     (atm (InstrumentR (AirspeedCruise Right))).

The mode is Alternate Law 2, and the left and central backup instruments falsely indicate that the airspeed is very slow, while the right side was not recorded, but because there was a conflict, we assume it remained correctly indicating a cruising airspeed.

The pilot’s dangerous input, a hard nose up command, is encoded as follows.

⬇ Definition Input1 := act Pilot Pilot Pri HardNoseUp

                   (Global Alternate2 (AirspeedSlow3 Left)

                                        (AirspeedSlow3 Middle)

                                        (AirspeedCruise Right))

                   (Global Normal (AirspeedCruise Left)

                                   (AirspeedCruise Middle)

                                   (AirspeedCruise Right)).

The action is represented in the object language by taking the dual of the dynamic modality, ${\neg}\mathbf{[{i,(A,a)}]}{\neg}True$, equivalently $\mathbf{\langle i,(A,a)\rangle}\,True$, indicating that the precondition is satisfied and the action token is executed.

⬇ Definition Act_1 := NOT (aft_ex_act Input1 (NOT TRUE)).

The actual configuration satisfies the precondition for the action, but it is inconsistent with the safety precondition. The safety precondition for the action indicates that the mode should be Normal and the readings should consistently indicate cruising airspeed. However, in Config_1, the conditions do not hold. Thus, the action is unsafe. From the configuration and the action, DASL allows us to deduce that the pilot lacks negative introspection of the action’s safety preconditions.

Negative introspection is an agent’s awareness of the current unknowns. To lack it is to be unaware of one’s unknown variables, so lacking negative introspection about one’s safety preconditions is to be unaware that they are unknown.

⬇ Theorem NegIntroFailMode :

               |– (Config_1 $\Longrightarrow\;$

                     Act_1 $\Longrightarrow\;$

                     ((NOT (K Pilot (pre_s(Action1)))) &

                      (NOT (K Pilot (NOT (K Pilot (pre_s(Action1)))))))).

In fact, in general it holds that if the safety preconditions for an action are false, and the pilot executes that action, then the pilot lacks negative introspection of those conditions. We have proven both the above theorem, and the more general theorem, in Coq.

⬇ Theorem neg_intro_failure :

forall (A Ao : Agents) (pi : PI) (inp : Inputs)

 (m : Mode)

 (rl : Readings Left) (rm : Readings Middle) (rr : Readings Right)

 (ms : Mode)

 (rls : Readings Left) (rms : Readings Middle) (rrs : Readings Right)

 phi,

|– (NOT

   (aft_ex_act

      (act A Ao pi inp (Global m rl rm rr) (Global ms rls rms rrs))

   (NOT phi)) $\Longrightarrow\;$

  NOT (atm (InstrumentsG (Global ms rls rms rrs))) $\Longrightarrow\;$

    (NOT (K A (atm (InstrumentsG (Global ms rls rms rrs)))) &

    (NOT (K A (NOT (K A (atm (InstrumentsG (Global ms rls rms rrs))))))))).

This indicates that negative introspection about safety preconditions is a desirable safety property to maintain, consistent with the official report’s criticism that the Airbus cockpit system did not clearly display the safety critical information. The logic described in this research accurately models the report’s findings that the pilot’s lack of awareness about safety-critical information played a key role in his decision to provide unsafe inputs. Furthermore, the logic supports efforts to automatically infer which safety-critical information the pilot is unaware of and effectively display it to him.

4 Additional Case Studies

To illustrate the flexibility of this approach, we now formalize additional case studies in the logic. We begin with two additional aviation incidents, Copa Airlines flight 201 and Asiana Airlines flight 214, and then turn our attention to the domains of emergency health care and powerplant operations.

We make use of the following lemma.

[TABLE]

$\mathbf{Proof}$. From the fact that the belief modality is serial, it holds that

[TABLE]

which is equivalent to

[TABLE]

Due to axiom EP1, it follows that

[TABLE]

$\Box$

4.1 Copa 201 and Asiana 214

Copa flight 201 departed Panama City, Panama for Cali, Colombia in June, 1992. Due to faulty wiring in the captain’s Attitude Indicator, he incorrectly believed he was in a left bank position. In response to this, he directed the plane into an 80 degree roll to the right, which caused the plane to enter a steep dive. A correctly functioning backup indicator was available to the captain, and investigators believe that the captain intended to direct the backup indicator’s readings to his own, but due to an outdated training module, the flip he switched actually sent his own faulty readings to the co-pilot’s indicator. Approximately 29 minutes after takeoff, the plane crashed into the jungle and all passengers and crew perished. We formalize the moment at which the pilot provides the hard right roll input.

$\mathit{(LeftAIHorLeft2)}{\ \wedge\ }{\neg}\mathit{(MiddleAIHorLeft2)}\dots$——————– configuration. 2. 2.

$\mathbf{\langle\mathit{pilot},\mathit{hardwingright}\rangle}\,\mathit{true}$———————————————— pilot input. 3. 3.

$\mathbf{B}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2})$———————————— from axiom PR, $\mathit{pre_{s}}$. 4. 4.

${\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2})$——————————- from axiom K-Reflexive. 5. 5.

$\mathbf{B}_{\mathbf{\mathit{pilot}}}\,\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2})$————————— from (3), axiom EP2. 6. 6.

${\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2})$——————— from (5), B-Serial, EP1. 7. 7.

${\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2}){\ \wedge\ }{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2})$– (4), (6). 8. 8.

${\neg}({\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2}){\ \Rightarrow\ }\mathbf{K}_{\mathbf{\mathit{pilot}}}\,{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{MiddleAIHorLeft2}))$ - (7).

Asiana flight 214 from South Korea to San Francisco departed in the evening of July 6, 2013 and was schedule to land just before noon that morning. The weather was good and air traffic control cleared the pilots to perform a visual approach to the runway. The plane came in short and crashed against an embankment in front of the runway, resulting in the deaths of three passengers and 187 injured. The National Transportation Safety Board (NTSB) investigation found that the captain had mismanaged the approach and monitoring of the airspeed, resulting in the plane being too high for a landing. Upon noticing this, the captain selected a flight mode (flight level change speed) which unexpectedly cause the plane to climb higher. In response to this, the captain disconnected the autopilot and pulled back on the thrust. This caused an autothrottle (A/T) protection to turn off, so when the captain pitched the nose down, the plane descended fast than was safe, causing it to come down too quickly and collide with the embankment in front of the runway. We will formalize the moment at which the pilot pitches the nose down.

$\mathit{(A/T=Off)}{\ \wedge\ }\mathit{(AirspeedSlow3)}\dots$—————————– configuration. 2. 2.

$\mathbf{\langle\mathit{pilot},\mathit{hardthrustminus}\rangle}\,\mathit{true}$——————————————- pilot input. 3. 3.

$\mathbf{B}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On})$—————————————— from axiom PR, $\mathit{pre_{s}}$. 4. 4.

${\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On})$————————————- from axiom K-Reflexive. 5. 5.

$\mathbf{B}_{\mathbf{\mathit{pilot}}}\,\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On})$———————————– from (3), axiom EP2. 6. 6.

${\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On})$————————— from (5), B-Serial, EP1. 7. 7.

${\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On}){\ \wedge\ }{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On})$—————- (4), (6). 8. 8.

${\neg}({\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On}){\ \Rightarrow\ }\mathbf{K}_{\mathbf{\mathit{pilot}}}\,{\neg}\mathbf{K}_{\mathbf{\mathit{pilot}}}\,(\mathit{A/T=On}))$ —————— (7).

The above formalizations follow the same format as that of Air France 447. A pilot provides an input whose safety precondition conflicts with one of the instruments in the configuration, and we infer that the pilot lacks negative introspection of the safety precondition. This is distinct from but related to the property that the pilots, in engaging in an unsafe action, are unaware of the unsafe instrument readings. Thus, we describe our first safety properties.

Safety Negative Introspection (SNI). If a safety precondition does not hold, then agent knows that he does not know it to hold.

[TABLE] 2. 2.

Unsafety Delivery (UD). If a safety precondition is false, then agent knows that it is false.

[TABLE]

Our above formalizations show that SNI is false when a pilot provides an unsafe input. Notice that UD implies SNI.

$\mathbf{Proof}$. It suffices to show that $\mathbf{K}_{\mathbf{i}}\,{\neg}\varphi{\ \Rightarrow\ }\mathbf{K}_{\mathbf{i}}\,{\neg}\mathbf{K}_{\mathbf{i}}\,\varphi.$ Assume $\mathbf{K}_{\mathbf{i}}\,{\neg}\varphi$ holds. From EP1, it follows that $\mathbf{B}_{\mathbf{i}}\,{\neg}\varphi$, and because knowledge is a normal modality, it follows that $\mathbf{K}_{\mathbf{i}}\,\mathbf{B}_{\mathbf{i}}\,{\neg}\varphi$ holds. From lemma 1, and again the fact that knowledge is normal modality, it follows that $\mathbf{K}_{\mathbf{i}}\,{\neg}\mathbf{K}_{\mathbf{i}}\,{\neg}{\neg}\varphi$, or equivalently, that $\mathbf{K}_{\mathbf{i}}\,{\neg}\mathbf{K}_{\mathbf{i}}\,\varphi$. $\Box$

However, the converse does not hold. We can satisfy SNI when the safety precondition is false, the agent knows that he doesn’t know it, but doesn’t know that it is false. A counterexample consists of a model with three worlds: {u,v}. Let $\varphi$ be the safety precondition, with the following truth assignment: {False, True}. Let the epistemic relation include (u,v), (v,u), and the reflexive relations. Then at world u $\varphi$ is false, and $\mathbf{K}_{\mathbf{i}}\,{\neg}\mathbf{K}_{\mathbf{i}}\,\varphi$ is true, but $\mathbf{K}_{\mathbf{i}}\,{\neg}\varphi$ is false.

The formalization show that from the pilot’s unsafe action, it follows that he lacks negative introspection of the safety precondition.

[TABLE]

This situation violates SNI, because the pilot doesn’t know that he doesn’t know the safety precondition. Since UD implies SNI, UD is also violated.

[TABLE]

So, from an unsafe action, we can also infer that the pilot does not know that the safety precondition is false, a stronger conclusion.

Thus, by restoring knowledge that the safety precondition is false, it follows that either the safety precondition is true, or the unsafe action is not executed.

[TABLE]

The pilot’s knowledge in the antecedent implies that the safety precondition is false, so this simplifies to:

[TABLE]

This squares with the standard game theoretic inference, wherein a rational agent with knowledge of the situation executes a good action. Because our model of knowledge and rationality is weaker, we make the weaker claim that a minimally rational pilot with knowledge of the safety-critical information does not execute a bad action.

5 Future Work

The case study presented in this paper is overly simplified due to space constraints. Future work will undertake the task of extending the approach to other actions in the Air France 447 incident, and the safety-critical information expressed by them. For example, when both pilots provided conflicting inputs to the aircraft, the computer could have inferred that neither was aware of the other’s actions. This will illustrate the use of the approach in a multi-agent context. Similarly, as recommended by an anonymous reviewer, we shall apply the approach to other aviation mishaps involving complicated safety-critical information flow, specifically Asiana Airlines Flight 214 [14].

An important extension of the foundational work provided by this paper is the construction of a system that takes advantage of the logic as a runtime safety monitor. It will monitor the pilot’s control inputs and current flight configurations, and in the event that an action’s safety preconditions do not hold, infer which instrument readings the pilot is unaware of and act to correct this. In order to avoid further information overload, the corrective action taken by the computer should be to temporarily remove or dim the non-safety-critical information from competition for the pilot’s attention, until the pilot’s unsafe control inputs are corrected, indicating awareness of the safety-critical information. Construction of a prototype of this system is underway.

6 Conclusion

This paper has described Dynamic Agent Safety Logic (DASL), a logic for reasoning about safety-critical information flow. It formalized actions and knowledge in the way common to Dynamic Epistemic Logic, but also formalized the notion of safe actions and beliefs. Additionally, it formalized a more realistic model of human reasoning, capturing a weaker notion of knowledge than most epistemic logics, and modeled the logical relationship between knowledge and belief. It formalized a realistic notion of rationality. The logic was mechanized in the Coq proof assistant and applied to the case of Air France 447 to validate its usefulness as a formal method for aviation safety.

$\mathbf{Acknowledgements.}$ Seth Ahrenbach was partially supported by NSF CNS 1553548. The author is grateful for the criticism and suggestions provided by anonymous reviewers, and for the very generous assistance from Alwyn Goodloe, Rohit Chadha, and Chris Hathhorn.