Efficient reachability analysis and refinement checking of timed automata using BDDs

DOI10.1007/3-540-44798-9_6MaRDI QIDQ4787215zbMATH OpenFDO

Authors D. Beyer

Publication date 9 January 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2144/21440086

zbMATH Keywords

formal verificationreal-time systemstimed automata

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Improvements in BDD-based reachability analysis of timed automata
• Efficient verification of timed automata with BDD-like data-structures
• Bounded model checking for timed automata
• Improved BDD-based discrete analysis of timed systems
• scientific article; zbMATH DE number 5024617
• Bounded Model Checking for Parametric Timed Automata
• Bounded model checking for timed systems
• scientific article; zbMATH DE number 7297846
• The power of reachability testing for timed automata

Cited in

(6)

• Improvements in BDD-based reachability analysis of timed automata
• Improvement of a reachability analysis algorithm for real-time systems
• Improvements for the Symbolic Verification of Timed Automata
• Efficient verification of timed automata with BDD-like data-structures
• Improved BDD-based discrete analysis of timed systems
• Formal Modeling and Analysis of Timed Systems

Describes a project that uses

Uses Software

• Kronos
• Uppaal
• Rabbit

This page was built for publication: Efficient reachability analysis and refinement checking of timed automata using BDDs

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