A No-go Theorem for Coalgebraic Product Construction
Mayuko Kori, Kazuki Watanabe
TL;DR
The work investigates coalgebraic composition for model checking probabilistic systems by combining Markov chains with automata under a distributive-law framework. It proves a no-go theorem: there exists no coalgebraic product of MCs and NFAs that satisfies the standard correctness criterion for accepting traces. It also introduces a polynomial-time coalgebraic product for MCs and MFAs that computes the expected number of accepting runs by reducing to a system of linear equations. Together, these results delineate fundamental limits of coalgebraic product constructions and present a practical alternative for MCs with MFAs, clarifying the role of natural transformations between branching functors.
Abstract
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.