PRISM References

• ASW00
  N. Asokan and V. Shoup and M. Waidner
  Optimistic fair exchange of digital signatures
  IEEE Selected Areas in Communications, 18(4):593-610, 2000
  
  
• AH90
  J. Aspnes and M. Herlihy
  Fast randomized consensus using shared memory
  Journal of Algorithms, 15(1):441-460, 1990
  
  
• ASSB96
  A. Aziz, K. Sanwal, V. Singhal, and R. Brayton
  Verifying continuous time Markov chains
  In Proc. CAV'96, pp 269-276, 1996 (Available as Volume 1102 of LNCS, © Springer Verlag)
  
  
• Bai98
  C. Baier
  On algorithmic verification methods for probabilistic systems
  Habilitation thesis, Universität Mannheim, 1998
  
  
• BHHK00
  C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen
  Model checking continuous-time Markov chains by transient analysis
  In Proc. CAV'00, pp. 358-372, 2000 (Available as Volume 1855 of LNCS, © Springer Verlag)
  
  
• BKH99
  C. Baier, J.-P. Katoen and H. Hermanns
  Approximative symbolic model checking of continuous-time markov chains
  In Proc. CONCUR'99, pp 146-161, 1999 (Available as Volume 1664 of LNCS, © Springer Verlag)
  
  
• BGJ99
  J. Beauquier, M. Gradinariu and C. Johnen
  Memory space requirements for self-stabilizing leader election protocols
  In Proc. ACM Symposium on Principles of Distributed Computing, pp. 199-208, ACM Press, 1999
  
  
• Ben83
  M. Ben-Or
  Another advantage of free choice: completely asynchronous agreement protocols
  In Proc. ACM Symposium on Principles of Distributed Computing, pp 27-30, ACM Press, 1983
  
  
• BGMR90
  M. Ben-Or, O. Goldreich, S. Micali and R. Rivest
  A fair protocol for signing contracts
  IEEE Transactions on Information Theory, 36(1):40-46, 1990
  
  
• BBM00
  L. Benini, A Bogliolo and G. De Micheli
  A survey of design techniques for system-level dynamic power management
  IEEE Transactions on Very Large Scale Integration (TVLSI) Systems, 8(3), 2000
  
  
• BBPM99
  L. Benini, A. Bogliolo, G. Paleologo and G. De Micheli
  Policy optimization for dynamic power management
  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 8(3):299-316, 2000
  
  
• BN01
  D. Beyer and A. Noack
  Efficient verification of timed automata using BDDs
  In Proc. 6th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, pp 95-113, 2001
  
  
• BdA95
  A. Bianco and L. de Alfaro
  Model checking of probabilistic and nondeterministic systems
  In Proc. Foundations of Software Technology and Theoretical Computer Science, pp. 499-513, 1995
  (Available as Volume 1026 of LNCS, © Springer Verlag)
  
  
• BHZV02
  H. Bohnenkamp, H. Hermanns, M Zang and F. Vaandrager
  Cost opimisation of the IPv4 zeroconf protocol
  In Proc. 3rd PROGRESS Workshop on Embedded Systems, 2002
  
  
• BHZV03
  H. Bohnenkamp, P. van der Stok, H. Hermanns and F. Vaandrager
  Cost-Optimisation of the IPv4 Zeroconf protocol
  In Proc. 3rd IPDS 2003, IEEE CS Press, 2003
  
  
• Buc96
  P. Buchholz
  Structured analysis approaches for large Markov chains - A tutorial
  Tutorial at Performance'96, Lausanne, Switzerland, 1996
  
  
• CKS00
  C. Cachin and K. Kursawe and V. Shoup
  Random oracles in Constantinople: Practical asynchronous Byzantine agreement using cryptography (extended abstract)
  In Proc. Symposium on Principles of Distributed Computing, pp 123-132, 2000
  
  
• CAG02
  S. Cheshire, B. Adoba and E. Gutterman
  Dynamic configuration of IPv4 link local addresses
  Available from http://www.ietf.org/rfc/rfc3927.txt
  
  
• CT96
  G. Ciardo and M. Tilgner
  On the use of Kronecker operators for the solution of generalized stochastic Petri nets
  ICASE Report No. 96-35, 1996
  
  
• CT93
  G. Ciardo and K.S. Trivedi
  A decomposition approach for stochastic reward networks
  Performance Evaluation, 18(1):37-59, 1993
  
  
• Clu03
  J. Clulow
  The design and analysis of cryptographic APIs for security devices
  Master's thesis, University of Natal, Durban, 2003
  
  
