首页/论文/1706.02701

arXiv 1706.027012017-06-08cs.LO

从模型检验到部分模型的时间证明：初步实例

From model checking to a temporal proof for partial models: preliminary example

A. Bernasconi, C. Menghi, P. Spoletini, L. D. Zuck, C. Ghezzi

备注：: 5 pages, 3 figures

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文详细介绍了THRIVE初步评价中介绍的实例。具体而言，它评估了为验光师和眼科医生用于检测视觉问题的医疗器械的关键组件提出的基础模型的抽象THRIVE。

英文摘要：

This paper describes in detail the example introduced in the preliminary evaluation of THRIVE. Specifically, it evaluates THRIVE over an abstraction of the ground model proposed for a critical component belonging to a medical device used by optometrists and ophtalmologits to dected visual problems.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

基于逻辑的部分模型的模型检验与模型综合

Model checking and model synthesisfrom partial models: a logic-based perspective

我考虑以下一般情况：一个抽象的模型M的一些“真正的”系统只是部分介绍，或部分已知的，我们必须确保实际的系统满足给定的规范，形式化的一些逻辑语言。这种情况至少有两个本质上不同的解释，导致两个本质上不同的形式逻辑和算法问题：“部分模型的模型合成”，其中M到完整模型的一些“可接受”扩展必须满足规范，和“部分模型的模型检验”，其中M到完整模型的所有“可接受”扩展必须满足规范。这些问题自然地扩展了经典的可满足性、有效性和模型检验的逻辑决策问题。在这里，我简要地讨论这两个问题的背景下，经典，模态和时间逻辑。我做了一些观察，状态一些开放的问题，并概述了一个一般的表格式的程序，解决了几个著名的模态和时序逻辑，包括有限的部分模型的无约束模型合成的问题。K、LTL、CTL、ATL。

2020-12-22cs.LO

基于标号迁移系统和Boole方程系统网络的部分模型检验

Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems

部分模型检验是Andersen于1995年提出的一种基于过程组合的时序逻辑公式检验方法。它包括将从一个过程中获取的行为信息逐步纳入公式-一个称为“验证”的操作-以获得一个新的公式，该公式可以在较小的组合物上进行验证，该组合物中已去除了所纳入的过程。必须在每一步对公式进行简化，以便使公式保持在易于处理的规模。在本文中，我们重温部分模型检验。首先，我们扩展到网络的标记的过渡系统模型，其中包括大多数并行组合运算符，包括m-之间的n同步和并行组合使用同步接口，可在CRTOS标准。其次，我们重新制定一个简单的同步产品之间的图形表示的公式（称为公式图）和一个过程中，从而使recruenting被有效地和容易地实现，通过重用现有的工具专用于图形组合物。第三，我们提出了简化的公式作为一个组合的互模拟和减少使用布尔方程系统直接应用到公式图，从而使公式简化也可以有效地实现。最后，我们描述了在CADP（分布式进程的构建和分析）工具箱中的实现，并提出了一些实验结果，其中部分模型检验使用的内存比飞行模型检验少几百倍。

2013-09-30cs.LO

目标导向回答集程序设计中的动态一致性检验

Dynamic Consistency Checking in Goal-Directed Answer Set Programming

在回答集编程中，当程序上的约束变得不可满足时，就会出现不一致。在本文中，我们介绍了一种技术，为我们的目标导向的方法计算答案集的动态一致性检查，只有那些被认为是相关的部分答案集的约束进行测试，允许不一致的知识库被成功地查询。然而，该算法保证，如果一个程序至少有一个一致的答案集，返回的任何部分答案集将是某个一致答案集的子集。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）

2014-05-14cs.LO

（ω-）正则模型检验中处理线性时态性质的框架

A Framework to Handle Linear Temporal Properties in (ω-)Regular Model Checking

自从几年前这个话题出现以来，关于定期模型检验的工作主要致力于状态可达性和安全性的验证。虽然人们知道，线性时间属性也可以在这个框架内检查，很少有人做了工作，以解决相应的细节。本文解决了这个问题的背景下，定期模型检验的基础上编码的状态由有限或无限的话。它工作的确切结构，在这两种情况下使用，并提出了一个部分解决方案的问题所产生的事实，无限计算的无界配置可能永远不会包含相同的配置两次，从而使循环检测的问题。

2009-01-26cs.LO

具有知识、不完全信息、完全回忆和通信联盟的交替时序逻辑的模型检验

Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions

