21.04.2005

Automaty czasowe z jednym zegarem
(Timed automata with one clock)

Niedeterministyczne automaty czasowe stanowią naturalne rozszerzenie klasycznegopojęcia automatu i są szeroko stosowane do modelowania systemów zależnych od czasu.
Są one dodatkowo wyposażone w pewną liczbę zegarów, umożliwiających pomiar czasu, który upłynął pomiędzy zdarzeniami. Analiza automatów czasowych jest jednak trudniejsza niz w przypadku klasycznym; np. problem uniwersalności jest nierozstrzygalny. Okazuje się jednak, że dla automatów z jednym zegarem problem ten jest rozstrzygalny - jest to wynik Ouaknine'a i Worrel'a zaprezentowany na konferencji LICS'04.
W czasie referetu zaprezentuję pojęcie alternującego automatu czasowego i pokażę, że przy ograniczeniu do jednego zegara automaty te mają rozstrzygalny problem pustości (i również dualny problem uniwersalności). Pokażę również, że problem ten ma bardzo wysoką złożoność (nie jest pierwotnie rekurencyjny) i to nawet dla automatów niedeterministycznych z jednym zegarem. Ponadto, wykażę, że dla pewnych naturalnych rozszerzeń (tranzycje epsilonowe, automaty Buchi'ego) problem universalności jest już nierozstrzygalny. Oznacza to, że poruszamy się tutaj bardzo blisko granicy rozstrzygalności. Zaprezentowane wyniki rozwiązują dwa otwarte problemy postawione przez Ouaknine'a i Worrel'a.

Nondeterministic timed automata are a natural extension of classical automata widely used for modelling time-dependent systems. They are additionally equipped with clocks, enabling to measure amount of time that elapses between events. However, timed automata are more difficult to analyse; in particular, universality is undecidable. Recently (LICS'04) it has been shown by Ouaknine and Worrell that the problem is decidable form automata with only one clock.
In the talk I will present a notion of alternating timed automata. I will show that such automata with only one clock have decidable emptiness problem. I will also prove the lower bound for complexity of the problem (non-primitive recursive); in fact, the the same lower bound applies even for the universality problem for nondeterministic timed automata with one clock.Furthermore, I will discuss several natural extensions of nondeterministic timed automata (epsilon moves, Buchi acceptance condition) and show that they all lead to undecidable universality problem, even for automata with one clock. These results solve two open problems posed by Ouaknine and Worrell.