10.4230/LIPICS.STACS.2011.81
Segoufin, Luc
Luc
Segoufin
Torunczyk, Szymon
Szymon
Torunczyk
Automata based verification over linearly ordered data domains
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
register automata
data values
linear order
Schwentick, Thomas
Thomas
Schwentick
Dürr, Christoph
Christoph
Dürr
2011
2011-03-11
2011-03-11
2011-03-11
en
urn:nbn:de:0030-drops-30017
10.4230/LIPIcs.STACS.2011
978-3-939897-25-5
1868-8969
10.4230/LIPIcs.STACS.2011
LIPIcs, Volume 9, STACS 2011
28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)
2013
9
7
81
92
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Schwentick, Thomas
Thomas
Schwentick
Dürr, Christoph
Christoph
Dürr
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
9
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
627853 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011), pages 81-92