Page - 383 - in Intelligent Environments 2019 - Workshop Proceedings of the 15th International Conference on Intelligent Environments

It is important that this property holds to ensure proper synchronization between the Aircraft Movement System (used by the SS) the Crew Tracking System (monitored by the CCo). • Policy P2 - Property 1: If SS believes that there is a mechanical failure, then AOS should call the AE within 5 minutes the to verify the information. Formally: ∀t ∀x:AIRCRAFT ∀y:AIRPORT at(Belief(SS, Disruption(mechanical_failure, x, y)),t) ⇒ ∃t’ t’ > t & t’ ≤ t+5 & at(Communicate_from_to(AOS, AE, ask, Check_disruption(mechanical_failure, x, y)), t’) It is important for this property to hold because under policy P2, the AOS must challenge information about a maitnenance situation, and query the information source. • Policy P2 - Property 2: if CCO believes there is a crew problem, then, within 2 minutes, CCO should ask the Flight Crew (FC) to extend their crew duty time. Formally: ∀t ∀x:CREW_PROBLEM at(Belief(CCO, Crew_problem(x)),t) ⇒ ∃t’ t’ > t & t’ ≤ t+2 & at(Communicate_from_to(CCO, FC, ask, extend_crew_hours), t’) It is important for this property to hold because under policy P2, when the CCo is facing with a crew problem, he must challenge crew limits and seek extensions to crew duty time, for instance through negotiating with the Flight Crew (FC). • Policy P3 - Property 1: If SS believes that there is a mechanical failure, then within 5 minutes, AOS should organize a conference call with AE and Maintenance Watch Engineer to recheck information. Formally: ∀t ∀x:AIRCRAFT ∀y:AIRPORT at(Belief(SS, Disruption(mechanical_failure, x, y)),t) ⇒ ∃t’ t’ > t & t’ ≤ t+5 & at(Start_conf_call(AOS, Disruption(mechanical_failure, x, y), AE, MWE), t’) It is important for this property to hold because under policy P3, the AOS must seek alternative information and recheck information source and reliability, e.g., through seeking a second opinion from the MWE. • Policy P3 - Property 2: if MWE believes there is a mechanical failure, then within 5 minutes, the CCo should notice the aircraft solution on the CTS. Formally: ∀t ∀x:AIRCRAFT ∀y:AIRPORT at(Belief(MWE, Disruption(mechanical_failure, x, y)),t) ⇒ ∃t’ t’ > t & t’ ≤ t+5 & ∃s:AIRCRAFT_SOLUTION at(Observation(CCo, Aircraft_problem(s))), t’) This property is checked to verify a proper synchronization between the CTS (monitored by the CCo) and the AMS (used by the ACo). After hearing the confirmation from MWE in the conference call, the ACo directly reports the aircraft solution through AMS. • Policy P4 - Property 1: Before announcing an integrated disruption management solution to ACo and CCo, the AOS should have noticed the solutions to the aircraft problem and crew problem reported on the AMS by the ACo and CCo respectively. Formally: S.Bouarfaetal. /AMulti-AgentNegotiationApproach forAirlineOperationControl 383