ScholarBank@NUShttps://scholarbank.nus.edu.sgThe DSpace digital repository system captures, stores, indexes, preserves, and distributes digital research material.Wed, 05 Aug 2020 08:46:39 GMT2020-08-05T08:46:39Z50451- Quasi-static scheduling of communicating taskshttps://scholarbank.nus.edu.sg/handle/10635/42168Title: Quasi-static scheduling of communicating tasks
Authors: Darondeau, P.; Genest, B.; Thiagarajan, P.S.; Yang, S.
Abstract: Good scheduling policies for distributed embedded applications are required for meeting hard real time constraints and for optimizing the use of computational resources. We study the quasi-static scheduling problem in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. Our abstracted distributed task model consists of a network of sequential processes that communicate via point-to-point buffers. In each round, the task gets activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we prove that determining the existence of a scheduling policy that guarantees upper bounds on buffer capacities is undecidable. However, we show that the problem is decidable for the important subclass of "data-branching" systems in which control flow branchings are exclusively due to data-dependent internal choices made by the sequential components. This decidability result exploits ideas derived from the Karp and Miller coverability tree for Petri nets as well as the existential boundedness notion of languages of message sequence charts. © 2010 Elsevier Inc. All rights reserved.
Fri, 01 Jan 2010 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/421682010-01-01T00:00:00Z
- Modular discrete time approximations of distributed hybrid automatahttps://scholarbank.nus.edu.sg/handle/10635/39754Title: Modular discrete time approximations of distributed hybrid automata
Authors: Thiagarajan, P.S.; Yang, S.
Abstract: We consider a network of controllers that observe and control a plant whose dynamics is determined by a finite set of continuous variables. At any given time a variable evolves at a constant rate. However, a controller can switch the rates of a designated subset of the continuous variables. These mode changes are determined by the current values of a designated subset of the variables that the controller can observe. Each variable's rate is controlled by exactly one controller and its value is observed by at most one controller. We model this setting as a network of hybrid automata and study its discrete time behavior. We show that the set of global control state sequences displayed by the network is regular. More importantly, we show that one can succinctly represent this regular language as a family of communicating finite state automata. We allow the observation of the variables and the changes in the rates of the variables to incur delays. We also permit the digital clocks associated with the controllers to evolve at differentbut rationally relatedrates. © 2012 Elsevier B.V. All rights reserved.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/397542012-01-01T00:00:00Z
- Approximate probabilistic analysis of biopathway dynamicshttps://scholarbank.nus.edu.sg/handle/10635/39171Title: Approximate probabilistic analysis of biopathway dynamics
Authors: Liu, B.; Hagiescu, A.; Palaniappan, S.K.; Chattopadhyay, B.; Cui, Z.; Wong, W.-F.; Thiagarajan, P.S.
Abstract: Motivation: Biopathways are often modeled as systems of ordinary differential equations (ODEs). Such systems will usually have many unknown parameters and hence will be difficult to calibrate. Since the data available for calibration will have limited precision, an approximate representation of the ODEs dynamics should suffice. One must, however, be able to efficiently construct such approximations for large models and perform model calibration and subsequent analysis. Results: We present a graphical processing unit (GPU) based scheme by which a system of ODEs is approximated as a dynamic Bayesian network (DBN). We then construct a model checking procedure for DBNs based on a simple probabilistic linear time temporal logic. The GPU implementation considerably extends the reach of our previous PC-cluster-based implementation (Liu et al., 2011b). Further, the key components of our algorithm can serve as the GPU kernel for other Monte Carlo simulations-based analysis of biopathway dynamics. Similarly, our model checking framework is a generic one and can be applied in other systems biology settings. We have tested our methods on three ODE models of biopathways: the epidermal growth factor-nerve growth factor pathway, the segmentation clock network and the MLC-phosphorylation pathway models. The GPU implementation shows significant gains in performance and scalability whereas the model checking framework turns out to be convenient and efficient for specifying and verifying interesting pathways properties. © The Author 2012. Published by Oxford University Press. All rights reserved.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/391712012-01-01T00:00:00Z
- Modeling and analysis of biopathways dynamicshttps://scholarbank.nus.edu.sg/handle/10635/39657Title: Modeling and analysis of biopathways dynamics
Authors: Liu, B.; Thiagarajan, P.S.
Abstract: Cellular processes are governed and coordinated by a multitude of biopathways. A pathway can be viewed as a complex network of biochemical reactions. The dynamics of this network largely determines the functioning of the pathway. Hence the modeling and analysis of biochemical networks dynamics is an important problem and is an active area of research. Here we review quantitative models of biochemical networks based on ordinary differential equations (ODEs). We mainly focus on the parameter estimation and sensitivity analysis problems and survey the current methods for tackling them. In this context we also highlight a recently developed probabilistic approximation technique using which these two problems can be considerably simplified. © 2012 Imperial College Press.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/396572012-01-01T00:00:00Z
- GPU code generation for ODE-based applications with phased shared-data access patternshttps://scholarbank.nus.edu.sg/handle/10635/77863Title: GPU code generation for ODE-based applications with phased shared-data access patterns
Authors: Hagiescu, A.; Bing, L.; Ramanathan, R.; Palaniappan, S.K.; Cui, Z.; Chattopadhyay, B.; Thiagarajan, P.S.; Wong, W.-F.
Abstract: We present a novel code generation scheme for GPUs. Its key feature is the platform-aware generation of a heterogeneous pool of threads. This exposes more data-sharing opportunities among the concurrent threads and reduces the memory requirements that would otherwise exceed the capacity of the on-chip memory. Instead of the conventional strategy of focusing on exposing as much parallelism as possible, our scheme leverages on the phased nature of memory access patterns found in many applications that exhibit massive parallelism. We demonstrate the effectiveness of our code generation strategy on a computational systems biology application. This application consists of computing a Dynamic Bayesian Network (DBN) approximation of the dynamics of signalling pathways described as a system of Ordinary Differential Equations (ODEs). The approximation algorithm involves (i) sampling many (of the order of a few million) times from the set of initial states, (ii) generating trajectories through numerical integration, and (iii) storing the statistical properties of this set of trajectories in Conditional Probability Tables (CPTs) of a DBN via a prespecified discretization of the time and value domains. The trajectories can be computed in parallel. However, the intermediate data needed for computing them, as well as the entries for the CPTs, are too large to be stored locally. Our experiments show that the proposed code generation scheme scales well, achieving significant performance improvements on three realistic signalling pathways models. These results suggest how our scheme could be extended to deal with other applications involving systems of ODEs. © 2013 ACM.
Sun, 01 Dec 2013 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/778632013-12-01T00:00:00Z
- Approximate verification of the symbolic dynamics of markov chainshttps://scholarbank.nus.edu.sg/handle/10635/40726Title: Approximate verification of the symbolic dynamics of markov chains
Authors: Agrawal, M.; Akshay, S.; Genest, B.; Thiagarajan, P.S.
Abstract: A finite state Markov chain M is often viewed as a probabilistic transition system. An alternative view - which we follow here - is to regard M as a linear transform operating on the space of probability distributions over its set of nodes. The novel idea here is to discretize the probability value space [0,1] into a finite set of intervals. A concrete probability distribution over the nodes is then symbolically represented as a tuple D of such intervals. The i-th component of the discretized distribution D will be the interval in which the probability of node i falls. The set of discretized distributions is a finite set and each trajectory, generated by repeated applications of M to an initial distribution, will induce a unique infinite string over this finite set of letters. Hence, given a set of initial distributions, the symbolic dynamics of M will consist of an infinite language L over the finite alphabet of discretized distributions. We investigate whether L meets a specification given as a linear time temporal logic formula whose atomic propositions will assert that the current probability of a node falls in an interval. Unfortunately, even for restricted Markov chains (for instance, irreducible and aperiodic chains), we do not know at present if and when L is an (omega)-regular language. To get around this we develop the notion of an epsilon-approximation, based on the transient and long term behaviors of M. Our main results are that, one can effectively check whether (i) for each infinite word in L, at least one of its epsilon-approximations satisfies the specification; (ii) for each infinite word in L all its epsilon approximations satisfy the specification. These verification results are strong in that they apply to all finite state Markov chains. Further, the study of the symbolic dynamics of Markov chains initiated here is of independent interest and can lead to other applications. © 2012 IEEE.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/407262012-01-01T00:00:00Z
- Automatic generation of protocol converters from scenario-based specificationshttps://scholarbank.nus.edu.sg/handle/10635/40230Title: Automatic generation of protocol converters from scenario-based specifications
Authors: Roychoudhury, A.; Thiagarajan, P.S.; Tran, T.-A.; Zvereva, V.A.
Abstract: Reuse of IP blocks is an important design philosophy for embedded systems. This allows shorter design cycles under tight time-to-market constraints. However, reusing IP blocks often requires designing converters (glue logic) to enable their communication. In this paper, we study the problem of automatically generating a protocol converter which enables various embedded system components (possibly with incompatible protocols) to talk to each other. Our work takes as input, a rich description of inter-component interactions described as a collection of Message Sequence Charts. We then automatically synthesize from this input a protocol converter in SystemC. Our work is not restricted to uni-directional communication and the converter can be used to broker communication among many components. We demonstrate the feasibility of our approach by modelling some simplified bus protocols that capture key features of existing System-on-Chip bus protocols. We then generate the bus controller as the protocol converter. © 2004 IEEE.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/402302004-01-01T00:00:00Z
- OpenComet: An automated tool for comet assay image analysishttps://scholarbank.nus.edu.sg/handle/10635/77899Title: OpenComet: An automated tool for comet assay image analysis
Authors: Gyori, B.M.; Venkatachalam, G.; Thiagarajan, P.S.; Hsu, D.; Clement, M.-V.
Abstract: Reactive species such as free radicals are constantly generated in vivo and DNA is the most important target of oxidative stress. Oxidative DNA damage is used as a predictive biomarker to monitor the risk of development of many diseases. The comet assay is widely used for measuring oxidative DNA damage at a single cell level. The analysis of comet assay output images, however, poses considerable challenges. Commercial software is costly and restrictive, while free software generally requires laborious manual tagging of cells. This paper presents OpenComet, an open-source software tool providing automated analysis of comet assay images. It uses a novel and robust method for finding comets based on geometric shape attributes and segmenting the comet heads through image intensity profile analysis. Due to automation, OpenComet is more accurate, less prone to human bias, and faster than manual analysis. A live analysis functionality also allows users to analyze images captured directly from a microscope. We have validated OpenComet on both alkaline and neutral comet assay images as well as sample images from existing software packages. Our results show that OpenComet achieves high accuracy with significantly reduced analysis time. © 2014 The Authors.
Wed, 01 Jan 2014 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/778992014-01-01T00:00:00Z
- Probabilistic approximations of ODEs based bio-pathway dynamicshttps://scholarbank.nus.edu.sg/handle/10635/39380Title: Probabilistic approximations of ODEs based bio-pathway dynamics
Authors: Liu, B.; Hsu, D.; Thiagarajan, P.S.
Abstract: Bio-chemical networks are often modeled as systems of ordinary differential equations (ODEs). Such systems will not admit closed form solutions and hence numerical simulations will have to be used to perform analyses. However, the number of simulations required to carry out tasks such as parameter estimation can become very large. To get around this, we propose a discrete probabilistic approximation of the ODEs dynamics. We do so by discretizing the value and the time domain and assuming a distribution of initial states w.r.t. the discretization. Then we sample a representative set of initial states according to the assumed initial distribution and generate a corresponding set of trajectories through numerical simulations. Finally, using the structure of the signaling pathway we encode these trajectories compactly as a dynamic Bayesian network. This approximation of the signaling pathway dynamics has several advantages. First, the discretized nature of the approximation helps to bridge the gap between the accuracy of the results obtained by ODE simulation and the limited precision of experimental data used for model construction and verification. Second and more importantly, many interesting pathway properties can be analyzed efficiently through standard Bayesian inference techniques instead of resorting to a large number of ODE simulations. We have tested our method on ODE models of the EGF-NGF signaling pathway [1] and the segmentation clock pathway [2]. The results are very promising in terms of accuracy and efficiency. © 2011 Elsevier B.V. All rights reserved.
Sat, 01 Jan 2011 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/393802011-01-01T00:00:00Z
- A theory of regular MSC languageshttps://scholarbank.nus.edu.sg/handle/10635/39782Title: A theory of regular MSC languages
Authors: Henriksen, J.G.; Mukund, M.; Kumar, K.N.; Sohoni, M.; Thiagarajan, P.S.
Abstract: Message sequence charts (MSCs) are an attractive visual formalism widely used to capture system requirements during the early design stages in domains such as telecommunication software. It is fruitful to have mechanisms for specifying and reasoning about collections of MSCs so that errors can be detected even at the requirements level. We propose, accordingly, a notion of regularity for collections of MSCs and explore its basic properties. In particular, we provide an automata-theoretic characterization of regular MSC languages in terms of finite-state distributed automata called bounded message-passing automata. These automata consist of a set of sequential processes that communicate with each other by sending and receiving messages over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs. A commonly used technique to generate a collection of MSCs is to use a hierarchical message sequence chart (HMSC). We show that the class of languages arising from the so-called bounded HMSCs constitute a proper subclass of the class of regular MSC languages. In fact, we characterize the bounded HMSC languages as the subclass of regular MSC languages that are finitely generated. © 2005 Elsevier Inc. All rights reserved.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/397822005-01-01T00:00:00Z
- Model-driven SoC design: The UML-SystemC bridgehttps://scholarbank.nus.edu.sg/handle/10635/78467Title: Model-driven SoC design: The UML-SystemC bridge
Authors: Nguyen, K.D.; Sun, Z.; Thiagarajan, P.S.; Wong, W.-F.
Abstract: We present a system level description mechanism based on UML notations from which one can automatically extract SystemC code. Our modelling framework is based on a restricted set of UML diagram types together with some extensions developed using stereotypes. As a result, applications as well as platform features can be captured at this level. Our system models are developed using the UML compatible tool, Rhapsody 4.2 [172]. © 2005 Springer.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/784672005-01-01T00:00:00Z
- Designing communicating transaction processes by supervisory control theoryhttps://scholarbank.nus.edu.sg/handle/10635/39127Title: Designing communicating transaction processes by supervisory control theory
Authors: Feng, L.; Wonham, W.M.; Thiagarajan, P.S.
Abstract: A Communicating Transaction Process (CTP) is a computational model that serves as a high level specification language for reactive embedded system components and their interactions. It consists of a network of communicating processes coordinating their behaviors via common actions and the common actions are refined as a set of guarded Message Sequence Charts (MSCs). There has been little work devoted to developing CTP models systematically. This paper takes the first step towards bridging this gap. In our work, communicating processes of embedded components are modeled and controlled as Discrete-Event Systems (DES). The control logic among communicating components is derived by Supervisory Control Theory (SCT), so as to guarantee that the communicating processes meet all predefined constraints and possess other desirable system behavioral properties. The control logic is then translated into propositional formulas for guarded MSCs which then results in a CTP model with guaranteed behavioral properties. © Springer Science+Business Media, LLC 2007.
Mon, 01 Jan 2007 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/391272007-01-01T00:00:00Z
- Interface design for rationally clocked GALS systemshttps://scholarbank.nus.edu.sg/handle/10635/40358Title: Interface design for rationally clocked GALS systems
Authors: Mekie, J.; Chakraborty, S.; Venkataramani, G.; Thiagarajan, P.S.; Sharma, D.K.
Abstract: We investigate the problem of designing interface circuits for rationally clocked modules in GALS systems. As a key contribution, we show that knowledge of flow-control protocols can be used to significantly optimize synchronization mechanisms. We present delayaugmented netcharts as a formalism for representing communication protocols and describe techniques to analyze them. We use the results of our analysis to design a simple yet generic interface, that is optimized for the given protocol and is free from synchronization failures. We show by means of case studies the inherent advantages of our methodology over an existing solution technique. © 2006 IEEE.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/403582006-01-01T00:00:00Z
- A UML-based design framework for time-triggered applicationshttps://scholarbank.nus.edu.sg/handle/10635/40923Title: A UML-based design framework for time-triggered applications
Authors: Nguyen, K.D.; Thiagarajan, P.S.; Wong, W.-F.
Abstract: Time-triggered architectures (TTAs) are strong candidate platforms for safety-critical real-time applications. A typical time-triggered architecture is constituted by one or more clusters. Each cluster consists of nodes communicating with one another via a time-triggered communication protocol. Designing applications to run on such a platform is a challenging task. We address this problem by constructing a UML-based design framework which exposes the essential features of the time-triggered platforms at the UML-level and allows applications to be developed at a more abstract level before full implementation. To support preliminary functional validation, we have constructed a translator by which SystemC code can be automatically generated from UML designs. Our framework enables fast prototyping of time-triggered applications and early design validation. It also supports key design principles of TTAs, such as temporal firewalls and composability. © 2007 IEEE.
Mon, 01 Jan 2007 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/409232007-01-01T00:00:00Z
- Component-based construction of bio-pathway models: The parameter estimation problemhttps://scholarbank.nus.edu.sg/handle/10635/40971Title: Component-based construction of bio-pathway models: The parameter estimation problem
Authors: Koh, G.; Hsu, D.; Thiagarajan, P.S.
Abstract: Constructing and analyzing large biological pathway models is a significant challenge. We propose a general approach that exploits the structure of a pathway to identify pathway components, constructs the component models, and finally assembles the component models into a global pathway model. Specifically, we apply this approach to pathway parameter estimation, a main step in pathway model construction. A large biological pathway often involves many unknown parameters and the resulting high-dimensional search space poses a major computational difficulty. By exploiting the structure of a pathway and the distribution of available experimental data over the pathway, we decompose a pathway into components and perform parameter estimation for each component. However, some parameters may belong to multiple components. Independent parameter estimates from different components may be in conflict for such parameters. To reconcile these conflicts, we represent each component as a factor graph, a standard probabilistic graphical model. We then combine the resulting factor graphs and use a probabilistic inference technique called belief propagation to obtain the maximally likely parameter values that are globally consistent. We validate our approach on a synthetic pathway model based on the Akt-MAPK signaling pathways. The results indicate that the approach can potentially scale up to large pathway models. © 2011 Elsevier B.V. All rights reserved.
Sat, 01 Jan 2011 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/409712011-01-01T00:00:00Z
- A decompositional approach to parameter estimation in pathway modeling: A case study of the Akt and MAPK pathways and their crosstalkhttps://scholarbank.nus.edu.sg/handle/10635/43269Title: A decompositional approach to parameter estimation in pathway modeling: A case study of the Akt and MAPK pathways and their crosstalk
Authors: Koh, G.; Teong, H.F.C.; Clément, M.-V.; Hsu, D.; Thiagarajan, P.S.
Abstract: Parameter estimation is a critical problem in modeling biological pathways. It is difficult because of the large number of parameters to be estimated and the limited experimental data available. In this paper, we propose a decompositional approach to parameter estimation. It exploits the structure of a large pathway model to break it into smaller components, whose parameters can then be estimated independently. This leads to significant improvements in computational efficiency. We present our approach in the context of Hybrid Functional Petri Net modeling and evolutionary search for parameter value estimation. However, the approach can be easily extended to other modeling frameworks and is independent of the search method used. We have tested our approach on a detailed model of the Akt and MAPK pathways with two known and one hypothesized crosstalk mechanisms. The entire model contains 84 unknown parameters. Our simulation results exhibit good correlation with experimental data, and they yield positive evidence in support of the hypothesized crosstalk between the two pathways. © 2006 Oxford University Press.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/432692006-01-01T00:00:00Z
- A computational and experimental study of the regulatory mechanisms of the complement systemhttps://scholarbank.nus.edu.sg/handle/10635/43008Title: A computational and experimental study of the regulatory mechanisms of the complement system
Authors: Liu, B.; Zhang, J.; Tan, P.Y.; Hsu, D.; Blom, A.M.; Leong, B.; Sethi, S.; Ho, B.; Ding, J.L.; Thiagarajan, P.S.
Abstract: The complement system is key to innate immunity and its activation is necessary for the clearance of bacteria and apoptotic cells. However, insufficient or excessive complement activation will lead to immune-related diseases. It is so far unknown how the complement activity is up- or down- regulated and what the associated athophysiological mechanisms are. To quantitatively understand the modulatory mechanisms of the complement system, we built a computational model involving the enhancement and suppression mechanisms that regulate complement activity. Our model consists of a large system of Ordinary Differential Equations (ODEs) accompanied by a dynamic Bayesian network as a probabilistic approximation of the ODE dynamics. Applying Bayesian inference techniques, this approximation was used to perform parameter estimation and sensitivity analysis. Our combined computational and experimental study showed that the antimicrobial response is sensitive to changes in pH and calcium levels, which etermines the strength of the crosstalk between CRP and L-ficolin. Our study also revealed differential regulatory effects of C4BP. While C4BP delays but does not decrease the classical complement activation, it attenuates but does not significantly delay the lectin pathway activation. We also found that the major inhibitory role of C4BP is to facilitate the decay of C3 convertase. In summary, the present work elucidates the regulatory mechanisms of the complement system and demonstrates how the bio-pathway achinery maintains the balance between activation and inhibition. The insights we have gained could contribute to the development of therapies targeting the complement system. © 2011 Liu et al.
Sat, 01 Jan 2011 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/430082011-01-01T00:00:00Z
- A multi-mode real-time calculushttps://scholarbank.nus.edu.sg/handle/10635/41962Title: A multi-mode real-time calculus
Authors: Phan, L.T.X.; Chakraborty, S.; Thiagarajan, P.S.
Abstract: The Real-Time Calculus (RTC) framework proposed in [Chakraborty et al., DATE 2003] and subsequently extended in [Wandeler et al., Real-Time Systems 29(2-3), 2005] and a number of other papers is geared towards the analysis of real-time systems that process various types of streaming data. The main strength of RTC is a count-based abstraction, where arrival patterns of event streams are specified as constraints on the number of events that may arrive over any specified time interval. In this framework, algebraic techniques can be used to compute system properties in a compositional way. However, the main drawback of RTC is that it cannot model state information in a natural way. For example, when a scheduling policy depends on the fill-level of a certain buffer or there is a shift from one type of data stream into another. In this paper, we extend RTC in a manner that enables state information to be easily captured while limiting the state-space explosion caused by fine grained state-based models such as timed automata. Our model, called multi-mode RTC, specifies event streams as finite automata whose states are annotated with functions that specify constraints on the arrival patterns of event streams or the service available to process them. Our new framework combines the expressiveness of state-based models with the algebraic and compositional features of the RTC formalism. In particular, system properties within a single mode can be analyzed using the RTC-based algebraic techniques and state-space exploration can be used to piece together the results obtained algebraically for the individual modes. We show how to determine typical system properties with the focus on efficient approximate techniques and illustrate the advantages of multi-mode RTC using two case studies. ©2008 IEEE.
Tue, 01 Jan 2008 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/419622008-01-01T00:00:00Z
- A hybrid factored frontier algorithm for dynamic bayesian networks with a biopathways applicationhttps://scholarbank.nus.edu.sg/handle/10635/39314Title: A hybrid factored frontier algorithm for dynamic bayesian networks with a biopathways application
Authors: Palaniappan, S.K.; Akshay, S.; Liu, B.; Genest, B.; Thiagarajan, P.S.
Abstract: Dynamic Bayesian Networks (DBNs) can serve as succinct probabilistic dynamic models of biochemical networks [CHECK END OF SENTENCE]. To analyze these models, one must compute the probability distribution over system states at a given time point. Doing this exactly is infeasible for large models; hence one must use approximate algorithms. The Factored Frontier algorithm (FF) is one such algorithm [CHECK END OF SENTENCE]. However FF as well as the earlier Boyen-Koller (BK) algorithm [CHECK END OF SENTENCE] can incur large errors. To address this, we present a new approximate algorithm called the Hybrid Factored Frontier (HFF) algorithm. At each time slice, in addition to maintaining probability distributions over local states-as FF does-HFF explicitly maintains the probabilities of a number of global states called spikes. When the number of spikes is 0, we get FF and with all global states as spikes, we get the exact inference algorithm. We show that by increasing the number of spikes one can reduce errors while the additional computational effort required is only quadratic in the number of spikes. We validated the performance of HFF on large DBN models of biopathways. Each pathway has more than 30 species and the corresponding DBN has more than 3,000 nodes. Comparisons with FF and BK show that HFF is a useful and powerful approximate inferencing algorithm for DBNs. © 2004-2012 IEEE.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/393142012-01-01T00:00:00Z
- Abstract cyclic communicating processes: A logical viewhttps://scholarbank.nus.edu.sg/handle/10635/77995Title: Abstract cyclic communicating processes: A logical view
Authors: Thiagarajan, P.S.
Abstract: Temporal logics have been very successful as tools for specifying and verifying dynamic properties of finite state distributed systems. An intriguing fact is that these logics, in order to be effective, must semantically filter out at least one of the two basic features of the behavior of distributed systems: indeterminacy and concurrency. To be precise, linear time temporal logics use as models the interleaved runs of a system in which both indeterminacy (i.e. the choices presented to the system) and concurrency (i.e. causally independent occurrences of actions) have been, in some sense, defined away. In branching time temporal logics, the (interleaved) runs glued together into a single object -usually called a computation treeserves as a model. Here, speaking again loosely, indeterminacy is present through the branching nature of the computation tree but information regarding concurrency has been filtered out. There are also families of linear time temporal logics which are interpreted over the partially ordered runs (often represented as Mazurkiewicz traces) of a system. In this setting, concurrency is in but indeterminacy is out. © Springer-Verlag Berlin Heidelberg 2002.
Tue, 01 Jan 2002 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/779952002-01-01T00:00:00Z
- Behavioural approximations for restricted linear differential hybrid automatahttps://scholarbank.nus.edu.sg/handle/10635/43256Title: Behavioural approximations for restricted linear differential hybrid automata
Authors: Agrawa, M.; Stephan, F.; Thiagarajan, P.S.; Yang, S.
Abstract: We show the regularity of the discrete time behaviour of hybrid automata in which the rates of continuous variables are governed by linear differential operators in a diagonal form and in which the values of the continuous variables can be observed only with finite precision. We do not demand resetting of the values of the continuous variables during mode changes. We can cope with polynomial guards and we can tolerate bounded delays both in sampling the values of the continuous variables and in effecting changes in their rates required by mode switchings. We also show that if the rates are governed by diagonalizable linear differential operators with rational eigenvalues and there is no delay in effecting rate changes, the discrete time behaviour of the hybrid automaton is recursive. However, the control state reachability problem in this setting is undecidable. © Springer-Verlag Berlin Heidelberg 2006.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/432562006-01-01T00:00:00Z
- The discrete time behavior of lazy linear hybrid automatahttps://scholarbank.nus.edu.sg/handle/10635/40727Title: The discrete time behavior of lazy linear hybrid automata
Authors: Agrawal, M.; Thiagarajan, P.S.
Abstract: We study the class of lazy linear hybrid automata with finite precision. The key features of this class are: - The observation of the continuous state and the rate changes associated with mode switchings take place with bounded delays. - The values of the continuous variables can be observed with only finite precision. - The guards controlling the transitions of the automaton are finite conjunctions of arbitrary linear constraints. We show that the discrete time dynamics of this class of automata can be effectively analyzed without requiring resetting of the continuous variables during mode changes. In fact, our result holds for guard languages that go well beyond linear constraints. © Springer-Verlag Berlin Heidelberg 2005.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/407272005-01-01T00:00:00Z
- Succinct discrete time approximations of distributed hybrid automatahttps://scholarbank.nus.edu.sg/handle/10635/40271Title: Succinct discrete time approximations of distributed hybrid automata
Authors: Thiagarajan, P.S.; Yang, S.
Abstract: We consider a network of hybrid automata that observe and control a plant whose state space is determined by a finite set of continuous variables. We assume that at any instant, these variables are evolving at (possibly different) constant rates. Each automaton in the network controls-i.e. can switch the rates of-a designated subset of the continuous variables without having to reset their values. These mode changes are determined by the current values of a designated subset of the variables that the automaton can observe. We require the variables controlled-in terms of effecting mode changes - by different hybrid automata to be disjoint. However, the same variable may be observed by more than one automaton. We study the discrete time behavior of such networks of hybrid automata. We show that the set of global control state sequences displayed by the network is regular. More importantly, we show that one can effectively and succinctly represent this regular language as a product of local finite state automata. © 2010 ACM.
Fri, 01 Jan 2010 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/402712010-01-01T00:00:00Z
- Probabilistic approximations of signaling pathway dynamicshttps://scholarbank.nus.edu.sg/handle/10635/40349Title: Probabilistic approximations of signaling pathway dynamics
Authors: Liu, B.; Thiagarajan, P.S.; Hsu, D.
Abstract: Systems of ordinary differential equations (ODEs) are often used to model the dynamics of complex biological pathways. We construct a discrete state model as a probabilistic approximation of the ODE dynamics by discretizing the value space and the time domain. We then sample a representative set of trajectories and exploit the discretization and the structure of the signaling pathway to encode these trajectories compactly as a dynamic Bayesian network. As a result, many interesting pathway properties can be analyzed efficiently through standard Bayesian inference techniques. We have tested our method on a model of EGF-NGF signaling pathway [1] and the results are very promising in terms of both accuracy and efficiency. © 2009 Springer Berlin Heidelberg.
Thu, 01 Jan 2009 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/403492009-01-01T00:00:00Z
- Statistical model checking based calibration and analysis of bio-pathway modelshttps://scholarbank.nus.edu.sg/handle/10635/78360Title: Statistical model checking based calibration and analysis of bio-pathway models
Authors: Palaniappan, S.K.; Gyori, B.M.; Liu, B.; Hsu, D.; Thiagarajan, P.S.
Abstract: We present a statistical model checking (SMC) based framework for studying ordinary differential equation (ODE) models of bio-pathways. We address cell-to-cell variability explicitly by using probability distributions to model initial concentrations and kinetic rate values. This implicitly defines a distribution over a set of ODE trajectories, the properties of which are to be characterized. The core component of our framework is an SMC procedure for verifying the dynamical properties of an ODE system accompanied by such prior distributions. To cope with the imprecise nature of biological data, we use a formal specification logic that allows us to encode both qualitative properties and experimental data. Using SMC, we verify such specifications in a tractable way, independent of the system size. This further enables us to develop SMC based parameter estimation and sensitivity analysis procedures. We have evaluated our method on two large pathway models, namely, the segmentation clock network and the thrombin-dependent MLC phosphorylation pathway. The results show that our method scales well and yields good parameter estimates that are robust. Our sensitivity analysis framework leads to interesting insights about the underlying dynamics of these systems. © Springer-Verlag 2013.
Tue, 01 Jan 2013 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/783602013-01-01T00:00:00Z
- Regular event structures and finite petri nets: The conflict-free casehttps://scholarbank.nus.edu.sg/handle/10635/78320Title: Regular event structures and finite petri nets: The conflict-free case
Authors: Nielsen, M.; Thiagarajan, P.S.
Abstract: We present the notion of regular event structures and conjecture that they correspond exactly to finite 1-safe Petri nets. We show that the conjecture holds for the conflict-free case. Even in this restricted setting, the proof is non-trivial and involves a natural subclass of regular event structures that admit a sensible labeling with Mazurkiewicz trace alphabets. © Springer-Verlag Berlin Heidelberg 2002.
Tue, 01 Jan 2002 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/783202002-01-01T00:00:00Z
- Simulating calcineurin-centered calcium signaling network in cardiac myocyteshttps://scholarbank.nus.edu.sg/handle/10635/78472Title: Simulating calcineurin-centered calcium signaling network in cardiac myocytes
Authors: Cui, J.; Kaandorp, J.A.; Sloot, P.M.A.; Thiagarajan, P.S.
Abstract: Calcium ion has been found to play critical roles regulating both the beating and the growth of the heart. Mathematical modeling and computational simulations are required for understanding the complex dynamics arising from the calcium signaling networks controlling the heart growth, which is critical for devising therapeutic drugs for the treatment of pathologic hypertrophy and heart failure. In this paper, we will report our newest results of simulating the relevant calcineurin-centered calcium signaling pathways under the hypertrophic stimulus of pressure overload. We will show how the dual roles of RCAN protein in cardiac hypertrophy under different hypertrophic stimuli can be explained by the complex interactions of multiple signaling pathways and indicate how this particular example can help us understand the mystery of specificity encoding in calcium signaling networks. We will also discuss how to push forward the realistic modeling of calcium signaling network in mammalian hearts and how it can benefit from the corresponding calcium signaling research in simpler organisms such as yeast. © 2010 Nova Science Publishers, Inc. All rights reserved.
Fri, 01 Jan 2010 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/784722010-01-01T00:00:00Z
- Event count automata: A state-based model for stream processing systemshttps://scholarbank.nus.edu.sg/handle/10635/78129Title: Event count automata: A state-based model for stream processing systems
Authors: Chakraborty, S.; Phan, L.T.X.; Thiagarajan, P.S.
Abstract: Recently there has been a growing interest in models and methods targeted towards the (co)design of stream processing applications; e.g. those for audio/video processing. Streams processed by such applications tend to be highly bursty and exhibit a high data-dependent variability in their processing requirements. As a result, classical event and service models such as periodic, sporadic, etc. can be overly pessimistic when dealing with such applications. In this paper, we present a new model called event count automata (ECA) for capturing the timing properties of such streams. Our model can be used to cleanly formulate properties relevant to stream processing on heterogeneous multiprocessor architectures, such as buffer overflow/underflow constraints. It can also provide the basis for developing analysis methods to compute delay/timing properties of the processed streams under different scheduling policies. Our ECAs, though similar in flavor to timed and hybrid automata, have a different semantics, are more light-weight, and are specifically suited for modeling stream processing applications and architectures. We present the basic aspects of this model and illustrate its modeling potential. We then apply it in a specific stream processing setting and develop an analysis technique based on the formalism of colored Petri nets (CPNs). Finally, we validate our modeling and analysis techniques with the help of preliminary experimental results generated using the CPN simulation tool. © 2005 IEEE.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/781292005-01-01T00:00:00Z
- Model-driven SoC design via executable UML to systemChttps://scholarbank.nus.edu.sg/handle/10635/40986Title: Model-driven SoC design via executable UML to systemC
Authors: Nguyen, K.D.; Sun, Z.; Thiagarajan, P.S.; Wong, W.-F.
Abstract: We present a system level description mechanism based on UML-notations from which one can automatically extract SystemC code. Our modelling framework is based on a restricted set of UML diagram types and some standard extensions influenced by the communication infrastructure of SystemC. The system specifications are developed using the UML-compatible tool, Rhapsody [18]. We then translate the internal representation of the design generated by Rhapsody into SystemC code. The extensions we have implemented using the stereotype feature of the Rhapsody tool pull up the communication infrastructure and timing feaures of SystemC to the UML-level. Consequently, we can describe executable platforms at the UML-level as well as translate UML-based application descriptions to SystemC level. © 2004 IEEE.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/409862004-01-01T00:00:00Z
- Incremental signaling pathway modeling by data integrationhttps://scholarbank.nus.edu.sg/handle/10635/40977Title: Incremental signaling pathway modeling by data integration
Authors: Koh, G.; Hsu, D.; Thiagarajan, P.S.
Abstract: Constructing quantitative dynamic models of signaling pathways is an important task for computational systems biology. Pathway model construction is often an inherently incremental process, with new pathway players and interactions continuously being discovered and additional experimental data being generated. Here we focus on the problem of performing model parameter estimation incrementally by integrating new experimental data into an existing model. A probabilistic graphical model known as the factor graph is used to represent pathway parameter estimates. By exploiting the network structure of a pathway, a factor graph compactly encodes many parameter estimates of varying quality as a probability distribution. When new data arrives, the parameter estimates are refined efficiently by applying a probabilistic inference algorithm known as belief propagation to the factor graph. A key advantage of our approach is that the factor graph model contains enough information about the old data, and uses only new data to refine the parameter estimates without requiring explicit access to the old data. To test this approach, we applied it to the Akt-MAPK pathways, which regulate the apoptotic process and are among the most actively studied signaling pathways. The results show that our new approach can obtain parameter estimates that fit the data well and refine them incrementally when new data arrives. © Springer-Verlag Berlin Heidelberg 2010.
Fri, 01 Jan 2010 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/409772010-01-01T00:00:00Z
- Composing globally consistent pathway parameter estimates through belief propagationhttps://scholarbank.nus.edu.sg/handle/10635/40966Title: Composing globally consistent pathway parameter estimates through belief propagation
Authors: Koh, G.; Tucker-Kellogg, L.; Hsu, D.; Thiagarajan, P.S.
Abstract: Parameter estimation of large bio-pathway models is an important and difficult problem. To reduce the prohibitive computational cost, one approach is to decompose a large model into components and estimate their parameters separately. However, the decomposed components often share common parts that may have conflicting parameter estimates, as they are computed independently within each component. In this paper, we propose to use a probabilistic inference technique called belief propagation to reconcile these independent estimates in a principled manner and compute new estimates that are globally consistent and fit well with data. An important advantage of our approach in practice is that it naturally handles incomplete or noisy data. Preliminary results based on synthetic data show promising performance in terms of both accuracy and efficiency. © Springer-Verlag Berlin Heidelberg 2007.
Mon, 01 Jan 2007 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/409662007-01-01T00:00:00Z
- A decidable class of asynchronous distributed controllershttps://scholarbank.nus.edu.sg/handle/10635/40753Title: A decidable class of asynchronous distributed controllers
Authors: Madhusudan, P.; Thiagarajan, P.S.
Abstract: We study the problem of synthesizing controllers in a natural distributed asynchronous setting: a finite set of plants interact with their local environments and communicate with each other by synchronizing on common actions. The controller-synthesis problem is to come up with a local strategy for each plant such that the controlled behaviour of the network meets a specification. We consider linear time specifications and provide, in some sense, a minimal set of restrictions under which this problem is effectively solvable: we show that the controller-synthesis problem under these restrictions is decidable while the problem becomes undecidable if any one or more of these three restrictions are dropped. © Springer-Verlag Berlin Heidelberg 2002.
Tue, 01 Jan 2002 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/407532002-01-01T00:00:00Z
- Timed vs. Time-triggered automatahttps://scholarbank.nus.edu.sg/handle/10635/39362Title: Timed vs. Time-triggered automata
Authors: Krčál, P.; Mokrushin, L.; Thiagarajan, P.S.; Yi, W.
Abstract: To establish a semantic foundation for the synthesis of executable programs from timed models, we study in what sense the timed language (i.e. sequences of events with real-valued time-stamps) of a timed automaton is recognized by a digital machine. Based on the noninstant observability of events, we propose an alternative semantics for timed automata. We show that the new semantics gives rise to a natural notion of digitalization for timed languages. As a model for digital machines we use time-triggered automata - a subclass of timed automata with simplified syntax accepting digitalized timed languages. A time-triggered automaton is essentially a time table for a digital machine (or a digital controller), describing what the machine should do at a given time point, and it can be easily transformed to an executable program. Finally, we present a method to check whether a time-triggered automaton recognizes the language of a timed automaton according to the new semantics. © Springer-Verlag 2004.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/393622004-01-01T00:00:00Z
- Dynamic bayesian networks: A factored model of probabilistic dynamicshttps://scholarbank.nus.edu.sg/handle/10635/41336Title: Dynamic bayesian networks: A factored model of probabilistic dynamics
Authors: Palaniappan, S.K.; Thiagarajan, P.S.
Abstract: The modeling and analysis of probabilistic dynamical systems is becoming a central topic in the formal methods community. Usually, Markov chains of various kinds serve as the core mathematical formalism in these studies. However, in many of these settings, the probabilistic graphical model called dynamic Bayesian networks (DBNs) [4] can be amore appropriate model to work with. This is so since a DBN is often a factored and succinct representation of an underlying Markov chain. Our goal here is to describe DBNs from this standpoint. After introducing the basic formalism, we discuss inferencing algorithms for DBNs. We then consider a simple probabilistic temporal logic and the associated model checking problem for DBNs with a finite time horizon. Finally, we describe how DBNs can be used to study the behavior of biochemical networks. © 2012 Springer-Verlag.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/413362012-01-01T00:00:00Z
- An executable specification language based on message sequence chartshttps://scholarbank.nus.edu.sg/handle/10635/39003Title: An executable specification language based on message sequence charts
Authors: Roychoudhnry, A.; Thiagarajan, P.S.
Abstract: Message Sequence Charts (MSCs) are an appealing visual formalism that play a useful role in the early design stages of reactive systems such as telecommunication protocols. They also constitute one of the behavioral diagram types in the UML framework [4]. MSCs are usually intended to capture system requirements. However there is no standard relationship between such requirements and an executable specification . Here we deploy MSCs instead as refinements of actions at the executable level by formulating a state-based model called Cyclic Transaction Processes. We provide a transition system semantics for the CTP model as also a detailed example to illustrate its modeling and behavioral features. © Springer-Verlag Berlin Heidelberg 2003.
Wed, 01 Jan 2003 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/390032003-01-01T00:00:00Z
- Communicating transaction processes: An MSC-based model of computation for reactive embedded systemshttps://scholarbank.nus.edu.sg/handle/10635/39359Title: Communicating transaction processes: An MSC-based model of computation for reactive embedded systems
Authors: Roychoudhury, A.; Thiagarajan, P.S.
Abstract: Message Sequence Charts (MSC) have been traditionally used to depict execution scenarios in the early stages of design cycle. MSCs portray inter-object interactions. Synthesizing intra-object executable specifications from an MSC-based description is a non-trivial task. Here we present a model of computation called Communicating Transaction Processes (CTP) based on MSCs from which an executable specification can be extracted in a straightforward manner. Our model describes a network of communicating processes in which the processes interact via common action labels. Each action is a non-atomic interaction described as a guarded choice of MSCs. Thus our model achieves a separation of concerns: the high-level network of processes depicting intra-process computations and control flow, while the common non-atomic communication actions capture inter-process interaction via MSCs. We show how to extract an ordinary Petri net from a CTP model thereby leading to a standard operational semantics. We also discuss the connection of our formalism to Live Sequence Charts, an extension of MSCs which also has an executable semantics. © Springer-Verlag Berlin Heidelberg 2004.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/393592004-01-01T00:00:00Z
- Causal Message Sequence Chartshttps://scholarbank.nus.edu.sg/handle/10635/39777Title: Causal Message Sequence Charts
Authors: Gazagnaire, T.; Genest, B.; Hélouët, L.; Thiagarajan, P.S.; Yang, S.
Abstract: Scenario languages based on Message Sequence Charts (MSCs) have been widely studied in the last decade. The high expressive power of MSCs renders many basic problems concerning these languages undecidable. However, several of these problems are decidable for languages that possess a behavioral property called "existentially bounded". Unfortunately, collections of scenarios outside this class are frequently exhibited by systems such as sliding window protocols. We propose here an extension of MSCs called causal Message Sequence Charts and a natural mechanism for defining languages of causal MSCs called causal HMSCs (CaHMSCs). These languages preserve decidable properties without requiring existential bounds. Further, they can model collections of scenarios generated by sliding window protocols. We establish here the basic theory of CaHMSCs as well as the expressive power and complexity of decision procedures for various subclasses of CaHMSCs. We also illustrate the modeling power of our formalism with the help of a realistic example based on the TCP sliding window feature. © 2009 Elsevier B.V. All rights reserved.
Thu, 01 Jan 2009 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/397772009-01-01T00:00:00Z
- Quasi-static scheduling of communicating taskshttps://scholarbank.nus.edu.sg/handle/10635/42163Title: Quasi-static scheduling of communicating tasks
Authors: Darondeau, P.; Genest, B.; Thiagarajan, P.S.; Yang, S.
Abstract: Good scheduling policies for distributed embedded applications are required for meeting hard real time constraints and for optimizing the use of computational resources. We study the quasi-static scheduling problem in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. Our abstracted task model consists of a network of sequential processes that communicate via point-to-point buffers. In each round, the task gets activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we prove that determining existence of quasi-static scheduling policies is undecidable. However, we show that the problem is decidable for the important sub-class of "data branching" systems in which control flow branchings are due exclusively to data-dependent internal choices made by the sequential components. This decidability result-which is non-trivial to establish-exploits ideas derived from the Karp and Miller coverability tree [8] as well as the existential boundedness notion of languages of message sequence charts [6]. © Springer-Verlag Berlin Heidelberg 2008.
Tue, 01 Jan 2008 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/421632008-01-01T00:00:00Z
- Causal message sequence chartshttps://scholarbank.nus.edu.sg/handle/10635/42167Title: Causal message sequence charts
Authors: Gazagnaire, T.; Genes, B.; Hélouët, L.; Thiagarajan, P.S.; Shaofa, Y.
Abstract: Scenario languages based on Message Sequence Charts (MSCs) and related notations have been widely studied in the last decade [14,13,2,9,6,12,8]. The high expressive power of scenarios renders many basic problems concerning these languages undecidable. The most expressive class for which several problems are known to be decidable is one which possesses a behavioral property called "existentially bounded". However, scenarios outside this class are frequently exhibited by asynchronous distributed systems such as sliding window protocols. We propose here an extension of MSCs called Causal Message Sequence Charts, which preserves decidability without requiring existential bounds. Interestingly, it can also model scenarios from sliding window protocols. We establish the expressive power and complexity of decision procedures for various subclasses of Causal Message Sequence Charts. © Springer-Verlag Berlin Heidelberg 2007.
Mon, 01 Jan 2007 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/421672007-01-01T00:00:00Z
- A hybrid factored frontier algorithm for dynamic Bayesian network models of biopathwayshttps://scholarbank.nus.edu.sg/handle/10635/39901Title: A hybrid factored frontier algorithm for dynamic Bayesian network models of biopathways
Authors: Palaniappan, S.K.; Akshay, S.; Genest, B.; Thiagarajan, P.S.
Abstract: Dynamic Bayesian Networks (DBNs) can serve as succinct models of large biochemical networks [19]. To analyze these models, one must compute the probability distribution over system states at a given time point. Doing this exactly is infeasible for large models and hence approximate methods are needed. The Factored Frontier algorithm (FF) is a simple and efficient approximate algorithm [25] that has been designed to meet this need. However the errors it incurs can be quite large. The earlier Boyen-Koller (BK) algorithm [3] can also incur significant errors. To address this, we present here a novel approximation algorithm called the Hybrid Factored Frontier (HFF) algorithm. HFF may be viewed as a parametrized version of FF. At each time slice, in addition to maintaining probability distributions over local states -as FF does- we also maintain explicitly the probabilities of a small number of global states called spikes. When the number of spikes is 0, we get FF and with all global states as spikes, we get the - computationally infeasible- exact inference algorithm. We show that by increasing the number of spikes one can reduce errors while the additional computational effort required is only quadratic in the number of spikes. We have validated the performance of our algorithm on large DBN models of biopathways. Each pathway has more than 30 species and the corresponding DBN has more than 3000 nodes. Comparisons with the performances of FF and BK show that HFF can be a useful and powerful approximation algorithm for analyzing DBN models of biopathways. © 2011 ACM.
Sat, 01 Jan 2011 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/399012011-01-01T00:00:00Z
- Lazy rectangular hybrid automatahttps://scholarbank.nus.edu.sg/handle/10635/39145Title: Lazy rectangular hybrid automata
Authors: Agrawal, M.; Thiagarajan, P.S.
Abstract: We introduce the class of lazy rectangular hybrid automata. The key feature of this class is that both the observation of the continuous state and the rate changes associated with mode switchings take place with bounded delays. We show that the discrete time dynamics of this class of automata can be effectively analyzed without requiring resetting of the continuous variables during mode changes. © Springer-Verlag 2004.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/391452004-01-01T00:00:00Z
- The MSO theory of connectedly communicating processeshttps://scholarbank.nus.edu.sg/handle/10635/41913Title: The MSO theory of connectedly communicating processes
Authors: Madhusudan, P.; Thiagarajan, P.S.; Yang, S.
Abstract: We identify a network of sequential processes that communicate by synchronizing frequently on common actions. More precisely, we demand that there is a bound k such that if the process p executes k steps without hearing from process q - directly or indirectly - then it will never hear from q again. The non-interleaved branching time behavior of a system of connectedly communicating processes (CCP) is given by its event structure unfolding. We show that the monadic second order (MSO) theory of the event structure unfolding of every CCP is decidable. Using this result, we also show that an associated distributed controller synthesis problem is decidable for linear time specifications that do not discriminate between two different linearizations of the same partially ordered execution. © Springer-Verlag Berlin Heidelberg 2005.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/419132005-01-01T00:00:00Z
- Composing functional and state-based performance models for analyzing heterogeneous real-time systemshttps://scholarbank.nus.edu.sg/handle/10635/41964Title: Composing functional and state-based performance models for analyzing heterogeneous real-time systems
Authors: Phan, L.T.X.; Chakraborty, S.; Thiagarajan, P.S.; Thiele, L.
Abstract: We present a performance analysis technique for distributed real-time systems in a setting where certain components are modeled in a purely functional manner, while the remaining components require additional modeling of state information. The functional models can be efficiently analyzed but have restricted expressiveness. On the other hand, state-based models are more expressive and offer a richer set of analyzable properties but are computationally more expensive to analyze. We show that by appropriately composing these two classes of models it is possible to leverage on their respective advantages. To this end, we propose an interface between components that are modeled using Real-Time Calculus [Chakraborty, Künzli and Thiele, DATE 2003] and those that are modeled using Event Count Automata [Chakraborty, Phan and Thiagarajan, RTSS 2005]. The resulting modeling technique is as expressive as Event Count Automata, but is amenable to more efficient analysis. We illustrate these advantages using a number of examples and a detailed case study. © 2007 IEEE.
Mon, 01 Jan 2007 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/419642007-01-01T00:00:00Z
- Netcharts: Bridging the gap between HMSCs and executable specificationshttps://scholarbank.nus.edu.sg/handle/10635/39648Title: Netcharts: Bridging the gap between HMSCs and executable specifications
Authors: Mukund, M.; Kumar, K.N.; Thiagarajan, P.S.
Abstract: We define a new notation called netcharts for describing sets of message sequence chart scenarios (MSCs). Netcharts correspond to a distributed version of High-level Message Sequence Charts (HMSCs). Netcharts improve on HMSCs in two respects. (i) Netcharts admit a natural and direct translation into communicating finite-state machines, unlike HMSCs, for which the realization problem is nontrivial. (ii) Netcharts can describe all regular MSC languages (sets of MSCs in which channel capacities have a finite upper bound), unlike HMSCs, which can only describe finitely-generated regular MSC languages. © Springer-Verlag Berlin Heidelberg 2003.
Wed, 01 Jan 2003 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/396482003-01-01T00:00:00Z
- Interacting process classeshttps://scholarbank.nus.edu.sg/handle/10635/41845Title: Interacting process classes
Authors: Goel, A.; Meng, S.; Roychoudhury, A.; Thiagarajan, P.S.
Abstract: Many reactive control systems consist of classes of interacting objects where the objects belonging to a class exhibit similar behaviors. Such interacting process classes appear in telecommunication, transportation and avionics domains. In this paper, we propose a modeling and simulation technique for interacting process classes. Our modeling style uses standard notations to capture behavior. In particular, the control flow of a process class is captured by a labeled transition system, unit interactions between process objects are described by Message Sequence Charts and the structural relations are captured via class diagrams. The key feature of our approach is that our execution semantics leads to a symbolic simulation technique. Our simulation strategy is both time and memory efficient and we demonstrate this on well-studied non-trivial examples of reactive systems. Copyright 2006 ACM.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/418452006-01-01T00:00:00Z