Sigref - A Symbolic Bisimulation Tool Box

Ralf Wimmer; Marc Herbstritt; Holger Hermanns; Kelley Strampp; Bernd Becker

doi:10.1007/11901914_35

Sigref - A Symbolic Bisimulation Tool Box

Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

41 Citations (Scopus)

59 Downloads (Pure)

Abstract

We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation.

We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.

Original language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings
Editors	Susanne Graf, Wenhui Zhang
Publisher	Springer
Pages	477-492
Number of pages	16
ISBN (Electronic)	978-3-540-47238-4
ISBN (Print)	978-3-540-47237-7
DOIs	https://doi.org/10.1007/11901914_35
Publication status	Published - 2006
Event	4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 - Beijing, China Duration: 23 Oct 2006 → 26 Oct 2006 Conference number: 4

Publication series

Name	Lecture notes in Computer Science
Publisher	Springer Verlag
Volume	4218
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006
Abbreviated title	ATVA
Country	China
City	Beijing
Period	23/10/06 → 26/10/06

Keywords

IR-66950
EWI-9273
METIS-238781

Access to Document

10.1007/11901914_35

fulltext
open

Fingerprint Dive into the research topics of 'Sigref - A Symbolic Bisimulation Tool Box'. Together they form a unique fingerprint.

Cite this

Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., & Becker, B. (2006). Sigref - A Symbolic Bisimulation Tool Box. In S. Graf, & W. Zhang (Eds.), Automated Technology for Verification and Analysis: 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings (pp. 477-492). (Lecture notes in Computer Science; Vol. 4218). Springer. https://doi.org/10.1007/11901914_35

Wimmer, Ralf ; Herbstritt, Marc ; Hermanns, Holger ; Strampp, Kelley ; Becker, Bernd. / Sigref - A Symbolic Bisimulation Tool Box. Automated Technology for Verification and Analysis: 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings. editor / Susanne Graf ; Wenhui Zhang. Springer, 2006. pp. 477-492 (Lecture notes in Computer Science).

@inproceedings{ec3f39f52aad4fcc92488891601d3ca6,

title = "Sigref - A Symbolic Bisimulation Tool Box",

abstract = "We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation.We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.",

keywords = "IR-66950, EWI-9273, METIS-238781",

author = "Ralf Wimmer and Marc Herbstritt and Holger Hermanns and Kelley Strampp and Bernd Becker",

year = "2006",

doi = "10.1007/11901914_35",

language = "English",

isbn = "978-3-540-47237-7",

series = "Lecture notes in Computer Science",

publisher = "Springer",

pages = "477--492",

editor = "Susanne Graf and Wenhui Zhang",

booktitle = "Automated Technology for Verification and Analysis",

}

Wimmer, R, Herbstritt, M, Hermanns, H, Strampp, K & Becker, B 2006, Sigref - A Symbolic Bisimulation Tool Box. in S Graf & W Zhang (eds), Automated Technology for Verification and Analysis: 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings. Lecture notes in Computer Science, vol. 4218, Springer, pp. 477-492, 4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006, Beijing, China, 23/10/06. https://doi.org/10.1007/11901914_35

Sigref - A Symbolic Bisimulation Tool Box. / Wimmer, Ralf; Herbstritt, Marc; Hermanns, Holger; Strampp, Kelley; Becker, Bernd.

Automated Technology for Verification and Analysis: 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings. ed. / Susanne Graf; Wenhui Zhang. Springer, 2006. p. 477-492 (Lecture notes in Computer Science; Vol. 4218).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Sigref - A Symbolic Bisimulation Tool Box

AU - Wimmer, Ralf

AU - Herbstritt, Marc

AU - Hermanns, Holger

AU - Strampp, Kelley

AU - Becker, Bernd

PY - 2006

Y1 - 2006

N2 - We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation.We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.

AB - We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation.We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.

KW - IR-66950

KW - EWI-9273

KW - METIS-238781

U2 - 10.1007/11901914_35

DO - 10.1007/11901914_35

M3 - Conference contribution

SN - 978-3-540-47237-7

T3 - Lecture notes in Computer Science

SP - 477

EP - 492

BT - Automated Technology for Verification and Analysis

A2 - Graf, Susanne

A2 - Zhang, Wenhui

PB - Springer

ER -

Wimmer R, Herbstritt M, Hermanns H, Strampp K, Becker B. Sigref - A Symbolic Bisimulation Tool Box. In Graf S, Zhang W, editors, Automated Technology for Verification and Analysis: 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings. Springer. 2006. p. 477-492. (Lecture notes in Computer Science). https://doi.org/10.1007/11901914_35