Distributed Branching Bisimulation Minimization by Inductive Signatures

Research output: Book/ReportReportProfessional

5 Citations (Scopus)
37 Downloads (Pure)

Abstract

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.
Original languageUndefined
Place of PublicationEnschede
PublisherFormal Methods and Tools (FMT)
Number of pages18
Publication statusPublished - 9 Oct 2009

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology
No.TR-CTIT-09-37
ISSN (Print)1381-3625

Keywords

  • EWI-11506
  • EC Grant Agreement nr.: FP6/043235
  • IR-68145
  • METIS-263678

Cite this

Blom, S., & van de Pol, J. C. (2009). Distributed Branching Bisimulation Minimization by Inductive Signatures. (CTIT Technical Report Series; No. TR-CTIT-09-37). Enschede: Formal Methods and Tools (FMT).
Blom, Stefan ; van de Pol, Jan Cornelis. / Distributed Branching Bisimulation Minimization by Inductive Signatures. Enschede : Formal Methods and Tools (FMT), 2009. 18 p. (CTIT Technical Report Series; TR-CTIT-09-37).
@book{d9c5af5acd8c479891dacd1b2498a5a8,
title = "Distributed Branching Bisimulation Minimization by Inductive Signatures",
abstract = "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.",
keywords = "EWI-11506, EC Grant Agreement nr.: FP6/043235, IR-68145, METIS-263678",
author = "Stefan Blom and {van de Pol}, {Jan Cornelis}",
year = "2009",
month = "10",
day = "9",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Formal Methods and Tools (FMT)",
number = "TR-CTIT-09-37",

}

Blom, S & van de Pol, JC 2009, Distributed Branching Bisimulation Minimization by Inductive Signatures. CTIT Technical Report Series, no. TR-CTIT-09-37, Formal Methods and Tools (FMT), Enschede.

Distributed Branching Bisimulation Minimization by Inductive Signatures. / Blom, Stefan; van de Pol, Jan Cornelis.

Enschede : Formal Methods and Tools (FMT), 2009. 18 p. (CTIT Technical Report Series; No. TR-CTIT-09-37).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Distributed Branching Bisimulation Minimization by Inductive Signatures

AU - Blom, Stefan

AU - van de Pol, Jan Cornelis

PY - 2009/10/9

Y1 - 2009/10/9

N2 - 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.

AB - 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.

KW - EWI-11506

KW - EC Grant Agreement nr.: FP6/043235

KW - IR-68145

KW - METIS-263678

M3 - Report

T3 - CTIT Technical Report Series

BT - Distributed Branching Bisimulation Minimization by Inductive Signatures

PB - Formal Methods and Tools (FMT)

CY - Enschede

ER -

Blom S, van de Pol JC. Distributed Branching Bisimulation Minimization by Inductive Signatures. Enschede: Formal Methods and Tools (FMT), 2009. 18 p. (CTIT Technical Report Series; TR-CTIT-09-37).