of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in escherichia coli. Bioinformatics 21 (2005), 19− 28.

8. blinov, M.l., faeder, J.r., goldstein, b. and hlavacek, W.s. bioNetgen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics 20 (2001), 3289−3291.

9. calder, M., vyshemirsky, v., gilbert, d. and orton, r. analysis of signaling pathways using the prism model checker. in Proc. 3rd International Conference on Computational Methods in Systems Biology. g. plotkin, ed. (edinburgh, scotland, 2005), 179–190.

10. calzone, l., fages, f. and soliman, s. biochaM: an environment for modeling biological systems and formalizing experimental knowledge. Bioinformatics 22, 14 (2006), 1805−1807.

11. cardelli, l. brane caluli. in Proc. Computational Methods in Systems Biology (paris, May 26, 2004) v. danos and v. schächter, eds. lNcs 3082, 257 (2004).

12. cardelli, l. abstract machines of systems biology. in Transactions on Computational Systems Biology III. c. priami et al. eds. lNcs 3737, (2005), 145−168.

13. cerny, p., henzinger, t.a. and radhakrishna, a. simulation distances. in Proc. Concurrency Theory 2010. lNcs 2011, 253−268.

14. clarke, e., grumberg, o., Jha, s., lu, y. and veith, h. counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, (2003), 752−794.

15. clarke, e., grumberg, o. and peled, d. Model Checking, Mit press, 2000.

16. cohen, i.r. and harel, d. explaining a complex living system: dynamics, multi-scaling and emergence. J. Royal Society Interface 4, (2007), 175−182.

17. cousot, p. and cousot, r. abstract interpretation. in Proc. Symp. Principles of Programming Languages 4, (1977), 238−252.

18. curti, M., degano, p., priami, c. and baldari, c. Modeling biochemical pathways through enhanced pi-calculus. Theor. Comput. Sci. 325, (2004), 111−140.

19. damm, W. and harel, d. lscs: breathing life into message sequence charts. Formal Methods in System Design 19, 1, (2001), 45− 80.

20. danos, v., feret, J., fontana, W., harmer, r. and Krivine, J. rule-based modelling of cellular signalling. Concur 2007, lNcs 4703, 17− 41.

21. didier, f., henzinger, t.a., Mateescu, M. and Wolf, v. approximation of event probabilities in noisy cellular processes. Computational Methods in Systems Biology 7, (2009) 173−188.

22. didier, f., henzinger, t.a., Mateescu, M. and Wolf, v. fast adaptive uniformization of the chemical master equation. High-Performance Computational Systems Biology 1, (2009).

23. dill, d.l., Knapp, M.a., gage, p., talcott, c., laderoute, K. and lincoln, p. the pathalyzer: a tool for analysis of signal transduction pathways. in Proc. 1st Annual Recomb Satellite Workshop on Systems Biology, 2005.

24. efroni, s., harel, d. and cohen, i.r. reactive animation: realistic modeling of complex dynamic systems.

Computer 38, (2005), 38− 47.

25. efroni, s., harel, d., and cohen, i.r. emergent dynamics of thymocyte development and lineage determination. PLoS Computational Biology 3, 1 ( 2007), 127−136.

26. elowitz, M.b., levine, a.J., siggia, e.d. and swain, p.s. stochastic gene expression in a single cell. Science

297, (2002), 1183−1186.

27. emerson, e.a. temporal and modal logic. in Handbook of Theoretical Computer Science, (1990), 995−1072.

28. faeder, J.r., hlavacek, J.s., reischl, i., blinov, M.l., Metzger, h., redondo, a., Wofsy, c. and goldstein, b. investigation of early events in fcεri-mediated signaling using a detailed mathematical model. J. Immunol. 170, (2003), 3769−3781.

29. fedoroff, N. and fontana, W. small numbers of big molecules. Science 297, (2002), 1129−1131.

30. feret, J., danos, v., Krivine, J., harmer, r. and fontana,
W. internal coarse-graining of molecular systems.
Proc. Natl. Acad. Sci. 106, 16, (2009), 6453–6458.

31. fisher, J., piterman, N., hajnal, a., and henzinger, t.a. predictive modeling of signaling crosstalk during c.

elegans vulval development. PLoS Computational Biology 3, 5, (2007) 92.

