An Efficient Simulation Algorithm on Kripke Structures

TL;DR

This paper introduces a new simulation algorithm for Kripke structures that is both space and time efficient, achieving near-optimal bounds and improving computational performance for model checking tasks.

Contribution

The paper presents a novel simulation algorithm that combines optimal space complexity with near-optimal time complexity for Kripke structure analysis.

Findings

Runs in O(|Psim|^2 log|Psim| + |Sigma|log|Sigma|) space

Operates in O(|Psim||->|log|Sigma|) time

Achieves best space bounds while closely approaching best time complexity

Abstract

A number of algorithms for computing the simulation preorder (and equivalence) on Kripke structures are available. Let Sigma denote the state space, -> the transition relation and Psim the partition of Sigma induced by simulation equivalence. While some algorithms are designed to reach the best space bounds, whose dominating additive term is |Psim|^2, other algorithms are devised to attain the best time complexity O(|Psim||->|). We present a novel simulation algorithm which is both space and time efficient: it runs in O(|Psim|^2 log|Psim| + |Sigma|log|Sigma|) space and O(|Psim||->|log|Sigma|) time. Our simulation algorithm thus reaches the best space bounds while closely approaching the best time complexity.