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