Accession Number:

ADA278858

Title:

A Determinizable Class of Timed Automata

Descriptive Note:

Interim rept.,

Corporate Author:

CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Alur, Rajeev
• Fix, Limor
• Henzinger, Thomas A.

Report Date:

1993-01-01

Pagination or Media Count:

14.0

Abstract:

We introduce the class of event-recording timed automata ERA. An event-recording automaton contains, for every event a, a clock that records the time of the last occurrence of alpha. The class ERA is, on one hand, expressive enough to model finite timed transition systems and, on the other hand, determinizable and closed under all boolean operations. As a result, the language inclusion problem is decidable for event-recording automata. We present a translation from timed transition systems to event-recording automata, which leads to an algorithm for checking if two timed transition systems have the same set of timed behaviors. We also consider event-predicting timed automata EPA, which contain clocks that predict the time of the next occurrence of an event. The claw of event-clock automata ECA, which contain both event-recording and event-predicting clocks, is a suitable specification language for real-time properties. We provide an algorithm for checking if a timed automaton meets a specification that is given as an event-clock automaton. Real-time systems, Formal specification, Timing verification.

Descriptors:

• *CLOCKS
• *REAL TIME
• *AUTOMATA
• ALGORITHMS
• SPECIFICATIONS
• OPERATION
• TRANSLATIONS
• RECORDS
• TRANSITIONS
• LANGUAGE
• TIME
• VERIFICATION
• PREDICTIONS

Subject Categories:

• Computer Systems Management and Standards
• Cybernetics
• Test Facilities, Equipment and Methods

Distribution Statement:

APPROVED FOR PUBLIC RELEASE