Abstract
We describe the main features of the Probabilistic Timed I/O Automata (PTIOA)—a framework for modeling and analyzing discretely communicating probabilistic hybrid systems. A PTIOA can choose the post-state of a discrete transition either nondeterministically or according to (possibly continuous) probability distributions. The framework supports modeling of large systems as compositions of concurrently executing PTIOAs, which interact through shared transition labels. We develop a trace-based semantics for PTIOAs and show that PTIOAs are compositional with respect a new notion of external behavior.
Supported by the MURI project:DARPA/AFOSR MURI F49620-02-1-0325 grant.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bujorianu, M., Lygeros, J.: General stochastic hybrid systems: Modelling and optimal control. In: IEEE Conference on Decision and Control, December 2004, IEEE Computer Society Press, Los Alamitos (2004)
Canetti, R., et al.: Task-structured probabilistic I/O automata. Tech. Report MIT-CSAIL-TR-2006-060, MIT, Cambridge (2006)
Cattani, S., et al.: Stochastic transition systems for continuous state spaces and non-determinism. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 125–139. Springer, Heidelberg (2005)
Cheung, L.: Reconciling nondeterministic and probabilistic choices. PhD thesis, ICIS, Radboud University Nijmegen, The Netherlands (2006)
Danos, V., et al.: Bisimulation and cocongruence for probabilistic systems. Information and Computation, Special issue for selected papers from CMCS04 (2005)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, CA, Technical Report STAN-CS-TR-98-1601 (1997)
Smolka, S., Stark, E., Cleaveland, R.: A process-algebraic language for probabilistic I/O automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 189–203. Springer, Heidelberg (2003)
Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. Springer, Heidelberg (2002)
Kaynar, D., et al.: The Theory of Timed I/O Automata. Synthesis Lectures on Computer Science. Morgan Claypool, San Rafael (2005)
Mitra, S., Lynch, N.: Trace-based Semantics for Probabilistic Timed I/O Automata. Full version, http://theory.lcs.mit.edu/~mitras/research/PTIOA06-full.pdf
Mitra, S., Lynch, N.: Approximate simulations for task-structured probabilistic I/O automata. In: LICS Workshop on Probabilistic Automata and Logics (2006)
van Breugel, F., et al.: Domain theory, testing and simulation for labelled markov processes. In: Theoretical Computer Science (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Mitra, S., Lynch, N. (2007). Trace-Based Semantics for Probabilistic Timed I/O Automata. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds) Hybrid Systems: Computation and Control. HSCC 2007. Lecture Notes in Computer Science, vol 4416. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71493-4_69
Download citation
DOI: https://doi.org/10.1007/978-3-540-71493-4_69
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71492-7
Online ISBN: 978-3-540-71493-4
eBook Packages: Computer ScienceComputer Science (R0)