sigref
Subproject |
S3 |
Categories |
Model reduction |
Overview |
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. |
R. Wimmer, M. Herbstritt, H. Hermanns, K. Strampp, and B. Becker. Sigref – A symbolic bisimulation tool box. In Susanne Graf and Wenhui Zhang, editors, Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4218 of Lecture Notes in Computer Science, pages 477–492, 2006. R. Wimmer and B. Becker. Correctness issues of symbolic bisimulation computation for Markov chains. In Bruno Müller-Clostermann, Klaus Echtle, and Erwin Rathgeb, editors, Proceedings of the 15th International GI/ITG Conference on "Measurement, Modelling and Evaluation of Computing Systems" (MMB), volume 5987 of Lecture Notes in Computer Science, pages 287–301, 2010. R. Wimmer, S. Derisavi, and H. Hermanns. Symbolic partition refinement with automatic balancing of time and space. Performance Evaluation, 67(9):815–835, 2010. |
|
ETCS Break Risk Assessment, Kanban Production System, Fault-Tolerant Workstation Cluster |
|
Download |
Click here for the sources. |
Manual |
See the README file for more information on how sigref can be used. |
Status |
Stable |