32. fisher, J. and henzinger, t.a. executable cell biology. Nat. Biotechnol. 25, 11, (2007), 1239− 49.

33. fisher, J., henzinger, t.a., Mateescu, M. and piterman, N. bounded asynchrony: a biologically-inspired notion of concurrency. in Proc. of FMSB ’08 Cambridge, UK.

springer, 2008.

34. fisher, J., piterman, N., hubbard, e. J., stern, M.J. and harel, d. computational insights into caenorhabditis elegans vulval development. in Proc. Natl. Acad. Sci. USA 102, (2005), 1951–1956.

35. ghosh, r. and tomlin, c.J. symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modeling: delta-Notch protein signaling. IEE Transactions on Systems Biology 1, 1, (2004), 170−183.

36. gillespie, d.t. exact stochastic simulation of coupled chemical reactions. J. of Physical Chemistry 81, (1977), 2340−2361.

37. gillespie, d.t. Markov processes. 1992: academic press.

38. harel, d. statecharts: a visual formalism for complex systems. Sci. Comput. Programming 8, (1987),

231−274.

39. harel, d. a grand challenge for computing: full reactive modeling of a multi-cellular animal. bulletin of the eatcs 81, (2003), 226-235. (reprinted in Current Trends in Theoretical Computer Science: The Challenge of the New Century, Algorithms and Complexity, vol i. g. paun et al. eds. World scientific, (2004), 559−568.

40. harel, d. a turing-like test for biological modelling. Nature Biotechnology 23, (2005), 495−496.

41. harel, d. and gery, e. executable object modeling with statecharts. Computer 30, 7, (July 1997). ieee press, 31− 42.

42. harel, d. and pnueli, a. on the development of reactive systems. in Logics and Models of Concurrent Systems. K.r. apt, ed. Nato asi series, vol. f- 13, springer-verlag, Ny, (1985), 477−498.

43. haugh, J. M., schneider, i.c. and lewis, J. M. on the cross-regulation of protein tyrosine phosphatases and receptor tyrosine kinases in intracellular signaling. J. Theor. Biol. 230, (2004), 119–132.

44. henzinger, t.a., Jobstmann, b. and Wolf, v. formalisms for specifying Markovian population models. in Proc. 3rd Int. Workshop on Reachability Problems. lNcs 5797, springer, 2009.

45. henzinger, t.a., Mateescu, M., Mikeev, l. and Wolf, v. hybrid numerical solution of the chemical master equation. in Proc. 8th Int. Conf. on Computational Methods in Systems Biology. lecture Notes in bioinformatics, springer, 2010.

46. henzinger, t.a., and sifakis, J. the discipline of embedded systems design. IEEE Computer 40, 10, (2007), 36− 44.

47. hlavacek, W.s., faeder, J.r., blinov, M.l., posner, r.g., hucka, M., and fontana, W. rules for modelling signal transduction systems. Science STKE 2006/344/re6.

48. Kam, N., harel, d. and cohen, i.r. Visual Languages and Formal Methods. (stressa, italy, sept. 5− 7, 2001). ieee, 2001.

49. Kam, N., Kugler, h., Marelly, r., appleby, l., fisher, J., pnueli, a., harel, d., stern, M. J. and hubbard, e. J.a. scenario-based approach to modeling development: a prototype model of C. Elegans vulval cell fate specification. Developmental Biology 323 (2008), 1− 5.

50. Kwiatkowska, M., Norman, g. and parker, d. prisM: probabilistic symbolic model checker. in Proc. TOOLS 2002. t. field et al. eds. lNcs 2324, (2002), 200−204.

51. Kwiatkowska, M., Norman, g., parker, d., tymchyshyn, o., heath, J., and gaffney, e. simulation and verification for computational modeling of signalling pathways. in Proc. Winter Simulation Conference (Monterey, ca, dec. 2–6, 2006). ieee, 2006, 1666–1674 .

52. Kugler, h., larjo, a. and harel, d. biocharts: a visual formalism for complex biological systems. J. Royal Society Interface, 2010.

53. lee, K.h., dinner, a.r., tu, c., campi, g., raychaudhuri, s., varma, r., sims, t. N., burack, W.r., Wu, h., Wang, J.,

Kanagawa, o., Markiewicz, M., allen, p.M., dustin, M.l., chakraborty, a.K. and shaw, a.s. the immunological synapse balances t cell receptor signaling and degradation. Science 302, (2003), 1218–1222.

54. li, Q.J., dinner, a.r., Qi, s., irvine, d.J., huppa, J.b., davis, M.M., and chakraborty, a.K. cd4 enhances t cell sensitivity to antigen by coordinating lck accumulation at the immunological synapse. Nat. Immunol. 5, (2004)791–799.

55. Mcadams, h.h. and arkin, a. stochastic mechanisms in gene expression. Proceedings of the National

Academy of Science 94, (1997), 814−819.

56. Mcadams, h.h. and arkin, a. it’s a noisy business! Trends in Genetics 15, 2 (1999), 65− 69.

57. Milner, r. A Calculus of Communicating Systems. springer verlag, 1980

58. Milner, r. operational and algebraic semantics of concurrent processes. Handbook of Theoretical Computer Science B, (1990), 1201−1242.

59. Milner, r. Communicating and Mobile Systems: The pi-Calculus. cambridge university press, cambridge, uK, 1999).

