Symbolic Reachability Analysis of Lazy Linear Hybrid Automata

DOI10.1007/978-3-540-75454-1_18MaRDI QIDQ3510848zbMATH OpenOpenAlexFDO

Authors Susmit Jha, Bryan A. Brady, Sanjit A. Seshia

Publication date 3 July 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75454-1_18

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Recommendations

• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• scientific article; zbMATH DE number 2085314
• The algorithmic analysis of hybrid systems
• 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

(17)

• Time-triggered conversion of guards for reachability analysis of hybrid automata
• PTIME parametric verification of safety properties for reasonable linear hybrid automata
• Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
• Symbolic-numeric reachability analysis of closed-loop control software
• Rigorous simulation-based analysis of linear hybrid systems
• Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
• Symbolic reachability analysis of multirate hybrid systems
• Towards Component Based Design of Hybrid Systems: Safety and Stability
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
• SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
• Quantifier-free encoding of invariants for hybrid systems
• Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement
• Non-convex invariants and urgency conditions on linear hybrid automata
• Hybrid Systems: Computation and Control
• Symbolic analysis of linear hybrid automata -- 25 years later
• HAT: analyzing linear hybrid automata as labelled transition system

Describes a project that uses

Uses Software

• PHAVer

This page was built for publication: Symbolic Reachability Analysis of Lazy Linear Hybrid Automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3510848)