Mar, 2022

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

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

    本文研究基于关系型数据中心动态系统的（一阶）μ 演算验证，展示了在一些特殊情况下可决定性成立，并提供了一些避免不可决情况的句法条件，构建了一些注意到每个服务调用激活会生成新值的新概念以避免无限积累问题。

    Feb, 2012

  • 带算术条件的数据感知过程的准确性

    本研究提供了一个建立在基础和操作框架之上的 DPN 合法性评估方法，其具备算术数据条件，评估方法采用了 SMT 技术在文献和合成集合范例中得到了验证。

    Mar, 2022

  • 使用线性时间微积分理论模拟动态系统

    本文研究在一个规范上执行广泛的推断任务的可行性，通过将 IDP3 扩展到与动态规范相关的领域中使用的多种推断技术。

    May, 2014

  • 基于数据驱动的时态逻辑推理的开关非线性系统模型鉴别

    本文研究数据驱动模型识别的问题，提出了逼近未知动态和推断未知逻辑规范的数据驱动方法，并利用基于优化的算法分析了学习 / 推断的模型 - 任务对的区别，为该集合中与新观察不一致的模型 - 任务对规定模型推断的逻辑规范的大小，以增加模型鉴别算法的计算效率。

    Jun, 2023

  • 通过高斯过程回归形式化验证未知动态系统

    本文提出了一个基于高斯过程回归的验证框架，将连续空间系统抽象为有限状态不确定马尔可夫决策过程，利用模型检测工具验证抽象的不确定性，并将结果扩展到基础的部分可观测系统，有效地应用于线性、非线性和切换系统等多种情况下。

    Dec, 2021

  • 对比时空抽象概括和比较代理动态

    本文提出了一种数据驱动、模型无关的技术，用于生成一个易于人理解的摘要，概括一个演变动力系统（如控制代理的学习过程）中的显著对比要点。该技术根据信息论差异度沿时间和空间维度对转换数据进行聚合，并以图形和文本通信方法为辅助，对连续状态空间下的深度强化学习代理的学习历史进行摘要。我们期望我们的方法能够补充现有的代理可解释性技术。

    Jan, 2022

  • Warded Datalog+- 中算术的复杂性

    本文定义了一种新的语言，将 Warded Datalog+- 扩展到算术，证明了其 P 完备性，并为一种最近引入的整数算术 Datalog 片段提供了描述性复杂度结果，为高度表达 Datalog+- 语言奠定了理论基础，这些语言结合了先进递归规则和算术的优势，同时保证了现代 AI 系统中应用的高效推理算法，例如知识图谱。

    Feb, 2022

  • DLV 系统中聚合函数的设计与实现

    通过在视角内引入聚合函数，我们将 DLP（Disjunctive Logic Programming）这种表达有限结构性质的表达形式进行扩展，以便更好地表示复杂的实际应用属性，并保持语言的可判定性和计算复杂度不变。

    Feb, 2008

  • 度量动态均衡逻辑

    在这篇研究论文中，我们发展了基于时间序列的线性时间扩展的动态均衡逻辑的度量扩展，它通过整数区间对动态运算符进行约束，从而提供了用于指定定性和定量动态约束条件的基于 ASP 的方法。

    Jan, 2024

  • 信息分享系统中战略能力的模型验证

    本文介绍了一种带有私有数据共享能力的不完美信息的并发博弈结构子类，这些结构可以通过特定的 ATL 片段模型检查，被称为 A-cast 系统，可以编码安全领域的复杂问题，如身份验证中的恐怖主义欺诈攻击。

    Apr, 2022