Symbolic model checking of timed guarded commands using difference decision diagrams
type: Item
instance of: scholarly article
title: Symbolic model checking of timed guarded commands using difference decision diagrams
zbMATH Open document ID: 1008.68031
DOI: 10.1016/S1567-8326(02)00023-1
author: Jesper Møller
author: Henrik Hulgaard
author: Henrik Reif Andersen
published in: The Journal of Logic and Algebraic Programming
publication date: 2003-02-13T00:00:00Z
Mathematics Subject Classification ID: 68N17
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 1868272
zbMATH Keywords: real-time systems
zbMATH Keywords: timed automata
zbMATH Keywords: timed guarded commands
zbMATH Keywords: symbolic model checking
zbMATH Keywords: timedCTL
zbMATH Keywords: difference constraint systems
zbMATH Keywords: difference decision diagrams
zbMATH Keywords: quantifier elimination
describes a project that uses: Kronos
MaRDI profile type: Publication
cites work: Disjunctive Programming
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Q3336675
cites work: Q4079605
cites work: The complexity of theorem-proving procedures
cites work: Q5674430
cites work: Guarded commands, nondeterminacy and formal derivation of programs
cites work: An efficient decision procedure for the theory of rational order
cites work: A Decision Procedure for the First Order Theory of Real Addition with Order
cites work: Q4082296
cites work: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
cites work: Symbolic model checking for real-time systems
cites work: Q5592246
cites work: A new polynomial-time algorithm for linear programming
cites work: Model-checking for real-time systems
cites work: Applying Linear Quantifier Elimination
cites work: Q3992568
cites work: Q4945220
cites work: Q4255572
cites work: A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
cites work: Q3221403
cites work: On the SUP-INF Method for Proving Presburger Formulas
cites work: A lattice-theoretical fixpoint theorem and its applications
cites work: Q5807665
cites work: Kronos: A verification tool for real-time systems
description: scientific article; zbMATH DE number 1868272