Seite - 382 - in Intelligent Environments 2019 - Workshop Proceedings of the 15th International Conference on Intelligent Environments

The LEADSTO format is defined as follows: let and be predicates, and be non-negative real numbers. Then means: If predicate holds for a certain time interval with duration , then after some delay (between and ) predicate will hold for a certain time interval of length . An example of a dynamic property in the LEADSTO format is where represents the predicate Communication_from_to(external_world, AE, observe, leak) and represents the predicate Communication_from_to(AE,SS,inform,pump_change_required). This property expresses the fact that, if the airport engineer AE observes that there is a hydraulic leak during 1 time unit, then after a delay between 0.25 and 1 time unit, AE will inform the station supervisor SS about the problem during 1.5 time units. By executing this rule, a trace of predicates holding true or false can be generated and visualized. The time units in this case study are in minutes. For the temporal parameters, the following assumptions were made: Solving an aircraft/crew problem takes 8 minutes; synchronization between IT systems takes 0.1 minutes following an update; an observation-belief-action cycle takes 1.5 minutes. These assumptions were based on observations made at two AOC centres in Europe. 4. Model Verification For the identified policies P1-P4, it is important to ensure that some required dynamic properties hold. Such properties may for example represent system requirements, desired performance characteristics, absence of deadlocks and other forbidden states. To verify the identified policies in the context of the case study, automated model verification tools can be used, such as TTL Checker [17]. The dynamic properties in TTL Checker need to be specified in Temporal Trace Language (TTL) [18]. LEADSTO is an executable sublanguage of TTL. TTL is also a variant of order-sorted predicate logic with the possibility to specify and reason about time. By using TTL Checker, dynamic properties in TTL could be checked automatically on simulation traces automatically generated by LEADSTO software based on agent-based model specifications. • Policy P1 - Property 1: If the Station Supervisor (SS) believes that there is a mechanical failure, then within 5 minutes the Airline Operations Supervisor (AOS) also believes there is a mechanical failure. Formally: ∀t at(Belief(SS, Disruption(mechanical_failure, LHB, CDG)),t) & ∃t’ ∃c:MSG_TYPE t’<t & at(Communicate_from_to(AE, SS, c, Disruption(mechanical_failure, LHB, CDG)), t’) ⇒ ∃t’’ t’’ > t & t’’ ≤ t+10 & at(Observation (CCo, Disruption(mechanical_failure, LHB, CDG)), t’’) It is important for this property to hold because under policy P1, AOS must accept maintenance information content and act on it without challenging the information. • Policy P1 - Property 2: If SS believes that maintenance information reported to him by the Airport Engineer (AE) is true, then this information should be noticed by the Crew Controller (CCo) within 10 minutes. Formally: ∀t ∀x:AIRCRAFT ∀y:AIRPORT at(Belief(SS, Disruption(mechanical_failure, x, y)),t) ⇒ ∃t’ t’ > t & t’ ≤ t+5 & at(Belief(AOS, Disruption(mechanical_failure, x, y)),t’) S.Bouarfaetal. /AMulti-AgentNegotiationApproach forAirlineOperationControl382