模型检验：一种余代数方法

状态爆炸问题是模型检验的主要障碍。在本文中，我们尝试从余代数方法解决这一问题。我们建立了一种有效方法，用于一致地证明关于互模拟的最小的Kripke结构的存在性，该结构描述了Kripke结构的所有行为且无冗余。我们随后证明，对于每个给定的有限Kripke结构以及某些类型的无限Kripke结构，这个最小的Kripke结构生成一个具体的最小结构。该方法基于适当自函子的终余代数的存在性，并可平滑地推广到其他余代数结构。该方法的一个朴素实现在Ocaml中开发。