Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Nested Timed Automata with Frozen Clocks
verfasst von : Guoqiang Li, Mizuhito Ogawa, Shoji Yuen
Erschienen in: Formal Modeling and Analysis of Timed Systems
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
A nested timed automaton (NeTA) is a pushdown system whose control locations and stack alphabet are
timed automata (TAs)
. A control location describes a working TA, and the stack presents a pile of interrupted TAs. In NeTAs, all local clocks of TAs proceed uniformly also in the stack. This paper extends NeTAs with frozen local clocks (NeTA-Fs). All clocks of a TA in the stack can be either frozen or proceeding when it is pushed. A NeTA-F also allows global clocks adding to local clocks in the working TA, which can be referred and/or updated from the working TA. We investigate the reachability of NeTA-Fs showing that (1) the reachability with a single global clock is
decidable
, and (2) the reachability with multiple global clocks is
undecidable
.