Distributed Branching Bisimulation Minimization by Inductive Signatures
We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the input graph contains no tau-loops. The optimizatio...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2009-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/0912.2550v1 |
| _version_ | 1811246221251051520 |
|---|---|
| author | Stefan Blom Jaco van de Pol |
| author_facet | Stefan Blom Jaco van de Pol |
| author_sort | Stefan Blom |
| collection | DOAJ |
| description | We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the input graph contains no tau-loops. The optimization in the refinement process is meant to reduce both the number of iterations needed and the memory requirements. In the former case we cannot prove that there is an improvement, but our experiments show that in many cases the number of iterations is smaller. In the latter case, we can prove that the worst case memory use of the new algorithm is linear in the size of the state space, whereas the old algorithm has a quadratic upper bound. The paper includes a proof of correctness of the new algorithm and the results of a number of experiments that compare the performance of the old and the new algorithms. |
| first_indexed | 2024-04-12T14:50:30Z |
| format | Article |
| id | doaj.art-29b369dcb7944346b94ade0b3f114fb9 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T14:50:30Z |
| publishDate | 2009-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-29b369dcb7944346b94ade0b3f114fb92022-12-22T03:28:27ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802009-12-0114Proc. PDMC 2009324610.4204/EPTCS.14.3Distributed Branching Bisimulation Minimization by Inductive SignaturesStefan BlomJaco van de PolWe present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the input graph contains no tau-loops. The optimization in the refinement process is meant to reduce both the number of iterations needed and the memory requirements. In the former case we cannot prove that there is an improvement, but our experiments show that in many cases the number of iterations is smaller. In the latter case, we can prove that the worst case memory use of the new algorithm is linear in the size of the state space, whereas the old algorithm has a quadratic upper bound. The paper includes a proof of correctness of the new algorithm and the results of a number of experiments that compare the performance of the old and the new algorithms.http://arxiv.org/pdf/0912.2550v1 |
| spellingShingle | Stefan Blom Jaco van de Pol Distributed Branching Bisimulation Minimization by Inductive Signatures Electronic Proceedings in Theoretical Computer Science |
| title | Distributed Branching Bisimulation Minimization by Inductive Signatures |
| title_full | Distributed Branching Bisimulation Minimization by Inductive Signatures |
| title_fullStr | Distributed Branching Bisimulation Minimization by Inductive Signatures |
| title_full_unstemmed | Distributed Branching Bisimulation Minimization by Inductive Signatures |
| title_short | Distributed Branching Bisimulation Minimization by Inductive Signatures |
| title_sort | distributed branching bisimulation minimization by inductive signatures |
| url | http://arxiv.org/pdf/0912.2550v1 |
| work_keys_str_mv | AT stefanblom distributedbranchingbisimulationminimizationbyinductivesignatures AT jacovandepol distributedbranchingbisimulationminimizationbyinductivesignatures |