Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
This provides a theoretical framework for verification in computer science, but it appears incremental as it extends existing categorical concepts to specific fibrational settings.
The paper tackles the problem of verifying inductive properties like liveness by identifying a fibrational condition for the coincidence of initial algebras and final coalgebras, which allows using coinductive witnesses such as invariants. It demonstrates practical benefits through new witness notions for probabilistic liveness and tree automata verification problems.
The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.