Sigref - A Symbolic Bisimulation Tool Box

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

40 Citations (Scopus)
44 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 languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006. Proceedings
EditorsSusanne Graf, Wenhui Zhang
PublisherSpringer
Pages477-492
Number of pages16
ISBN (Electronic)978-3-540-47238-4
ISBN (Print)978-3-540-47237-7
DOIs
Publication statusPublished - 2006
Event4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006 - Beijing, China
Duration: 23 Oct 200626 Oct 2006
Conference number: 4

Publication series

NameLecture notes in Computer Science
PublisherSpringer Verlag
Volume4218
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Symposium on Automated Technology for Verification and Analysis, ATVA 2006
Abbreviated titleATVA
CountryChina
CityBeijing
Period23/10/0626/10/06

Fingerprint

Experiments

Keywords

  • IR-66950
  • EWI-9273
  • METIS-238781

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 proceedingConference contributionAcademicpeer-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