A number of algorithms for computing the simulation preorder are available. The best simulation algorithms are those by Gentilini, Piazza and Poli- criti (GPP) — subsequently corrected by van Glabbeek and Ploeger — and by Ranzato and Tapparo (RT). Let Σ denote the state space, -> the transition relation and Psim the partition of Σ induced by simulation equivalence. The algorithm GPP attains an optimal space bound of O(|Psim|^2 + |Σ| log |Psim|) — where optimal means that the space complexity is of the same order as the size of the output of the algorithm — while it runs in O(|Psim|^2|->|) time. The algorithm RT has the best time bound O(|Psim||->|) while it takes O(|Psim||Σ| log |Σ|) space. We present here a new time and space Efficient Simulation Algorithm (ESA) that runs in O(|Psim||->|) time and O(|Psim|^2 log |Σ| + |Σ| log |Psim|) space. Thus, ESA reaches in practice the optimal space bound of GPP while preserving the best time bound of RT. Analogously to GPP and RT, ESA is a symbolic algorithm, meaning that it maintains and iteratively refines a partition of the state space together with a preorder relation over this partition, while ESA achieves the above complexity bounds by following Hopcroft’s “process the smaller half” principle when updating some crucial data structures involving the blocks of the state partition.

A time and space efficient simulation algorithm

RANZATO, FRANCESCO;
2009

Abstract

A number of algorithms for computing the simulation preorder are available. The best simulation algorithms are those by Gentilini, Piazza and Poli- criti (GPP) — subsequently corrected by van Glabbeek and Ploeger — and by Ranzato and Tapparo (RT). Let Σ denote the state space, -> the transition relation and Psim the partition of Σ induced by simulation equivalence. The algorithm GPP attains an optimal space bound of O(|Psim|^2 + |Σ| log |Psim|) — where optimal means that the space complexity is of the same order as the size of the output of the algorithm — while it runs in O(|Psim|^2|->|) time. The algorithm RT has the best time bound O(|Psim||->|) while it takes O(|Psim||Σ| log |Σ|) space. We present here a new time and space Efficient Simulation Algorithm (ESA) that runs in O(|Psim||->|) time and O(|Psim|^2 log |Σ| + |Σ| log |Psim|) space. Thus, ESA reaches in practice the optimal space bound of GPP while preserving the best time bound of RT. Analogously to GPP and RT, ESA is a symbolic algorithm, meaning that it maintains and iteratively refines a partition of the state space together with a preorder relation over this partition, while ESA achieves the above complexity bounds by following Hopcroft’s “process the smaller half” principle when updating some crucial data structures involving the blocks of the state partition.
Short Talk at the 24th Annual IEEE Symposium on Logic in Computer Science (LICS'09)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/184591
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 2
social impact