Advertisement

Action Refinement for Probabilistic Processes with True Concurrency Models

  • Harald Fecher
  • Mila Majster-Cederbaum
  • Jinzhao Wu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2399)

Abstract

In this paper, we develop techniques of action refinement for probabilistic processes within the context of a probabilistic process algebra. A semantic counterpart is carried out in a non-interleaving causality based setting, probabilistic bundle event structures. We show that our refinement notion has the following nice properties: the behaviour of the refined system can be inferred compositionally from the behaviour of the original system and from the behaviour of the systems substituted for actions; the probabilistic extensions of pomset trace equivalence and history preserving bisimulation equivalence are both congruences under the refinement; and with respect to a cpo-based denotational semantics the syntactic and semantic refinements coincide with each other up to the aforementioned equivalence relations when the internal actions are abstracted away.

Keywords

Causality Relation Semantic Model Probabilistic Choice Parallel Composition Process Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abramsky, S., Jung, A., Domain Theory, Handbook of Logic in Computer Science (S. Abramsky and Dov M. Gabbay eds.), Clarendon Press, Volume 3: 1–168, 1994.Google Scholar
  2. 2.
    Aceto, L, Action Refinement in Process Algebra, Cambridge Univ. Press, 1992.Google Scholar
  3. 3.
    Bolognesi, T., Brinksma, E., Introduction to the ISO Specification Language LOTOS, Comp. Netw. and ISDN Syst., 14: 25–59, 1987.CrossRefGoogle Scholar
  4. 4.
    Bowman, H., Derrick, J., Extending LOTOS with Time: A True Concurrency Perspective, Lecture Notes in Computer Science, 1231: 383–399, 1997.Google Scholar
  5. 5.
    Bowman, H., Katoen, J.-P., A True Concurrency Semantics for ET-LOTOS, Proceedings Int. Conference on Applications of Concurrency to System Design, 228–239, 1998.Google Scholar
  6. 6.
    Brinksma, E., Katoen, J.-P., Langerak, R., and Latella, D., Partial-Order Models for Quantitative Extensions of LOTOS, Computer Networks and ISDN Systems, 30(9/10): 925–950, 1998.CrossRefGoogle Scholar
  7. 7.
    D’Argenio, P. R., Hermanns, H., and Katoen, J.-P., On Generative Parallel Composition, Electronic Notes in Theoretical Computer Science, 22, 1999.Google Scholar
  8. 8.
    Fecher, H., Majster-Cederbaum, M., and Wu, J., Bundle Event Structures: A Revised Cpo Approach, Information Processing Letters, accepted, 2001.Google Scholar
  9. 9.
    Fecher, H., Majster-Cederbaum, M., and Wu, J., Refinement of Actions in a Real-Time Process Algebra with a True Concurrency Model, REFINE 2002, accepted, 2002.Google Scholar
  10. 10.
    van Glabbeek, R., Goltz, U., Refinement of Actions and Equivalence Notions for Concurrent Systems, Acta Informatica, 37: 229–327, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    van Glabbeek, R., Smolka, S. A., and Steffen, B., Reactive, Generative and Stratified Models of Probabilistic Processes, Information and Computation, 121: 59–80, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    van Glabbeek, R., Smolka, S. A., Steffen, B., and Tofts, C. M. N., Reactive, Generative and Stratified Models of Probabilistic Processes, Proc. LICS’90, IEEE-CS Press, 130–141, 1990.Google Scholar
  13. 13.
    Gorrieri, R., Rensink, A., Action Refinement, Handbook of Process Algebra, Elsevier Science, 1047–1147, 2001.Google Scholar
  14. 14.
    Hoare, C.A.R., Communicating Sequential Processes, Prentice-Hall, 1985.Google Scholar
  15. 15.
    Katoen, J.-P., Quantitative and Qualitative Extensions of Event Structures, PhD Thesis, University of Twente, 1996.Google Scholar
  16. 16.
    Katoen, J.-P., Baier, C., and Latella, D., Metric Semantics for True Concurrent Real Time, Th. Comp. Sci., 254(1-2): 501–542, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Katoen, J-P., Langerak, R., Latella, D., and Brinksma, E., On Specifying Real-Time Systems in a Causality-Based Setting, in: Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, 1135: 385–405, 1996.Google Scholar
  18. 18.
    Langerak, R., Transformations and Semantics for LOTOS, PhD Thesis, University of Twente, 1992.Google Scholar
  19. 19.
    Loogn, R., Goltz, U., Modelling Nondeterministic Concurrent Processes with Event Structures, Fund. Inf., 14(1): 39–74, 1991.Google Scholar
  20. 20.
    Majster-Cederbaum, M., Salger, F., Correctness by Construction: Towards Verification in Hierarchical System Development, Lecture Notes in Computer Science, 1885: 163–180, 2000.Google Scholar
  21. 21.
    Majster-Cederbaum, M., Salger, F., and Sorea, M., A Priori Verification of Reactive Systems, Proc. FORTE/PSTV 2000, Kluwer Academic Publishers, 35–50, 2000.Google Scholar
  22. 22.
    Majster-Cederbaum, M., Wu, J., Action Refinement for True Concurrent Real Time, Proc. ICECCS 2001, IEEE Computer Society Press, 58–68, 2001.Google Scholar
  23. 23.
    Milner, R., Communication and Concurrency, Prentice-Hall, 1989.Google Scholar
  24. 24.
    Murphy, D., Pitt, D., Real-Timed Concurrent Refineable Behaviours, Lecture Notes in Computer Science, 571: 529–545, 1992.Google Scholar
  25. 25.
    Zic, J., Time-Constrained Buffer Specifications in CSP+T and Timed CSP, ACM Transactions on Programming and Systems, 16(6): 1661–1674, 1994.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Harald Fecher
    • 1
  • Mila Majster-Cederbaum
    • 1
  • Jinzhao Wu
    • 1
  1. 1.Fakultät für Mathematik und Informatik D7 27Universität MannheimMannheimGermany

Personalised recommendations