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接受运行期望次数的模型检测问题。我们证明该问题可在多项式时间内求解。