Abstract
In this paper we present a probabilistic extension of LOTOS which is upward compatible with LOTOS. We present testing semantics for the reactive and generative models described in [vGSST90]. While there is a certain lose of the meaning of probabilities in the reactive model, testing with probabilistic tests proves to be too strong because it does not relate behavior expressions which we expect to be equivalent. This is why we introduce the limited generative model, where tests are not allowed to have explicit probabilities. We give a fully abstract characterization for the reactive model, while we give alternative characterizations (based on a set of essential tests) for the generative and limited generative models. We also present some algebraic laws for each of the models, including some laws which establish the difference between the three models.
Chapter PDF
Similar content being viewed by others
References
E. Brinksma, G. Scollo, and C. Steenhergen. LOTOS specifications, their implementations and their tests. In PSTV VI, pages 349–360, 1986.
I. Christoff. Testing Equivalences for Probabilistic Processes. PhD thesis, Department of Computer Systems. Uppsala University, 1990.
R. Cleaveland, S.A. Smolka, and A.E. Zwarico. Testing preorders for probabilistic processes. In 19th ICALP, LNCS 623, pages 708–719, 1992.
D. de Frutos, G. Leduc, L. Léonard, L. Liana, C. Miguel, J. Quemada, and G. Rabay. Belgian-Spanish proposal for a time extended LOTOS. In Working Draft on Enhancements to LOTOS (Annex E). ISO/IEC JTC1/SC21/WG1, 1994.
D. de Frutos, M. Nrinez, and J. Quemada. Characterizing termination in LOTOS via testing. In PSTV XV, pages 225–240, 1995.
A. Giacalone, C.-C. Jou, and S.A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proceedings of Working Conference on Programming Concepts and Methods, IFIP TC 2, 1990.
M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32 (1): 137–161, 1985.
B. Jonsson and W. Yi. Compositional testing preorders for probabilistic processes. In 10th IEEE Symposium on Logic In Computer Science, 1995.
J.P. Katoen, R. Langerak, and D. Latella. Modeling systems by probabilistic process algebra: An event structures approach. In FORTE VI, 1994.
LOTOS. A formal description technique based on the temporal ordering of observational behaviour. IS 8807, TC97/SC21, 1988.
K.G. Larsen and A. Skou. Compositional verification of probabilistic processes. In CONCUR’92, LNCS 630, pages 456–471, 1992.
C. Miguel, A. Fernandez, and L. Vidaller. LOTOS extended with probabilistic behaviours. Formal Aspects of Computing, 5: 253–281, 1993.
R. Milner. A Calculus of Communicating Systems. LNCS 92, 1980.
NdFL95] M. Nunez, D. de Frutos, and L. Liana. Acceptance trees for probabilistic processes. In CONCUR’95 1995.
M. Nunez, P. Palao, and M.T. Morazan. Associativity in probabilistic process algebras. Technical Report DIA-UCM 14/94, Universidad Complutense de Madrid, 1994.
J. Quemada, D. de Frutos, and A. Azcorra. TIC: A TImed Calculus. Formal Aspects of Computing, 5: 224–252, 1993.
R. van Glabbeek, S.A. Smolka, B. Steffen, and C.M.N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In 5th IEEE Symposium on Logic In Computer Science, pages 130–141, 1990.
S. Yuen, R. Cleaveland, Z. Dayar, and S.A. Smolka. Fully abstract characterizations of testing preorders for probabilistic processes. In CONCUR’94, LNCS 836, pages 497–512, 1994.
W. Yi and K.G. Larsen. Testing probabilistic and nondeterministic processes. In PSTV XII, pages 47–61, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Nwnez, M., Frutos, D. (1996). Testing Semantics for Probabilistic LOTOS. In: Bochmann, G.v., Dssouli, R., Rafiq, O. (eds) Formal Description Techniques VIII. FORTE 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34945-9_27
Download citation
DOI: https://doi.org/10.1007/978-0-387-34945-9_27
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2958-9
Online ISBN: 978-0-387-34945-9
eBook Packages: Springer Book Archive