基于模拟和双模拟的指标可以用于系统验证和性能评估，适用于定量的 mu - 演算和相关概率逻辑，对于马尔可夫链，我们提供了一个 PSPACE 算法，以匹配最佳算法，并且这些算法可以通过二分搜索来逼近指标。

Sep, 2008

本文针对 MDPs 中 Bisimulation Metrics 的计算提出了新的算法，包括适用于连续状态 MDP 的可微损失函数，其中第一算法通过采样保证收敛性，第二算法通过学习实现了对大规模、确定性 MDP 的近似计算。

Nov, 2019

本文提出 Sinkhorn 距离可以定义 Bisimulation metrics，通过 Bisimulation-based discretization 的 Approximate Policy Iteration 可以在 Actor-Critic methods 中更好的学到状态表示，理论分析和实验结果支持我们的结论。

Feb, 2022

这篇论文研究了加权有限状态自动机和二阶循环神经网络之间的基本联系，提出了一个可靠的算法用于学习在连续输入向量序列上定义的线性二阶循环神经网络。

Jul, 2018

我们提出了一种新的框架，用于在马尔科夫链之间制定最佳输运距离的形式化。我们将此问题转化为在约化空间中求解线性规划的问题，并且通过 Sinkhorn Value Iteration 方法计算最佳输运距离，从而得到与马尔科夫链的 bisimulation metrics 完全匹配的结果。

Jun, 2024

本文运用网络优化和统计抽样技术，克服了计算 Kantorovich 度量在实践中的成本问题，提出了一系列用于 MDP 状态聚合的距离函数，这些函数在时间和空间复杂度以及聚合质量之间存在不同的权衡，并对这些权衡进行了实证评估。

Jun, 2012

我们介绍了一种基于数据驱动的方法来计算具有非常大，可能是无限状态空间的状态转换系统的有限双模拟。我们的新技术计算确定性系统的阻塞不敏感的双模拟，我们将其描述为学习状态分类器与每个类的排名函数的问题。我们的方法从一个有限的样本状态数据集中学习候选状态分类器和候选排名函数；然后，它使用可满足性模理论求解检查这些是否推广到整个状态空间。如果得到肯定答案，该过程得出结论，该分类器构成了系统的有效阻塞不敏感的双模拟。如果得到否定答案，求解器会生成一个反例状态，该状态违反了该分类器的断言，将其添加到数据集中，并在反例引导的归纳合成循环中重复学习和检查，直到找到有效的双模拟。我们在反应性验证和软件模型检查的一系列基准测试中展示了我们的方法在实践中优于其他最先进的工具的更快验证结果。我们的方法产生简洁的抽象，使得能够有效地验证不包含下一个运算符的线性时态逻辑，并且对于系统诊断具有解释能力。

May, 2024

使用回归方法进行等价查询的加权有限状态自动机（WFA）从循环神经网络（RNN）中提取的新算法实现了最近 Weiss、Goldberg 和 Yahav 的 DFA 提取方法的定量 / 加权扩展。

Apr, 2019

该研究提出了用于测量有限马尔可夫决策过程（MDP）状态相似性的度量标准，其基于 MDP 的这种有限状态的相似性概念构建，并可应用于强化学习任务的价值函数逼近器中。通过该度量标准，优化 MDP 中给定状态的最优值与度量距离之间关系的边界得到了提供。

Jul, 2012

本文介绍了如何使用改进的 backward 算法处理带有 failure transitions 的 weighted finite-state automata，方法非常高效，同时也给出了特殊情况下的算法复杂度分析。

Jan, 2023