×

zbMATH — the first resource for mathematics

An extension of the inverse method to probabilistic timed automata. (English) Zbl 1291.68240
Summary: Probabilistic timed automata can be used to model systems in which probabilistic and timing behaviour coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation \(\pi_0\) of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint \(K_0\) on timing parameters for which the reachability probabilities (1) remain invariant and (2) are equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the “inverse method”. The method presents the following advantages. First, since \(K_0\) corresponds to a dense domain around \(\pi_0\) on which the system behaves uniformly, it gives us a measure of robustness of the system. Second, it allows us to obtain a valuation satisfying \(K_0\) which is as small as possible while preserving reachability probabilities, thus making the probabilistic analysis of the system easier and faster in practice. We provide examples of the application of our technique to models of randomized protocols, and introduce an extension of the method allowing the generation of a “probabilistic cartography” of a system.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68Q45 Formal languages and automata
Software:
IMITATOR; PRISM
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R; Dill, DL, A theory of timed automata, Theor Comput Sci, 126, 183-235, (1994) · Zbl 0803.68071
[2] Alur, R; Henzinger, TA; Vardi, MY, Parametric real-time reasoning, 592-601, (1993), New York · Zbl 1310.68139
[3] André É. (2010) An inverse method for the synthesis of timing parameters in concurrent systems. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France · Zbl 1108.68497
[4] André, É.; Chatain, Th; Encrenaz, E; Fribourg, L, An inverse method for parametric timed automata, Int J Found Comput Sci, 20, 819-836, (2009) · Zbl 1187.68286
[5] André, É.; Fribourg, L; Kučera, A (ed.); Potapov, I (ed.), Behavioral cartography of timed automata, No. 6227, 76-90, (2010), Berlin · Zbl 1287.68089
[6] André, É.; Fribourg, L; Kühne, U; Soulat, R, IMITATOR 2.5: A tool for analyzing robustness in scheduling problems, No. 7436, 33-36, (2012), Berlin
[7] André É., Fribourg L, Sproston J (2009) An extension of the inverse method to probabilistic timed automata. In: Roggenbach M (ed) AVoCS’09, electronic communications of the EASST, vol 23. European Association of Software Science and Technology
[8] Chamseddine, N; Duflot, M; Fribourg, L; Picaronny, C; Sproston, J, Computing expected absorption times for parametric determinate probabilistic timed automata, 254-263, (2008), Los Alamitos
[9] Daws, C, Symbolic and parametric model checking of discrete-time Markov chains, No. 3407, 280-294, (2004), Berlin · Zbl 1108.68497
[10] Gregersen H, Jensen HE (1995) Formal design of reliable real time systems. Master’s thesis, Department of Mathematics and Computer Science, Aalborg University
[11] Han, T; Katoen, JP; Mereacre, A, Approximate parameter synthesis for probabilistic time-bounded reachability, 173-182, (2008), New York
[12] Hinton, A; Kwiatkowska, M; Norman, G; Parker, D, PRISM: a tool for automatic verification of probabilistic systems, No. 3920, 441-444, (2006), Berlin
[13] Hune, T; Romijn, J; Stoelinga, M; Vaandrager, F, Linear parametric model checking of timed automata, J Log Algebr Program, 52-53, 183-220, (2002) · Zbl 1008.68069
[14] Kemeny JG, Snell JL, Knapp AW (1976) Denumerable Markov chains, 2nd edn. Graduate texts in mathematics. Springer, Berlin · Zbl 0348.60090
[15] Kwiatkowska, M; Norman, G; Parker, D, Stochastic games for verification of probabilistic timed automata, No. 5813, 212-227, (2009), Berlin · Zbl 1262.68125
[16] Kwiatkowska, M; Norman, G; Parker, D; Sproston, J, Performance analysis of probabilistic timed automata using digital clocks, Form Methods Syst Des, 29, 33-78, (2006) · Zbl 1105.68063
[17] Kwiatkowska, M; Norman, G; Segala, R; Sproston, J, Automatic verification of real-time systems with discrete probability distributions, Theor Comput Sci, 282, 101-150, (2002) · Zbl 1050.68094
[18] Kwiatkowska, M; Norman, G; Sproston, J, Probabilistic model checking of the IEEE 802.11 wireless local area network protocol, No. 2399, 169-187, (2002), Berlin · Zbl 1065.68583
[19] Kwiatkowska, M; Norman, G; Sproston, J, Probabilistic model checking of deadline properties in the IEEE 1394 firewire root contention protocol, Form Asp Comput, 14, 295-318, (2003) · Zbl 1029.68017
[20] Kwiatkowska, M; Norman, G; Sproston, J; Wang, F, Symbolic model checking for probabilistic timed automata, Inf Comput, 205, 1027-1077, (2007) · Zbl 1122.68075
[21] Lanotte, R; Maggiolo-Schettini, A; Troina, A, Parametric probabilistic transition systems for system design and analysis, Form Asp Comput, 19, 93-109, (2007) · Zbl 1111.68084
[22] Segala R (1995) Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology
[23] Prism Web page: Prism web page. http://www.prismmodelchecker.org/
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.