Priority as extremal probability
Tóm tắt
We extend the stratified model of probabilistic processes to obtain a very general notion ofprocess priority. The main idea is to allow probability guards of value 0 to be associated with alternatives of a probabilistic summation expression. Such alternatives can be chosen only if the non-zero alternatives are precluded by contextual constraints. We refer to this model as one of “extremal probability” and to its signature asPCCS
ζ. We providePCCS
ζ with a structural operational semantics and a notionof probabilistic bisimulation, which is shown to be a congruence. Of particular interest is the abstractionPCCS
π ofPCCS
ζ in which all non-zero probability guards are identified.PCCS
π represents a customized framework for reasoning about priority, and covers all features of process algebras proposed for reasoning about priority that we know of.
Tài liệu tham khảo
Barrett, G.: The semantics of priority and fairness in occam. InMathematical Foundations of Programming Semantics, pages 194–208. Volume 442 ofLecture Notes in Computer Science, Springer-Verlag, 1989.
Baeten, J. C. M., Bergstra, J. A. and Klop, J. W.: Syntax and defining equations for an interrupt mechanism in process algebra.Fundamenta Informaticae IX, pages 127–168, 1986.
Best, E. and Koutny, M.: Petri net semantics of priority systems.Theoretical Computer Science, 96(1):175–215, 1992.
Camilleri, J. A.: Priority in process calculi. Technical Report No. 227, Computer Laboratory, Univesity of Cambridge, Ph.D. Thesis, Cambridge, England, June 1991.
Cousot, P. and Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. InConf. Record of the 4 th Annual ACM Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, CA, 1977.
Cleaveland, R. J. and Hennessy, M. C. B.: Priorities in process algebras.Information and Computation, 87(1/2):58–77, 1990.
Cleaveland, R., Lüttgen, G. and Natarajan, V.: A process algebra with distributed priorities. InProceedings of CONCUR '96 — Seventh International Conference on Concurrency Theory. Lecture Notes in Computer Science, Springer-Verlag, 1996.
Camilleri, J. A. and Winskel, G.: CCS with priority choice. InProceedings of the 6th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, July 1991.
Fidge, C. J.: A formal definition of priority in CSP.ACM Transactions on Programming Languages and Systems, 15(4):681–705, September 1993.
German, S. M.: Programming in a general model of synchronization. InProceedings of CONCUR '92 — Third International Conference on Concurrency Theory, pages 534–549. Volume 630 ofLecture Notes in Computer Science, Springer-Verlag, 1992.
Giacalone, A., Jou, C.-C. and Smolka, S. A.: Algebraic reasoning for probabilistic concurrent systems. InProceedings of Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990. IFIP TC 2, North-Holland.
Gerber, R. and Lee, I.: A Resource-Based Prioritized Bisimulation for Real-Time Systems.Information and Computation, 113(1):102–142, August 1994.
Hansson, H. A.:Time and Probability in Formal Design of Distributed Systems, volume 1of Real-Time Safety Critical Systems. H. Zedan, editor, Elsevier, Amsterdam, 1994.
Hansson, H. A. and Orava, F.: A process algebra with incomparable priorities. In S. Purushothaman and A. Zwarico, editor,First North American Process Algebra Workshop, Workshops in Computing, pages 216–230, Port Jefferson, USA, 1992. Springer-Verlag. 3-540-19822-9.
Larsen, K. G. and Skou, A.: Bisimulation through probabilistic testing.Information and Computation, 94(1):1–28, September 1992.
Milner, R.:A Calculus of Communicating Systems, volume 92 ofLecture Notes in Computer Science. Springer-Verlag, Berlin, 1980.
Milner, R.: Calculi for synchrony and asynchrony.Theoretical Computer Science, 25:267–310, 1983.
Milner, R.:Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
Natarajan, V., Christoff, L., Christoff, I. and Cleaveland, R.: Priorities and abstraction in process algebra. In P. S. Thiagarajan, editor,Proceedings of Foundations of Software Technology and Theoretical Computer Science, pages 217–230. Volume 880 ofLecture Notes in Computer Science, Springer-Verlag, 1994.
Park, D. M. R.: Concurrency and automata on infinite sequences. InProceedings of 5th G.I. Conference on Theoretical Computer Science, pages 167–183. Volume 104of Lecture Notes in Computer Science, Springer-Verlag, 1981.
Plotkin, G. D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In J. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Current Trends in Concurrency. Volume 224 ofLecture Notes in Computer Science, Springer-Verlag, 1986.
Shapley, L.S.: Stochastic games.Proc. Nat. Acad. Sci. U.S.A., 39:1095–1100, 1953.
Tofts, C. M. N.: A synchronous calculus of relative frequency. In J. C. M. Baeten and J. W. Klop, editors,Proceedings of CONCUR '90, volume 458, pages 467–480. Volume 458 ofLecture Notes in Computer Science, Springer-Verlag, 1990.
van Glabbeek, R. J., Smolka, S. A. and Steffen. B.: Reactive, generative, and stratified models of probabilistic processes.Information and Computation, 121(1):59–80, August 1995.