Automata based verification over linearly ordered data domains

Prelegent(ci)

Szymon Toruńczyk

Afiliacja

Uniwersytet Warszawski

Termin

17 lutego 2010 14:15

Pokój

p. 5870

Tytuł w języku angielskim

joint work with Luc Segoufin

Seminarium

Seminarium „Teoria automatów”

---

In this paper we work over linearly ordered data domains
equipped with finitely many unary predicates and constants. We consider
nondeterministic automata processing words and storing finitely many
variables ranging over the domain. During a transition, these automata
can compare the data values of the current configuration with those of
the previous configuration using the linear order, the unary predicates
and the constants. We show that emptiness for such automata is decidable, both over finite
and infinite words, under reasonable computability assumptions on the
linear order. Finally, we show how our automata model can be used for verifying
properties of workflow specifications in the presence of an underlying
database.

---