我们提出了一个变体的ATL与分布式知识运营商的基础上同步和完善的召回语义。这种逻辑中的联盟模式是基于对完整历史的部分观察，并结合了联盟成员之间的合作形式，其中代理基于该联盟的系统历史的分布式知识发布其行动。我们表明，模型检验是可判定的这种逻辑。该技术利用两个变种的游戏与不完美的信息和部分可观察的目标，以及一个子集的建设，用于识别状态的历史是无法区分的考虑联盟。

2010-06-08cs.LOcs.MA

保结巴偏序约简的不一致标号问题

The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

在模型检验中，偏序约简（POR）是一种减小状态空间大小的有效方法。顽固集是POR的一个已建立的变体，在过去的31年中有许多应用。顽固集的早期工作之一表明，几个条件的组合的减少是足以保持口吃的痕迹等价，使顽固集适合线性时间属性的模型检验。在本文中，我们确定了一个缺陷的推理和显示与一个反例，口吃迹等价不一定保留。我们提出了一个解决方案连同更新的正确性证明。此外，我们分析在哪些形式主义这个问题可能会发生。对实际实现的影响是有限的，因为它们都计算理论的正确近似。

2019-11-02cs.LO

更多相关论文收起更多论文

概率模型检验与自治

Probabilistic Model Checking and Autonomy

在不确定或对抗性环境中运行的自治系统的设计和控制可以通过正式的建模和分析来促进。概率模型检验是一种自动验证系统模型是否满足时序逻辑规范的技术，同时也是一种综合最优控制策略的技术。这种方法最近已扩展到多智能体系统，表现出竞争或合作行为建模通过随机游戏和合成的均衡策略。在本文中，我们提供了一个概述的概率模型检验，专注于模型支持的PRISM和PRISM游戏模型检查器。这包括完全可观察和部分可观察的马尔可夫决策过程，以及回合制和并发随机游戏，以及相关的概率时间逻辑。我们证明了该框架的适用性，通过说明性的例子自治系统。最后，我们强调了研究的挑战，并建议在这一领域的未来工作方向。

2021-11-20cs.LO

模型检验概率时间认知逻辑的不可判定案例（扩展摘要）

Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic (Extended Abstract)

我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。

2016-06-24cs.LO

概率时间认知逻辑中模型检验的不可判定情形

Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

2015-11-10cs.LO

集成拓扑证明和模型检验的仪器迭代设计

Integrating Topological Proofs with Model Checking to Instrument Iterative Design

系统开发不是一个线性的、一次性的过程。它通过改进和修订进行。为了支持系统满足其需求的保证，最好在每个细化或修订步骤之后执行连续验证。为了实现实际应用，形式化系统建模和验证必须有效地支持持续验证。我们的建议，以解决这个问题是TOrPEDO，一种验证方法，模型通过部分Kripke结构（PKS）和要求指定为线性时间时序逻辑（LTL）属性。PKS支持细化，通过故意指示模型中稍后完成的未指定部分。我们支持两种互补形式的验证：通过模型检验和证明。模型检验可用于提供反例，即，查明违反需求的模型行为。相反，证明是有用的，因为它们可以解释为什么需求得到满足。在我们的工作中，我们引入了一个特定的概念证明，称为拓扑证明（TP）。一个TP产生一个切片的原始PKS证明财产满意度。因为模型可能是不完整的，所以TOrPEDO支持对需求满足、违反和可能满足的推理（在满足取决于未知部分的情况下）。

2018-11-26cs.LO

关于保持停顿的偏序归约中不一致标记问题的详细说明

A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

本文指出保持停顿的偏序归约中一个不一致标记问题，通过反例证明原有条件不充分，提出更强归约条件并给出新正确性证明，分析问题出现的形式化体系。

2021-07-20cs.LO

递归概率程序的时态性质模型检测

Model Checking Temporal Properties of Recursive Probabilistic Programs

本文研究了递归概率程序（pPDA）针对 $ω$-可见下推语言的模型检测问题，给出了可判定性与复杂性结果，证明 CaRet 等逻辑可指定过程调用与返回匹配等结构化性质。

2023-12-14cs.FLcs.LO

单变量TPTL中的开放性与部分邻接性

Openness And Partial Adjacency In One Variable TPTL

该研究针对单变量定时命题时序逻辑（1-TPTL），证明更严格的开放性约束下无法恢复整点性质且可满足性复杂度未降低，还提出部分邻接约束的PA-1-TPTL，证明其可判定且表达能力强于部分整点MTL，是高表达力的可判定定时逻辑。

