Main /

References

AD94
R. Alur and D. Dill.
A theory of timed automata.
Theoretical Computer Science, 126:183-235, 1994.

AH99
R. Alur and T. Henzinger.
Reactive modules.
Formal Methods in System Design, 15(1):7-48, 1999.

ASSB96
A. Aziz, K. Sanwal, V. Singhal, and R. Brayton.
Verifying continuous time Markov chains.
In R. Alur and T. Henzinger, editors, Proc. 8th International Conference on Computer Aided Verification (CAV'96), volume 1102 of LNCS, pages 269-276. Springer, 1996.

Bai98
C. Baier.
On algorithmic verification methods for probabilistic systems, 1998.
Habilitation thesis, Fakultät für Mathematik & Informatik, Universität Mannheim.

BKH99
C. Baier, J.-P. Katoen, and H. Hermanns.
Approximate symbolic model checking of continuous-time Markov chains.
In J. Baeten and S. Mauw, editors, Proc. 10th International Conference on Concurrency Theory (CONCUR'99), volume 1664 of LNCS, pages 146-161. Springer, 1999.

BK98
C. Baier and M. Kwiatkowska.
Model checking for a probabilistic branching time logic with fairness.
Distributed Computing, 11(3):125-155, 1998.

BdA95
A. Bianco and L. de Alfaro.
Model checking of probabilistic and nondeterministic systems.
In P. Thiagarajan, editor, Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95), volume 1026 of LNCS, pages 499-513. Springer, 1995.

HJ94
H. Hansson and B. Jonsson.
A logic for reasoning about time and reliability.
Formal Aspects of Computing, 6(5):512-535, 1994.

HLMP04
T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet.
Approximate probabilistic model checking.
In Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), volume 2937 of LNCS, pages 307-329. Springer, 2004.

HKN+03
H. Hermanns, M. Kwiatkowska, G. Norman, D. Parker, and M. Siegle.
On the use of MTBDDs for performability analysis and verification of stochastic systems.
Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, 56(1-2):23-67, 2003.

Hil96
J. Hillston.
A Compositional Approach to Performance Modelling.
Cambridge University Press, 1996.

KSK76
J. Kemeny, J. Snell, and A. Knapp.
Denumerable Markov Chains.
Springer-Verlag, 2nd edition, 1976.

KNP04b
M. Kwiatkowska, G. Norman, and D. Parker.
Probabilistic symbolic model checking with PRISM: A hybrid approach.
International Journal on Software Tools for Technology Transfer (STTT), 6(2):128-142, 2004.

KNP07a
M. Kwiatkowska, G. Norman, and D. Parker.
Stochastic model checking.
In M. Bernardo and J. Hillston, editors, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of LNCS (Tutorial Volume), pages 220-270. Springer, 2007.

KNP09c
M. Kwiatkowska, G. Norman, and D. Parker.
Stochastic games for verification of probabilistic timed automata.
In J. Ouaknine and F. Vaandrager, editors, Proc. 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09), volume 5813 of LNCS, pages 212-227. Springer, 2009.

KNPS06
M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston.
Performance analysis of probabilistic timed automata using digital clocks.
Formal Methods in System Design, 29:33-78, 2006.

KNPS08
M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston.
Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, chapter Verification of Real-Time Probabilistic Systems, pages 249-288.
John Wiley & Sons, 2008.

Nim10
V. Nimal.
Statistical Approaches for Probabilistic Model Checking.
MSc Mini-project Dissertation, Oxford University Computing Laboratory, 2010.

Par02
D. Parker.
Implementation of Symbolic Model Checking for Probabilistic Systems.
Ph.D. thesis, University of Birmingham, 2002.

Seg95
R. Segala.
Modelling and Verification of Randomized Distributed Real Time Systems.
Ph.D. thesis, Massachusetts Institute of Technology, 1995.

Ste94
W. J. Stewart.
Introduction to the Numerical Solution of Markov Chains.
Princeton, 1994.

YS02
H. Younes and R. Simmons.
Probabilistic verification of discrete event systems using acceptance sampling.
In E. Brinksma and K. Larsen, editors, Proc. 14th International Conference on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 223-235. Springer, 2002.

PRISM Manual

[ View all ]