joint work with Luc Segoufin

Speaker(s)

Szymon Toruńczyk

Affiliation

Uniwersytet Warszawski

Date

Feb. 17, 2010, 2:15 p.m.

Room

room 5870

Title in Polish

Automata based verification over linearly ordered data domains

Seminar

Seminar Automata Theory

---

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.

---