Abstract
A switched probabilistic I/O automaton is a special kind of probabilistic I/O automaton (PIOA), enriched with an explicit mechanism to exchange control with its environment. Every closed system of switched automata satisfies the key property that, in any reachable state, at most one component automaton is active. We define a trace-based semantics for switched PIOAs and prove it is compositional. We also propose switch extensions of an arbitrary PIOA and use these extensions to define a new trace-based semantics for PIOAs.
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
Aggarwal, S.: Time optimal self-stabilizing spanning tree algorithms. Master’s thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology (May 1994), Available as Technical Report MIT/LCS/TR-632
Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: Proceedings of the 42nd IEEE Symposium on Foundations of Computing, pp. 136–145 (2001)
de Alfaro, L., Henzinger, T.A., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 351–365. Springer, Heidelberg (2001)
Lincoln, P., Mitchell, J.C., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: ACM Conference on Computer and Communications Security, pp. 112–121 (1998)
Lynch, N.A., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: Proceedings of the 13th Annual ACM Symposium on the Principles of Distributed Computing, Los Angeles, CA, pp. 314–323 (August 1994)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Compositionality for probabilistic automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 208–221. Springer, Heidelberg (2003)
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)
Pogosyants, A., Segala, R., Lynch, N.A.: Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing 13(3), 155–186 (2000)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology (June 1995), Available as Technical Report MIT/LCS/TR-676
Stoelinga, M.I.A.: An introduction to probabilistic automata. Bulletin of the European Association for Theoretical Computer Science 78, 176–198 (2002)
Stoelinga, M.I.A., Vaandrager, F.W.: Root contention in IEEE 1394. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 53–74. Springer, Heidelberg (1999)
Sokolova, A., de Vink, E.P.: Probabilistic automata: System types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1–43. Springer, Heidelberg (2004)
Wu, S.-H., Smolka, S.A., Stark, E.W.: Composition and behaviors of probabilistic i/o automata. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 513–528. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cheung, L., Lynch, N., Segala, R., Vaandrager, F. (2005). Switched Probabilistic I/O Automata. In: Liu, Z., Araki, K. (eds) Theoretical Aspects of Computing - ICTAC 2004. ICTAC 2004. Lecture Notes in Computer Science, vol 3407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31862-0_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-31862-0_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25304-4
Online ISBN: 978-3-540-31862-0
eBook Packages: Computer ScienceComputer Science (R0)