Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
DOI10.1007/978-3-540-71493-4_24zbMATH Open1221.93115OpenAlexW1844911504MaRDI QIDQ3612979FDOQ3612979
Authors: Sumit Kumar Jha, James Weimer, Bruce H. Krogh, Edmund Clarke
Publication date: 11 March 2009
Published in: Hybrid Systems: Computation and Control (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71493-4_24
Recommendations
- d-IRA: A Distributed Reachability Algorithm for Analysis of Linear Hybrid Automata
- Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
- scientific article; zbMATH DE number 2085314
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
- Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
Formal languages and automata (68Q45) Attainable sets, reachability (93B03) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)
Cited In (18)
- Computing bounded ε-reach set with finite precision computations for a class of linear hybrid automata
- Counterexample guided path reduction for static program analysis
- Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement
- Deriving Unbounded Reachability Proof of Linear Hybrid Automata during Bounded Checking Procedure
- Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints
- CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
- Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
- Reachability Problems for Hybrid Automata
- d-IRA: A Distributed Reachability Algorithm for Analysis of Linear Hybrid Automata
- Hybrid automata-based CEGAR for rectangular hybrid systems
- Refinement of Trace Abstraction
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
- Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
- Counterexample-Guided Refinement of Template Polyhedra
- The Discrete Time Behaviour of Restricted Linear Hybrid Automata
- Symbolic analysis of linear hybrid automata -- 25 years later
- Title not available (Why is that?)
- Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
Uses Software
This page was built for publication: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612979)