Formal Verification and Learning of Complex Systems - Professor Alessandro Abate

Explore formal verification techniques for complex systems in this 43-minute lecture by Professor Alessandro Abate at the Alan Turing Institute. Delve into innovative approaches that combine model-based and data-driven methods to address limitations in standard formal verification techniques. Learn about a new measurement-driven and model-based automated technique for quantitative verification of systems with partly unknown dynamics, formulated as a data-driven Bayesian inference problem. Discover the concept of 'Logically Constrained Reinforcement Learning' for learning actions in a model while verifying logical constraints. Gain insights into applications for complex physical systems, including Cyber-Physical Systems (CPS) and building automation systems. Explore topics such as parametric Markov chains, parameter synthesis, confidence computation, and strategy synthesis for experiment design. Understand how this research pushes the boundaries of existing algorithms and tools in formal verification, offering potential solutions for large-scale, complex models.

Intro
Automated formal verification successes and frontiers
Automated formal verification pushing the envelope
Building automation systems an exemplar of CPS
Building automation systems - a CPS exemplar
Building automation systems - problem setup
Learning and verification state of art and objective
Overview of method
Parametric Markov chains
Parameter synthesis
Bayesian inference
Confidence computation
Case study experiments
Dual role of actions in MDP
Strategy Synthesis for experiment design
Case study setup
Extensions to other model classes
Applications of method