Accession Number : ADA328835
Title : Benefits of Relaxing Punctuality,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Alur, R. ; Feder, T. ; Henzinger, T. A.
PDF Url : ADA328835
Report Date : MAY 1991
Pagination or Media Count : 43
Abstract : The most natural, compositional way of modeling real time systems uses a dense domain for time. The satisfiability of real time constraints that are capable of expressing punctual it in this model is, however, known to be undecidable. The authors introduce a temporal language that can constrain the time difference between events only with finite (yet arbitrary) precision and show the resulting logic to be EXPACE-complete. This result allows the authors to develop an algorithm for the verification of timing properties of real time systems with a dense semantics.
Descriptors : *MODELS, *REAL TIME, *PROGRAMMING LANGUAGES, *TIME DOMAIN, ALGORITHMS, VERIFICATION, SPECIFICATIONS, SEMANTICS, HIGH DENSITY, RELAXATION, COMPOSITION(PROPERTY), AUTOMATA.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE