Efficient timed reachability analysis using clock difference diagrams

DOI10.1007/3-540-48683-6_30MaRDI QIDQ4818802zbMATH OpenFDO

Authors Gerd Behrmann, Justin Pearson, Carsten Weise, Wang Yi, Kim G. Larsen

Publication date 24 September 2004

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

Full work available at URL https://doi.org/10.1007/3-540-48683-6_30

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1400094
• Can decision diagrams overcome state space explosion in real-time verification?
• Compact data structures and state-space reduction for model-checking real-time systems
• scientific article; zbMATH DE number 1324667
• Difference decision diagrams

Cited in

(21)

• Compact data structures and state-space reduction for model-checking real-time systems
• Zero, successor and equality in BDDs
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Superposition as a decision procedure for timed automata
• A partial order semantics approach to the clock explosion problem of timed automata
• Towards deriving test sequences by model checking
• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• Model Checking Real-Time Systems
• Improvements for the Symbolic Verification of Timed Automata
• Hierarchical Set Decision Diagrams and Regular Models
• scientific article; zbMATH DE number 139824 (Why is no real title available?)
• Efficient verification of timed automata with BDD-like data-structures
• Unification \& sharing in timed automata verification
• Reachability analysis for timed automata using max-plus algebra
• scientific article; zbMATH DE number 1400094 (Why is no real title available?)
• Difference decision diagrams
• To store or not to store.
• Can decision diagrams overcome state space explosion in real-time verification?
• Operations on timed scenarios
• Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
• On the existence of unions of timed scenarios

Describes a project that uses

Uses Software

• Uppaal

This page was built for publication: Efficient timed reachability analysis using clock difference diagrams

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