论文标题
对行为不等值的通用模态证人的准时间计算
Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence
论文作者
论文摘要
我们为构建公式提供了一种通用算法，该公式可以区分各种过渡类型的系统中的行为不相等状态，例如非确定性，概率或加权；过渡类型的通用性是通过与山地合作在通用山地范式中的SET函子合作实现的。对于给定系统中的每个行为等价类别，我们构建了一个公式，该公式恰好符合该类别的状态。该算法实例化以确定有限的自动机，过渡系统，标记的马尔可夫链和许多其他类型的系统。环境逻辑是一种模态逻辑，具有通常从函子中提取的模态。这些模式可以在后处理步骤中系统地转化为自定义方式集。新算法建立在现有的Calgebraic分区改进算法的基础上。它在具有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).