• D'AJJL01
  P. D'Argenio, B. Jeannet, H. Jensen and K. Larsen
  Reachability analysis of probabilistic systems by successive refinements
  In Proc. PAPM-PROBMIV'01, pp 39-56, 2001 (Available as Volume 2165 of LNCS, © Springer Verlag)
  
  
• DT98
  C. Daws and S. Tripakis
  Model-checking of real-time reachability properties using abstractions
  In Proc. TACAS'98, pp 313-329, 1998
  (Available as Volume 1384 of LNCS, © Springer Verlag)
  
  
• Dav81
  M. Davio
  Kronecker products and shuffle algebra
  IEEE Transactions on Computers, C-30(2):116-125, 1981
  
  
• dA97
  L. de Alfaro
  Formal verification of probabilistic systems
  Ph.D. Dissertation, Stanford University, 1997. Technical report STAN-CS-TR-98-1601.
  
  
• Dil89
  D. Dill
  Timing assumptions and verification of finite-state concurrent systems
  In, J. Sifakis editor, Proc. Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 197-212, Springer, 1989
  
  
• DO77
  R. Dobrushin and E. Ortyukov
  Upper bound on the redundancy of self-correcting arrangements of unreliable functional elements
  Problems of Information Transmission, 23(2):203-218, 1977
  
  
• DY83
  D. Dolev and A. Yao
  On the security of public key protocols
  IEEE Transactions on Information Theory, 29(2):198-208, 1983
  
  
• DFP04
  M. Duflot, L. Fribourg and C. Picaronny
  Randomized dining philosophers without fairness assumption
  Distributed Computing, 17(1):65-76, 2004
  
  
• EGL85
  S. Even, O. Goldreich and A. Lempel
  A randomized protocol for signing contracts
  Communications of the ACM, 28(6):637-647, 1985
  
  
• EP98
  W. Evans and N. Pippenger
  On the Maximum Tolerable Noise for Reliable Computation by Formulas
  IEEE Transactions on Information Theory, 44(3):1299-1305, 1988
  
  
• Fal90
  G.I. Falin
  A survey of retrial queues
  Queueing Systems, 7:127 - 168, 1990
  
  
  
• FT97
  G.I. Falin and J.G.C. Templeton
  Retrial Queues
  Chapman & Hall, 1997
  
  
• FLP85
  M. Fischer, N. Lynch and M. Paterson
  Impossibility of distributed consensus with one faulty process
  Journal of the ACM, 32(5):374-382, 1985
  
  
• GH02
  H. Garavel and H. Hermanns
  On combining functional verification and performance evaluation using CADP
  In FME 2002: International Symposium of Formal Methods Europe, pp 410-429, 2000
  (Available as Volume 2391 of LNCS, © Springer Verlag)
  
  
• Gra77
  W. Grassmann
  Transient solutions in Markovian queues
  European Journal of Operational Research, 1:396-402, 1977
  
  
