Aug, 2022

关系型动作基础：形式化、有效的安全验证和不变量（扩展版）

HTML
PDF
TL;DR介绍了关系型动态系统的建模和验证问题，提出了关系型动作基础（RABs）的通用框架，并通过（近似）基于SMT的反向搜索研究了RABs的参数化安全性，展示了这种方法在数据感知业务流程基准测试中的有效性，最后展示了如何利用通用不变量使得这个过程完全正确。
发现论文，激发创造
  • 概率模型的抽象化：逻辑视角

    本文提供了一个基于语义的框架，旨在分析高层次建模与其低层次对应模型间的一致性，以及针对概率模型的抽象方法和自动推导方法。

    Oct, 2018

  • 存在规则语言的模型论描述

    本研究旨在模型理论中建立存在规则语言的模型论特性，如嵌入依赖项，元组生成依赖项和线性依赖项，并确定它们的复杂度限制。

    Jan, 2020

  • 具算术的数据感知动态系统的线性时间验证

    本文研究了数据感知动态系统的模型和验证，并将其扩展为线性算术。我们提出了“有限总结”的新语义属性，展示了有限总结对于DDS的线性时间、有限跟踪性质的证明是可判定的，并且展现了有限总结在形式方法和数据库理论中的具体应用。此外，我们展示了有限总结抽象的统一性质如何导致模块化结果。最后，我们演示了在原型实现中使用我们的方法的可行性。

    Mar, 2022

  • 使用类型自然推理系统检查概率计算的可信度

    介绍了一种概率类型的自然推导演算法，能够推导出概率计算过程的可信性，并通过对频率和预期概率之间的距离进行假设检验来形式化信任。该演算法在验证自动分类算法方面有潜在应用。

    Jun, 2022

  • AI中的构造正确执行时强制执行-一项调查

    本文探讨了针对AI安全方面的应用开发运行时执行方式，介绍了监管工具的选型、适用的离散/连续动作空间等相关技术细节，旨在提高我们对不同执行应用的理解及未来应用方向。

    Aug, 2022

  • 在关系领域中从示例中学习概率时间安全属性

    在关系集合中，我们结合关系Markov决策过程与pCTL模型检查，提出了一个框架，从一组被标记为安全或不安全的状态中学习pCTL公式的片段。应用关系学习的原则，我们介绍了候选公式生成过程和为标记状态决定满意的规范的方法，以此作为该领域的安全说明。最后在合成的关系领域上评估了该方法。

    Nov, 2022

  • 逻辑谜题中的非对称性探究：利用Zero-suppressed Decision Diagrams进行符号化模型检验的动态认知逻辑

    本研究比较了不同 Zero-suppressed Decision Diagrams 变体在多智能体系统的符号编码中的记忆使用情况，结果表明使用合适的 ZDDs 可以显著减少 BDDs 的记忆使用量。

    Jul, 2023

  • 多智能体仅信仰的基于基础的模型检验（长篇）

    我们提出了一种新的关于多智能体仅信任利用信任基础的语言的语义，并展示了如何将其用于自动检查该语言及其具有私有信念扩展运算符的动态扩展的公式。我们提供了一个依赖于QBF和另一种专用算法的PSPACE模型检查算法，并提出了基于QBF的算法的实现和一个具体实例的计算时间的一些实验结果。

    Jul, 2023

  • 利用大型语言模型发现归纳循环不变量

    本文通过使用大语言模型，探索了在自动程序验证中找到归纳循环不变量的新方法，并证明了其可以改进目前的技术水平。

    Nov, 2023

  • 基于对象的同步一致性对齐（扩展版本）

    该研究论文提出了一种新的形式主义，结合了现有方法的关键建模特性，特别是以对象为中心的Petri网捕捉一对多的关系，以及具有标识符的Petri网根据对象的身份比较和同步。我们称之为'具有标识符的以对象为中心的Petri网'，并定义了此设置的对齐和符合性检查任务。我们提出了一种基于在满足性模理论中的编码的形式主义进行的一致性检查方法，并说明了如何有效地克服先前工作的缺点。为了评估其实用性，我们对文献中的数据进行了评估。

    Dec, 2023