Back to Search
Start Over
An efficient simulation algorithm on Kripke structures.
- Source :
-
Acta Informatica . Mar2014, Vol. 51 Issue 2, p107-125. 19p. - Publication Year :
- 2014
-
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. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 00015903
- Volume :
- 51
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- Acta Informatica
- Publication Type :
- Academic Journal
- Accession number :
- 94741340
- Full Text :
- https://doi.org/10.1007/s00236-014-0195-9