量化自动机的安全性与活性
摘要：量化安全和活性是形式语言中的基本概念，在验证中起着关键作用。最近，这种二元性也被应用于量化属性，该属性是从无限单词到偏序域的任意函数。我们研究如何利用这种二元性来处理由量化自动机表示的特定类别的量化属性。这些自动机包含有限数量的状态和有理数值的转换权重，并且它们的共有值函数Inf、Sup、LimInf、LimSup、LimInfAvg、LimSupAvg和DSum将无限单词映射到实数的全序域中。在这个自动机理论的环境中，我们建立了量化安全性和拓扑连续性之间的联系，并提供了量化安全性和活性的布尔对应项的替代特征描述。对于所有共有值函数，我们展示了如何在PTime中构造量化自动机的安全闭包，并提供了一个判断给定量化自动机是否安全或活性的PSpace完备检查，除了对于LimInfAvg和LimSupAvg自动机，其中安全性检查是在ExpSpace中的。此外，对于确定性的Sup、LimInf和LimSup自动机，我们给出了PTime分解为安全和活性自动机。这些分解使得我们可以针对量化规范的安全性和活性验证采用不同的技术。
作者：Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sarac{c}
论文ID：2307.06016
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-07-17