-A A +A

Verification and Control of Stochastic Processes

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: Francesco Cosentino, Nathalie Cauchi, Sofie Haesaert, Sadegh Soudjani, Alessandro Abate

Software:  StocHy, FAUST2

Publications:

CONTACT US

Oxford Control and Verification (OXCAV) Group

C/O Department of Computer Science

Wolfson Building, Parks Rd, Oxford OX1 3QD

T: +44 (0) 18656 10767

Education - This is a contributing Drupal Theme
Design by WeebPal.