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

Jul, 2023

本文研究了复杂超性质的运行时监测问题，并提出了第一个适用于更具表达能力的二阶超性质的监测算法 Hyper$^2$LTL$_f$。我们探讨了并行模型和顺序模型下的监测问题，并通过优化算法提高了二阶量化的效率。实验结果验证了算法的有效性。

Apr, 2024

本文探讨了具有标准框架的 POMDPs，以模拟现实世界中存在的不确定性，以及时间逻辑规范。我们研究了帕里目标下的 POMDP 定性分析问题，该问题在理论上难以计算，但我们提出了解决该问题的实用方法，并在许多机器人应用的已知示例中使用了我们的实现。

Sep, 2014

本文研究了具有共同特征的问题集合的一般策略的特征和计算，并介绍了如何通过利用轨迹约束以及 LTL 公式来消除策略的终止条件以及降低规划的复杂度。

Sep, 2019

本文讨论了针对具有博弈均衡策略的并发多智能体系统进行时间逻辑性质检查的合理性验证问题，并提出了减少验证复杂度的有效方法。同时研究了满足社会福利约束条件的多智能体系统的最优策略问题。

Jul, 2022

本文提出了一种使用线性时态逻辑公式生成机器人控制策略的方法，重点考虑了噪声传感器和执行器带来的影响，将其转换为马尔可夫决策过程来解决，包括案例分析。

Apr, 2011

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

Feb, 2020

本文讨论了在 Markov 决策过程中，使用 LTL 的公式作为代理规划的规范，通过形成多目标优化问题，从 MDP 中演示的行为轨迹中推断 LTL 规范，利用遗传编程解决该问题的有效性进行了证明。

Oct, 2017

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

Mar, 2024

本文利用标记的马尔可夫决策过程研究在有多个时间目标的用户偏好下的概率环境中的时间规划。提出了一种新的优先定性选择线性时间逻辑的规范语言，通过对有限的轨迹进行优先排序的连接和有序分离，使得可以简洁地指定每个时间任务的相应优先级。利用该计算模型，提出了一种计算最优策略的问题，该策略以最小化用户偏好的期望不满意度分数为目标。在几个案例研究中，我们演示了该逻辑和算法的有效性和适用性，并对每个案例进行了详细分析。

Apr, 2023