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).

翻译：我们提出了一种通用算法，用于构造区分系统中行为不等价状态的公式，该系统可涵盖非确定性、概率性或加权等多种变迁类型；通过在全称共代数范式中对集合函子进行共代数操作，实现了对变迁类型的通用性。对于给定系统中的每个行为等价类，我们构造一个公式，该公式精确地在该类中的状态上成立。该算法可实例化至确定性有限自动机、变迁系统、带标签马尔可夫链以及多种其他类型的系统。环境逻辑是一种模态逻辑，其特征模态从函子中通用提取；这些模态可在后续处理步骤中系统地转化为定制模态集。新算法基于现有的共代数划分精化算法构建。在具有n个状态和m个变迁的系统上，其运行时间为O((m+n) log n)，且相同的渐近界适用于所构造公式的有向无环图规模。相较于先前的算法，即使对于先前已知的具体实例（如变迁系统和马尔可夫链），该算法在运行时间和公式规模上均改进了界值；特别是，变迁系统的最佳先前界值为O(mn)。