Mobile platforms make use of dynamic voltage and frequency scaling (DVFS) to trade off runtime performance and power consumption for their systems-on-chip (SoCs). State-of-the-art governors in the OS use application-based characteristics to control the SoC's DVFS settings for CPU cores, as well as the GPU in some SoCs. Through experimental characterization of real-world mobile platforms, we find that key SoC components have a complex relationship with one another, which directly affects their performance and power usage. This relationship is dependent on the architecture of the SoC as it is caused by the interaction of processing elements such as the CPU and GPU through a shared main memory. Unfortunately, existing application-oriented governors do not explicitly capture this design-induced relationship.

Stochastic model checking is a technique for analyzing systems that possess probabilistic characteristics. However, its scalability is limited as probabilistic models of real-world applications typically have very large or infinite state space. This paper presents a new infinite state CTMC model checker, STAMINA, with improved scalability. It uses a novel state space approximation method to reduce large and possibly infinite state CTMC models to finite state representations that are amenable to existing stochastic model checkers. It is integrated with a new property-guided state expansion approach that improves the analysis accuracy. Demonstration of the tool on several benchmark examples shows promising results in terms of analysis efficiency and accuracy compared with a state-of-the-art CTMC model checker that deploys a similar approximation method.

MOTIVATION: Biological systems are complex and challenging to model and therefore model reuse is highly desirable. To promote model reuse, models should include both information about the specifics of simulations and the underlying biology in the form of metadata. The availability of computationally tractable metadata is especially important for the effective automated interpretation and processing of models. Metadata are typically represented as machine-readable annotations which enhance programmatic access to information about models. Rule-based languages have emerged as a modelling framework to represent the complexity of biological systems. Annotation approaches have been widely used for reaction-based formalisms such as SBML. However, rule-based languages still lack a rich annotation framework to add semantic information, such as machine-readable descriptions, to the components of a model. RESULTS: We present an annotation framework and guidelines for annotating rule-based models, encoded in the commonly used Kappa and BioNetGen languages. We adapt widely adopted annotation approaches to rule-based models. We initially propose a syntax to store machine-readable annotations and describe a mapping between rule-based modelling entities, such as agents and rules, and their annotations. We then describe an ontology to both annotate these models and capture the information contained therein, and demonstrate annotating these models using examples. Finally, we present a proof of concept tool for extracting annotations from a model that can be queried and analyzed in a uniform way. The uniform representation of the annotations can be used to facilitate the creation, analysis, reuse and visualization of rule-based models. Although examples are given, using specific implementations the proposed techniques can be applied to rule-based models in general. AVAILABILITY AND IMPLEMENTATION: The annotation ontology for rule-based models can be found at http://purl.org/rbm/rbmo The krdf tool and associated executable examples are available at http://purl.org/rbm/rbmo/krdf CONTACT: [email protected] or [email protected].

Synthetic genetic circuits have a number of exciting potential applications such as cleaning up toxic waste, hunting and killing tumor cells, and producing drugs and bio-fuels more efficiently. When designing and analyzing genetic circuits, researchers are often interested in the probability of observing certain behaviors. Discerning these probabilities typically involves simulating the circuit to produce some time series data and computing statistics over the resulting data. However, for very rare behaviors of complex genetic circuits, it becomes computationally intractable to obtain good results as the number of required simulation runs grows exponentially. It is, therefore, necessary to apply numerical methods to determine these probabilities directly. This article describes how stochastic model checking , a method for determining the likelihood that certain events occur in a system, can by applied to models of genetic circuits by translating them into continuous-time Markov chains (CTMCs) and analyzing them using Markov chain analysis to check continuous stochastic logic (CSL) properties. The utility of this approach is demonstrated with several case studies illustrating how this method can be used to perform design space exploration of two genetic oscillators and two genetic state-holding elements. Our results show that this method results in a substantial speedup as compared with conventional simulation-based approaches.

When designing and analyzing genetic circuits, researchers are often interested in the probability of the system reaching a given state within a certain amount of time. Usually, this involves simulating the system to produce some time series data and analyzing this data to discern the state probabilities. However, as the complexity of models of genetic circuits grow, it becomes more difficult for researchers to reason about the different states by looking only at time series simulation results of the models. To address this problem, this paper employs the use of stochastic model checking, a method for determining the likelihood that certain events occur in a system, with continuous stochastic logic (CSL) properties to obtain similar results. This goal is accomplished by the introduction of a methodology for converting a genetic circuit model (GCM) into a continuous-time Markov chain (CTMC). This CTMC is analyzed using transient Markov chain analysis to determine the likelihood that the circuit satisfies a given CSL property in a finite amount of time. This paper illustrates a use of this methodology to determine the likelihood of failure in a genetic toggle switch and compares these results to stochastic simulation-based analysis of this same circuit. Our results show that this method results in a substantial speedup as compared with conventional simulation-based approaches.

Researchers are now developing synthetic genetic circuits to manipulate the biochemical processes within living cells. In order to model and predict the behavior of these circuits, the designer must account for numerous reactions among many chemical species and genetic components. The analysis of genetic circuits is complicated by the fact that small molecule counts and sporadic gene expression makes stochastic simulation necessary. However, the examination of statistics on ensembles of stochastic simulation runs can hide important behavior. To address this problem, this paper introduces a new method called the incremental stochastic simulation algorithm (iSSA) which determines statistics on typical behavior. This paper illustrates the utility of this algorithm on a circadian rhythm model and a model of a synthetic dual-feedback genetic oscillator.

Electronic design automation (EDA) tools have facilitated the design of ever more complex integrated circuits each year. Synthetic biology would also benefit from the development of genetic design automation (GDA) tools. Existing GDA tools require biologists to design genetic circuits at the molecular level, roughly equivalent to designing electronic circuits at the layout level. Analysis of these circuits is also performed at this very low level. This paper presents the background and issues involved in the development of such a GDA tool for modeling, analysis, and design.

SUMMARY: iBioSim is a tool that supports learning of genetic circuit models, efficient abstraction-based analysis of these models and the design of synthetic genetic circuits. iBioSim includes project management features and a graphical user interface that facilitate the development and maintenance of genetic circuit models as well as both experimental and simulation data records. AVAILABILITY: iBioSim is available for download for Windows, Linux, and MacOS at http://www.async.ece.utah.edu/iBioSim/ CONTACT: [email protected].