Abstract
In this paper, we study behaviour descriptions with uncertain information such as “the probability of a system failure within a given time period is less than or equal to 0.3” in terms of process algebras. Typical systems that may show such behaviours include communicating systems with unreliable components, e.g. faulty medium. We present a process model for such behaviours, in which uncertain information is described by means of intervals of probabilities. In particular, we introduce a stochastic choice operator
[Φ i] E i, where Φ i's are intervals of probabilities. Roughly speaking, it is a process which may become E i in one unit of time with a probability within the interval Φ i. Such a process is considered as a specification specifying a set of processes with less uncertain information. We develop a notion of probabilistic simulation to order specifications in terms of the degree of uncertainty in the specifications, which generalize the notion of probabilistic bisimulation. A complete axiomatization for the induced congruence is provided.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G. Berry and L. Cosserat, The Synchronous Programming Language ESTEREL and its Mathematical Semantics, LNCS No. 197, 1983.
J.C.M. Baeten, J.A. Bergstra and S.A. Smolka. Axiomatizing Probabilistic Processes: ACP with Generative Probabilities, in the proc. of CONCUR92, LNCS 630, 1992.
I. Christoff, Testing Equivalence for Probabilistic Processes, Ph.D. Thesis, Uppsala University, Uppsala, Sweden, 1990.
Karlis Cerans, Jens Chr. Godskesen and Kim G. Larsen Time Modal Specification — Theory and Tools. Proceedings of the 5th Int. Conf. on Computer Aided Verificatio n, 1993.
J.F. Groote, Specification and Verification of Real Time Systems in ACP, Report CS-R9015, CWI, Amsterdam, 1990, in the proceedings of PSTV X, 1990.
R. van Glabbeek, S. A. Smolka, B. Steffen and C. Tofts, Reactive, Generative and Stratified Models of Probabilistic Processes, in the Proc. of LICS'90, 1990.
M. Hennessy, Algebraic Theory of Processes, MIT press, 1988.
H. Hansson and Bengt Jonsson, A Calculus for Communicating Systems with Time and Probability, in the Proc. of the 11'th IEEE Real Time Systems Symposium, 1990.
M. Hennessy and T. Regan, A Temporal Process Algebra, Technical Report 5/91, University of Sussex, 1991.
A. Jeffrey, Linear Time Process Algebra, In the proc. of to CAV91, Aalborg University, Denmark.
B. Jonsson and K. G. Larsen, Specification and Refinement of Probabilistic Processes, LICS'91, Amsterdam, 1991.
C. Jou and S.A. Smolka, Equivalences, Congruences and Complete Axiomatizations for Probabilistic Processes, in the Proc. of CONCUR'90, LNCS 458, 1989.
Gavin Lowe. Probabilities and Priorities in Timed CSP, Ph.D Thesis, Oxford, 1993.
K. G. Larsen and A. Skou, Bisimulation through Probabilistic Testing, in the Proc. of ACM POPL'89, 1989.
K. G. Larsen and A. Skou, Compositional Verification of Probabilistic Processes, in the proc. of CONCUR92, LNCS 630, 1992.
R. Milner, A Calculus of Communicating Systems, LNCS 92, 1980.
R. Milner, Calculi for Synchrony and Asynchrony, TCS, Vol 25, 1983.
R. Milner, Communication and Concurrency, Prentice Hall, 1989.
F. Moller and C. Tofts, A Temporal Calculus of Communicating Systems, LNCS, No. 458, 1990.
R. de Nicola, Extensional Equivalences For Transition Systems, Acta Informatia 24, 1987.
R. de Nicola and M. Hennessy, Testing equivalences for processes, TCS vol. 34, 1984.
W.P. de Roever and J.J.M. Hooman, Design and Verification of Real-time Distributed Computing: an Introduction to Compositional Methods, Proceeding of the 9th IFIP WG 6.1 International Symposium on Protocol Specification, Testing and Verification, 1989.
G.M. Reed and A.W. Roscoe, A Timed Model for Communicating Sequential Processes, LNCS, No. 226, 1986.
J. Sifakis et al. The Algebra of Timed Processes ATP: Theory and Application, Laboratoire de Genie Informatique, IMAG-Campus, B.P.53X, 38041 Grenoble Cedex, France, December 1990, in M. Broy and C.B. Jones, Programming Concepts and Methods, 1990.
Wang Yi, CCS + Time = an Interleaving Model for Real Time Systems, in the Proc. of ICALP'91, LNCS No. 510.
Wang Yi and Kim G Larsen, Testing Nondeterministic and Probabilistic Processes, in the Proc. of the 12th IFIP International Symposium on Protocol Specification, Testing and Verification, Florida, USA, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yi, W. (1994). Algebraic reasoning for real-time probabilistic processes with uncertain information. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_190
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_190
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58468-1
Online ISBN: 978-3-540-48984-9
eBook Packages: Springer Book Archive