Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

sigref

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Ralf Wimmer, Dr. Entwickler / Kontakt


Beschreibung

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.



Benchmarks

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



Publikationen
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