Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 2399))
Included in the following conference series:
390Accesses
Abstract
General methods have been proposed [2,4] for the model checking of probabilistic systems, where the verification of a probabilistic statement is reduced to the solution of a linear system over the system’s state space. To overcome the state space explosion problem, some probabilistic model checkers, such as PRISM [3], use MTBDDs. We propose a different solution, in which we use a Monte-Carlo algorithm [6] to approximateProb[ψ], the probability that a temporal formula is true. We show how to obtain a randomized estimator ofProb[ψ] for a fragment of LTL formulas. This fragment is sufficient to express interesting properties such as reachability and liveness.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDD’s.Proc. of 5th TACAS, LNCS 1573:193–207, 1999.
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification.Journal of the ACM, 42(4):857–907, 1995.
L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. InProc. of TACAS, LNCS 1785, 2000.
H. Hansson and B. Jonsson. A logic for reasoning about time and reliability.Formal Aspects of Computing, 6:512–535, 1994.
A. Itai and M. Rodeh. Symmetry breaking in distributed networks.Information and Computation, 88(1):60–87, 1990.
R.M. Karp and M. Luby. Monte-Carlo algorithms for enumeration and reliability problems.In Proceedings of the 24th FOCS, 56–64, 1983.
R. Motwani and P. Raghavan.Randomized Algorithms. Cambridge University Press, 1995.
A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols.Distributed Computing, pages 1:53–72, 1986.
Author information
Authors and Affiliations
Equipe de Logique, U. Paris VII, France
Richard Lassaigne
LRI, U. Paris XI, France
Sylvain Peyronnet
- Richard Lassaigne
You can also search for this author inPubMed Google Scholar
- Sylvain Peyronnet
You can also search for this author inPubMed Google Scholar
Editor information
Editors and Affiliations
Faculty of Computer Science Formal Methods and Tools Group, University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands
Holger Hermanns
Department of Computer Science, University of Verona, Strada Le Grazie 15, 37134, Verona, Italy
Roberto Segala
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lassaigne, R., Peyronnet, S. (2002). Approximate Verification of Probabilistic Systems. In: Hermanns, H., Segala, R. (eds) Process Algebra and Probabilistic Methods: Performance Modeling and Verification. PAPM-PROBMIV 2002. Lecture Notes in Computer Science, vol 2399. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45605-8_16
Download citation
Published:
Publisher Name:Springer, Berlin, Heidelberg
Print ISBN:978-3-540-43913-4
Online ISBN:978-3-540-45605-6
eBook Packages:Springer Book Archive
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative