This research concerns quantitative model checking of complex probabilistic models encompassing continuous/discrete dynamics, nondeterminism, and control inputs. Such models are often categorised within a class known as Stochastic Hybrid Systems (SHS), which is recognised as the theoretical underpinning for applications in the Cyber-Physical Systems (CPS) domain. This research works towards formally bridging Verification, Control Theory, and Stochastic Processes.
The computation of quantitative properties and the synthesis of related control architectures optimising properties of interest, is attained via the development of abstraction techniques based on quantitative approximations. This abstraction approach employs methods and concepts from the formal verification area, such as that of (approximate probabilistic) bisimulation, over models and problems known in the field of systems and control. Theory is complemented by algorithms, all packaged software tools that are freely available to users.
Themes: Stochastic Hybrid Systems, Automated Verification, Probabilistic Model Checking
People: Licio Romao, Francesco Cosentino, Yulong Gao, Nathalie Cauchi, Sofie Haesaert, Sadegh Soudjani, Alessandro Abate
Software: StocHy, FAUST2