Abstraction and Counterexample-Guided Construction of ω-Automata for Model Checking of Step-Discrete Linear Hybrid Models

DOI10.1007/978-3-540-73368-3_46zbMath1135.68482OpenAlexW1482183975MaRDI QIDQ5429335

Marc Segelken

Publication date: 29 November 2007

Published in: Computer Aided Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73368-3_46

zbMATH Keywords

model-checkingautomata constructioncounterexample guidanceiterative abstraction refinementstep-discrete hybrid systems

Mathematics Subject Classification ID

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

Related Items

Verification of Hybrid Systems, Hybrid automata-based CEGAR for rectangular hybrid systems, Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space, Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces, Unnamed Item, Refinement of Trace Abstraction

Uses Software

• HyTech