Bounded validity checking of interval duration logic
Tools and Algorithms for the Construction and Analysis of Systems: 11th …, 2005•Springer
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 …
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 …
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.
Springer