Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming

DOI10.1016/J.ENTCS.2006.12.023MaRDI QIDQ2864385zbMATH OpenOpenAlexFDO

Authors Xuandong Li, Sumit Jha Aanand, Lei Bu

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.12.023

zbMATH Keywords

linear programmingreachability analysisbounded model checkinglinear hybrid automata

Mathematics Subject Classification ID

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

Recommendations

• SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
• Path-oriented reachability verification of a class of nonlinear hybrid automata using convex programming
• Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• scientific article; zbMATH DE number 2085314

Cites work

• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• Algorithmic analysis of nonlinear hybrid systems
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• HyTech: A model checker for hybrid systems
• Hybrid Systems: Computation and Control
• Positive loop-closed automata: A decidable class of hybrid systems
• The algorithmic analysis of hybrid systems
• Verifying industrial hybrid systems with \textsc{MathSAT}
• What's decidable about hybrid automata?

Cited in

(5)

• Rigorous simulation-based analysis of linear hybrid systems
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
• Path-oriented reachability verification of a class of nonlinear hybrid automata using convex programming
• Symbolic Reachability Analysis of Lazy Linear Hybrid Automata

Describes a project that uses

Uses Software

• MathSAT
• HyTech
• PHAVer

This page was built for publication: Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming

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