• HHK00
  B. Haverkort, H. Hermanns and J.-P. Katoen
  On the use of model checking techniques for dependability evaluation
  In Proc. 19th IEEE Symposium on Reliable Distributed Systems (SRDS'00), pp 228-237, 2000
  
  
• B. Haverkort
  Markovian models for performance and dependability evaluation
  In Proc. Lectures on Formal Methods and Performance Analysis, volume 2090 of Lecture Notes in Computer Science 2090, pages 38-83, Springer-Verlag, Berlin, 2001
  
  
• HJ02
  J. Han and P. Jonker
  A System Architecture Solution for Unreliable Nanoelectronic Devices
  IEEE Transactions on Nanotechnology, 1:201-208, 12002
  
  
• HJ94
  H. Hansson and B. Jonsson
  A logic for reasoning about time and reliability
  Formal Aspects of Computing, 6:512-535, 1994
  
  
• HMPT00
  G. Haring, R. Marie, R. Puigjaner and K. Trivedi
  Loss formulae and their application to optimization for cellular networks
  IEEE Transaction on Vehicular Technology, 50(3):664 -673, 2000
  
  
• HSV94
  L. Helmink, M. Sellink and F Vaandrager
  Proof checking a data link protocol
  In Proc. Types for Proofs and Programs (TYPES'93), pp. 127-165, 1994
  (Available as Volume 806 of LNCS, © Springer Verlag)
  
  
• Her90
  T. Herman
  Probabilistic self-stabilization
  In Information Processing Letters, 35(2):63-67, 1990
  
  
• HMKS99
  H. Hermanns, J. Meyer-Kayser and M. Siegle
  Multi-terminal binary decision diagrams to represent and analyse continuous time Markov chains
  In Proc. 3rd International Workshop on the Numerical Solution of Markov Chains, pp. 188-207, 1999
  
  
• IT90
  O. Ibe and K. Trivedi
  Stochastic Petri net models of polling systems
  IEEE Journal on Selected Areas in Communications, 8(9):1649-1657, 1990
  
  
• IJ90
  A. Israeli and M. Jalfon
  Token management schemes and random walks yeild self-stabilizating mutual exclusion
  In Proc. ACM Symposium on Principles of Distributed Computing, pp. 119-131, 1990
  
  
• IR90
  A. Itai and M. Rodeh
  Symmetry breaking in distributed networks
  Information and Computation, 88:60-97, 1990
  
  
• Jen53
  A. Jensen
  Markoff chains as an aid in the study of Markoff processes
  Skand. Aktuarietiedskr., 36:87-91, 1953
  
  
• KY76
  D. E. Knuth and A. C. Yao
  The complexity of nonuniform random number generation
  In J. F. Traub, editor, Algorithms and Complexity: New Directions and Recent Results, Academic Press, New York, 1976
  
  
• V. Kulkarni
  Modeling and Analysis of Stochastic Systems
  Chapman & Hall, 1995
  
  
• KR92
  E. Kushilevitz and M. Rabin
  Randomized mutual exclusion algorithms revisited
  In 11th Annual Symposium on Principles of Distributed Systems, pp. 275-284, 1992
  
  
• LP03
  P. Lecca and C. Priami
  Cell Cycle Control in Eukaryotes: A BioSpi model
  In Proc. Workshop on Concurrent Models in Molecular Biology (BioConcur'03), ENTCS, 2004. To appear.
  
  
• LR81
  D. Lehmann and M. Rabin
  On the advantages of free choice: A symmetric fully distributed solution to the dining philosophers problem (extended abstract)
  In Proc. 8th Symposium on Principles of Programming Languages, pp. 133-138, 1981
  
  
• LSS94
  N. Lynch, I. Saias and R. Segala
  Proving time bounds for randomized distributed algorithms
  In Proc. 13th ACM Symposium on Principles of Distributed Computing, pp. 314-323, 1994
  
  
• MCT94
  J. Muppala, G. Ciardo and K. Trivedi
  Stochastic reward nets for reliability prediction
  Communications in Reliability, Maintainability and Serviceability1(2):9-20, 1994
  
  
• MM02
  A. McIver and C. Morgan
  Games, probability and the quantitative mu-calculus qMu
  In M. Baaz and A. Voronkov editors, Proc. LPAR'02, volume 2514 of LNAI, Springer, 2002
  
  
• MM04
  A. McIver and C. Morgan
  Abstraction, refinement and proof for probabilistic systems
  Springer, 2004
  (For more information, see here)
  
  
• MM05a
  A. McIver and C. Morgan
  An elementary proof that Herman's Ring is THETA(N-squared)
  Information Processing Letters, 94:2, pages 79-84, 2005
  
  
• MM05b
  A. McIver and C. Morgan
  Results on the quantitative mu-calculus qMu
  ACM Transactions on Computational Logic. To appear.
  (Available at http://www.acm.org/pubs/tocl/accepted/morgan.ps)
  
  
• McM98
  K. McMillan
  Verfication of an implementation of Tomasulo's algorithm by compositional model checking
  In A. Hu and M. Vardi editors, Proc. CAV'98, volume 1427 of LNCS, pp 110-121, Springer, 1998
  
  
• McM99
  K. McMillan
  Verification of infinite state systems by compositional model checking
  In L. Pierre and T. Kropf editors, Proc. CHARME'99, volume 1703 of LNCS, Springer, 1999
  
  
• MQS00
  K. McMillan and S. Qadeer and J. Saxe
  Induction and compositional model checking
  In E. Emerson, A. Sistla editors, Proc. CAV 2000, volume 1855 of LNCS, pp 312-327, Springer, 2000
  
  
• MM97
  C. Morgan and A. McIver
  A probabilistic temporal calculus based on expectations
  In L. Groves and S. Reeves editors, Proc. Formal Methods Pacific '97, Springer, Singapore, 1997
  
  
• NSY92
  X. Nicollin, J. Sifakis and S. Yovine
  Compiling real-time specifications into extended automata
  IEEE Transactions on Software Engineering, 18(9):794-804, 1992
  
  
• NSF01
  K. Nikolic, A. Sadek and M. Forshaw
  Architectures for Reliable Computing with Unreliable Nanodevices
  In Proc. 1st IEEE Conference on Nanotechnology, (IEEE-NANO), pages 254--259, 2001
  
  
• OR90
  M. Osborne and A. Rubinstein
  Bargaining and markets
  The Academic Press, 1990
  
  
• PBBM98
  G. Paleologo, L. Benini, A. Bogliolo and G. Micheli
  Policy optimization for dynamic power management
  In Proc. Design Automation Conference, pp 182-187, 1988
  
  
• PS01
  P. Pillai and K. Shin
  Real-time dynamic voltage scaling for low-powered embedded operating systems
  Operating Systems Review, 35(5):89-102, 2001
  
  
• Pip88
  N. Pippenger
  Reliable computation by formulas in the presence of noise
  IEEE Transactions on Information Theory, 34(2):194-197, 1988
  
  
• Pla85
  B. Plateau
  On the stochastic structure of parallelism and synchronisation models for distributed algorithms
  In Proc. 1985 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems, pp. 147-153, 1985
  
  
• PZ86
  A. Pnueli and L. Zuck
  Verification of multiprocess probabilistic protocols
  Distributed Computing, 1(1):53-72, 1986
  
  
• PSS00
  A. Pogosyants and R. Segala and N. Lynch
  Verification of the randomized consensus algorithm of Aspnes and Herlihy: A case study
  Distributed Computing, 13(3):155-186, J, 2000
  An extended abstract appears in Proc. WDAG, LNCS 1320, Springer, 1997.
  
• QP99
  Q. Qiu and M. Pedram
  Dynamic power management based on continuous-time Markov decision processes
  In Proc. Design Automation Conference, pp. 555-561, 1999
  
  
• QWP99
  Q. Qiu, Q. Wu and M. Pedram
  Stochastic modeling of a power-managed system: construction and optimization
  In Proc. International Symposium on Low Power Electronics and Design, pp 194-199, ACM Press, 1999
  
  
• Rab81
  M. Rabin
  Transaction protection by beacons
  Technical Report 29-81, Aiken Computation Laboratory, Harvard University, 1981
  
  
• Rab82
  M. Rabin
  N-process mutual exclusion with bounded waiting by 4log₂N-valued shared variable
  Journal of Computer and System Sciences, 25(1):66-75, 1982
  
  
• Rab83
  M. Rabin
  Randomized Byzantine generals
  In Proc. Symposium on Foundations of Computer Science, pp 403-409, 1983
  
  
• RS02
  A. Regev and E. Shapiro
  Cellular abstractions: Cells as computation
  Nature, 419(6905):343, 1982
  
  
• RR98
  M. Reiter and A. Rubin
  Crowds: Anonymity for web transactions
  ACM Transactions on Information and System Security (TISSEC), 1(1):66-92, 1998
  
  
• Ros97
  A. Roscoe
  The theory and practice of concurrency
  Prentice-Hall, 1997
  
  
• Sai92
  I. Saias
  Proving probabilistic correctness statements: The case of rabin's algorithm for mutual exclusion
  In 11th Annual Symposium on Principles of Distributed Systems, pp. 263-274, 1992
  
  
• SL94
  R. Segala and N. Lynch
  Probabilistic simulations for probabilistic processes
  In Proc. CONCUR'94, pp 481-496, 1994
  (Available as Volume 836 of LNCS, © Springer Verlag)
  
  
• SS01
  D. Simons. and M. Stoelinga
  Mechanical verification of the IEEE1394a root contention protocol using Uppaal2k
  International Journal on Software Tools for Technology Transfer 3(4):469-485, 2001
  
  
• SBM99
  T. Simunic, L. Benini and G. De Micheli
  Event driven power management of portable systems
  To Proc. International Symposium on System Synthesis, pp 18-23, 1999
  
  
• SV99
  M. Stoelinga and F. Vaandrager
  Root contention in IEEE 1394
  In Proc. 5th AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99), pp. 53-74, 1999
  (Available as Volume 1601 of LNCS, © Springer Verlag)
  
  
• Tri98
  S. Tripakis
  The analysis of timed systems in practice
  PhD Thesis, Universite Joseph Fourier, Grenoble, 1998
  
  
• vN56
  J. von Neumann
  Probabilistic logics and synthesis of reliable organisms from unreliable components
  Automata Studies, C. Shannon and J. McCarthy editors, pages 43-98, Princeton University Press, 1956
  
  
• YS02
  H. Younes and R. Simmons
  Probabilistic verification of discrete event systems using acceptance sampling
  In Proc. 14th International Conference on Computer Aided Verification (CAV'02), pp. 223-235, 2002
  (Available as Volume 2404 of LNCS, © Springer Verlag)
  
  
• ZV03
  M. Zhang and F. Vaandrager
  Analysis of a protocol for dynamic configuration of IPv4 link local addresses using Uppaal
  Technical Report NIII-R03XX, NIII, University of Nijmegen, 2003.