Record Details

Modal strength reduction in quantified discrete duration calculus

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Modal strength reduction in quantified discrete duration calculus
 
Creator KRISHNA, SN
PANDYA, PK
 
Subject logic
 
Description 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 DCVALID. 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.
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-23T19:03:46Z
2011-12-15T09:11:18Z
2011-10-23T19:03:46Z
2011-12-15T09:11:18Z
2005
 
Type Article; Proceedings Paper
 
Identifier FSTTCS 2005: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS,3821,444-456
3-540-30495-9
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15208
http://hdl.handle.net/100/1979
 
Source 25th International Conference on Foundations of Software Technology and Theoretical Computer Science,Hyderabad, INDIA,DEC 15-18, 2005
 
Language English