Benefits of Relaxing Punctuality,

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1991
Accession Number
ADA328835

Entities

People

  • R. Alur
  • T. A. Henzinger
  • T. Feder

Organizations

  • Stanford University

Tags

Communities of Interest

  • Energy and Power Technologies
  • Human Systems

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Automata
  • Classification
  • Clocks
  • Computer Science
  • Computers
  • Consistency
  • Construction
  • Language
  • Precision
  • Rational Numbers
  • Semantics
  • Theoretical Computer Science
  • Time Domain
  • Time Intervals
  • Verification

Fields of Study

  • Computer science

Readers

  • Computational Modeling and Simulation
  • Mathematical Modeling and Probability Theory.