Formal analysis of pilot error using agent safety logic

Abstract

Formal methods is the study of applying mathematical and logical techniques to verify and analyze information systems. Not much work has been done in applying formal methods techniques to the human component of information systems. This thesis makes progress on that front. The thesis looks at the specific problem of pilot error in aviation mishaps, and takes it to be a case of the human component of an information system failing. It uses logical and mathematical methods from philosophy and economics to analyze the pilot's decision-making. One such method is a logic for reasoning about knowledge, called epistemic logic, and another is a logic for reasoning about belief, called doxastic logic. Additionally, a logic is introduced for reasoning about the safety of an action. Combining these three logics yields a new logic called Agent Safety Logic. After formally describing the logic, the thesis applies it to a common class of pilot errors. Based on the formal analysis, a common feature of the mishaps emerges, and further logical analysis suggests a general approach to mitigating them. This potential solution is not fully explored, but its discovery validates the use of formal methods techniques in analyzing the human component of an information system.