×

Hiding resources that can fail: An axiomatic perspective. (English) Zbl 1003.68089

Summary: In earlier work, we presented a process algebra, PACSR, that uses a notion of resource failure to capture probabilistic behavior in reactive systems. PACSR also supports an operator for resource hiding. In this paper, we carefully consider the interaction between these two features from an axiomatic perspective. For this purpose, we introduce a subset of PACSR, called “PACSR-lite”, that allows us to isolate the semantic issues surrounding resource hiding in a probabilistic setting, and provide a sound and complete axiomatization of strong bisimulation for this fragment.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baeten, J.; Bergstra, J.; Smolka, S., Axiomatizing probabilistic processes: ACP with generative probabilities, Inform. and Comput., 121, 2, 234-255 (1995) · Zbl 0829.60044
[2] Brémond-Grégoire, P.; Choi, J.; Lee, I., A complete axiomatization of finite-states ACSR processes, Inform. and Comput., 138, 2, 124-159 (1997) · Zbl 0885.68064
[3] Giacalone, A.; Jou, C.; Smolka, S., Algebraic reasoning for probabilistic concurrent systems, (Proc. Working Conf. on Programming Concepts Methods, IFIP TC 2 (1990), North-Holland: North-Holland Amsterdam)
[4] Hansson, H., Time and probability in formal design of distributed systems, PhD thesis (1991), Department of Computer Systems, Uppsala University, DoCS 91/27
[5] Katoen, J.-P.; Langerak, R.; Latella, D., Modeling systems by probabilistic process algebra: An event structured approach, (Proc. FORTE’92 (1993)), 255-270
[6] Larsen, K.; Skou, A., Bisimulation through probabilistic testing, (Conf. Record 16th ACM Symposium on Principles of Programming Languages (1989)), 344-352
[7] Lee, I.; Brémond-Grégoire, P.; Gerber, R., A process algebraic approach to the specification and analysis of resource-bound real-time systems, Proc. IEEE, 82, 158-171 (1994)
[8] Milner, R., A Calculus of Communicating Systems. A Calculus of Communicating Systems, Lecture Notes in Comput. Sci., 92 (1980), Springer: Springer Berlin · Zbl 0452.68027
[9] Milner, R., A complete axiomatization for observational congruence of finite-state behaviors, Inform. and Comput., 81, 227-247 (1989) · Zbl 0688.68050
[10] Park, D., Concurrency and automata on infinite sequences, (Proc. 5th GI Conference. Proc. 5th GI Conference, Lecture Notes in Comput. Sci., 104 (1981), Springer: Springer Berlin), 167-183
[11] Philippou, A.; Sokolsky, O.; Cleaveland, R.; Lee, I.; Smolka, S., Probabilistic resource failure in a real-time process algebra, (Proc. CONCUR’98 (1998))
[12] Philippou, A.; Sokolsky, O.; Lee, I.; Cleaveland, R.; Smolka, S., Hiding resources that can fail: An axiomatic perspective, Technical Report TR-2001-1 (2001), Department of Computer Science, University of Cyprus, Available at http://www.cs.ucy.ac.cy/Research/Technical_reports.html · Zbl 1003.68089
[13] Seidel, K., Probabilistic CSP, PhD thesis (1992), Oxford University
[14] Tofts, C., Processes with probabilities, priorities and time, Formal Aspects Comput., 4, 536-564 (1994) · Zbl 0820.68072
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.