Verifying traces of systems is a central topic in formal verification. We study model checking of Markov chains (MCs) against temporal properties represented as (finite) automata. For instance, given an MC and a deterministic finite automaton (DFA), a simple but practically useful model checking problem asks for the probability of (terminating) traces accepted by the DFA, which can be computed via a product MC of the given MC and DFA and reduced to a simple reachability problem. Recently, Watanabe, Junges, Rot, and Hasuo proposed coalgebraic product constructions, a categorical framework that uniformly explains such coalgebraic constructions using distributive laws. This framework covers a range of instances, including the model checking of MCs against DFAs. In this paper, on top of their framework we first present a no-go theorem for product constructions, showing a case when we cannot do product constructions for model checking. Specifically, we show that there are no coalgebraic product MCs of MCs and nondeterministic finite automata for computing the probability of the accepting traces. The proof relies on a characterisation of natural transformations between certain functors that determine the type of branching, including nondeterministic or probabilistic branching. Second, we present a coalgebraic product construction of MCs and multiset finite automata (MFAs) as a new instance within our framework. This construction addresses a model checking problem that asks for the expected number of accepting runs on MFAs over traces of MCs. We show that this problem is solvable in polynomial time.

翻译：系统迹的验证是形式化验证的核心课题。我们研究了马尔可夫链（MC）相对于以（有限）自动机表示的时序性质的模型检测。例如，给定一个MC和一个确定性有限自动机（DFA），一个简单但实际有用的模型检测问题要求计算被DFA接受的（终止）迹的概率，这可以通过给定MC和DFA的积MC来计算，并简化为一个简单的可达性问题。最近，Watanabe、Junges、Rot和Hasuo提出了余代数积构造，这是一个使用分配律统一解释此类余代数构造的范畴论框架。该框架涵盖了一系列实例，包括MC相对于DFA的模型检测。在本文中，基于他们的框架，我们首先提出了一个关于积构造的不可能性定理，展示了在模型检测中无法进行积构造的情形。具体而言，我们证明了不存在用于计算接受迹概率的MC与非确定性有限自动机（NFA）的余代数积MC。该证明依赖于确定分支类型（包括非确定性或概率分支）的特定函子间自然变换的刻画。其次，我们提出了MC与多重集有限自动机（MFA）的余代数积构造，作为我们框架中的一个新实例。该构造解决了一个模型检测问题，该问题要求计算在MC的迹上MFA的接受运行次数的期望值。我们证明该问题可在多项式时间内求解。