abstract
- This chapter describes new analysis and verification techniques for synthetic genetic circuits. In particular, it applies stochastic model checking techniques to models of genetic circuits in order to ensure that they behave correctly and are as robust as possible for a variety of different inputs and parameter settings. In addition to stochastic model checking, this chapter proposes new variants to the incremental stochastic simulation algorithm (iSSA) that are capable of presenting a researcher with a simulation trace of the typical behavior of the system. Before the development of this algorithm, discerning this information was extremely error-prone as it involved performing many simulations and attempting to wade through the massive amounts of data. This algorithm greatly aids researchers in designing genetic circuits as it efficiently shows the researcher the most likely behavior of the circuit. Both the iSSA and stochastic model checking can be used in concert to give a researcher the likelihood that the system exhibits its most typical behavior, as well as, non-typical behaviors. This methodology is applied to several genetic circuits leading to new understanding of the effects of various parameters on the behavior of these circuits.