sigref

| project staff | description | benchmarks | publications |

Sigref is a tool for the minimization of different classes of finite state models, namely
- labeled transition systems (LTSs),
- discrete-time Markov chains (DTMCs),
- continuous-time Markov chains (CTMCs), and
- interactive Markov chains (IMCs)
with respect to a number of bisimulations like strong, weak, and branching bisimulation. For the minimization of CTMCs, it supports - besides the standard floating point arithmetic - the usage of exact arithmetic and the handling of transition rates as symbolic parameters. Furthermore there is a variant of sigref which uses two different partition representations and an automatic conversion in order to keep the memory consumption within the user-specified limit.

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