Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction

DOI10.1007/978-3-540-71493-4_24MaRDI QIDQ3612979zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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)

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

Cited in

(18)

• Computing bounded ε-reach set with finite precision computations for a class of linear hybrid automata
• Hybrid automata-based CEGAR for rectangular hybrid systems
• d-IRA: A Distributed Reachability Algorithm for Analysis of Linear Hybrid Automata
• Symbolic analysis of linear hybrid automata -- 25 years later
• scientific article; zbMATH DE number 1301612 (Why is no real title available?)
• CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
• Time-Bounded Reachability for Initialized Hybrid Automata with Linear Differential Inclusions and Rectangular Constraints
• The Discrete Time Behaviour of Restricted Linear Hybrid Automata
• Refinement of Trace Abstraction
• Counterexample guided path reduction for static program analysis
• Deriving Unbounded Reachability Proof of Linear Hybrid Automata during Bounded Checking Procedure
• Reachability Problems for Hybrid Automata
• Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
• Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
• Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
• Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement
• SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
• Counterexample-Guided Refinement of Template Polyhedra

Describes a project that uses

Uses Software

• HyTech

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)