Automata based verification over linearly ordered data domains
Automata based verification over linearly ordered data domains
复制标题
线性有序数据域上基于自动机的验证
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Szymon Toruńczyk
中科院分区：
文献类型：
--
作者：
L. Segoufin;Szymon Toruńczyk
在本文中，我们工作在线性有序的数据域配备了大量的一元谓词和常数。我们考虑非确定性自动机处理的话，并存储在域范围内的许多变量。在转换过程中，这些自动机可以使用线性顺序、一元谓词和常数来比较当前配置的数据值与先前配置的数据值。
我们表明，这种自动机的空是可判定的，在有限和无限的话，在合理的可计算性假设的线性顺序。
最后，我们展示了如何我们的自动机模型可以用于验证工作流规范的基础数据库中存在的属性。
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.