Model Checking Dense Time Duration Calculus Formulae

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.

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

- Paritosh Pandya (TIFR)

- Supratik Chakraborty (IIT, Bombay)

- Babita Sharma (IIT, Bombay)
- Gaurav Chakravorty (IIT, Kanpur)

- S. Krishna (IIT, Bombay)
- Dina Thomas (IIT, Bombay)

- 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).

Please click here to go to the directories containing full details of the 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.

- 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.

- DCVALID
and CTLDC -- a validity checker for discrete time duration calculus

- ICS
- MONA - a validity checker for WS1S
- PC/DC -- A Duration Calculus Proof Assistant based on PVS.
- Interval temporal logic by Ben Moszkowski and collegues
- SMV, and NuSMV
- Jonathan Bowen's Formal Methods Page
- Formal Methods in India
- GENTLE compiler construction system

This page was created by Paritosh K. Pandya on 21 October 2004. Last modified 24, October 2004.