60. parkinson, J.s., ames, p. and studdert, c.a. collaborative signaling by bacterial chemoreceptors. Curr. Opin. Microbiol. 8, (2005), 116−121.

61. paulsson, J. summing up the noise in gene networks. Nature 427, (2004), 415−418.

62. peterson, J.l. Petri Net Theory and the Modeling of Systems. prentice hall 1981

63. pnueli, a. the temporal logic of programs. in Proc. Symp. Found. Computer Science, (1977) 46− 57.

64. pnueli, a. and rosner, r. on the synthesis of a reactive module. in Proc. Symp. Principles of Programming Languages 16, (1989), 179−190.

65. popper, K. The logic of scientific discovery. hutchinson, london, 1959.

66. priami, c. the stochastic pi-calculus. Comp. J. 38, (1995), 578–589.

67. priami, c. algorithmic systems biology. Comm. ACM 52, 5, (May 2009) 80− 88.

68. priami, c., regev, a., shapiro, e.y., and silverman, W. application of a stochastic name passing calculus to representation and simulation of molecular processes. Inf. Process. Lett. 80, (2001) 25− 31.

69. regev, a., panina, e.M., silverman, W., cardelli, l., and shapiro, e.y. bioambients: an abstraction for biological compartments. Theor. Comput. Sci. 325, (2004),

141–167.

70. regev, a., silverman, W., and shapiro, e. representation and simulation of biochemical processes using the pi-calculus process algebra. Pac. Symp. Biocomput. (2001) 459–470.

71. sadot, a., fisher, J., barak, d., admanit, y., stern, M.J., hubbard, e. J.a. and harel, d. towards verified biological models, Transactions on Computational Biology and Bioinformatics 5, (2008), 1− 12.

72. schaub, M.a., henzinger, t.a., and fisher, J. Qualitative networks: a symbolic approach to analyze biological signaling networks. BMC Systems Biology 1, (2007).

73. setty, y., cohen, i.r., dor, y., and harel, d. four-dimensional realistic modeling of pancreatic organogenesis. in Proc. Natl. Acad. Sci. 105, 51 (2008), 20374−20379.

74. shen, X., collier, J., dill, d., shapiro, l., horowitz, M. and Mcadams, h.h. architecture and inherent robustness of a bacterial cell-cycle control system. PNAS. 105, 32 (2008), 11340−11345.

75. thomas, W. automata on infinite objects. in Handbook of Theoretical Computer Science B, (1990), 133−192.

76. Wang, d., cardelli l., phillips a., piterman N. and fisher J. computational modeling of the egfr network elucidates control mechanisms regulating signal dynamics. in BMC Systems Biology 3, 118, (2009), 22.

77. Wolf, v., goel, r., Mateescu, M. and henzinger, t.a. solving the chemical master equation using sliding windows. BMC Systems Biology 4, 42, (2010).

 

Jasmin Fisher ( [e-mail]) is a researcher at Microsoft research cambridge in the programming principles and tools group, cambridge, uK.

David harel ( [e-mail]) is the William sussman professorial chair of the dept. of computer science and applied Mathematics at the Weizmann institute of science, rehovot, israel.

Thomas A. henzinger (tah@ ist.ac.at) is president of the institute of science and technology austria (ist austria) and an adjunct professor of electrical engineering and computer sciences at the university of california, berkeley.