Apr, 2024

监控二阶超属性

PDF
TL;DR本文研究了复杂超性质的运行时监测问题，并提出了第一个适用于更具表达能力的二阶超性质的监测算法 Hyper$^2$LTL$_f$。我们探讨了并行模型和顺序模型下的监测问题，并通过优化算法提高了二阶量化的效率。实验结果验证了算法的有效性。
hyperpropertiesmonitoring algorithmsecond-order hyperpropertieshyper$^2$ltl$_f$sequential model
发现论文，激发创造
  • 超属性验证的非确定性规划

    验证超性质的自动化的算法，通过构建一个非确定性多机器人规划实例，确保一个规划存在则满足验证问题。

    May, 2024

  • 概率超性质的演绎式控制合成

    提出了一种新的方法来解决马尔可夫决策过程（MDPs）和概率超性质的控制器合成问题，该方法在超级概率计时逻辑（HyperPCTL）的基础上增加了合成控制器的结构约束，采用逐步修正策略修剪搜索空间并与先前的 SMT 模型检查工具相比取得了显著的性能改进。

    Jul, 2023

  • 用属性规范语言学习可解释模型

    本文主要介绍了一种用于从有限集的正面和负面例子中学习复杂系统可解释性描述的算法，通过在 IEEE 标准时间逻辑 PSL (Property Specification Language) 中学习公式来解决此问题，并比较了与现有 LTL 学习算法的效果。

    Feb, 2020

  • 关于交替时间逻辑、超属性和策略共享的研究

    HyperATLS$^*_S$ 是 ATL$^*$ 的扩展，可以比较多个战略互动的结果，并强制要求一些代理共用相同策略。它是一个丰富的规范语言，可以捕捉现有逻辑无法达到的重要 AI 相关属性。我们证明了在并发博弈结构上对 HyperATL$^*_S$ 的模型检查是可判定的，并在一系列基准测试中使用我们的模型检查算法实施，并对其进行评估。

    Dec, 2023

  • 度量时态逻辑中高效可监测公式的合成

    自动从系统执行中合成形式规范的学习算法，以实现有效可监控的 Metric Temporal Logic (MTL) 公式的综合。

    Oct, 2023

  • 描述逻辑进入二阶：使用全量量化概念扩展 EL

    该论文涉及描述逻辑的特性，首次引入普遍量化的概念，提出两种扩展的语义模型，包括模态逻辑中的公理原型和二阶逻辑中的量词的替代。研究表明，在某些扩展的语义中，所得出的结论与经典的描述逻辑相符，并证明了某种程度上用于这种扩展的算法的多项式可判定性。

    Aug, 2023

  • 使用超属性验证全局神经网络规范

    本研究引入超属性形式主义，提供了表达全局规范的方法，可以通过利用验证通用计算图形的能力验证全局规范，从而扩大了使用现有方法提供的保证范围。

    Jun, 2023

  • 基于模型设计的智能物理系统中的参数时序逻辑属性挖掘

    本文提出了一种针对具有多个参数的度量或信号时间逻辑（MTL 或 STL）的规范的框架，该框架可以自动地推断参数的范围，以便系统未满足属性标准。同时，我们还提供了用于多参数规范探索和可视化的算法，并且在实际工业应用引擎模型以及相关文献的例子中进行了演示。

    Dec, 2015

  • HyperMono: 超关联知识表示的一种考虑单调性的方法

    该研究论文提出了 HyperMono 模型，用于超关联知识图谱的完成，在考虑两个重要特性的基础上，通过阶段推理和限定性单调性实现了强大的性能。

    Apr, 2024

  • 超级策略逻辑

    提出了 Hyper Strategy Logic（HyperSL）作为多路径比较的战略逻辑，并给出了该逻辑的模型检查算法和实现。

    Mar, 2024