Bisimulation conversion and verification procedure for goal-based control systems

DOI10.1007/s10703-010-0109-6zbMath1213.93139OpenAlexW1969290144WikidataQ59813961 ScholiaQ59813961MaRDI QIDQ633304

Julia M. B. Braman, Richard M. Murray

Publication date: 31 March 2011

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

Full work available at URL: https://doi.org/10.1007/s10703-010-0109-6

zbMATH Keywords

verificationhybrid systemsmodel checkingfault-tolerant control

Mathematics Subject Classification ID

Automated systems (robots, etc.) in control theory (93C85)

Uses Software

• SPIN
• PVS
• PHAVer
• HyTech
• NuSMV
• Uppaal
• MATISSE
• Bebop

Cites Work

• Symbolic model checking: \(10^{20}\) states and beyond
• HyTech: A model checker for hybrid systems
• Uppaal in a nutshell
• Approximate bisimulation relations for constrained linear systems
• Bisimilar control affine systems
• Bisimulation relations for dynamical, control, and hybrid systems
• Dynamic partial-order reduction for model checking software
• Hybrid Systems: Computation and Control
• Unnamed Item
• Unnamed Item
• Unnamed Item