The complete proof theory of hybrid systems

Hybrid systems are a fusion of continuous dynamical
systems and discrete dynamical systems. They freely
combine dynamical features from both worlds. For that
reason, it has often been claimed that hybrid systems
are more challenging than continuous dynamical systems
and than discrete systems. We now show that,
proof-theoretically, this is not the case. We present a
complete proof-theoretical alignment that interreduces
the discrete dynamics and the continuous dynamics of
hybrid systems. We give a sound and complete
axiomatization of hybrid systems relative to continuous
dynamical systems and a sound and complete
axiomatization of hybrid systems relative to discrete
dynamical systems. Thanks to our axiomatization,
proving properties of hybrid systems is exactly the
same as proving properties of continuous dynamical
systems and again, exactly the same as proving
properties of discrete dynamical systems. This
fundamental cornerstone sheds light on the nature of
hybridness and enables flexible and provably perfect
combinations of discrete reasoning with continuous
reasoning that lift to all aspects of hybrid systems
and their fragments.

@inproceedings{DBLP:conf/lics/Platzer12b,
	pdf = {pub/completealign.pdf},
	slides = {pub/completealign-slides.pdf},
	TR = {DBLP:conf/lics/Platzer12b:TR},
	author = {['André Platzer']},
	title = {The Complete Proof Theory of
               Hybrid Systems},
	booktitle = {LICS},
	year = {2012},
	pages = {541-550},
	doi = {10.1109/LICS.2012.64},
	longbooktitle = {Proceedings of the 27th Annual ACM/IEEE
               Symposium on Logic in Computer Science, LICS
               2012, Dubrovnik, Croatia, June 25???28, 2012},
	publisher = {IEEE},
	isbn = {978-1-4673-2263-8},
	keywords = {proof theory, hybrid dynamical systems,
               differential dynamic logic, axiomatization,
               completeness},
	abstract = {
    Hybrid systems are a fusion of continuous dynamical
    systems and discrete dynamical systems. They freely
    combine dynamical features from both worlds. For that
    reason, it has often been claimed that hybrid systems
    are more challenging than continuous dynamical systems
    and than discrete systems. We now show that,
    proof-theoretically, this is not the case. We present a
    complete proof-theoretical alignment that interreduces
    the discrete dynamics and the continuous dynamics of
    hybrid systems. We give a sound and complete
    axiomatization of hybrid systems relative to continuous
    dynamical systems and a sound and complete
    axiomatization of hybrid systems relative to discrete
    dynamical systems. Thanks to our axiomatization,
    proving properties of hybrid systems is exactly the
    same as proving properties of continuous dynamical
    systems and again, exactly the same as proving
    properties of discrete dynamical systems. This
    fundamental cornerstone sheds light on the nature of
    hybridness and enables flexible and provably perfect
    combinations of discrete reasoning with continuous
    reasoning that lift to all aspects of hybrid systems
    and their fragments.}
}