MightyPPL：带过去和普劳尔模态的 MITL 验证
形式语言与自动机理论
2025-10-03 v1 计算机科学中的逻辑
摘要
度量区间时序逻辑（MITL）是指定具有时序约束的响应系统属性的流行形式。然而，现有的 MITL 用于验证任务的现有方法存在显著缺点：要么支持逻辑的有限片段，要么仅允许不完整的验证。本文引入 MightyPPL，一个用于将带过去和普劳尔模态的 MITL 公式（MITPPL）在点语义下翻译为时序自动机的新工具。MightyPPL 使能够对更具表达力的规格逻辑进行满意性和模型检查，适用于有限和无限单词，并包含若干性能优化，包括对转换的 novel 符号编码以及导致可达离散状态数指数级减少的对称性归约技术。对于给定的 MITPPL 公式，MightyPPL 可生成时序自动机网络或单个与多个验证后端（包括 Uppaal、TChecker 和 LTSmin）语言等价且兼容的单个时序自动机，这些后端支持多核模型检查。我们在各种案例研究和配置选项上评估了该工具链的性能。
引用
@article{arxiv.2510.01490,
title = {MightyPPL: Verification of MITL with Past and Pnueli Modalities},
author = {Hsi-Ming Ho and Shankara Narayanan Krishna and Khushraj Madnani and Rupak Majumdar and Paritosh Pandya},
journal= {arXiv preprint arXiv:2510.01490},
year = {2025}
}