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 on the MC that are accepted by the DFA. A standard approach to solving this problem constructs a product MC of the given MC and DFA, reducing the task to a simple reachability probability problem on the resulting product MC. In this paper, on top of our recent development of coalgebraic 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. This no-go theorem is established via 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. The problem is reduced to solving linear equations, which is solvable in polynomial-time under a reasonable assumption that ensures the finiteness of the solution.

翻译：系统迹的验证是形式化验证的核心课题。我们研究了马尔可夫链（MC）相对于以（有限）自动机表示的时序性质的模型检测。例如，给定一个MC和一个确定性有限自动机（DFA），一个简单但具有实际应用价值的模型检测问题要求计算MC上被DFA接受的（终止）迹的概率。解决该问题的标准方法是通过构造给定MC与DFA的乘积MC，将任务转化为对所得乘积MC上的简单可达概率问题求解。本文基于我们近期发展的余代数框架，首先提出了关于积构造的一个不可能性定理，展示了在模型检测中无法进行积构造的一种情形。具体而言，我们证明了不存在用于计算接受迹概率的MC与非确定性有限自动机（NFA）的余代数积MC。该不可能性定理是通过刻画决定分支类型（包括非确定性或概率性分支）的特定函子间的自然变换而建立的。其次，我们提出了MC与多重集有限自动机（MFA）的余代数积构造，作为我们框架中的一个新实例。该构造处理了一个模型检测问题，该问题要求计算MFA在MC迹上的接受运行次数的期望值。该问题被简化为求解线性方程组，在确保解有限性的合理假设下，该方程组可在多项式时间内求解。