Model checking for probabilistic timed automata

Alur R, Courcoubetis C, Dill D (1991) Model-checking for probabilistic real-time systems. In: Proc of 19th international colloquium on automata, languages and programming (ICALP’91). LNCS, vol 510. Springer, Berlin, pp 115–136

Alur R, Courcoubetis C, Dill D (1993) Model checking in dense real time. Inf Comput 104(1):2–34

Alur R, Courcoubetis C, Halbwachs N, Dill D, Wong-Toi H (1992) Minimization of timed transition systems. In: Cleaveland R (ed) Proc of 3rd int conf on concurrency theory (CONCUR’92). LNCS, vol 630. Springer, Berlin, pp 340–354

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

Alur R, La Torre S, Pappas G (2004) Optimal paths in weighted timed automata. Theor Comput Sci 318(3):297–322

Alur R, Trivedi A (2011) Relating average and discounted costs for quantitative analysis of timed systems. In: Proc of 11th int conf on embedded software (EMSOFT’11). ACM, New York, pp 165–174

André E, Fribourg L, Sproston J (2012) An extension of the inverse method to probabilistic timed automata. Form Methods Syst Des. doi: 10.1007/s10703-012-0169-x

Asarin E, Maler O, Pnueli A (1998) On discretization of delays in timed automata and digital circuits. In: Sangiorgi D, de Simone R (eds) Proc of 9th int conf on concurrency theory (CONCUR’98). LNCS, vol 1466. Springer, Berlin, pp 470–484

Assouramou J, Desharnais J (2011) Analysis of non-linear probabilistic hybrid systems. In: Massink M, Norman G (eds) Proc of 9th workshop on quantitative aspects of programming languages (QAPL’11), pp 104–119

Baier C, Kwiatkowska M (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125–155

Beauquier D (2003) On probabilistic timed automata. Theor Comput Sci 292(1):65–84

Behrmann G, Cougnard A, David A, Fleury E, Larsen K, Lime D (2007) UPPAAL-Tiga: time for playing games! In: Proc of 19th international conference on computer aided verification (CAV’07). LNCS, vol 4590. Springer, Berlin, pp 121–125

Behrmann G, David A, Larsen KG, Håkansson J, Pettersson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: Proc of 3rd int conf on quantitative evaluation of systems (QEST’06). IEEE Press, New York, pp 125–126

Behrmann G, Fehnker A, Hune T, Larsen K, Pettersson P, Romijn J, Vaandrager F (2001) Minimum-cost reachability for linearly priced timed automata. In: Benedetto MD, Sangiovanni-Vincentelli A (eds) Proc of 4th int workshop on hybrid systems: computation and control (HSCC’01). LNCS, vol 2034. Springer, Berlin, pp 147–162

Bérard B, Petit A, Diekert V, Gastin P (1998) Characterization of the expressive power of silent transitions in timed automata. Fundam Inform 36(2–3):145–182

Berendsen J, Chen T, Jansen D (2009) Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen J, Cooper SB (eds) Proc of 6th conf on theory and applications of models of computation (TAMC’09). LNCS, vol 5532. Springer, Berlin, pp 128–137

Berendsen J, Jansen D, Katoen JP (2006) Probably on time and within budget: on reachability in priced probabilistic timed automata. In: Proc of 3rd int conf on quantitative evaluation of systems (QEST’06). IEEE Press, New York, pp 311–322

Berendsen J, Jansen D, Vaandrager F (2010) Fortuna: model checking priced probabilistic timed automata. In: Proc of 7th int conf on quantitative evaluation of systems (QEST’10). IEEE Press, New York, pp 273–281

Beyer D (2001) Improvements in BDD-based reachability analysis of timed automata. In: Oliveira J, Zave P (eds) Int symp of formal methods Europe, FME 2001: formal methods for increasing software productivity. LNCS, vol 2021. Springer, Berlin, pp 318–343

Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan P (ed) Proc of 15th conf on foundations of software technology and theoretical computer science (FSTTCS’95). LNCS, vol 1026. Springer, Berlin, pp 499–513

Bohnenkamp H, D’Argenio P, Hermanns H, Katoen JP (2006) Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10):812–830

