Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space

DOI10.1007/978-3-540-75596-8_30zbMath1141.68461OpenAlexW2121909093MaRDI QIDQ3510811

Jun Pang, Stefan Disch, Uwe Waldmann, Christoph Scholl, Hardi Hungar, Werner Damm, Boris Wirtz, Florian Pigorsch, Swen Jacobs

Publication date: 3 July 2008

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-75596-8_30

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Related Items

Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces, Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints, Don't care words with an application to the automata-based approach for real addition, Can we build it: formal synthesis of control strategies for cooperative driver assistance systems

Uses Software

• HySAT
• HyTech
• d/dt

Cites Work

• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Hybridization methods for the analysis of nonlinear systems
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• HyTech: A model checker for hybrid systems
• Applying Linear Quantifier Elimination
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
• Automatic Verification of Hybrid Systems with Large Discrete State Space
• The Image Computation Problem in Hybrid Systems Model Checking
• Approximation Metrics for Discrete and Continuous Systems
• Hybrid Systems: Computation and Control
• Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models
• An axiomatic basis for computer programming
• Hybrid Systems: Computation and Control
• The Power of Hybrid Acceleration