Record Details


Field	Value

Title	Bounded validity checking of interval duration logic

Names	SHARMA, B PANDYA, PK CHAKRABORTY, S
Date Issued	2005 (iso8601)
Abstract	A rich dense-time logic, called Interval Duration Logic (IDL), is useful for specifying quantitative properties of timed systems. The logic is undecidable in general. However, several approaches can be used for checking validity (and model checking) of IDL formulae in practice. In this paper, we propose bounded validity checking of IDL formulae by polynomially reducing this to checking unsatisfiability of lin-sat formulae. We implement this technique and give performance results obtained by checking the unsatisfiability of the resulting lin-sat formulae using the ICS solver. We also perform experimental comparisons of several approaches for checking validity of IDL formulae, including (a) digitization followed by automata-theoretic analysis, (b) digitization followed by pure propositional SAT solving, and (c) lin-sat solving as proposed in this paper. Our experiments use a rich set of examples drawn from the Duration Calculus literature.
Genre	Article; Proceedings Paper
Identifier	TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS,3440,301-316

ICAR Research Data Repository for Knowledge Management