file.pdf (200.29 kB)
Combining Deduction and Algebraic Constraints for Hybrid System Analysis
journal contribution
posted on 2006-07-01, 00:00 authored by Andre PlatzerWe show how theorem proving and methods for handling real algebraic
constraints can be combined for hybrid system verification. In particular, we highlight
the interaction of deductive and algebraic reasoning that is used for handling the joint
discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur
when verifying scenarios with cooperative traffic agents. From the experience with
these examples, we analyse proof strategies for dealing with the practical challenges for
integrated algebraic and deductive verification of hybrid systems, and we propose an
iterative background closure strategy.