Hybrid automata-based CEGAR for rectangular hybrid systems

DOI10.1007/s10703-015-0225-4zbMath1341.68109OpenAlexW1967100715MaRDI QIDQ888464

Mahesh Viswanathan, Parasara Sridhar Duggirala, Pavithra Prabhakar, Sayan Mitra

Publication date: 30 October 2015

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-015-0225-4

zbMATH Keywords

hybrid systemabstraction refinementsafety verificationrectangular hybrid automatacounter-example guided abstraction refinement

Mathematics Subject Classification ID

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

Related Items (1)

Using Symmetry Transformations in Equivariant Dynamical Systems for Their Safety Verification

Uses Software

• SPIN
• PHAVer
• HyTech
• RSOLVER
• HSolver
• Bandera
• Bebop
• d/dt
• HARE
• SpaceEx

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• HyTech: A model checker for hybrid systems
• Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems
• Automatic Abstraction Refinement for Timed Automata
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• Lazy abstraction
• Hybrid Systems: Computation and Control
• Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Formal Modeling and Analysis of Timed Systems

This page was built for publication: Hybrid automata-based CEGAR for rectangular hybrid systems