QDDC is a logic for specifying quantitative timing properties of reactive systems. An automata theoretic decision procedure for QDDC reduces each formula to a finite state automaton accepting precisely the models of the formula. This construction has been implemented into a validity/model checking tool for QDDC called DC VALID. Unfortunately, the size of the final automaton as well as the intermediate automata which are encountered in the construction can some times be prohibitively large. In this paper, we present some validity preserving transformations to QDDC formulae which result into more efficient construction of the formula automaton and hence reduce the validity checking time. The transformations can be computed in linear time. We provide a theoretical as well as an experimental analysis of the improvements in the formula automaton size and validity checking time due to our transformations. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Krishna, S. N., & Pandya, P. K. (2005). Modal strength reduction in quantified discrete duration calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3821 LNCS, pp. 444–456). https://doi.org/10.1007/11590156_36
Mendeley helps you to discover research relevant for your work.