一句话：提出在余代数框架下通用构造区分行为不等价状态的模态公式的拟线性时间算法，统一覆盖多种迁移系统。
该论文研究如何为行为不等价的状态构造可区分的模态公式，即见证。作者在通用余代数范式下，针对集合函子的余代数给出通用算法：对每个行为等价类构造一个恰好在该类状态上成立的公式，其模态由函子通用提取，并可在后处理中翻译为具体模态。算法建立在已有的余代数划分精化算法之上，适用于确定性有限自动机、迁移系统、标记马尔可夫链等多种系统。在 n 个状态、m 个迁移的系统上，运行时间为 O((m+n) log n)，所构造公式的 DAG 大小也有相同渐近界，优于此前针对迁移系统和马尔可夫链等特例的最佳界（如迁移系统的 O(mn)）。
We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time O((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was O(mn).
@article{paperbot1643,
title = {Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence},
author = {Thorsten Wißmann and Stefan Milius and Lutz Schröder},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 4},
year = {2022},
doi = {10.46298/lmcs-18(4:6)2022}
}