Analysis and Verification of Stochastic Hybrid Systems
|Project members:||Dr.ir. A. Abate (Alessandro)|
|Keywords:||Discrete-event systems, Probabilistic models, Analysis, verification, and control, Hybrid and nonlinear systems|
Stochastic Hybrid Systems (SHS) are dynamical models that are employed to characterize the probabilistic evolution of systems with interleaved and interacting continuous and discrete components.
The formal analysis, verification, and optimal control of SHS models represent relevant goals because of their theoretical generality and for their applicability to a wealth of studies in the Sciences and in Engineering.
Indeed in a number of practical instances the presence of a discrete number of continuously operating modes (e.g., in fault-tolerant industrial systems), the effect of uncertainty (e.g., in safety-critical air-traffic systems), or both occurrences (e.g., in models of biological entities) advocate the use of a mathematical framework, such as that of SHS, which is structurally predisposed to model such heterogeneous systems.
In this project, we plan to investigate and develop innovative analysis and verification techniques that are directly applicable to general SHS models, while being computationally scalable.
The first stage of the study entails mostly analytical work: the project aims at generating results that are both theoretically formal and computationally attractive.
It will furthermore develop dedicated software for the analysis of SHS.
The theoretical and computational outcomes will be tested in or applied to a number of studies, in particular to models drawn from Biology.
This latter stage will thus involve the collaboration with researchers from the Computer Science or the cooperation with experimentalists from the Life Sciences.