Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics

By André Platzer. 2010

382 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Computer Networks and Communications, Hardware and Architecture

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Computer Networks and Communications

In Hardware and Architecture

Citations in the corpus

Research Priorities for Robust and Beneficial Artificial Intelligence (2015, background): “Work in adaptive control theory [31], the theory of so-called cyberphysical systems [32], and veriﬁcation of hybrid or robotic systems [33, 34] is highly relevant but also faces the same diﬃculties.”
Cyber–Physical Systems: A Perspective at the Centennial (2012, methodology): “A more general modeling framework for CPSs is hybrid automaton (HA), which can be used to model complex dynamics of CPSs through various mathematical formalisms [93]–[98] that can capture both the transition between discrete states and also the evolution of continuous states over time.”
Differential Privacy Techniques for Cyber Physical Systems: A Survey (2018, background): “complex dynamic nature of CPSs via several mathematical and computational formalisms [131], [132].”
Formal verification of hybrid systems (2011, methodology): “The tool KeYmaera offers support to prove correctness of hybrid systems using deductive verification [43,44].”
Flow*: An Analyzer for Non-linear Hybrid Systems (2013, methodology): “A few notable non-linear analysis tools include KeYmaera [8], Ariadne [9] and HySAT/iSAT [10].”
Practical verification of decision-making in agent-based autonomous systems (2013, neutral): “Platzer has developed a theorem proving approach for verifying hybrid automata which is implemented in theKeYmaera system (Platzer 2010).”
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System (2015, methodology): “We model our system using Differential Dynamic Logic dL [17,18,19], a logic for reasoning about hybrid programs.”