# IDLVALID : Model Checking Dense Time Duration Calculus Formulae

(Page under Construction)

• Introduction
• Team Members
• Tools
• Examples
• Papers
• Lecture Notes/Slides

• ## Introduction

Duration Calculus is a dense time interval temporal logic with constructs which allow measurement of amount of time for which a proposition holds in a time interval. Interval Duration Logic is its variant where models are finite timed state sequences.  An number of examples illustrate the expressive abilities of these logics.

While the validity of formulae in these logics is undecidable, for practical applicability there has been considerable interest in finding techniques and tools for validity and model checking of formulae of these logics.  However, there are very few available tools implementing these approaches.

This page provide tool sets for validity checking of IDL formulae using two different approaches. Full details of these approaches can be found in the following technical  report.
• Bounded Validity Checking by Reduction to Lin-Sat Solving
• Digitization to Discrete Duration Calculus followed by automata Theoretic Analysis.
Several standard examples drawn from Duration Calculus literature can be checked using these tools.

Acknowledgements The compiler construction system GENTLE was used in the implementation.

## Team Members

• Paritosh Pandya (TIFR)
• Supratik Chakraborty (IIT, Bombay)
• Babita Sharma (IIT, Bombay)
• Gaurav Chakravorty (IIT, Kanpur)
• S. Krishna (IIT, Bombay)
• Dina Thomas (IIT, Bombay)

## Tool Distribution

• Bounded Validity Checking:  idl2ics
Reduces  k-validity of IDL formulae to validity of lin-sat formulae, solvable by the ICS tool from SRI Internation.
• Digitization: idl2ddc
Reduces validity of dense-time logic IDL to validity of discrete-time logic DDC.
DDC formulae can be checked for validity using tools DCVALID from TIFR.
• Reductions and transformations in Discrete Duration Calculus:
ddc2ddcr  transforms ddc formulae to equivalent ddcr formulae without timing constructs.
• Validity and model checker for discrete time duration calculus:  DCVALID
It has its own page.

Please click here to go to the directory containing sample input file (idl) as well as output files (ics as ddc).

## Examples

These directories contain the ICS files for the examples (for various bounds k)  obtained using idl2ics tool as well as ddc files obtained using idl2ddc by  digitization.

## Papers and Technical Reports

• P.K. Pandya, S.N. Krishna and K. Loya, On sampling abstraction of a continuous time logic with durations, in Proc. TACAS 2007, Braga, LNCS, Springer-Verlag, 2007

• D. Thomas, S. Chakraborty and P.K. Pandya, Efficient guided symbolic reachability using reachability expressions, in Proc. TACAS 2006, Vienna, LNCS 3920, Springer-Verlag, 2006.

• S.N. Krishna and P.K. Pandya, Modal Strength Reduction in Quantified Discrete Duration Calculus, in Proc. FSTTCS 2005, Hyderabad, LNCS 3821, Springer-Verlag, 2005.

• B. Sharma, P.K. Pandya and S. Chakraborty, Bounded Validity Checking of Interval Duration Logic, in Proc. TACAS 2005, Edinburgh, LNCS 3440, Springer-Verlag, 2005 (Technical Report, October 2004.)

• Gaurav Chakravorty and P.K. Pandya, Digitizing Interval Duration Logic, in Proc. CAV 2003, Colorado, Boulder, July 2003. (Technical Report, TCS-02-PKP-1, Tata Institute of Fundamental Research, 2002).
• P.K. Pandya, Interval Duration Logic: Expressiveness and Decidability, in Proc. Workshop on Theory and Practice of Timed Systems TPTS'2002, Grenoble, 2002 (affiliated with EATPS 2002), Electronic Notes on Theoertical Computer Science ENTCS 65.6, Elsevier Scientific Publishers, 2002. (Technical Report TCS-00-PKP-5, Tata Institute of Fundamental Research, Mumbai, 2000.)
• P.K. Pandya, Specifying and Deciding Qauntified Discrete-time Duration Calculus formulae using DCVALID, in Proc. Real-Time Tools, RTTOOLS'2001, Aalborg, August, 2001 (affiliated with CONCUR 2001). Technical Report TCS-00-PKP-1, Tata Institute of Fundamental Research, Mumbai, 2000.
• P.K. Pandya, Model checking CTL[DC], in Proc. TACAS 2001, Genova, LNCS 2031, Springer-Verlag, April 2001. Technical Report TCS-00-PKP-2, Tata Institute of Fundamental Research, Mumbai, 2000.