Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/7150
Title: A Determinizable Class of Timed Automata
Authors: Alur, Rajeev
Fix, Limor
Henzinger, Thomas A.
Keywords: computer science
technical report
Issue Date: Mar-1995
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1492
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 A. 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 class 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.
URI: http://hdl.handle.net/1813/7150
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
95-1492.pdf256.5 kBAdobe PDFView/Open
95-1492.ps310.01 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us