专栏首页arxiv.org翻译专栏证明无限状态系统时间性质的时间预言(CS)

证明无限状态系统时间性质的时间预言(CS)

时序特性的各种验证技术将时序验证转化为安全性验证。对于无限状态系统,这些转换本质上是不精确的。也就是说,在某些情况下,时间属性成立,但由此产生的安全属性不成立。本文介绍了一种解决这种不精确性的机制。这个机制,我们称之为时间预言,是受预言变量的启发。时间预言通过一个合适的表构造,利用一阶线性时间逻辑公式提炼了一个无限状态系统。对于特定的基于一阶逻辑的生命-安全转换,我们表明使用时间预测严格地提高了精度。此外,时间预言使证明方法具有鲁棒性,并通过一个割消定理加以证明。我们将我们的方法集成到Ivy推理验证系统中,并表明它可以处理具有挑战性的时间验证实例。

原文题目:Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems

原文:Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophecy, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.

原文链接:https://arxiv.org/abs/2106.00966

原文作者:Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham

我来说两句

0 条评论
登录 后参与评论

相关文章

  • ACL论文 | 深度学习大神新作,神经网络的自然语言翻译应用

    在 8月7日在德国柏林召开的2016 计算语言学(ACL)大会上,学者Thang Luong、Kyunghyun Cho 和 Christopher D. Ma...

    AI科技评论
  • 万物皆可状态机

    状态机是逻辑设计的重要内容,状态机的设计水平直接反应工程师的逻辑功底,所以很多公司在硬件工程师及逻辑工程师面试中,状态机设计几乎是必选题目。本篇在引入状态机设计...

    数字芯片社区
  • 一文谈尽边缘计算

    最近半年里,AI谈累了、区块链谈倦了,大批云计算公司找到了新的热点——边缘计算。我认可边缘计算是比肩云计算的星辰大海,但是我看到这些PR稿都是炒冷饭和自吹的尬聊...

    边缘计算
  • 一文谈尽边缘计算

    最近半年里,AI谈累了、区块链谈倦了,大批云计算公司找到了新的热点——边缘计算。我认可边缘计算是比肩云计算的星辰大海,但是我看到这些PR稿都是炒冷饭和自吹的尬聊...

    SDNLAB
  • 在PyTorch中使用Seq2Seq构建的神经机器翻译模型

    在这篇文章中,我们将构建一个基于LSTM的Seq2Seq模型,使用编码器-解码器架构进行机器翻译。

    deephub
  • Biological Psychiatry:正念训练后海马回路活动的增强是 改善消退恐惧记忆提取的基础

    请点击上面“思影科技”四个字,选择关注我们,思影科技专注于脑影像数据处理,涵盖(fMRI,结构像,DTI,ASL,EEG/ERP,FNIRS,眼动)等,希望专业...

    用户1279583
  • 以太网中时间同步的那点事

    对于普通人来讲,时间就是大脑神经元中记忆碎片构建的意识。正是由于神经元的记忆特征,才能在“现在”随时的回忆“过去”。也就是说“过去”存在于“现在”之中,“过去”...

    网络交换FPGA
  • Rest Notes-基于网络应用的架构风格

    itliusir
  • 游戏服务器架构:网络游戏同步技术概述

    注:本文的锁步同步(Lockstep)特指只同步操作的确定性锁步同步。本文将快照同步等同于状态同步。

    用户3479834

扫码关注云+社区

领取腾讯云代金券