Symbolic model checking of timed guarded commands using difference decision diagrams

DOI10.1016/S1567-8326(02)00023-1zbMath1008.68031MaRDI QIDQ1858438

Henrik Reif Andersen, Henrik Hulgaard, Jesper Møller

Publication date: 13 February 2003

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

zbMATH Keywords

quantifier eliminationreal-time systemstimed automatasymbolic model checkingdifference constraint systemsdifference decision diagramstimed guarded commandstimedCTL

Mathematics Subject Classification ID

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

Uses Software

• Kronos

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new polynomial-time algorithm for linear programming
• An efficient decision procedure for the theory of rational order
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• Symbolic model checking for real-time systems
• Kronos: A verification tool for real-time systems
• A lattice-theoretical fixpoint theorem and its applications
• Applying Linear Quantifier Elimination
• Graph-Based Algorithms for Boolean Function Manipulation
• On the SUP-INF Method for Proving Presburger Formulas
• A Decision Procedure for the First Order Theory of Real Addition with Order
• Guarded commands, nondeterminacy and formal derivation of programs
• Disjunctive Programming
• Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
• Model-checking for real-time systems
• The complexity of theorem-proving procedures

This page was built for publication: Symbolic model checking of timed guarded commands using difference decision diagrams