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

    Tool Distribution

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


    Gas Burner Problem
    Minepump Problem
    Lift Control Problem
    Joshop Scheduling  J24

    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

    Lecture Notes/Slides

    Some links of Interest

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