Nie jesteś zalogowany |
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
- 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.
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.
