nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities

verfasst von : Jeremy Sproston

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Clock-dependent probabilistic timed automata extend classical timed automata with discrete probabilistic choice, where the probabilities are allowed to depend on the exact values of the clocks. Previous work has shown that the quantitative reachability problem for clock-dependent probabilistic timed automata with at least three clocks is undecidable. In this paper, we consider the subclass of clock-dependent probabilistic timed automata that have one clock, that have clock dependencies described by affine functions, and that satisfy an initialisation condition requiring that, at some point between taking edges with non-trivial clock dependencies, the clock must have an integer value. We present an approach for solving in polynomial time quantitative and qualitative reachability problems of such one-clock initialised clock-dependent probabilistic timed automata. Our results are obtained by a transformation to interval Markov decision processes.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Derivation of Heard-of Predicates from Elementary Behavioral Patterns

Nächstes Kapitel A Formal Framework for Consent Management

From [18, Lemma 4.10], without loss of generality we can assume henceforth that schedulers map to distributions assigning positive probability to finite sets of actions, i.e., schedulers \(\sigma \) for which \(|\mathsf {support}(\sigma (r))|\) is finite for all \(r\in Paths ^{\mathcal {M}}_*\).

Given that there is only one action available from states such as \(((1,3),p_\mathrm {W},\mathsf {lb})\) and \(((1,3),p_\mathrm {W},\mathsf {rb})\), we omit both the action and the usual black box from the figure.

Note that \(\mathfrak {A}_{\mathfrak {M}[{\mathcal {P}}]}({l,B}) \ne \emptyset \) for each \((l,B) \in S_{\mathfrak {M}[{\mathcal {P}}]}^\mathsf {reg}\), by the assumptions that we made on 1c-cdPTA in Sect. 3 (namely, that it is always possible to take a probabilistic edge, either immediately or after letting time elapse).

We recall that \(\mathfrak {D}_{\mathfrak {M}[{\mathcal {P}}]}(s,\mathfrak {a}) = \bot \) for \(s\in S_{\mathfrak {M}[{\mathcal {P}}]}\) and \(\mathfrak {a}\in \mathfrak {A}_{\mathfrak {M}[{\mathcal {P}}]} \setminus \mathfrak {A}_{\mathfrak {M}[{\mathcal {P}}]}({s})\).

Akshay, S., Bouyer, P., Krishna, S.N., Manasa, L., Trivedi, A.: Stochastic timed games revisited. In: Faliszewski, P., Muscholl, A., Niedermeier, R., (eds.) Proceedings of MFCS 2016 LIPIcs, vol. 58, pp. 8:1–8:14. Leibniz-Zentrum für Informatik (2016)

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRef

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Bertrand, N., Bordais, B., Hélouët, L., Mari, T., Parreaux, J., Sankur, O.: Performance evaluation of metro regulations using probabilistic model-checking. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 59–76. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-18744-6_4CrossRef

Bertrand, N., et al.: Stochastic timed automata. Log. Methods Comput. Sci. 10(4), 1–73 (2014)MathSciNetCrossRef

Bertrand, N., Brihaye, T., Genest, B.: Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 313–328. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10696-0_25CrossRef

Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1001–1046. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_29CrossRefMATH

Bouyer, P., Larsen, K.G., Markey, N.: Model checking one-clock priced timed automata. Log. Methods Comput. Sci. 4(2), 1–28 (2008)MathSciNetCrossRef

Chakraborty, S., Katoen, J.-P.: Model checking of open interval markov chains. In: Gribaudo, M., Manini, D., Remke, A. (eds.) ASMTA 2015. LNCS, vol. 9081, pp. 30–42. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-18579-8_3CrossRef

10.

Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checking \(\omega \)-regular properties of interval Markov chains. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 302–317. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78499-9_22CrossRefMATH

11.

Chen, T., Han, T., Kwiatkowska, M.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210–216 (2013)MathSciNetCrossRef

12.

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)CrossRef

13.

Feng, L., Wiltsche, C., Humphrey, L.R., Topcu, U.: Synthesis of human-in-the-loop control protocols for autonomous systems. IEEE Trans. Autom. Sci. Eng. 13(2), 450–462 (2016)CrossRef

14.

Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4_3CrossRef

15.

Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1–2), 71–109 (2000)MathSciNetCrossRef

16.

Gregersen, H., Jensen, H.E.: Formal design of reliable real time systems. Master’s thesis, Department of Mathematics and Computer Science, Aalborg University (1995)

17.

Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111–131 (2018)MathSciNetCrossRef

18.

Hahn, E.M.: Model checking stochastic hybrid systems. Ph.D., thesis, Universität des Saarlandes (2013)

19.

Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146–161. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_12CrossRef

20.

Hashemi, V., Hatefi, H., Krcál, J.: Probabilistic bisimulations for PCTL model checking of interval MDPs. In: André, É., Frehse, G., (eds.) Proceedings of SynCoP 2014 EPTCS, vol. 145, pp. 19–33 (2014)

21.

Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRef

22.

Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings of LICS 1991, pp. 266–277. IEEE Computer Society (1991)

23.

Jurdziński, M., Laroussinie, F., Sproston, J.: Model checking probabilistic timed automata with one or two clocks. Log. Methods Comput. Sci. 4(3), 1–28 (2008)MathSciNetCrossRef

24.

Kozine, I.O., Utkin, L.V.: Interval-valued finite Markov chains. Reliab. Comput. 8(2), 97–113 (2002)MathSciNetCrossRef

25.

Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 286, 101–150 (2002)MathSciNetCrossRef

26.

Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking timed automata with one or two clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 387–401. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_25CrossRef

27.

Nilim, A., El Ghaoui, L.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780–798 (2005)MathSciNetCrossRef

28.

Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164–190 (2013)CrossRef

29.

Papadimitriou, C.H., Tsitsiklis, J.N.: The complexity of Markov decision processes. Math. Oper. Res. 12(3), 441–450 (1987)MathSciNetCrossRef

30.

Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527–542. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_35CrossRef

31.

Sen, K., Viswanathan, M., Agha, G.: Model-checking markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006). https://doi.org/10.1007/11691372_26CrossRefMATH

32.

Sproston, J.: Probabilistic timed automata with clock-dependent probabilities. In: Hague, M., Potapov, I. (eds.) RP 2017. LNCS, vol. 10506, pp. 144–159. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67089-8_11CrossRef

33.

Sproston, J.: Qualitative reachability for open interval Markov chains. In: Potapov, I., Reynier, P.-A. (eds.) RP 2018. LNCS, vol. 11123, pp. 146–160. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00250-3_11CrossRefMATH

34.

Sproston, J.: Probabilistic timed automata with one clock and initialised clock-dependent probabilities. CoRR (2020)

35.

Winkler, T., Junges, S., Pérez, G.A., Katoen, J.: On the complexity of reachability in parametric Markov decision processes. In: Fokkink, W., van Glabbeek, R. (eds.) Proceedings of CONCUR 2019 LIPIcs, vol. 140, pp. 14:1–14:17. Leibniz-Zentrum für Informatik (2019)

36.

Wu, D., Koutsoukos, X.D.: Reachability analysis of uncertain systems using bounded-parameter Markov decision processes. Artif. Intell. 172(8–9), 945–954 (2008)MathSciNetCrossRef

Titel: Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities
verfasst von: Jeremy Sproston
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-50085-6

Electronic ISBN: 978-3-030-50086-3

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-50086-3_9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"