Verification of Linear Duration Invariants by Model Checking CTL Properties

DOI10.1007/978-3-540-85762-4_27zbMath1161.68595OpenAlexW1785398866MaRDI QIDQ5505616

Miaomiao Zhang, Zhi-Ming Liu, Dang Van Hung

Publication date: 27 January 2009

Published in: Theoretical Aspects of Computing - ICTAC 2008 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-85762-4_27

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (2)

Checking Integral Real-Time Automata for Extended Linear Duration Invariants ⋮ A practical approach to model checking duration calculus using Presburger arithmetic

Uses Software

• Kronos
• Uppaal

Cites Work

• Unnamed Item
• A calculus of durations
• A theory of timed automata
• Duration calculus. A formal approach to real-time systems.
• Checking temporal duration properties of timed automata.
• Checking timed automata for linear duration properties
• Kronos: A verification tool for real-time systems
• Interval Duration Logic
• Model Checking Duration Calculus: A Practical Approach
• “Sometimes” and “not never” revisited
• Formal Methods for the Design of Real-Time Systems
• Theoretical Aspects of Computing - ICTAC 2004
• Deciding an Interval Logic with Accumulated Durations

This page was built for publication: Verification of Linear Duration Invariants by Model Checking CTL Properties