Logic for Hybrid Systems

Overview

I work in the area of hybrid system verification. My primary interest is to use methods from logic for verifying hybrid systems.

The behaviour of safety-critical systems typically depends on both the state of a discrete controller and continuous physical quantities. Hybrid systems are mathematical models for dynamic systems with interacting discrete and continuous behaviour. Their behaviour combines continuous evolution (called flow) characterised by differential equations and discrete jumps.

Hybrid systems are a fascinating area of research. Verification methods for hybrid systems involve a large variety of techniques from several areas of mathematics, computer science, and electrical engineering. The challenges imposed by their combined discrete and continuous behaviour require quite interesting combinations of "solution" methods from those areas. For example, techniques from the following areas can be used:

logic, theorem proving, model checking, computer algebra, theory of differential equations, differential algebra, model theory, approximation theory.

For verifying hybrid systems, I have developed a famliy of logics and proof calculi, including the differential dynamic logic (dL). There also is a verification tool implementation of dL in a theorem prover, which is called KeYmaera.