The Timestamp of Timed Automata

Research output: Contribution to journalArticleResearch

Abstract

Given a member A of the class of non-deterministic timed automata with silent transitions (eNTA), we show how one can effectively compute its timestamp: the set of all pairs of time values and the corresponding actions of all observable timed traces of A, and also a deterministic timed automaton with the same timestamp as that of A. The timestamp is eventually periodic and is constructed via a finite periodic augmented region automaton. A consequence of this construction is the periodicity of the language of timed automata with respect to suffixes. Applications include the decidability of the 1-bounded language inclusion problem for the class eNTA, and a partial method, not bounded by time or number of steps, for the general language non-inclusion problem for eNTA.
Original languageEnglish
JournalarXiv.org e-Print archive
Publication statusPublished - 17 Dec 2014

Fingerprint

Timestamp
Timed Automata
Suffix
Decidability
Periodicity
Automata
Inclusion
Trace
Partial
Language
Class

Keywords

  • cs.FL
  • F.1.1; D.2.4

Cite this

The Timestamp of Timed Automata. / Rosenmann, Amnon.

In: arXiv.org e-Print archive, 17.12.2014.

Research output: Contribution to journalArticleResearch

@article{b654ba47859e4aecbb3c942ff184ed85,
title = "The Timestamp of Timed Automata",
abstract = "Given a member A of the class of non-deterministic timed automata with silent transitions (eNTA), we show how one can effectively compute its timestamp: the set of all pairs of time values and the corresponding actions of all observable timed traces of A, and also a deterministic timed automaton with the same timestamp as that of A. The timestamp is eventually periodic and is constructed via a finite periodic augmented region automaton. A consequence of this construction is the periodicity of the language of timed automata with respect to suffixes. Applications include the decidability of the 1-bounded language inclusion problem for the class eNTA, and a partial method, not bounded by time or number of steps, for the general language non-inclusion problem for eNTA.",
keywords = "cs.FL, F.1.1; D.2.4",
author = "Amnon Rosenmann",
note = "31 pages, 7 figures",
year = "2014",
month = "12",
day = "17",
language = "English",
journal = "arXiv.org e-Print archive",
publisher = "Cornell University Library",

}

TY - JOUR

T1 - The Timestamp of Timed Automata

AU - Rosenmann, Amnon

N1 - 31 pages, 7 figures

PY - 2014/12/17

Y1 - 2014/12/17

N2 - Given a member A of the class of non-deterministic timed automata with silent transitions (eNTA), we show how one can effectively compute its timestamp: the set of all pairs of time values and the corresponding actions of all observable timed traces of A, and also a deterministic timed automaton with the same timestamp as that of A. The timestamp is eventually periodic and is constructed via a finite periodic augmented region automaton. A consequence of this construction is the periodicity of the language of timed automata with respect to suffixes. Applications include the decidability of the 1-bounded language inclusion problem for the class eNTA, and a partial method, not bounded by time or number of steps, for the general language non-inclusion problem for eNTA.

AB - Given a member A of the class of non-deterministic timed automata with silent transitions (eNTA), we show how one can effectively compute its timestamp: the set of all pairs of time values and the corresponding actions of all observable timed traces of A, and also a deterministic timed automaton with the same timestamp as that of A. The timestamp is eventually periodic and is constructed via a finite periodic augmented region automaton. A consequence of this construction is the periodicity of the language of timed automata with respect to suffixes. Applications include the decidability of the 1-bounded language inclusion problem for the class eNTA, and a partial method, not bounded by time or number of steps, for the general language non-inclusion problem for eNTA.

KW - cs.FL

KW - F.1.1; D.2.4

M3 - Article

JO - arXiv.org e-Print archive

JF - arXiv.org e-Print archive

ER -