Modeling And Error Analysis For Controller’s Response Execution Based On Temporal Logic

Controller response execution plays an important role in air traffic control. Many incidents have relation to controller response execution faults. This paper intends to offer a formal reasoning method based on temporal logic in hoping to realize the dynamic analysis of incident’s process, improve automation analysis of unsafe incidents and overcome shortcomings of natural language description.Materials concerning research status of temporal logic both at home and abroad are learned first. then, some characteristics of the predicate-logical Temporal Trace Language are summarized. Meanwhile, the theoretical basis of Agent and characteristics of Multi-Agent system are also introduced. Based on these theories, the method of formal modeling on Multi-Agent system are proposed. The human information processing model proposed by Wickens is referenced, with certain factors of control operation, Multi-Agent system model is constructed according to the interactive features of scenario.Secondly, From the perspective of temporal logic, formal model and simulation model are built based on the response execution scenario model. First, the static concept related to the scenario are collected, and then the dynamic relationship between attribute elements are also abstracted, then formalized concept, relationship and attribute according to the specification of TTL. Finally, language structure characteristics, semantics, and syntax of LEADSTO are gived, and the concrete steps of the modeling and simulation are expounded.Taking a typical controller response execution scenario in runway incursion incidents as an example to establish the temporal logic model. In order to perform formal analysis, we have constructed the formal rule properties with certain interlevel relations at different aggregation levels in the runway incursion scenario. Moreover, this paper has developed simulation models in a declarative manner and realized the dynamic simulation of a real incident case. And then, we have taken the simulation traces and formal rule properties as inputs, the potential hazards are automatically identified by the formal reasoning and verification. Finally, the different sets of properties are changed for comparison analysis, it enables the analyst to explore the effective measures to prevent the errors and incidents. The results show that this method has benefit on dynamic simulation and formal analysis by predicate-logical language to overcome shortcomings of natural language description. It is also provides a scientific guidance for the subsequent analysis of such incidents.