
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Gethin Norman, Catuscia Palamidessi, David Parker, Peng Wu, "Model Checking Probabilistic and Stochastic Extensions of the πCalculus," IEEE Transactions on Software Engineering, vol. 35, no. 2, pp. 209223, March/April, 2009.  
BibTex  x  
@article{ 10.1109/TSE.2008.77, author = {Gethin Norman and Catuscia Palamidessi and David Parker and Peng Wu}, title = {Model Checking Probabilistic and Stochastic Extensions of the πCalculus}, journal ={IEEE Transactions on Software Engineering}, volume = {35}, number = {2}, issn = {00985589}, year = {2009}, pages = {209223}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2008.77}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Model Checking Probabilistic and Stochastic Extensions of the πCalculus IS  2 SN  00985589 SP209 EP223 EPD  209223 A1  Gethin Norman, A1  Catuscia Palamidessi, A1  David Parker, A1  Peng Wu, PY  2009 KW  Model checking KW  Markov processes KW  Stochastic processes VL  35 JA  IEEE Transactions on Software Engineering ER   
[1] R. Milner, J. Parrow, and D. Walker, “A Calculus of Mobile Processes, I,” Information and Computation, vol. 100, pp. 140, 1992.
[2] M. Reiter and A. Rubin, “Crowds: Anonymity for Web Transactions,” ACM Trans. Information and System Security, vol. 1, no. 1, pp. 6692, 1998.
[3] S. Even, O. Goldreich, and A. Lempel, “A Randomized Protocol for Signing Contracts,” Comm. ACM, vol. 28, no. 6, pp. 637647, 1985.
[4] O. Herescu and C. Palamidessi, “Probabilistic Asynchronous $\pi$ Calculus,” Proc. Third Int'l Conf. Foundations of Software Science and Computation Structures, J. Tiuryn, ed., pp. 146160, 2000.
[5] K. Chatzikokolakis and C. Palamidessi, “A Framework to Analyze Probabilistic Protocols and Its Application to the Partial Secrets Exchange,” Proc. Int'l Symp. Trustworthy Global Computing, R.D.Nicola and D. Sangiorgi, eds., pp. 146162. Springer, 2005.
[6] M. Bhargava, C. Palamidessi, “Probabilistic Anonymity,” Proc. 16th Int'l Conf. Concurrency Theory, M. Abadi and L. de Alfaro, eds., pp. 171185, 2005.
[7] C. Priami, “Stochastic $\pi$ Calculus,” Computer J., vol. 38, no. 7, pp. 578589, 1995.
[8] A. Regev, W. Silverman, and E. Shapiro, “Representation and Simulation of Biochemical Processes Using the $\pi$ Calculus Process Algebra,” Proc. Pacific Symp. Biocomputing, R. Altman, A. Dunker, L. Hunter, and T. Klein, eds., vol. 6, pp. 459470, 2001.
[9] C. Priami, A. Regev, W. Silverman, and E. Shapiro, “Application of a Stochastic Name Passing Calculus to Representation and Simulation of Molecular Processes,” Information Processing Letters, vol. 80, pp. 2531, 2001.
[10] P. Yang, C. Ramakrishnam, and S. Smolka, “A Logic Encoding of the $\pi$ Calculus: Model Checking Mobile Processes Using Tabled Resolution,” Int'l J. Software Tools Technology Transfer, vol. 4, pp. 129, 2004.
[11] A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, “PRISM: A Tool for Automatic Verification of Probabilistic Systems,” Proc. 12th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, H. Hermanns and J. Palsberg, eds., pp. 441444, 2006.
[12] B. Victor and F. Moller, “The Mobility Workbench—A Tool for the $\pi$ Calculus,” Proc. Sixth Int'l Conf. Computer Aided Verification, R.Alur and D. Peled, eds., pp. 428440, 1994.
[13] B. Blanchet, ProVerif: Automatic Cryptographic Protocol Verifier User Manual, www.preverif.ens.frproverifmanual.ps.gz , 2005.
[14] S. Chaki, S. Rajamani, and J. Rehof, “Types as Models: Model Checking MessagePassing Programs,” Proc. 29th Symp. Principles of Programming Languages, pp. 4557, 2002.
[15] P. Wu, “Interpreting $\pi$ Calculus with Spin/Promela,” Computer Science, vol. 8, pp. 79, supplement, 2003.
[16] H. Song and K. Compton, “Verifying $\pi$ Calculus Processes by Promela Translation,” Technical Report CSETR47203, Univ. of Michigan, 2003.
[17] A. Venet, “Abstract Interpretation of the $\pi$ Calculus,” Proc. Fifth LOMAPS Workshop Analysis and Verification of MultipleAgent Languages, M. Dam, ed., pp. 5175, 1996.
[18] C. Bodei, P. Degano, F. Nielson, and H.R. Nielson, “Static Analysis for the $\pi$ Calculus with Applications to Security,” Information and Computation, vol. 165, pp. 6892, 2001.
[19] A. Phillips and L. Cardelli, “Efficient, Correct Simulation of Biological Processes in the Stochastic $\pi$ Calculus,” Proc. Fifth Int'l Workshop Computational Methods in Systems Biology, M. Calder and S. Gilmore, eds., pp. 184199, 2007.
[20] G. Norman, C. Palamidessi, D. Parker, and P. Wu, “Model Checking the Probabilistic $\pi$ Calculus,” Proc. Fourth Int'l Conf. Quantitative Evaluation of Systems, pp. 169178, 2007.
[21] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[22] R. Segala and N. Lynch, “Probabilistic Simulations for Probabilistic Processes,” Nordic J. Computing, vol. 2, no. 2, pp. 250273, 1995.
[23] M. Hennessy and H. Lin, “Symbolic Bisimulations,” Theoretical Computer Science, vol. 138, pp. 353389, 1995.
[24] P. Wu, C. Palamidessi, and H. Lin, “Symbolic Bisimulations for Probabilistic Systems,” Proc. Fourth Int'l Conf. Quantitative Evaluation of Systems, pp. 179188, 2007.
[25] H. Lin, “Symbolic Bisimulation and Proof Systems for the $\pi$ Calculus,” technical report, School of Cognitive and Computer Science, Univ. of Sussex, 1994.
[26] M. Boreale and R.D. Nicola, “A Symbolic Semantics for the $\pi$ Calculus,” Information and Computation, vol. 126, no. 1, pp. 3452, Apr. 1996.
[27] H. Lin, “Complete Inference Systems for Weak Bisimulation Equivalences in the $\pi$ Calculus,” Information and Computation, vol. 180, no. 1, pp. 129, 2003.
[28] A. Ingólfsdóttir and H. Lin, “A Symbolic Approach to ValuePassing Processes,” Handbook of Processes Algebra, chapter 7, Elsevier, 2001.
[29] J. Hillston, A Compositional Approach to Performance Modelling. Cambridge Univ. Press, 1996.
[30] G. Norman, C. Palamidessi, D. Parker, and P. Wu, “Translating the Probabilistic $\pi$ Calculus to PRISM,” Technical Report CSR0702, School of Computer Science, Univ. of Birmingham, 2007.
[31] A. Roscoe, The Theory and Practice of Concurrency. PrenticeHall, 1997.
[32] Online PRISM documentation, www.prismmodelchecker.orgdoc/, 2009.
[33] H. Hansson and B. Jonsson, “A Logic for Reasoning about Time and Reliability,” Formal Aspects of Computing, vol. 6, no. 5, pp. 512535, 1994.
[34] A. Bianco and L. de Alfaro, “Model Checking of Probabilistic and Nondeterministic Systems,” Proc. 15th Conf. Foundations of Software Technology and Theoretical Computer Science, P.Thiagarajan, ed., pp.499513, 1995.
[35] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, “Verifying Continuous Time Markov Chains,” Proc. Eighth Int'l Conf. Computer Aided Verification, R. Alur and T.Henzinger, eds., pp.269276, 1996.
[36] C. Baier, B. Haverkort, H. Hermanns, and J.P. Katoen, “ModelChecking Algorithms for ContinuousTime Markov Chains,” IEEE Trans. Software Eng., vol. 29, no. 6, pp. 524541, June 2003.
[37] M. Goldsmith, N. Moffat, B. Roscoe, T. Whitworth, and I. Zakiuddin, “Watchdog Transformations for PropertyOriented ModelChecking,” Proc. Second Int'l Symp. Formal Methods Europe, K.Araki, S. Gnesi, and D. Mandrioli, eds., pp. 600616, 2003.
[38] L. Caires and L. Cardelli, “A Spatial Logic for Concurrency (PartI),” Information and Computation, vol. 186, no. 2, pp. 194235, 2003.
[39] D. Chaum, “The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability,” J. Cryptology, vol. 1, pp. 6575, 1988.
[40] G. Norman and V. Shmatikov, “Analysis of Probabilistic Contract Signing,” J. Computer Security, vol. 14, no. 6, pp. 561589, 2006.
[41] F. Orava and J. Parrow, “An Algebraic Verification of a Mobile Network,” Formal Aspects of Computing, vol. 4, pp. 497543, 1992.
[42] C. Priami, “Stochastic Analysis of Mobile Telephony Networks,” Proc. Fifth Int'l Workshop Process Algebra and Performance Modeling, E.Brinskma and A. Nymeyer, eds., pp. 145171, 1997.
[43] J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn, “Probabilistic Model Checking of Complex Biological Pathways,” Proc. Fourth Int'l Workshop Computational Methods in Systems Biology, C. Priami, ed., pp. 3247, 2006.