Bouyer P (2003) Untameable timed automata! In: Alt H, Habib M (eds) Proc of 20th int symp on theoretical aspects of computer science (STACS’03). LNCS, vol 2607. Springer, Berlin, pp 620–631

Bouyer P (2009) From qualitative to quantitative analysis of timed systems. Mémoire d’habilitation. Université Paris 7, Paris, France

Bouyer P, Brinksma E, Larsen K (2008) Optimal infinite scheduling for multi-priced timed automata. Form Methods Syst Des 32(1):3–23

Bouyer P, Chevalier F (2005) On conciseness of extensions of timed automata. J Autom Lang Comb 10(4):393–405

Bouyer P, Dufourd C, Fleury E, Petit A (2004) Updatable timed automata. Theor Comput Sci 321(2–3):291–345

Bouyer P, Fahrenberg U, Larsen K, Markey N (2011) Quantitative analysis of real-time systems using priced timed automata. Commun ACM 54(9):78–87

Chen T, Han T, Katoen JP (2008) Time-abstracting bisimulation for probabilistic timed automata. In: Proc of 2nd IEEE int symp on theoretical aspects of software engineering (TASE’08). IEEE Press, New York, pp 177–184

Clarke E, Emerson A (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen D (ed) Proc of workshop on logic of programs. LNCS, vol 131. Springer, Berlin

Daws C, Yovine S (1995) Two examples of verification of multirate timed automata with KRONOS. In: Proc of IEEE real-time systems symposium (RTSS’95). IEEE Press, New York, pp 66–75

Eisentraut C, Hermanns H, Zhang L (2010) On probabilistic automata in continuous time. In: Proc of 25th annual IEEE symposium on logic in computer science (LICS’10). IEEE Comput. Soc., Los Alamitos, pp 342–351

Forejt V, Kwiatkowska M, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V (eds) Formal methods for eternal networked software systems (SFM’11). LNCS, vol 6659. Springer, Berlin, pp 53–113

Fruth M (2006) Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: Proc of 2nd int symp on leveraging applications of formal methods, verification and validation (ISOLA’06)

Glässer U, Rastkar S, Vajihollahi M (2008) Modeling and validation of aviation security. In: Intelligence and security informatics, vol 135. Springer, Berlin, pp 337–355

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

Hahn EM, Norman G, Parker D, Wachter B, Zhang L (2011) Game-based abstraction and controller synthesis for probabilistic hybrid systems. In: Proc of 8th int conf on quantitative evaluation of systems (QEST’11). IEEE Press, New York, pp 69–78

Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6(5):512–535

Hartmanns A, Hermanns H (2009) A modest approach to checking probabilistic timed automata. In: Proc of 6th int conf on quantitative evaluation of systems (QEST’09). IEEE Press, New York, pp 187–196

Henzinger T, Manna Z, Pnueli A (1992) What good are digital clocks? In: Kuich W (ed) Proc of 19th int colloq on automata, languages and programming (ICALP’92). LNCS, vol 623. Springer, Berlin, pp 545–558

Henzinger T, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model checking for real-time systems. Inf Comput 111(2):193–244

Hermanns H (2002) Interactive Markov chains and the quest for quantified quality. LNCS, vol 2428. Springer, Berlin

Jensen H (1996) Model checking probabilistic real time systems. In: Bjerner B, Larsson M, Nordström B (eds) Proc of 7th Nordic workshop on programming theory. Report, vol 86. Chalmers University of Technology, Chalmers, pp 247–261

Jurdziński M, Kwiatkowska M, Norman G, Trivedi A (2009) Concavely-priced probabilistic timed automata. In: Bravetti M, Zavattaro G (eds) Proc of 20th int conf on concurrency theory (CONCUR’09). LNCS, vol 5710. Springer, Berlin, pp 415–430

Jurdzinski M, Sproston J, Laroussinie F (2008) Model checking probabilistic timed automata with one or two clocks. Logical Methods in Computer Science 4(3)

Katoen JP, Hahn EM, Hermanns H, Jansen D, Zapreev I (2009) The ins and outs of the probabilistic model checker MRMC. In: Proc of 6th int conf on quantitative evaluation of systems (QEST’09). IEEE Press, New York, pp 167–176

Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2010) A game-based abstraction-refinement framework for Markov decision processes. Form Methods Syst Des 36(3):246–280

