sigref
| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen
|
| Lehrstuhl für Rechnerarchitektur | |
| Ralf Wimmer, Dr. | Entwickler / Kontakt |
Sigref ist ein Werkzeug zur Minimierung verschiedener Klassen von endlichen Transitionssystemen, nämlich
- beschrifteten Transitionssystemen (engl.: labeled transition systems, LTSs),
- Markow-Ketten mit diskreter Zeit (engl.: discrete-time Markov chains, DTMCs),
- Markow-Ketten mit kontinuierlicher Zeit (engl.: continuous-time Markov chains, CTMCs), and
- interaktiven Markow-Ketten (engl.: interactive Markov chains, IMCs)
anhand einer ganzen Reihe von Minimierungskriterien wie zum Beispiel starker, schwacher oder branching Bisimulation. Bei der Minimierung von CTMCs wird - neben der Verwendung der üblichen Gleikommaarithmetik - auch die Verwendung rationaler Arithmetik und die Behandlung der verschiedenen Übergangraten als uninterpretierte Symbole unterstützt. Darüber hinaus gibt es eine Variante von sigref, die zwei verschiedene symbolische Partitionsdarstellungen verwenden und automatisch zwischen beiden hin- und herschaltet, um den Speicherverbrauch bei bestmöglicher Geschwindigkeit zu begrenzen.
Cyclic polling server (*)
Grid-world robot (*)
ETCS (**)
Kanban production system (*)
Milner scheduler (**)
Work station cluster (*)
P2P network (*)
Fibroblast growth factor signalling (*)
Cell cycle control (*)
(*) http://www.prismmodelchecker.org/casestudies/index.php
(**) http://www.avacs.org
|
Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker Sigref - A symbolic bisimulation tool box Int'l Symposium on Automated Technology for Verification and Analysis, 2006 |
|
Ralf Wimmer, Bernd Becker Correctness issues of symbolic bisimulation computation for Markov chains Int'l GI/ITG Conference on Measurement, Modelling and Evaluation of Computing Systems, 2010 |
|
Ralf Wimmer, Salem Derisavi, Holger Hermanns Symbolic partition refinement with automatic balancing of time and space Performance Evaluation, 67(9):815--835, 2010 |