Differential logic for reasoning about hybrid systems

We propose a first-order dynamic logic for reasoning
about hybrid systems. As a uniform model for discrete
and continuous evolutions in hybrid systems, we
introduce hybrid programs with differential actions.
Our logic can be used to specify and verify correctness
statements about hybrid programs, which are suitable
for symbolic processing by calculus rules. Using
first-order variables, our logic supports systems with
symbolic parameters. With dynamic modalities, it is
prepared to handle multiple system components.

@inproceedings{DBLP:conf/hybrid/Platzer07,
	pdf = {pub/dL-short.pdf},
	author = {['André Platzer']},
	title = {Differential Logic for Reasoning about
               Hybrid Systems},
	booktitle = {HSCC},
	longbooktitle = {Hybrid Systems: Computation and Control,
               10th International Conference, HSCC 2007,
               Pisa, Italy, Proceedings},
	year = {2007},
	pages = {746-749},
	doi = {10.1007/978-3-540-71493-4_75},
	editor = {['Alberto Bemporad', 'Antonio Bicchi', 'Giorgio Buttazzo']},
	publisher = {Springer},
	series = {LNCS},
	volume = {4416},
	isbn = {978-3-540-71492-7},
	keywords = {dynamic logic, hybrid systems, parametric
               verification},
	abstract = {
    We propose a first-order dynamic logic for reasoning
    about hybrid systems. As a uniform model for discrete
    and continuous evolutions in hybrid systems, we
    introduce hybrid programs with differential actions.
    Our logic can be used to specify and verify correctness
    statements about hybrid programs, which are suitable
    for symbolic processing by calculus rules. Using
    first-order variables, our logic supports systems with
    symbolic parameters. With dynamic modalities, it is
    prepared to handle multiple system components.}
}