Record Details

Bounded validity checking of interval duration logic

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Bounded validity checking of interval duration logic
 
Creator SHARMA, B
PANDYA, PK
CHAKRABORTY, S
 
Description 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.
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-23T17:45:32Z
2011-12-15T09:11:16Z
2011-10-23T17:45:32Z
2011-12-15T09:11:16Z
2005
 
Type Article; Proceedings Paper
 
Identifier TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS,3440,301-316
3-540-25333-5
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15192
http://hdl.handle.net/100/1958
 
Source 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Edinburgh, SCOTLAND,APR 04-08, 2005
 
Language English