192
J. Kolˇ c´ ak et al.
with unprecedented degrees of automation; ensuring the safety and reliability of
these automated driving systems is a pressing social and economic challenge.
The hybridity of cyber-physical systems, the combination of continuous physical dynamics and discrete digital control, poses unique scientific challenges. To
address these challenges, two communities have naturally joined forces: control
theory whose traditional application domain is continuous dynamics and formal
methods that have mainly focused on the analysis of software systems. This has
been a fruitful cross-pollination: techniques from formal methods such as bisimilarity [9] and temporal logic specification [8] have been imported to control
theory, and conversely, control theory notions such as Lyapunov functions have
been used in formal methods [26].
Deductive Verification of Hybrid Systems In the formal methods community, two major classes of techniques are model checking (usually automatabased and automatic) and deductive verification (based on logic and can be
automated or interactive). Model checking techniques rely on exhaustive search
in state spaces and therefore cannot be applied per se to hybrid systems with
infinite state spaces. This has led to the active study of discrete abstraction of
hybrid dynamics, see e.g. [9]; or of bounded model checking, see [5].
In contrast, nothing immediately rules out the use of the deductive approach
for hybrid systems. Finitely many variables in logical formulas can represent
infinitely many states, and proofs in suitably designed logics are valid even when
the semantic domain is uncountable. That said, designing such a logic, proving
the soundness of its rules, and showing that logics is actually useful in hybrid
system verification is a difficult task.
Platzer’s differential dynamic logic dL [21] is a remarkable success in this direction. Its syntax is systematic and intuitive, extending the classic formalism of
dynamic logic [10] with differential equations as programs. Its proof rules encapsulate several essential proof principles about differential equations, including a
differential invariant (DI) rule for universal properties and side deduction for
existential properties. The logic dL has served as a general platform that accommodates a variety of techniques, including those which come from real algebraic
geometry [22]. Furthermore, dL comes with sophisticated tool support: the latest
tool KeYmaera X [15] comes with graphical interface for interactive proving
and a number of automation heuristics.
Relational Reasoning on Hybrid Systems In this work, we introduce
proof-based techniques for relational reasoning to the deductive verification of
hybrid systems. Here, by relational reasoning we mean analyzing how changes in
the system will affect the overall system behavior. One of the applications of such
reasoning in our mind is to deduce the safety of a system by checking the most
aggressive settings. To make such reduction sound, we need to verify that less
aggressive versions result in less dangerous outcomes than the aggressive ones.
As a simple example, consider the following case distilled from our collaboration
with an industrial partner.
Example 1 (leading example: collision speed). Consider two cars C and
C, whose positions and velocities are real numbers denoted by x, x and v, v,
J. Kolˇ c´ ak et al.
with unprecedented degrees of automation; ensuring the safety and reliability of
these automated driving systems is a pressing social and economic challenge.
The hybridity of cyber-physical systems, the combination of continuous physical dynamics and discrete digital control, poses unique scientific challenges. To
address these challenges, two communities have naturally joined forces: control
theory whose traditional application domain is continuous dynamics and formal
methods that have mainly focused on the analysis of software systems. This has
been a fruitful cross-pollination: techniques from formal methods such as bisimilarity [9] and temporal logic specification [8] have been imported to control
theory, and conversely, control theory notions such as Lyapunov functions have
been used in formal methods [26].
Deductive Verification of Hybrid Systems In the formal methods community, two major classes of techniques are model checking (usually automatabased and automatic) and deductive verification (based on logic and can be
automated or interactive). Model checking techniques rely on exhaustive search
in state spaces and therefore cannot be applied per se to hybrid systems with
infinite state spaces. This has led to the active study of discrete abstraction of
hybrid dynamics, see e.g. [9]; or of bounded model checking, see [5].
In contrast, nothing immediately rules out the use of the deductive approach
for hybrid systems. Finitely many variables in logical formulas can represent
infinitely many states, and proofs in suitably designed logics are valid even when
the semantic domain is uncountable. That said, designing such a logic, proving
the soundness of its rules, and showing that logics is actually useful in hybrid
system verification is a difficult task.
Platzer’s differential dynamic logic dL [21] is a remarkable success in this direction. Its syntax is systematic and intuitive, extending the classic formalism of
dynamic logic [10] with differential equations as programs. Its proof rules encapsulate several essential proof principles about differential equations, including a
differential invariant (DI) rule for universal properties and side deduction for
existential properties. The logic dL has served as a general platform that accommodates a variety of techniques, including those which come from real algebraic
geometry [22]. Furthermore, dL comes with sophisticated tool support: the latest
tool KeYmaera X [15] comes with graphical interface for interactive proving
and a number of automation heuristics.
Relational Reasoning on Hybrid Systems In this work, we introduce
proof-based techniques for relational reasoning to the deductive verification of
hybrid systems. Here, by relational reasoning we mean analyzing how changes in
the system will affect the overall system behavior. One of the applications of such
reasoning in our mind is to deduce the safety of a system by checking the most
aggressive settings. To make such reduction sound, we need to verify that less
aggressive versions result in less dangerous outcomes than the aggressive ones.
As a simple example, consider the following case distilled from our collaboration
with an industrial partner.
Example 1 (leading example: collision speed). Consider two cars C and
C, whose positions and velocities are real numbers denoted by x, x and v, v,