A Coalgebraic Representation of Reduction by Cone of Influence

The Cone of Influence Reduction is a fundamental abstraction technique for reducing the size of models used in symbolic model checking. We develop coalgebraic representations of systems as composites of state transition maps and connectors. These representations include synchronous systems, asynchronous systems, asynchronous systems with synchronization by channels, and those with shared variables, probabilistic synchronous systems and so on. We schematically show the cone of influence reduction using these coalgebraic representations, which give a unified framework for providing the technique for various kinds of systems.