|Adaptive cyber-physical systems rely on the composition and coordinated interaction of different decision-making procedures, each typically realized with specific AI methods. Cyber components capabilities and semantics are usually captured by operational models (such as automata) and modal logics. Physical components and their controllers are instead formalized via dynamical systems of equations, primarily structured by physics laws, or relying on model-free control strategies learned via suitable policy learning. The heterogeneity of these mathematical formalisms makes it difficult to formalize and reason about cross-cutting properties emerging from the interaction of the discrete-event logic used to manage cyber components and the differential equations used to control the physical parts of the system. Such properties involve both functional requirements of the system — what it is supposed to do — and non-functional ones — how reliable, secure, performant, or expensive its operations can be.|
To complete the picture, intrinsic randomness, partial observability, and limited measurability of both the physical environment and the internal state of off-the-shelf software components require means to represent uncertainty and its propagation across all the levels of decision making, with additional challenges in terms of expressiveness and complexity.
This PhD project aims to investigate design and verification techniques at the interface between cyber and physical elements and relevant classes of decision-making procedures their operation involves. In particular, the identification of what information they should share and how the different mathematical abstractions capturing each element’s semantics can be reconciled to allow engineering and learning more effective, runtime-efficient, and secure adaptation decision strategies.