Abstract
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 | |
| 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 |
Fingerprint
Keywords
- IR-66950
- EWI-9273
- METIS-238781
Cite this
}
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 -