[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
article

Remarks on Testing Probabilistic Processes

Published: 01 April 2007 Publication History

Abstract

We develop a general testing scenario for probabilistic processes, giving rise to two theories: probabilistic may testing and probabilistic must testing. These are applied to a simple probabilistic version of the process calculus CSP. We examine the algebraic theory of probabilistic testing, and show that many of the axioms of standard testing are no longer valid in our probabilistic setting; even for non-probabilistic CSP processes, the distinguishing power of probabilistic tests is much greater than that of standard tests. We develop a method for deriving inequations valid in probabilistic may testing based on a probabilistic extension of the notion of simulation. Using this, we obtain a complete axiomatisation for non-probabilistic processes subject to probabilistic may testing.

References

[1]
Andova, S. and Baeten, J.C.M., Abstraction in probabilistic process algebra. In: LNCS, 2031. Springer. pp. 204-219.]]
[2]
Andova, S., Baeten, J.C.M. and Willemse, T.A.C., A complete axiomatisation of branching bisimulation for probabilistic systems with an application in protocol verification. In: LNCS, 4137. Springer. pp. 327-342.]]
[3]
Abramsky, S. and Jung, A., Domain theory. In: Handbook of Logic and Computer Science, volume 3. Clarendon Press. pp. 1-168.]]
[4]
Andova, S. and Willemse, T.A.C., Branching bisimulation for probabilistic systems: Characteristics and decidability. Theoretical Computer Science. v356 i3. 325-355.]]
[5]
Brookes, S.D., Hoare, C.A.R. and Roscoe, A.W., A theory of communicating sequential processes. Journal of the ACM. v31 i3. 560-599.]]
[6]
. In: Bjørner, D., Jones, C.B. (Eds.), LNCS, 61. Springer.]]
[7]
Bandini, E. and Segala, R., Axiomatizations for probabilistic bisimulation. In: LNCS, 2076. Springer. pp. 370-381.]]
[8]
Cazorla, D., Cuartero, F., Ruiz, V.V., Pelayo, F.L. and Pardo, J.J., Algebraic theory of probabilistic and nondeterministic processes. Journal of Logic and Algebraic Programming. v55 i1--2. 57-103.]]
[9]
Christoff, I., Testing equivalences and fully abstract models for probabilistic processes. In: LNCS, 458. Springer. pp. 126-140.]]
[10]
Cleaveland, R., Smolka, S.A. and Zwarico, A.E., Testing preorders for probabilistic processes. In: LNCS, 623. Springer. pp. 708-719.]]
[11]
Derman, C., Finite State Markovian Decision Processes. Academic Press.]]
[12]
De Nicola, R. and Hennessy, M., Testing equivalences for processes. Theoretical Computer Science. v34. 83-133.]]
[13]
Deng, Y. and Palamidessi, C., Axiomatizations for probabilistic finite-state behaviors. In: LNCS, 3441. Springer. pp. 110-124.]]
[14]
Deng, Y., Palamidessi, C. and Pang, J., Compositional reasoning for probabilistic finite-state behaviors. In: LNCS, 3838. Springer. pp. 309-337.]]
[15]
Elgot, C.C. and Robinson, A., Random-access stored-program machines, an approach to programming languages. Journal of the ACM. v11 i4. 365-399.]]
[16]
A. Giacalone, C.-C. Jou & S.A. Smolka (1990): Algebraic reasoning for probabilistic concurrent systems. In Proceedings of IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 443--458]]
[17]
van Glabbeek, R.J., Smolka, S.A., Steffen, B. and Tofts, C.M.N., Reactive, generative, and stratified models of probabilistic processes. In: Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press. pp. 130-141.]]
[18]
van Glabbeek, R.J. and Weijland, W.P., Branching time and abstraction in bisimulation semantics. Journal of the ACM. v43 i3. 555-600.]]
[19]
Hennessy, M., Powerdomains and nondeterministic recursive definitions. In: LNCS, 137. Springer. pp. 178-193.]]
[20]
Hennessy, M., An Algebraic Theory of Processes. MIT Press.]]
[21]
Hansson, H. and Jonsson, B., A calculus for communicating systems with time and probabilities. In: Proceedings of the Real-Time Systems Symposium, Computer Society Press. pp. 278-287.]]
[22]
Hoare, C.A.R., Communicating Sequential Processes. Prentice-Hall.]]
[23]
He, Jifeng, Seidel, K. and McIver, A.K., Probabilistic models for the guarded command language. Science of Computer Programming. v28. 171-192.]]
[24]
Jonsson, B., Ho-Stuart, C. and Yi, Wang, Testing and refinement for nondeterministic and probabilistic processes. In: LNCS, 863. Springer. pp. 418-430.]]
[25]
Jonsson, B. and Larsen, K.G., Specification and refinement of probabilistic processes. In: Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press. pp. 266-277.]]
[26]
Jones, C. and Plotkin, G., A probabilistic powerdomain of evaluations. In: Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press. pp. 186-195.]]
[27]
Jonsson, B. and Yi, Wang, Compositional testing preorders for probabilistic processes. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, Computer Society Press. pp. 431-441.]]
[28]
Jonsson, B. and Yi, Wang, Fully abstract characterization of probabilistic may testing. In: LNCS, 1601. Springer. pp. 1-18.]]
[29]
Jonsson, B. and Yi, Wang, Testing preorders for probabilistic processes can be characterized by simulations. Theoretical Computer Science. v282 i1. 33-51.]]
[30]
Jonsson, B., Yi, Wang and Larsen, K.G., Probabilistic extensions of process algebras. In: Handbook of Process Algebra, Elsevier. pp. 685-710.]]
[31]
Kwiatkowska, M.Z. and Norman, G., A testing equivalence for reactive probabilistic processes. Electronic Notes in Theoretical Computer Science. v16 i2.]]
[32]
Landin, P.J., The mechanical evaluation of expressions. Computer Journal. v6 i4. 308-320.]]
[33]
G. Lowe (1993): Representing nondeterminism and probabilistic behaviour in reactive processes. Technical Report TR-11-93, Computing laboratory, Oxford University]]
[34]
Lowe, G., Probabilistic and prioritized models of timed CSP. Theoretical Computer Science. v138. 315-352.]]
[35]
Larsen, K.G. and Skou, A., Bisimulation through probabilistic testing. Information and Computation. v94 i1. 1-28.]]
[36]
Larsen, K.G. and Skou, A., Compositional verification of probabilistic processes. In: LNCS, 630. Springer. pp. 456-471.]]
[37]
Lynch, N., Segala, R. and Vaandrager, F.W., Compositionality for probabilistic automata. In: LNCS, 2761. Springer. pp. 204-222.]]
[38]
Lucas, P., Formal definition of programming languages and systems. In: IFIP Congress, volume 1. pp. 291-297.]]
[39]
Milner, R., Communication and Concurrency. Prentice-Hall.]]
[40]
Mislove, M.W., Nondeterminism and probabilistic choice: Obeying the laws. In: LNCS, 1877. Springer. pp. 350-364.]]
[41]
McIver, A.K. and Morgan, C.C., Partial correctness for probabilistic programs. Theoretical Computer Science. v266 i1--2. 513-541.]]
[42]
Morgan, C.C., McIver, A.K. and Seidel, K., Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems. v18 i3. 325-353.]]
[43]
Morgan, C.C., McIver, A.K., Seidel, K. and Sanders, J.W., Refinement-oriented probability for CSP. Formal Aspects of Computing. v8 i6. 617-647.]]
[44]
Mislove, M.W., Ouaknine, J. and Worrell, J., Axioms for probability and nondeterminism. Electronic Notes in Theoretical Computer Science. v96. 7-28.]]
[45]
Olderog, E.-R. and Hoare, C.A.R., Specification-oriented semantics for communicating processes. Acta Informatica. v23. 9-66.]]
[46]
Park, D.M.R., Concurrency and automata on infinite sequences. In: LNCS, 104. Springer. pp. 167-183.]]
[47]
G.D. Plotkin (1981): A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus]]
[48]
Plotkin, G.D., A Structural Approach to Operational Semantics. Journal of Logic and Algebraic Programming. v60--61. 17-139.]]
[49]
Philippou, A., Lee, I. and Sokolsky, O., Weak bisimulation for probabilistic systems. In: LNCS, 1877. Springer. pp. 334-349.]]
[50]
Rabin, M.O., Probabilistic automata. Information and Control. v6. 230-245.]]
[51]
R. Segala (1995): Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT]]
[52]
Segala, R., Testing probabilistic automata. In: LNCS, 1119. Springer. pp. 299-314.]]
[53]
Probabilistic simulations for probabilistic processes. In: LNCS, 836. Springer. pp. 481-496.]]
[54]
Stoelinga, M.I.A. and Vaandrager, F.W., A testing scenario for probabilistic automata. In: LNCS, 2719. Springer. pp. 407-418.]]
[55]
Tix, R., Keimel, K. and Plotkin, G.D., Semantic domains for combining probability and non-determinism. Electronic Notes in Theoretical Computer Science. v129. 1-104.]]
[56]
M.Y. Vardi (1985): Automatic verification of probabilistic concurrent finite-state programs. In Proceedings 26th Annual Symposium on Foundations of Computer Science, pp. 327--338]]
[57]
Varacca, D. and Winskel, G., Distributing probability over non-determinism. Mathematical Structures in Computer Science. v16 i1. 87-113.]]
[58]
Yi, Wang and Larsen, K.G., Testing probabilistic and nondeterministic processes. In: IFIP Transactions, C-8. North-Holland. pp. 47-61.]]

Cited By

View all

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Electronic Notes in Theoretical Computer Science (ENTCS)
Electronic Notes in Theoretical Computer Science (ENTCS)  Volume 172, Issue
April, 2007
639 pages

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 April 2007

Author Tags

  1. CSP
  2. Probabilistic processes
  3. complete axiomatisations
  4. nondeterminism
  5. simulation
  6. structural operational semantics
  7. testing equivalences
  8. transition systems

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 14 Jan 2025

Other Metrics

Citations

Cited By

View all

View Options

View options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media