A practical approach to model checking duration calculus using Presburger arithmetic

DOI10.1007/s10472-013-9373-7zbMath1315.68180MaRDI QIDQ2251131

Aske W. Brekling, Michael R. Hansen, Anh-Dung Phan

Publication date: 11 July 2014

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-013-9373-7

zbMATH Keywords

model checking; duration calculus; interval temporal logic; Presburger arithmetic

Mathematics Subject Classification ID

68W30: Symbolic computation and algebraic computation

03B70: Logic in computer science

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

03F30: First-order arithmetic and fragments

03B44: Temporal logic

Related Items

An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic, Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives

Uses Software

• z3
• DCVALID

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model checking duration calculus: a practical approach
• A calculus of durations
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• Model-checking discrete duration calculus
• Duration calculus. A formal approach to real-time systems.
• Model-checking dense-time duration calculus
• Decidability of a Hybrid Duration Calculus
• A propositional modal logic of time intervals
• Presburger arithmetic with bounded quantifier alternation
• Automata, Languages and Programming
• Verification of Linear Duration Invariants by Model Checking CTL Properties
• Tools and Algorithms for the Construction and Analysis of Systems
• Theoretical Aspects of Computing - ICTAC 2004
• Linear Quantifier Elimination as an Abstract Decision Procedure
• Deciding an Interval Logic with Accumulated Durations