An efficient simulation algorithm on Kripke structures |
| |
Authors: | Francesco Ranzato |
| |
Affiliation: | 1. Dipartimento di Matematica, University of Padova, Padova, Italy
|
| |
Abstract: | A number of algorithms for computing the simulation preorder (and equivalence) on Kripke structures are available. Let $\varSigma $ denote the state space, ${\rightarrow }$ the transition relation and $P_{\mathrm {sim}}$ the partition of $\varSigma $ induced by simulation equivalence. While some algorithms are designed to reach the best space bounds, whose dominating additive term is $|P_{\mathrm {sim}}|^2$ , other algorithms are devised to attain the best time complexity $O(|P_{\mathrm {sim}}||{\rightarrow }|)$ . We present a novel simulation algorithm which is both space and time efficient: it runs in $O(|P_ {\mathrm {sim}}|^2 \log |P_{\mathrm {sim}}| + |\varSigma |\log |\varSigma |)$ space and $O(|P_{\mathrm {sim}}||{\rightarrow }|\log |\varSigma |)$ time. Our simulation algorithm thus reaches the best space bounds while closely approaching the best time complexity. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|