×

Compositional design of stochastic timed automata. (English) Zbl 1475.68146

Kulikov, Alexander S. (ed.) et al., Computer science – theory and applications. 11th international computer science symposium in Russia, CSR 2016, St. Petersburg, Russia, June 9–13, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9691, 117-130 (2016).
Summary: 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.
For the entire collection see [Zbl 1337.68014].

MSC:

68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Software:

MoDeST
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) Automata, Languages and Programming. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990) · Zbl 0765.68150
[2] Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994) · Zbl 0803.68071
[3] Alur, R., Fix, L., Henzinger, T.A.: A determinizable class of timed automata. In: Dill, D.L. (ed.) Computer Aided Verification. LNCS, vol. 818, pp. 1–13. Springer, Heidelberg (1994) · Zbl 0912.68132
[4] Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(7), 524–541 (2003) · Zbl 05113886
[5] Baier, C., Hermanns, H., Katoen, J.-P., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200, 149–214 (2005) · Zbl 1101.68053
[6] Baier, C., Hermanns, H., Katoen, J.-P., Wolf, V.: Bisimulation and simulation relations for Markov chains. In: Proceedings of the Workshop Essays on Algebraic Process Calculi, vol. 162. ENTCS, pp. 73–78 (2006) · Zbl 1316.68085
[7] Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076
[8] Bertrand, N., Bouyer, P., Brihaye, T., Menet, Q., Baier, Ch., Größer, M., Jurdziński, M.: Stochastic timed automata. Logical Methods Comput. Sci. 10(4), 1–73 (2014) · Zbl 1448.68256
[9] Bertrand, N., Bouyer, P., Brihaye, Th., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: Proceedings of 5th International Conference on Quantitative Evaluation of Systems (QEST 2008). IEEE Computer Society Press (2008)
[10] Bohnenkamp, H., D’Argenio, P., Hermanns, H., Katoen, J.-P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812–830 (2006) · Zbl 05341944
[11] Bouyer, P., Brihaye, T., Carlier, P., Menet, Q.: Compositional design of stochastic timed automata. Research Report LSV-15-06, Laboratoire Spécification et Vérification, ENS Cachan, France, 51 pages, December 2015 · Zbl 1475.68146
[12] Bravetti, M., Gorrieri, R.: The theory of interactive generalized semi-Markov processes. Theor. Comput. Sci. 282(1), 5–32 (2002) · Zbl 0997.68083
[13] Brázdil, T., Hermanns, H., Krcál, J., Kretínský, J., Rehák, V.: Verification of open interactive Markov chains. In: Proceedings of the 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), vol. 18. LIPIcs, pp. 474–485. Springer (2012) · Zbl 1354.68170
[14] Brázdil, T., Krčál, J., Křetínský, J., Řehák, V.: Fixed-delay events in generalized semi-Markov processes revisited. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 140–155. Springer, Heidelberg (2011) · Zbl 1343.68161
[15] D’Argenio, P., Katoen, J.-P.: A theory of stochastic systems Part I: Stochastic automata. Inf. Comput. 203(1), 1–38 (2005) · Zbl 1105.68061
[16] D’Argenio, P., Katoen, J.-P.: A theory of stochastic systems part II: Process algebra. Inf. Comput. 203(1), 39–74 (2005) · Zbl 1106.68073
[17] Desharnais, J., Panangaden, P.: Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. J. Logic Algebraic Program. 56, 99–115 (2003) · Zbl 1053.68065
[18] Glynn, P.W.: A GSMP formalism for discrete event systems. Proc. IEEE 77(1), 14–23 (1989)
[19] Hartmanns, A.: Modest - a unified language for quantitative models. In: Proceedings of the Forum on Specification and Design Languages (FDL 2012), pp. 44–51. IEEE Computer Society Press (2012)
[20] Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 593–598. Springer, Heidelberg (2014) · Zbl 06400500
[21] Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002) · Zbl 1012.68142
[22] Hermanns, H., Katoen, J.-P.: The how and why of interactive Markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311–337. Springer, Heidelberg (2010) · Zbl 1312.68152
[23] Hermanns, H., Krčál, J., Křetínský, J.: Compositional verification and optimization of interactive Markov chains. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 364–379. Springer, Heidelberg (2013) · Zbl 1390.68472
[24] Hermanns, H., Zhang, L.: From concurrency models to numbers - performance and dependability. In: Software and Systems Safety - Specification and Verification, vol. 30. NATO Science for Peace and Security Series, pp. 182–210. IOS Press (2011)
[25] Stoelinga, M.: Fun with FireWire: a comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal Aspects Comput. 14(3), 328–337 (2003) · Zbl 1029.68022
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.