IDLVALID
:
Model Checking Dense Time Duration Calculus Formulae
(Page under Construction)
Introduction
Team Members
Tools
Examples
Papers
Lecture
Notes/Slides
Links
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
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.
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.
Lecture Notes/Slides
Some links of Interest
This page was created by Paritosh
K. Pandya on 21 October 2004. Last
modified 24, October 2004.