License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2011.81
URN: urn:nbn:de:0030-drops-30017
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3001/
Go to the corresponding LIPIcs Volume Portal

Segoufin, Luc ; Torunczyk, Szymon

Automata based verification over linearly ordered data domains

pdf-format:
11.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{segoufin_et_al:LIPIcs:2011:3001,
  author =	{Luc Segoufin and Szymon Torunczyk},
  title =	{{Automata based verification over linearly ordered data domains}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011) },
  pages =	{81--92},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Thomas Schwentick and Christoph D{\"u}rr},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3001},
  URN =		{urn:nbn:de:0030-drops-30017},
  doi =		{10.4230/LIPIcs.STACS.2011.81},
  annote =	{Keywords: register automata, data values, linear order}
}

Keywords: register automata, data values, linear order
Collection: 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)
Issue Date: 2011
Date of publication: 11.03.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI