TY - CONF AB - The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets. In this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest. The behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions. AU - Guet, Calin C AU - Henzinger, Thomas A AU - Igler, Claudia AU - Petrov, Tatjana AU - Sezgin, Ali ID - 7147 SN - 0302-9743 T2 - 17th International Conference on Computational Methods in Systems Biology TI - Transient memory in gene regulation VL - 11773 ER - TY - JOUR AB - We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. AU - Daca, Przemyslaw AU - Henzinger, Thomas A AU - Kretinsky, Jan AU - Petrov, Tatjana ID - 471 IS - 2 JF - ACM Transactions on Computational Logic (TOCL) SN - 15293785 TI - Faster statistical model checking for unbounded temporal properties VL - 18 ER - TY - JOUR AB - The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights. AU - Giacobbe, Mirco AU - Guet, Calin C AU - Gupta, Ashutosh AU - Henzinger, Thomas A AU - Paixao, Tiago AU - Petrov, Tatjana ID - 1351 IS - 8 JF - Acta Informatica SN - 00015903 TI - Model checking the evolution of gene regulatory networks VL - 54 ER - TY - CONF AB - When designing genetic circuits, the typical primitives used in major existing modelling formalisms are gene interaction graphs, where edges between genes denote either an activation or inhibition relation. However, when designing experiments, it is important to be precise about the low-level mechanistic details as to how each such relation is implemented. The rule-based modelling language Kappa allows to unambiguously specify mechanistic details such as DNA binding sites, dimerisation of transcription factors, or co-operative interactions. Such a detailed description comes with complexity and computationally costly executions. We propose a general method for automatically transforming a rule-based program, by eliminating intermediate species and adjusting the rate constants accordingly. To the best of our knowledge, we show the first automated reduction of rule-based models based on equilibrium approximations. Our algorithm is an adaptation of an existing algorithm, which was designed for reducing reaction-based programs; our version of the algorithm scans the rule-based Kappa model in search for those interaction patterns known to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional checks are then performed in order to verify if the reduction is meaningful in the context of the full model. The reduced model is efficiently obtained by static inspection over the rule-set. The tool is tested on a detailed rule-based model of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has 11 rules and 5 agents, and provides a dramatic reduction in simulation time of several orders of magnitude. AU - Beica, Andreea AU - Guet, Calin C AU - Petrov, Tatjana ID - 1524 TI - Efficient reduction of kappa models by static inspection of the rule-set VL - 9271 ER - TY - CONF AB - We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. AU - Daca, Przemyslaw AU - Henzinger, Thomas A AU - Kretinsky, Jan AU - Petrov, Tatjana ID - 1093 TI - Linear distances between Markov chains VL - 59 ER - TY - CONF AB - We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. AU - Daca, Przemyslaw AU - Henzinger, Thomas A AU - Kretinsky, Jan AU - Petrov, Tatjana ID - 1234 TI - Faster statistical model checking for unbounded temporal properties VL - 9636 ER - TY - JOUR AB - In this paper, we present a method for reducing a regular, discrete-time Markov chain (DTMC) to another DTMC with a given, typically much smaller number of states. The cost of reduction is defined as the Kullback-Leibler divergence rate between a projection of the original process through a partition function and a DTMC on the correspondingly partitioned state space. Finding the reduced model with minimal cost is computationally expensive, as it requires an exhaustive search among all state space partitions, and an exact evaluation of the reduction cost for each candidate partition. Our approach deals with the latter problem by minimizing an upper bound on the reduction cost instead of minimizing the exact cost. The proposed upper bound is easy to compute and it is tight if the original chain is lumpable with respect to the partition. Then, we express the problem in the form of information bottleneck optimization, and propose using the agglomerative information bottleneck algorithm for searching a suboptimal partition greedily, rather than exhaustively. The theory is illustrated with examples and one application scenario in the context of modeling bio-molecular interactions. AU - Geiger, Bernhard AU - Petrov, Tatjana AU - Kubin, Gernot AU - Koeppl, Heinz ID - 1840 IS - 4 JF - IEEE Transactions on Automatic Control SN - 0018-9286 TI - Optimal Kullback-Leibler aggregation via information bottleneck VL - 60 ER - TY - CONF AB - The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs –an important problem of interest in evolutionary biology– more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights. AU - Giacobbe, Mirco AU - Guet, Calin C AU - Gupta, Ashutosh AU - Henzinger, Thomas A AU - Paixao, Tiago AU - Petrov, Tatjana ID - 1835 TI - Model checking gene regulatory networks VL - 9035 ER - TY - JOUR AB - We consider a continuous-time Markov chain (CTMC) whose state space is partitioned into aggregates, and each aggregate is assigned a probability measure. A sufficient condition for defining a CTMC over the aggregates is presented as a variant of weak lumpability, which also characterizes that the measure over the original process can be recovered from that of the aggregated one. We show how the applicability of de-aggregation depends on the initial distribution. The application section is devoted to illustrate how the developed theory aids in reducing CTMC models of biochemical systems particularly in connection to protein-protein interactions. We assume that the model is written by a biologist in form of site-graph-rewrite rules. Site-graph-rewrite rules compactly express that, often, only a local context of a protein (instead of a full molecular species) needs to be in a certain configuration in order to trigger a reaction event. This observation leads to suitable aggregate Markov chains with smaller state spaces, thereby providing sufficient reduction in computational complexity. This is further exemplified in two case studies: simple unbounded polymerization and early EGFR/insulin crosstalk. AU - Ganguly, Arnab AU - Petrov, Tatjana AU - Koeppl, Heinz ID - 2056 IS - 3 JF - Journal of Mathematical Biology TI - Markov chain aggregation and its applications to combinatorial reaction networks VL - 69 ER - TY - JOUR AB - Deposits of phosphorylated tau protein and convergence of pathology in the hippocampus are the hallmarks of neurodegenerative tauopathies. Thus we aimed to evaluate whether regional and cellular vulnerability patterns in the hippocampus distinguish tauopathies or are influenced by their concomitant presence. Methods: We created a heat map of phospho-tau (AT8) immunoreactivity patterns in 24 hippocampal subregions/layers in individuals with Alzheimer's disease (AD)-related neurofibrillary degeneration (n = 40), Pick's disease (n = 8), progressive supranuclear palsy (n = 7), corticobasal degeneration (n = 6), argyrophilic grain disease (AGD, n = 18), globular glial tauopathy (n = 5), and tau-astrogliopathy of the elderly (n = 10). AT8 immunoreactivity patterns were compared by mathematical analysis. Results: Our study reveals disease-specific hot spots and regional selective vulnerability for these disorders. The pattern of hippocampal AD-related tau pathology is strongly influenced by concomitant AGD. Mathematical analysis reveals that hippocampal involvement in primary tauopathies is distinguishable from early-stage AD-related neurofibrillary degeneration. Conclusion: Our data demonstrate disease-specific AT8 immunoreactivity patterns and hot spots in the hippocampus even in tauopathies, which primarily do not affect the hippocampus. These hot spots can be shifted to other regions by the co-occurrence of tauopathies like AGD. Our observations support the notion that globular glial tauopathies and tau-astrogliopathy of the elderly are distinct entities. AU - Milenković, Ivan AU - Petrov, Tatjana AU - Kovács, Gábor ID - 1913 IS - 5-6 JF - Dementia and Geriatric Cognitive Disorders SN - 1420-8008 TI - Patterns of hippocampal tau pathology differentiate neurodegenerative dementias VL - 38 ER - TY - JOUR AB - The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a mathematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the combinatorial complexity by quotienting the reachable set of molecular species into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently, we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper, we prove that this quotienting yields a sufficient condition for weak lumpability (that is to say that the quotient system is still Markovian for a given set of initial distributions) and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system (which means that the conditional probability of being in a given state in the original system knowing that we are in its equivalence class is an invariant of the system). We illustrate the framework on a case study of the epidermal growth factor (EGF)/insulin receptor crosstalk. AU - Feret, Jérôme AU - Henzinger, Thomas A AU - Koeppl, Heinz AU - Petrov, Tatjana ID - 3168 JF - Theoretical Computer Science TI - Lumpability abstractions of rule based systems VL - 431 ER - TY - CONF AB - The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a math- ematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the com- binatorial complexity by quotienting the reachable set of molecular species, into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper we prove that this quotienting yields a sufficient condition for weak lumpability and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system. We illustrate the framework on a case study of the EGF/insulin receptor crosstalk. AU - Feret, Jérôme AU - Henzinger, Thomas A AU - Koeppl, Heinz AU - Petrov, Tatjana ID - 3719 TI - Lumpability abstractions of rule-based systems VL - 40 ER - TY - CONF AB - Interface theories have been proposed to support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, maintaining compatibility. We show that these interface theories provide no formal support for component reuse, meaning that the same component cannot be used to implement several different interfaces in a design. We add a new operation to interface theories in order to support such reuse. For example, different interfaces for the same component may refer to different aspects such as functionality, timing, and power consumption. We give both stateless and stateful examples for interface theories with component reuse. To illustrate component reuse in interface-based design, we show how the stateful theory provides a natural framework for specifying and refining PCI bus clients. AU - Doyen, Laurent AU - Thomas Henzinger AU - Jobstmann, Barbara AU - Tatjana Petrov ID - 4533 TI - Interface theories with component reuse ER -