Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces

DOI10.1016/J.SCICO.2011.07.006zbMath1243.68212OpenAlexW2170622387MaRDI QIDQ436418

Stefan Disch, Uwe Waldmann, Christoph Scholl, Willem Hagemann, Werner Damm, Boris Wirtz, Florian Pigorsch, Henning Dierks

Publication date: 20 July 2012

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2011.07.006

zbMATH Keywords

verificationsymbolic representationsredundancy eliminationlinear hybrid automatanon-convex polyhedrasatisfiability modulo theories (SMT)

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (5)

A layered algorithm for quantifier elimination from linear modular constraints ⋮ Crossing the Bridge between Similar Games ⋮ PTIME parametric verification of safety properties for reasonable linear hybrid automata ⋮ Efficient geometric operations on convex polyhedra, with an application to reachability analysis of hybrid systems ⋮ Zone-based verification of timed automata: extrapolations, simulations and what next?

Uses Software

• Unnamed Item
• PHAVer
• HyTech
• CUDD
• CLN
• MathSAT
• d/dt
• LinAIG

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Hybridization methods for the analysis of nonlinear systems
• Symbolic model checking: \(10^{20}\) states and beyond
• HyTech: A model checker for hybrid systems
• Applying Linear Quantifier Elimination
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
• 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
• Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
• Lower bounds for resolution and cutting plane proofs and monotone computations
• 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
• Automated Technology for Verification and Analysis
• An axiomatic basis for computer programming
• The Transitive Reduction of a Directed Graph
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• Formal Techniques for Networked and Distributed Systems - FORTE 2003

This page was built for publication: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces