专栏首页arxiv.org翻译专栏有界CTL的充要条件(CS AI)
原创

有界CTL的充要条件(CS AI)

计算树逻辑(CTL)是形式验证中的主要形式主义之一。作为一种规范语言,它用于表示预期现有系统可以满足的属性。从验证和系统设计的角度来看,由于各种原因,这种特性的某些信息内容可能与系统无关,例如,随着时间的流逝可能变得过时,或者由于实际困难而可能变得不可行。然后,出现了如何在不改变相关系统行为或不违反现有规范的情况下减去此类信息的问题。此外,在这种情况下,两个关键概念是有意义的:给定属性的最强必要条件(SNC)和最弱充分条件(WSC)。为了从原则上解决这种情况,我们在CTL中引入了基于遗忘的方法,并证明了该方法可用于计算给定模型下属性的SNC和WSC。我们研究了它的理论特性,也表明我们的遗忘概念可以满足现有的基本假设。此外,我们分析了基本任务的计算复杂性,包括相关片段CTLAF的各种结果。

原文标题:On Sufficient and Necessary Conditions in Bounded CTL

原文:Computation Tree Logic (CTL) is one of the central formalisms in formal verification. As a specification language, it is used to express a property that the system at hand is expected to satisfy. From both the verification and the system design points of view, some information content of such property might become irrelevant for the system due to various reasons e.g., it might become obsolete by time, or perhaps infeasible due to practical difficulties. Then, the problem arises on how to subtract such piece of information without altering the relevant system behaviour or violating the existing specifications. Moreover, in such a scenario, two crucial notions are informative: the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a given property. To address such a scenario in a principled way, we introduce a forgetting-based approach in CTL and show that it can be used to compute SNC and WSC of a property under a given model. We study its theoretical properties and also show that our notion of forgetting satisfies existing essential postulates. Furthermore, we analyse the computational complexity of basic tasks, including various results for the relevant fragment CTLAF.

作者:Renyan Feng, Erman Acar, Stefan Schlobach, Yisong Wang, Wanwei Liu

链接:https://arxiv.org/abs/2003.06492

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 实现OCC模型的可视化简体汉字情感仿真器(cs AI)

    在这篇论文中,我们提出了一个可视化的仿真人物在故事中的情绪。该系统基于Ortony、Clore和Collins (OCC模型)对情绪认知结构的简化观点。本文的目...

    RockNPeng
  • 用于检测眼动数据中的混淆的神经体系结构(CS AI)

    受到深度学习在各个领域的成功的鼓舞,我们研究了其方法在眼动数据中检测用户混乱的有效性方面的新颖应用。 我们介绍一种并行使用RNN和CNN子模型的架构,以利用我们...

    RockNPeng
  • 使用多模式低秩双线性注意力网络融合的并行意图和插槽预测(CS AI)

    目的和位置识别是语音理解(SLU)中的两个重要任务。对于自然语言的话,这两个任务之间有很高的相关性。使用递归神经网络(RNN),卷积神经网络(CNN)和基于注意...

    RockNPeng
  • 【论文推荐】最新5篇图像分割相关论文—条件随机场和深度特征学习、移动端网络、长期视觉定位、主动学习、主动轮廓模型、生成对抗性网络

    【导读】专知内容组整理了最近五篇视觉图像分割(Image Segmentation)相关文章,为大家进行介绍,欢迎查看! 1. Conditional Rand...

    WZEARW
  • 研究用于社交媒体中仇恨语音检测的深度学习方法(CS CL)

    互联网的迅猛发展有助于增强个人的表达能力,但滥用表达自由的行为也导致各种网络犯罪和反社会活动的增加。仇恨言论就是一个这样的问题,需要非常认真地解决,否则,这可能...

    刘子蔚
  • 原创译文 | 区块链不仅仅是技术,而是新的经济体系

    转载声明 本文为灯塔大数据原创内容,欢迎个人转载至朋友圈,其他机构转载请在文章开头标注:“转自:灯塔大数据;微信:DTbigdata” 导读:上一期了解了关于将...

    灯塔大数据
  • 2017美国数学建模MCM C题(大数据)翻译 “合作和导航”

    Traffic capacity is limited in many regions of the United States due to the numb...

    AI那点小事
  • 《风格的要素》中的编程格言

    之所以翻译这篇文章,因为它与我之前关于如何/为什么要写出更易懂的代码的思考有很多关联,但更进一步的是,这篇文章直接指出了写作与编程在原则上的相似性,本质上他们都...

    ThoughtWorks
  • 【论文推荐】最新九篇目标检测相关论文—常识性知识转移、尺度不敏感、多尺度位置感知、渐进式域适应、时间感知特征图、人机合作

    【导读】专知内容组整理了最近七篇目标检测(Object Detection)相关文章,为大家进行介绍,欢迎查看! 1.Single-Shot Object De...

    WZEARW
  • 【论文推荐】最新八篇目标跟踪相关论文—自适应相关滤波、因果关系图模型、TrackingNet、ClickBAIT、图像矩模型

    【导读】专知内容组整理了最近八篇目标跟踪(Object Tracking)相关文章,为大家进行介绍,欢迎查看! 1. Adaptive Correlation ...

    WZEARW

扫码关注云+社区

领取腾讯云代金券