Abstract
We extend the trace semantics for labeled transition systems to a randomized model of concurrent computation. The main objective is to obtain a compositional semantics. The role of a trace in the randomized model is played by a probability distribution over traces, called a trace distribution. We show that the preorder based on trace distribution inclusion is not a precongruence, and we build an elementary context, called the principal context, that is sufficiently powerful to characterize the coarsest precongruence that is contained in the trace distribution preorder. Finally, we introduce a notion of a probabilistic forward simulation and we prove that it is sound for the trace distribution precongruence. An important characteristic of probabilistic forward simulations is that they relate states to probability distributions over states.
Supported by NSF grant CCR-92-25124, by DARPA contract N00014-92-J-4033, and by AFOSRONR contract F49620-94-1-0199.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 21(4), 1985.
J. Aspnes and M.P. Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms, 15(1):441–460, September 1990.
M. Ben-Or. Another advantage of free choice: completely asynchronous agreement protocols. In Proceedings of the 2 nd Annual ACM PODC, 1983.
S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560–599, 1984.
I. Christoff. Testing Equivalences for Probabilistic Processes. PhD thesis, Department of Computer Science, Uppsala University, 1990.
R. Gawlick, R. Segala, J.F. Søgaard-Andersen, and N.A. Lynch. Liveness in timed and untimed systems. In Proceedings 21 th ICALP, Jerusalem, LNCS 820, 1994. A full version appears as MIT Technical Report number MIT/LCS/TR-587.
R.J. van Glabbeek, S.A. Smolka, B. Steffen, and C.M.N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proceedings 5 th Annual Symposium on Logic in Computer Science, Philadelphia, USA, pages 130–141. IEEE Computer Society Press, 1990.
H. Hansson. Time and Probability in Formal Design of Distributed Systems, volume 1 of Real-Time Safety Critical Systems. Elsevier, 1994.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
B. Jonsson and K.G. Larsen. Specification and refinement of probabilistic processes. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science, pages 266–277, July 1991.
B. Jonsson and J. Parrow, editors. Proceedings of CONCUR 94, LNCS 836, 1994.
C.C. Jou and S.A. Smolka. Equivalences, congruences, and complete axiomatizations for probabilistic processes. In Proceedings of CONCUR 90, LNCS 458, pages 367–383, 1990.
K.G. Larsen and A. Skou. Compositional verification of probabilistic processes. In Proceedings of CONCUR 92 LNCS 630, pages 456–471, 1992.
N.A. Lynch, I. Saias, and R. Segala. Proving time bounds for randomized distributed algorithms. In Proceedings of the 13 th Annual ACM PODC, pages 314–323, 1994.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations for timing-based systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop “Real-Time: Theory in Practice”, LNCS 600, pages 397–446, 1991.
G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer science Department, Aarhus University, 1981.
A. Pogosyants and R. Segala. Formal verification of timed properties of randomized distributed algorithms. In Proceedings of the 14 th Annual ACM PODC, 1995.
M.O. Rabin. Probabilistic automata. Information and Control, 6:230–245, 1963.
R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, Dept. of Electrical Engineering and Computer Science, 1995.
R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. In Jonsson and Parrow [11], pages 481–496.
K. Seidel. Probabilistic communicating processes. Technical Report PRG-102, Ph.D. Thesis, Programming Research Group, Oxford University Computing Laboratory, 1992.
M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of 26th IEEE Symposium on Foundations of Computer Science, pages 327–338, 1985.
S.H. Wu, S. Smolka, and E.W. Stark. Composition and behaviors of probabilistic I/O automata. In Jonsson and Parrow [11].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Segala, R. (1995). A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_17
Download citation
DOI: https://doi.org/10.1007/3-540-60218-6_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60218-7
Online ISBN: 978-3-540-44738-2
eBook Packages: Springer Book Archive