行为非等价的通用模态证明的准线性时间计算
摘要：用于构造在各种过渡类型（如非确定性、概率性或加权）系统中行为等价状态的公式的通用算法的一项提供。通过在通用同态的范例中使用集合函子的同同态（universal coalgebra）实现了过渡类型的通用性。对于给定系统中的每个行为等价类，我们构造出一个在该类中精确地成立的公式。该算法可用于确定有限自动机、过渡系统、标记马尔可夫链和许多其他类型的系统。该环境逻辑是一种包含从函子中一般提取的特征模态的模态逻辑。这些模态可以在后期处理阶段中系统地转换为自定义模态集合。这一新算法基于现有的同同态分区细化算法。在具有n个状态和m个转换的系统上，其运行时间为O((m+n)log n)，并且对所构建的公式的dag大小也适用相同的渐进界限。与以前的算法相比，即使是对于先前已知的特定实例（如过渡系统和马尔可夫链），它也改善了运行时间和公式尺寸的界限；特别地，过渡系统的最佳先前界限为O(mn)。
作者：Thorsten Wi{ss}mann, Stefan Milius, Lutz Schr"oder
论文ID：2203.11175
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22