2012/12/05 by Francesco Ranzato, Ranzato, Francesco
Computer Science · #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #cs.DS #cs.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1212.1089
Conference version appeared in Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13)
openalex publication_date 2012/12/05 · arxiv created 2013/07/29 · arxiv updated 2013/07/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.