Verification of Two-Variable Logic Revisited
Verification of Two-Variable Logic Revisited
复制标题
重新审视二变量逻辑的验证
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
J. Worrell
中科院分区：
文献类型：
--
作者：
Michael Benedikt;R. Lenhardt;J. Worrell
双变量逻辑是一阶逻辑的一部分，它允许可确定的验证问题。在之前的工作中，我们开发了一种对概率系统特别有用的FO2验证方法，该方法基于对将FO2转换为自动机的分析。在这项工作中，我们展示了这里引入的技术可以应用于提供其他逻辑的信息，并且可以在概率验证的背景下与线性时间逻辑（LTL）的自动机理论技术结合使用。首先，我们从没有后继关系的FO2开始重新审视我们之前工作的技术。利用Weis最近的结果，我们可以得到这些公式的小自动机。然后，我们证明我们可以通过对没有后继的FO2的自举结果重新获得一般FO2公式的自动机大小界限。接下来，我们将考虑将FO2验证技术与LTL验证技术相结合。我们在这里提出了一种包含了FO2和LTL的语言，并继承了这两种语言的模型检查属性。我们的自动机翻译为这种大型语言的非确定性系统提供了新的模型检查界限，并且对概率系统特别有用：例如马尔可夫链，递归马尔可夫链和马尔可夫决策过程。
Two-variable logic is a fragment of first-order logic that allows for decidable verification problems. In previous work, we developed an approach to FO2 verification that is particularly useful for probabilistic systems, based on analysis of the translation of FO2 to automata. In this work we show that the techniques introduced there can be applied to give information on other logics, and can be used in conjunction with automata-theoretic techniques for Linear Temporal Logic (LTL) in the context of probabilistic verification. First we revisit the technique of our prior work starting with FO2 without the successor relation. Making use of recent results by Weis we show here that we can get quite small automata for these formula. We then show that we can recapture the automata size bounds for general FO2 formulas by bootstrapping results for FO2 without successor. Next, we look at combining FO2 verification techniques with those for LTL. We present here a language that subsumes both FO2 and LTL, and inherits the model checking properties of both languages. Our automata translation gives new bounds on model-checking for this large language for non-deterministic systems, and is particularly useful for probabilistic systems: e.g Markov Chains, Recursive Markov Chains, and Markov Decision Processes.
模型检查和博弈中的二变量与线性时态逻辑
影响因子：
0.6
作者：
Benedikt M
通讯作者：
Benedikt M