Symbolic model checking of timed guarded commands using difference decision diagrams

DOI10.1016/S1567-8326(02)00023-1zbMATH Open1008.68031MaRDI QIDQ1858438FDOQ1858438

Authors: Jesper Møller, Henrik Hulgaard, Henrik Reif Andersen 

Publication date: 13 February 2003

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

Recommendations

• scientific article; zbMATH DE number 1324667
• scientific article; zbMATH DE number 1424030
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Symbolic model checking for real-time systems
• scientific article; zbMATH DE number 2102690

zbMATH Keywords

real-time systemstimed automataquantifier eliminationsymbolic model checkingdifference constraint systemsdifference decision diagramstimed guarded commandstimedCTL

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (6)

• Improved BDD-based discrete analysis of timed systems
• Title not available (Why is that?)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Finding extremal models of discrete duration calculus formulae using symbolic search
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• Kronos

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

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