Quantitative reactive modeling and verification

Fisher J, Henzinger T (2007) Executable cell biology. Nat Biotechnol 25:1239–1249 Morgan C, McIver A, Seidel K (1996) Probabilistic predicate transformers. ACM Trans Program Lang Syst 18:325–353 Huth M, Kwiatkowska M (1997) Quantitative analysis and model checking. Log Comput Sci 12:111–122 Henzinger T (2008) Two challenges in embedded systems design: predictability and robustness. Philos Trans R Soc A 366:3727–3736 Thomas W (1990) Automata on infinite objects. In: Handbook of theoretical computer science, vol B, pp 133–192 Emerson EA (1990) Temporal and modal logic. In: Handbook of theoretical computer science, vol B, pp 995–1072 Milner R (1990) Operational and algebraic semantics of concurrent processes. In: Handbook of theoretical computer science, vol B, pp 1201–1242 Clarke E, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge Alur R, Henzinger T (1999) Reactive modules. Form Methods Syst Des 15:7–48 Cousot P, Cousot R (1977) Abstract interpretation. Princ Program Lang 4:238–252 Pnueli A, Rosner R (1989) On the synthesis of a reactive module. Princ Program Lang 16:179–190 Alur R, Dill D (1990) Automata for modeling real-time systems. Autom Lang Program 17:322–335 Henzinger T (1996) The theory of hybrid automata. Log Comput Sci 11:278–292 Hermanns H (2002) Interactive Markov chains. Springer, Berlin Baier C, Haverkort B, Siegle M, Katoen J-P (eds) (2004) Validation of stochastic systems. Springer, Berlin Droste M, Kuich W, Vogler H (eds) (2009) Handbook of weighted automata. Springer, Berlin Chakrabarti A, de Alfaro L, Henzinger T, Stoelinga M (2003) Resource interfaces. Embed Softw 3:117–133 Kwiatkowska M, Norman G, Sproston J, Wang F (2007) Symbolic model checking for probabilistic timed automata. Inf Comput 205:1027–1077 Larsen K (2009) Priced timed automata. Found Softw Technol Theor Comput Sci 28:417–425 Jain R (1991) The art of computer systems performance analysis. Wiley, New York Shatz S, Wang J-P, Goto M (1992) Task allocation for maximizing reliability of distributed computer systems. IEEE Trans Comput 41:1156–1168 Baier C, Haverkort B, Hermanns H, Katoen J-P (2010) Performance evaluation and model checking join forces. Commun ACM 53:76–85 Sommerville I (2001) Software engineering. Addison-Wesley, Reading van Breugel F (2001) An introduction to metric semantics. Theor Comput Sci 258:1–98 de Alfaro L, Faella M, Stoelinga M (2009) Linear and branching system metrics. IEEE Trans Softw Eng 35:258–273 Desharnais J, Gupta V, Jagadeesan R, Panangaden P (2004) Metrics for labeled Mrkov processes. Theor Comput Sci 318:323–354 van Breugel F, Worrell J (2006) Approximating and computing behavioral distances in probabilistic transition systems. Theor Comput Sci 360:373–385 de Alfaro L, Henzinger T, Majumdar R (2003) Discounting the future in systems theory. Autom Lang Program 30:1022–1037 Caspi P, Benveniste A (2002) Toward an approximation theory for computerized control. Embed Softw 2:294–304 Kuhn H (ed) (1997) Classics in game theory. Princeton University Press, Princeton Grädel E, Thomas W, Wilke T (eds) (2002) Automata, logics, and infinite games. Springer, Berlin Zwick U, Paterson M (1996) The complexity of mean-payoff games on graphs. Theor Comput Sci 158:343–359 Koller D, Friedman N (2009) Probabilistic graphical models. MIT Press, Cambridge Zadeh L (1965) Fuzzy sets. Inf Control 8:338–353 Eiben A, Smith J (2003) Introduction to evolutionary computing. Springer, Berlin Curti M, Degano P, Priami C, Baldari C (2004) Modeling biochemical pathways through enhanced π-calculus. Theor Comput Sci 325:111–140 Chaouiya C (2007) Petri net modeling of biological networks. Brief Bioinform 8:210–219 Cardelli L (2005) Abstract machines of systems biology. Trans Comput Syst Biol 3:145–168 Fisher J, Piterman N, Hubbard E, Stern M, Harel D (2005) Computational insights into C elegans vulval development. Proc Natl Acad Sci USA 102:1951–1956 Ghosh R, Tomlin C (2004) Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modeling. IEE Trans Syst Biol 1:170–183 Danos V, Feret J, Fontana W, Harmer R, Krivine J (2007) Rule-based modeling of cellular signaling. Concurr Theory 18:17–41 Ciocchetta F, Hillston J (2009) Bio-PEPA: a framework for the modeling and analysis of biological systems. Theor Comput Sci 410:3065–3084 Tzeng W-G (1992) A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J Comput 21:216–227 Blondel V, Canterini V (2003) Undecidable problems for probabilistic automata of fixed dimension. Theory Comput Syst 36:231–245 Degorre A, Doyen L, Gentilini R, Raskin J-F, Torunczyk S (2010) Energy and mean-payoff games with imperfect information. Comput Sci Log 24:260–274 Chatterjee K, Doyen L, Edelsbrunner H, Henzinger T, Rannou P (2010) Mean-payoff automaton expressions. Concurr Theory 21:269–283 Chatterjee K, Doyen L, Henzinger T (2008) Quantitative languages. Comput Sci Log 17:385–400 Chatterjee K, Doyen L, Henzinger T (2009) Expressiveness and closure properties for quantitative languages. Log Comput Sci 24:199–208 Colcombet T (2009) The theory of stabilisation monoids and regular cost functions. Autom Lang Program 36:139–150 Alur R, Raghothaman M (2013) Decision problems for additive regular functions. Autom Lang Program 40:37–48 Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM 47:312–360 Cerný P, Henzinger T, Radhakrishna A (2010) Simulation distances. Concurr Theory 21:253–268 Chatterjee K, Henzinger T, Jurdziński M (2005) Mean-payoff parity games. Log Comput Sci 20:178–187 Henzinger T, Kupferman O, Rajamani S (2002) Fair simulation. Inf Comput 173:64–81 Henzinger T, Majumdar R, Prabhu V (2005) Quantifying similarities between timed systems. Form Model Anal Timed Syst 3:226–241 Bloem R, Chatterjee K, Henzinger T, Jobstmann B (2009) Better quality in synthesis through quantitative objectives. Comput-Aided Verification 21:140–156 Chatterjee K, Henzinger T, Jobstmann B, Singh R (2010) Measuring and synthesizing systems in probabilistic environments. Comput-Aided Verification 22:380–395 Cerný P, Gopi S, Henzinger T, Radhakrishna A, Totla N (2012) Synthesis from incompatible specifications. Embed Softw 12:53–62 Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50:752–794 Larsen K, Larsson F, Pettersson P, Yi W (2003) Compact data structures and state-space reduction for model checking real-time systems. Real-Time Syst 25:255–275 Chatterjee K, de Alfaro L, Faella M, Henzinger T, Majumdar R, Stoelinga M (2006) Compositional quantitative reasoning. Quant Eval Syst 3:179–188 de Alfaro L, Henzinger T, Jhala R (2001) Compositional methods for probabilistic systems. Concurr Theory 12:351–365 Boker U, Henzinger T (2012) Approximate determinization of quantitative automata. Found Softw Technol Theor Comput Sci 31:362–373 Henzinger T, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. Princ Program Lang 29:58–70 Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2009) Abstraction refinement for probabilistic software. Verification Model Checking Abstr Interpret 10:182–197 Cerný P, Henzinger T, Radhakrishna A (2013) Quantitative abstraction refinement. Princ Program Lang 40:115–128 Wagner A (2005) Robustness and evolvability in living systems. Princeton University Press, Princeton Gupta V, Henzinger T, Jagadeesan R (1997) Robust timed automata. In: Hybrid and real-time systems. LNCS, vol 1201. Springer, Berlin, pp 331–345 De Wulf M, Doyen L, Markey N, Raskin J-F (2004) Robustness and implementability of timed automata. Form Model Anal Timed Syst 2:118–133 Majumdar R, Saha I (2009) Symbolic robustness analysis. IEEE Real-Time Syst Symp 30:355–363 Chaudhuri S, Gulwani S, Lublinerman R (2010) Continuity analysis of programs. Princ Program Lang 37:57–70 Bloem R, Greimel K, Henzinger T, Jobstmann B (2009) Synthesizing robust systems. Form Methods Comput-Aided Des 9:85–92 Larus J, Rajwar R (2006) Transactional memory. Morgan-Claypool, San Rafael Dean J, Ghemawat S (2008) MapReduce: simplified data processing on large clusters. Commun ACM 51:107–113 Burckhardt S, Alur R, Martin M (2007) CheckFence: checking consistency of concurrent data types on relaxed memory models. Program Lang Des Implement 12–21 Emmi M, Fischer J, Jhala R, Majumdar R (2007) Lock allocation. Princ Program Lang 34:291–296 Guerraoui R, Henzinger T, Singh V (2009) Software transactional memory on relaxed memory models. Comput-Aided Verification 21:321–336 Heckmann R, Langenbach M, Thesing S, Wilhelm R (2003) The influence of processor architecture on the design and the results of WCET tools. Proc IEEE 91:1038–1054 Armbrust M, Fox A, Griffith R, Joseph A, Katz R, Konwinski A, Lee G, Patterson D, Rabkin A, Stoica I, Zaharia M (2009) Above the clouds: a Berkeley view of cloud computing. White paper. http://berkeleyclouds.blogspot.com Cerný P, Chatterjee K, Henzinger T, Radhakrishna A, Singh R (2011) Quantitative synthesis for concurrent programs. Comput-Aided Verification 23:243–259 Gillespie D (1977) Exact stochastic simulation of coupled chemical reactions. J Phys Chem 81:2340–2361 Didier F, Henzinger T, Mateescu M, Wolf V (2009) Approximation of event probabilities in noisy cellular processes. Comput Methods Syst Biol 7:173–188 Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O (2008) Probabilistic model checking of complex biological pathways. Theor Comput Sci 391:239–257 Henzinger T, Mateescu M, Wolf V (2009) Sliding-window abstraction for infinite Markov chains. Comput-Aided Verification 21:337–352 Didier F, Henzinger T, Mateescu M, Wolf V (2009) Fast adaptive uniformization of the chemical master equation. High-Perform Comput Syst Biol 1