In this paper, we study the model of stochastic timed automata and we target the definition of adequate composition operators that will allow a compositional approach to the design of stochastic systems with hard real-time constraints. This paper achieves the first step towards that goal. Firstly, we define a parallel composition operator that (we prove) corresponds to the interleaving semantics for that model; we give conditions over probability distributions, which ensure that the operator is well-defined; and we exhibit problematic behaviours when this condition is not satisfied. We furthermore identify a large and natural subclass which is closed under parallel composition. Secondly, we define a bisimulation notion which naturally extends that for continuous-time Markov chains. Finally, we importantly show that the defined bisimulation is a congruence w.r.t. the parallel composition, which is an expected property for a proper modular approach to system design.
CITATION STYLE
Bouyer, P., Brihaye, T., Carlier, P., & Menet, Q. (2016). Compositional design of stochastic timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9691, pp. 117–130). Springer Verlag. https://doi.org/10.1007/978-3-319-34171-2_9
Mendeley helps you to discover research relevant for your work.