Abstract
In this paper we present a probabilistic-timed process algebra, which tries to unify the best solutions of previous probabilistic and timed algebras. We provide an operational semantics for the new language (PTPA), and from this operational semantics we define a testing semantics based on the probability with which processes pass tests. Afterwards the induced testing equivalence is operationally characterized by probabilistic timed traces.
Research supported in part by the CICYT project TIC 94-0851-C02-02
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J. C. M. Baeten and J. A. Bergstra. Real time process algebra. Formal Aspects of Computing, 3:142–188, 1993.
J.C.M. Baeten, J.A. Bergstra, and S.A. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities. Information and Computation, 121(2):234–255, 1995.
I. Christoff. Testing Equivalences for Probabilistic Processes. PhD thesis, Department of Computer Systems. Uppsala University, 1990.
R. Cleaveland, I. Lee, P. Lewis, and S.A. Smolka. A theory of testing for soft real-time processes. In 8th International Conference on Software Engineering and Knowledge Engineering, 1996.
R. Cleaveland, S.A. Smolka, and A.E. Zwarico. Testing preorders for probabilistic processes. In 19th ICALP, LNCS 623, pages 708–719, 1992.
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.
C. Gregorio, L. Llana, M. Núñez, and P. Palao. Testing semantics for a probabilistic-timed process algebra. Technical Report 49/97, Dpt. Informática y Automática, Universidad Complutense de Madrid, 1997.
C. Gregorio and M. Núñez. Specifying and verifying the Alternating Bit Protocol with Probabilistic-Timed LOTOS. In COST 247 International Workshop on Applied Formal Methods in System Design, pages 38–50, 1996.
Jan Friso Groote. Transition system specifications with negative premises. Theoretical Computer Science, 118:263–299, 1993.
Hans A. Hansson. Time and Probability in Formal Design of Distributed Systems. PhD thesis, Department of Computer Systems. Uppsala University, 1991.
M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.
M. Hennessy and T. Regan. A process algebra for timed systems. Information and Computation, 117(2):221–239, 1995.
B. Jonsson, C. Ho-Stuart, and W. Yi. Testing and refinement for nonde-terministic and probabilistic processes. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, pages 418–430, 1994.
B. Jonsson and W. Yi. Compositional testing preorders for probabilistic processes. In 10th IEEE Symposium on Logic In Computer Science, pages 431–443, 1995.
L. Llana, D. de Frutos, and M. Núñez. Testing semantics for urgent timed algebras. In 3rd AMAST Workshop on Real-Time Systems, 1996.
G. Lowe. Probabilistic and prioritized models of timed CSP. Theoretical Computer Science, 138:315–352, 1995.
K. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, 1991.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
M. Núñez and D. de Frutos. Testing semantics for probabilistic LOTOS. In Formal Description Techniques VIII, pages 365–380, 1995.
M. Núñez, D. de Frutos, and L. Llana. Acceptance trees for probabilistic processes. In CONCUR'95, LNCS 962, pages 249–263, 1995.
X. Nicollin and J.Sifakis. An overview and synthesis on timed process algebras. In Computer Aided Verification'91, LNCS 575, pages 376–398, 1991.
M. Núñez. Semánticas de Pruebas para Álgebras de Procesos Probabilísticos. PhD thesis, Universidad Complutense de Madrid, 1996. In Spanish.
Y. Ortega-Mallén and D. de Frutos. Timed observations: a semantic model for real-time concurrency. In Proceedings of Working Conference on Programming Concepts and Methods, IFIP TC 2, 1990.
G.M. Reed and A.W. Roscoe. A timed model for CSP. In 13th ICALP, LNCS 226, pages 314–323, 1986.
S. Schneider. An operational semantics for timed CSP. Information and Computation, 116:193–213, 1995.
E.W. Stark and S.A. Smolka. A complete axiom system for finite-state probabilistic processes, 1996.
C. Tofts. Processes with probabilities, priority and time. Formal Aspects of Computing, 6:536–564, 1994.
R. van Glabbeek, S.A. Smolka, and B. Steffen. Reactive, generative and stratified models of probabilistic processes. Information and Computation, 121(1):59–80, 1995.
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. CCS+Time = an interleaving model for real time systems. In 18th ICALP, LNCS 510, pages 217–228, 1991.
W. Yi and K.G. Larsen. Testing probabilistic and nondeterministic processes. In Protocol Specification, Testing and Verification XII, pages 47–61, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gregorio-Rodríguez, C., Llana-Díaz, L., Núñez, M., Palao-Gostanza, P. (1997). Testing semantics for a probabilistic-timed process algebra. In: Bertran, M., Rus, T. (eds) Transformation-Based Reactive Systems Development. ARTS 1997. Lecture Notes in Computer Science, vol 1231. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63010-4_24
Download citation
DOI: https://doi.org/10.1007/3-540-63010-4_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63010-4
Online ISBN: 978-3-540-69058-0
eBook Packages: Springer Book Archive