Kemeny J, Snell J, Knapp A (1976) Denumerable Markov chains, 2nd edn. Springer, Berlin

Krause C, Giese H (2011) Model checking probabilistic real-time properties for service-oriented systems with service level agreements. In: Proc of 13th int workshop on verification of infinite-state systems (INFINITY’11), EPTCS, vol 73. Elsevier, Amsterdam, pp 64–78

Kwiatkowska M, Norman G, Parker D (2006) Game-based abstraction for Markov decision processes. In: Proc of 3rd int conf on quantitative evaluation of systems (QEST’06). IEEE Press, New York, pp 157–166

Kwiatkowska M, Norman G, Parker D (2009) Stochastic games for verification of probabilistic timed automata. In: Ouaknine J, Vaandrager F (eds) Proc of 7th int conf on formal modelling and analysis of timed systems (FORMATS’09). LNCS, vol 5813. Springer, Berlin, pp 212–227

Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proc of 23rd int conf on computer aided verification (CAV’11). LNCS, vol 6806. Springer, Berlin, pp 585–591

Kwiatkowska M, Norman G, Parker D, Sproston J (2006) Performance analysis of probabilistic timed automata using digital clocks. Form Methods Syst Des 29:33–78

Kwiatkowska M, Norman G, Segala R, Sproston J (2000) Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi C (ed) Proc of 11th international conference on concurrency theory (CONCUR’00). LNCS, vol 1877. Springer, Berlin, pp 123–137

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

Kwiatkowska M, Norman G, Sproston J (2003) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Form Asp Comput 14(3):295–318

Kwiatkowska M, Norman G, Sproston J, Wang F (2007) Symbolic model checking for probabilistic timed automata. Inf Comput 205(7):1027–1077

Lanotte R, Maggiolo-Schettini A, Troina A (2005) Automatic analysis of a non-repudiation protocol. In: Proc of second workshop on quantitative aspects of programming languages (QAPL 2004). ENTCS, vol 112, pp 113–129

Larsen K, Skou A (1991) Bisimulation through probabilistic testing. Inf Comput 94:1–28

Larsen K, Yi W (1997) Time-abstracted bisimulation: implicit specifications and decidability. Inf Comput 134(2):75–101

Maler O, Larsen K, Krogh B (2010) On zone-based analysis of duration probabilistic automata. In: Proc of 12th int workshop on verification of infinite-state systems (INFINITY’10), EPTCS, vol 39, pp 33–46

Markowitch O, Roggeman Y (1999) Probabilistic non-repudiation without trusted third party. In: Proc of 2nd workshop on security in communication networks

Segala R, Lynch N (1995) Probabilistic simulations for probabilistic processes. Nord J Comput 2(2):250–273

Sproston J (2009) Strict divergence for probabilistic timed automata. In: Bravetti M, Zavattaro G (eds) Proc of 20th int conf on concurrency theory (CONCUR 2009). LNCS, vol 5710. Springer, Berlin, pp 620–636

Sproston J (2011) Discrete-time verification and control for probabilistic rectangular hybrid automata. In: Proc of 8th int conf on quantitative evaluation of systems (QEST’11). IEEE Press, New York, pp 79–88

Tripakis S (1998) The analysis of timed systems in practice. PhD thesis, Université Joseph Fourier, Grenoble

Tripakis S (1999) Verifying progress in timed systems. In: Katoen JP (ed) Proc of 5th int AMAST workshop on real-time and probabilistic systems (ARTS’99). LNCS, vol 1601. Springer, Berlin, pp 299–314

Tripakis S, Yovine S, Bouajjani A (2005) Checking timed Büchi automata emptiness efficiently. Form Methods Syst Des 26(3):267–292

UPPAAL PRO web site. http://people.cs.aau.dk/~arild/uppaal-probabilistic/

Zhang M, Hung DV (2006) Formal analysis of streaming downloading protocol for system upgrading. In: Proc of 4th workshop on quantitative aspects of programming languages (QAPL 06), ENTCS, vol 164, pp 205–224