Abstract
We present Ymer, a tool for verifying probabilistic transient properties of stochastic discrete event systems. Ymer implements both statistical and numerical model checking techniques. We focus on two features of Ymer: distributed acceptance sampling and statistical model checking of nested probabilistic statements.
Supported by the Army Research Office (ARO) under contract no. DAAD190110485 and a grant from the Royal Swedish Academy of Engineering Sciences (IVA).
Chapter PDF
Similar content being viewed by others
Keywords
- Model Check
- Execution Path
- Pseudorandom Number Generator
- Sequential Probability Ratio Test
- Master Process
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(6), 524–541 (2003)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A Markov chain model checker. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 347–362. Springer, Heidelberg (2000)
Ibe, O.C., Trivedi, K.S.: Stochastic Petri net models of polling systems. IEEE Journal on Selected Areas in Communications 8(9), 1649–1657 (1990)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer 6(2), 128–142 (2004)
Matsumoto, M., Nishimura, T.: Dynamic creation of pseudorandom number generators. In: Monte-Carlo and Quasi-Monte Carlo Methods 1998, pp. 56–69. Springer, Heidelberg (2000)
Metropolis, N., Ulam, S.M.: The Monte Carlo method. Journal of the American Statistical Association 44(247), 335–341 (1949)
Michie, D.: “Memo” functions and machine learning. Nature 218(5136), 19–22 (1968)
Wald, A.: Sequential tests of statistical hypotheses. Annals of Mathematical Statistics 16(2), 117–186 (1945)
Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Computer Science Department, Carnegie Mellon University, CMU-CS-05-105 (2005)
Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (2005) (Forthcoming)
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Younes, H.L.S. (2005). Ymer: A Statistical Model Checker. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_43
Download citation
DOI: https://doi.org/10.1007/11513988_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)