PHAVer: algorithmic verification of hybrid systems past HyTech

By Goran Frehse. International Journal on Software Tools for Technology Transfer (STTT), 2005

801 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/1f60c13f242fa6c9236dbee8cb6f6789c5ecdd65

How researchers see this paper

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

In Artificial Intelligence

1. Matthias Althoff
2. Jan-David Quesel
3. Daniele Magazzeni
4. Martin Buss
5. Olaf Stursberg
6. Michael Fisher
7. Alexei P. Lisitsa
8. Murray Campbell

In Computational Theory and Mathematics

1. Kyoung-Dae Kim
2. P. Arun Raj Kumar
3. Jan-David Quesel
4. Daniele Magazzeni
5. Matthias Althoff
6. Michael Fisher
7. Alexei P. Lisitsa
8. Sandor M. Veres

In Software

1. Michael Fisher
2. Alexei P. Lisitsa
3. Sandor M. Veres
4. Richard M. Murray
5. Sergiy Bogomolov
6. Magnus Egerstedt
7. Daniele Magazzeni
8. Youakim Badr

Citations in the corpus

• Autonomous driving in urban environments: approaches, lessons and challenges (2010, background): “New techniques in hybrid systems (Frehse 2008), model checking (Lamport 2002; Holzmann 2003) and stability certificates (Parrilo 2003) provide promising directions for future research.”
• Planning as Model Checking in Hybrid Domains (2014, methodology): “In the last years, powerful model checking techniques and tools based on, e. g., SMT (Cimatti et al. 2000) and symbolic search (Frehse 2008; Frehse et al. 2011), have been developed for this formalism.”
• Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization (2008, background): “in [13], [14] which has been advanced in [15] using on-the-fly partitioning.”
• Cyber–Physical Systems: A Perspective at the Centennial (2012, methodology): “Some examples are UPPAAL [118], a verification tool for real-time systems based on timed automata, HyTech [99] and PHAVer [119] for LHA, SpaceEx [120], which is based on the LeGuernic–Girard (LGG) algorithm [121] that can efficiently handle HAs with linear differential equations with a larger number”
• Practical verification of decision-making in agent-based autonomous systems (2013, methodology): “PHAVer (Frehse 2005) is a model-checking system for linear hybrid automata that uses assume-guarantee style reasoning to allow the model checking to be approached in a compositional fashion (Frehse et al.”
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) (2008, background): “Model checkers [7, 5] verify correctness properties by exploring the state space exhaustively, which provides a good mechanism to find bugs or concrete counterexamples for specifications.”
• Internet of Medical Things: A Review of Recent Contributions Dealing With Cyber-Physical Systems in Medicine (2018, positive): “To perform verification of IoMT models, several tools and algorithms were developed for hybrid state machine models [32], [35] or for Petri net derived models [34].”
• Reachability Analysis and its Application to the Safety Assessment of Autonomous Cars (2010, methodology): “Abstractions for general hybrid automata to linear hybrid automata have been developed in [64].”
• Differential Dynamic Logic for Hybrid Systems (2008, background): “Beyond standard approaches [3, 29, 36] for linear systems with constant dynamics, Lafferriere et al.”