2024-10-31cs.FLcs.LO

部分谓词抽象和反例引导的精化

Partial Predicate Abstraction and Counter-Example Guided Refinement

在本文中，我们提出了一个反例引导抽象和近似细化（CEGAAR）技术{ \em部分谓词抽象}，它结合了谓词抽象和不动点近似的模型检验无限状态系统。所提出的方法递增地考虑抽象细化的谓词集的增长。该方法的新颖性源于对不精确性来源的认识：抽象或近似。我们使用Craig插值来处理由于抽象而导致的不精确。在由于近似而不精确的情况下，我们延迟近似的应用。我们对各种模型的实验结果提供了深入了解部分谓词抽象的有效性，以及在这种情况下的细化技术。

2017-12-05cs.LOcs.SC

时序逻辑的同步团队语义

Synchronous Team Semantics for Temporal Logics

University of Tübingen（蒂宾根大学）；Institut für Theoretische Informatik, Leibniz Universität Hannover（汉诺威莱布尼茨大学理论计算机科学研究所）；School of Computing Science, University of Glasgow（格拉斯哥大学计算科学学院）；Department of Computer Science, Aalborg University（奥尔堡大学计算机系）

本文为LTL和CTL提出团队语义，使其能表达超性质，研究其计算复杂度并证明带有团队语义的LTL是HyperLTL的可行替代方案。

2026-10-06cs.LO

面向并发软件与系统线性时序逻辑模型检测的最优探索即时展开

On-the-fly Unfolding with Optimal Exploration for Linear Temporal Logic Model Checking of Concurrent Software and Systems

针对并发系统LTL模型检测中的状态爆炸与即时展开难题，本文基于PDNet提出带延迟变迁探索树的最优即时展开算法，实现工具并在基准上优于SPIN与DiVine。

2024-06-12cs.FLcs.LO

基于机器学习和基于轨迹检查的监控实现可解释的早期故障检测

Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring

University of Udine, Italy（乌迪内大学）

针对监控技术中确定性自动机复杂度高的问题，提出将STL纯过去（共）安全片段监控简化为轨迹检查的方法，构建GPU加速的遗传编程学习框架，实现可解释早期故障检测，关键性能指标提升2-10%。

2025-08-25cs.AIcs.FLcs.LG

回答集编程中的路由与调度应用于多智能体路径寻找：初步报告

Routing and Scheduling in Answer Set Programming applied to Multi-Agent Path Finding: Preliminary Report

University of Potsdam（波茨坦大学）；Potassco Solutions（Potassco解决方案公司）；New Mexico State University（新墨西哥州立大学）；Charles University Prague（布拉格查理大学）

本文提出基于偏序的ASP路由与调度方法，应用于多智能体路径寻找，消除时间步与上界限制，并通过实证验证其有效性。

2024-03-18cs.AIcs.LOcs.SC

时间认知逻辑模型检验的丰富反例

Rich Counter-Examples for Temporal-Epistemic Logic Model Checking

模型检验验证系统的模型是否满足给定的属性，否则会产生一个反例来解释违规。验证的性质正式表示在时间逻辑。一些时态逻辑，如CTL，是分支的：它们允许表达关于模型的整个计算树的事实，而不是每个线性计算。当处理多模态逻辑时，这个分支方面甚至更加关键，即用几个转移关系表达系统事实的逻辑。一个突出的例子是CTLK，一个逻辑，原因的时间和认知属性的多智能体系统。一般来说，模型检查器为失败的属性生成线性反例，由模型的单个计算路径组成。但是一些分支性质只能通过一个线性反例来很好地和部分地解释。本文提出了更丰富的反例结构，称为树型注释反例（TLACE），属性的限制性CTL（ARCTL），CTL量化路径的扩展限制在动作标记的模型过渡。这些反例有一个分支结构，支持更完整地描述违反属性。这些反例的元素都注释了部分属性，以便更好地理解它们的结构。这些更丰富的反例的可视化和浏览成为一个关键问题，因为对于深度嵌套的属性，分支和状态的数量可以呈指数级增长。本文形式化地定义了TLACE的结构，刻画了TLACE的充分反例。模型和失效属性，并给出了ARCTL属性的生成算法。它还用CTLK中的例子说明了这种方法，使用CTLK到ARCTL的简化。所提出的方法已经实施，首先通过扩展NuSMV模型检查器来生成和导出分支反例，其次通过提供交互式图形界面来可视化和浏览它们。

2012-02-21cs.LOcs.MA