QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
The Markov Reward Model Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions....
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
—The departure process of a BMAP/MAP/1 queue can be approximated in different ways: as a Markovian arrival process (MAP) or as a matrix-exponential process (MEP). Both approximat...
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
—Traviando is a trace analyzer and visualizer for simulation traces of discrete event dynamic systems. In this paper, we briefly outline recent extensions of Traviando towards a...
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
—In this paper we consider Quasi-Birth-and-Death (QBD) processes where the upward (resp. downward) transitions are restricted to occur only from (resp. to) a subset of the phase ...
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
—Symmetry reduction is a technique for combating state-space explosion in model checking. The generic representatives approach to symmetry reduction uses a language-level transla...
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
—We consider a distributed shuffling algorithm for sharing data in a distributed network. Nodes executing the algorithm periodically contact each other and exchange data. The be...
QEST
2009
IEEE
14 years 6 months ago
2009
IEEE
