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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
Aceto, L, Action Refinement in Process Algebra, Cambridge Univ. Press, 1992.
Bolognesi, T., Brinksma, E., Introduction to the ISO Specification Language LOTOS, Comp. Netw. and ISDN Syst., 14: 25–59, 1987.
Bowman, H., Derrick, J., Extending LOTOS with Time: A True Concurrency Perspective, Lecture Notes in Computer Science, 1231: 383–399, 1997.
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.
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.
D’Argenio, P. R., Hermanns, H., and Katoen, J.-P., On Generative Parallel Composition, Electronic Notes in Theoretical Computer Science, 22, 1999.
Fecher, H., Majster-Cederbaum, M., and Wu, J., Bundle Event Structures: A Revised Cpo Approach, Information Processing Letters, accepted, 2001.
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.
van Glabbeek, R., Goltz, U., Refinement of Actions and Equivalence Notions for Concurrent Systems, Acta Informatica, 37: 229–327, 2001.
van Glabbeek, R., Smolka, S. A., and Steffen, B., Reactive, Generative and Stratified Models of Probabilistic Processes, Information and Computation, 121: 59–80, 1995.
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.
Gorrieri, R., Rensink, A., Action Refinement, Handbook of Process Algebra, Elsevier Science, 1047–1147, 2001.
Hoare, C.A.R., Communicating Sequential Processes, Prentice-Hall, 1985.
Katoen, J.-P., Quantitative and Qualitative Extensions of Event Structures, PhD Thesis, University of Twente, 1996.
Katoen, J.-P., Baier, C., and Latella, D., Metric Semantics for True Concurrent Real Time, Th. Comp. Sci., 254(1-2): 501–542, 2001.
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.
Langerak, R., Transformations and Semantics for LOTOS, PhD Thesis, University of Twente, 1992.
Loogn, R., Goltz, U., Modelling Nondeterministic Concurrent Processes with Event Structures, Fund. Inf., 14(1): 39–74, 1991.
Majster-Cederbaum, M., Salger, F., Correctness by Construction: Towards Verification in Hierarchical System Development, Lecture Notes in Computer Science, 1885: 163–180, 2000.
Majster-Cederbaum, M., Salger, F., and Sorea, M., A Priori Verification of Reactive Systems, Proc. FORTE/PSTV 2000, Kluwer Academic Publishers, 35–50, 2000.
Majster-Cederbaum, M., Wu, J., Action Refinement for True Concurrent Real Time, Proc. ICECCS 2001, IEEE Computer Society Press, 58–68, 2001.
Milner, R., Communication and Concurrency, Prentice-Hall, 1989.
Murphy, D., Pitt, D., Real-Timed Concurrent Refineable Behaviours, Lecture Notes in Computer Science, 571: 529–545, 1992.
Zic, J., Time-Constrained Buffer Specifications in CSP+T and Timed CSP, ACM Transactions on Programming and Systems, 16(6): 1661–1674, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fecher, H., Majster-Cederbaum, M., Wu, J. (2002). Action Refinement for Probabilistic Processes with True Concurrency Models. In: Hermanns, H., Segala, R. (eds) Process Algebra and Probabilistic Methods: Performance Modeling and Verification. PAPM-PROBMIV 2002. Lecture Notes in Computer Science, vol 2399. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45605-8_6
Download citation
DOI: https://doi.org/10.1007/3-540-45605-8_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43913-4
Online ISBN: 978-3-540-45605-6
eBook Packages: Springer Book Archive