IDLVALID : Model Checking Dense Time Duration Calculus Formulae. 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.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Konur, Savas: A survey on temporal logics for specifying and verifying real-time systems (2013)
- Della Monica, Dario; Goranko, Valentin; Sciavicco, Guido: Hybrid metric propositional neighborhood logics with interval length binders (2011)
- Meyer, Roland; Faber, Johannes; Hoenicke, Jochen; Rybalchenko, Andrey: Model checking duration calculus: a practical approach (2008)
- Pandya, Paritosh K.; Krishna, Shankara Narayanan; Loya, Kuntal: On sampling abstraction of continuous time logic with durations (2007)
- Thomas, Dina; Chakraborty, Supratik; Pandya, Paritosh: Efficient guided symbolic reachability using reachability expressions (2006)
- Krishna, Shankara Narayanan; Pandya, Paritosh K.: Modal strength reduction in quantified discrete duration calculus (2005)
- Sharma, Babita; Pandya, Paritosh. K.; Chakraborty, Supratik: Bounded validity checking of interval duration logic (2005)
- Chakravorty, Gaurav; Pandya, Paritosh K.: Digitizing interval duration logic. (2003)
- Pandya, Paritosh K.: Interval duration logic: expressiveness and decidability (2002)
- Pandya, Paritosh K.: Model checking CTL*[DC] (2001)