A practical approach to model checking duration calculus using Presburger arithmetic
From MaRDI portal
Publication:2251131
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
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
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