In complexity science a property or behaviour of a system is called emergent if it is not a property or behaviour of the constituting elements of the system, though results from the interactions between its constituting elements. In the socio-technical air transportation system these interactions are between human operators, technical systems and procedures, at airlines, airports and air traffic centres. Safety is a clear example of an emergent property of the complex socio-technical air transportation system: it is not a property of any constituting element, though results from the interactions between the constituting elements. Safety as well as other emergent properties and behaviours of the current air transportation system are results from decades of evolutionary development and improvement. For example, each commerical aviation accident is well investigated, the findings of which often leads to various kinds of improvements regarding elements of the air transportation system. Aviation statistics show that the factual result has been a steady increase of air traffic in combination with a steady improvement of safety, e.g. (Roelen & Blom, 2013). Therefore, one may conclude: current aviation works thanks to the implicit use of emergent behaviour. @en

Two formal stochastic models are said to be bisimilar if their solutions as a stochastic process are probabilistically equivalent. Bisimilarity between two stochastic model formalisms means that the strengths of one stochastic model formalism can be used by the other stochastic model formalism.
The aim of this paper is to explain bisimilarity relations between stochastic hybrid automata, stochastic differential equations on hybrid space and stochastic hybrid Petri nets. These bisimilarity relations make it possible to combine the formal verification power of automata with the analysis power of
stochastic differential equations and the compositional specification power of Petri nets. The relations and their combined strengths are illustrated for an air traffic example.@en

The high volume of air traffic over Europe is expected to double within the next 15 years. This requires changes in the airspace structure and in the organisation of air transport operations that involve multiple stakeholders. Changes, by regulation, require a sufficient safety validation, in order to show that the changed situation is safe and will remain safe during an applicable period. Many methods and techniques exist that can be used to support such safety validation process. However, for air transport operations, the stakeholders involved are numerous and diverse, and there are no guidelines on how to address their roles, responsibilities and goals during development and validation.
This paper develops a safety validation framework that emphasises the active roles and collaboration of multiple stakeholders during the development phases of air transport operations. The framework is developed in three steps: First, established validation views from literature are identified and analysed
to reveal open issues when it comes to their use for multi-stakeholder changes in air transport operations. Next, validation views emerging beyond the established ones are identified, and evaluated on whether they address the open issues. Finally, the strong points of established and emerging views are
combined into a novel framework.@en

With jump linear quadratic Gaussian (JLQG) control, one refers to the control under a quadratic performance criterion of a linear Gaussian system, the coefficients of which are completely observable, while they are jumping according to a finite-state Markov process. With adaptive JLQG, one refers to the more complicated situation that the finite-state process is only partially observable. Although many practically applicable results have been developed, JLQG and adaptive JLQG control are lagging behind those for linear quadratic Gaussian (LQG) and adaptive LQG. The aim of this paper is to help improve the situation by introducing an exact transformation which embeds adaptive JLQG control into LQM (linear quadratic Martingale) control with a Completely observable stochastic control matrix. By LQM control, we mean the control of a martingale driven linear system under a quadratic performance criterion. With the LQM transformation, the adaptive JLQG control can be studied within the framework of robust or minimax control without the need for the usual approach of averaging or approximating the adaptive JLQG dynamics. To show the effectiveness of our transformation, it is used to characterize the open-loop-optimal feedback (OLOF) policy for adaptive JLQG control.@en