Revisiting Underapproximate Reachability for Multipushdown Systems
Ontology highlight
ABSTRACT:
SUBMITTER: Biere A
PROVIDER: S-EPMC7439744 | biostudies-literature | 2020 Mar
REPOSITORIES: biostudies-literature
Similar Datasets
Project description:Chemical reaction networks (CRNs) and DNA strand displacement systems (DSDs) are widely-studied and useful models of molecular programming. However, in order for some DSDs in the literature to behave in an expected manner, the initial number of copies of some reagents is required to be fixed. In this paper we show that, when multiple copies of all initial molecules are present, general types of CRNs and DSDs fail to work correctly if the length of the shortest sequence of reactions needed to produce any given molecule exceeds a threshold that grows polynomially with attributes of the system.
| S-EPMC4224742 | biostudies-other
Project description:Since their appearance at the end of the 19th century, traffic lights have been the primary mode of granting access to road intersections. Today, this centuries-old technology is challenged by advances in intelligent transportation, which are opening the way to new solutions built upon slot-based systems similar to those commonly used in aerial traffic: what we call Slot-based Intersections (SIs). Despite simulation-based evidence of the potential benefits of SIs, a comprehensive, analytical framework to compare their relative performance with traffic lights is still lacking. Here, we develop such a framework. We approach the problem in a novel way, by generalizing classical queuing theory. Having defined safety conditions, we characterize capacity and delay of SIs. In the 2-road crossing configuration, we provide a capacity-optimal SI management system. For arbitrary intersection configurations, near-optimal solutions are developed. Results theoretically show that transitioning from a traffic light system to SI has the potential of doubling capacity and significantly reducing delays. This suggests a reduction of non-linear dynamics induced by intersection bottlenecks, with positive impact on the road network. Such findings can provide transportation engineers and planners with crucial insights as they prepare to manage the transition towards a more intelligent transportation infrastructure in cities.
| S-EPMC4794159 | biostudies-literature
Project description:Network properties govern the rate and extent of various spreading processes, from simple contagions to complex cascades. Recently, the analysis of spreading processes has been extended from static networks to temporal networks, where nodes and links appear and disappear. We focus on the effects of accessibility, whether there is a temporally consistent path from one node to another, and reachability, the density of the corresponding accessibility graph representation of the temporal network. The level of reachability thus inherently limits the possible extent of any spreading process on the temporal network. We study reachability in terms of the overall levels of temporal concurrency between edges and the structural cohesion of the network agglomerating over all edges. We use simulation results and develop heterogeneous mean-field model predictions for random networks to better quantify how the properties of the underlying temporal network regulate reachability.
| S-EPMC6989038 | biostudies-literature
Project description:Recent advances in spatial and temporal networks have enabled researchers to more-accurately describe many real-world systems such as urban transport networks. In this paper, we study the response of real-world spatio-temporal networks to random error and systematic attack, taking a unified view of their spatial and temporal performance. We propose a model of spatio-temporal paths in time-varying spatially embedded networks which captures the property that, as in many real-world systems, interaction between nodes is non-instantaneous and governed by the space in which they are embedded. Through numerical experiments on three real-world urban transport systems, we study the effect of node failure on a network's topological, temporal and spatial structure. We also demonstrate the broader applicability of this framework to three other classes of network. To identify weaknesses specific to the behaviour of a spatio-temporal system, we introduce centrality measures that evaluate the importance of a node as a structural bridge and its role in supporting spatio-temporally efficient flows through the network. This exposes the complex nature of fragility in a spatio-temporal system, showing that there is a variety of failure modes when a network is subject to systematic attacks.
| S-EPMC4929911 | biostudies-literature
Project description:Logical models are well-suited to capture salient dynamical properties of regulatory networks. For networks controlling cell fate decisions, cell fates are associated with model attractors (stable states or cyclic attractors) whose identification and reachability properties are particularly relevant. While synchronous updates assume unlikely instantaneous or identical rates associated with component changes, the consideration of asynchronous updates is more realistic but, for large models, may hinder the analysis of the resulting non-deterministic concurrent dynamics. This complexity hampers the study of asymptotical behaviors, and most existing approaches suffer from efficiency bottlenecks, being generally unable to handle cyclical attractors and quantify attractor reachability. Here, we propose two algorithms providing probability estimates of attractor reachability in asynchronous dynamics. The first algorithm, named Firefront, exhaustively explores the state space from an initial state, and provides quasi-exact evaluations of the reachability probabilities of model attractors. The algorithm progresses in breadth, propagating the probabilities of each encountered state to its successors. Second, Avatar is an adapted Monte Carlo approach, better suited for models with large and intertwined transient and terminal cycles. Avatar iteratively explores the state space by randomly selecting trajectories and by using these random walks to estimate the likelihood of reaching an attractor. Unlike Monte Carlo simulations, Avatar is equipped to avoid getting trapped in transient cycles and to identify cyclic attractors. Firefront and Avatar are validated and compared to related methods, using as test cases logical models of synthetic and biological networks. Both algorithms are implemented as new functionalities of GINsim 3.0, a well-established software tool for logical modeling, providing executable GUI, Java API, and scripting facilities.
| S-EPMC6137237 | biostudies-literature
Project description:Prior research has shown how to construct a mechanically verified model checker for timed automata, a popular formalism for modeling real-time systems. In this paper, we shift the focus from verified model checking to certifying unreachability. This allows us to benefit from better approximation operations for symbolic states, and reduces execution time by exploring fewer states and by exploiting parallelism. Moreover, this gives us the ability to audit results of unverified model checkers that implement a range of further optimizations, including certificate compression. The resulting tool is evaluated on a set of standard benchmarks to demonstrate its practicality, using a new unverified model checker implementation in Standard ML to construct the certificates.
| S-EPMC7439749 | biostudies-literature
Project description:Studying biological networks is of extreme importance in understanding cellular functions. These networks model interactions between molecules in each cell. A large volume of research has been done to uncover different characteristics of biological networks, such as large-scale organization, node centrality and network robustness. Nevertheless, the vast majority of research done in this area assume that biological networks have deterministic topologies. Biological interactions are however probabilistic events that may or may not appear at different cells or even in the same cell at different times.In this paper, we present novel methods for characterizing probabilistic signaling networks. Our methods do this by computing the probability that a signal propagates successfully from receptor to reporter genes through interactions in the network. We characterize such networks with respect to (i) centrality of individual nodes, (ii) stability of the entire network, and (iii) important functions served by the network. We use these methods to characterize major H. sapiens signaling networks including Wnt, ErbB and MAPK.
| S-EPMC4674881 | biostudies-literature
Project description:It is hard to assess experimentally the importance of microbial diversity in soil for the functioning of terrestrial ecosystems. An approach that is often used to make such assessment is the so-called dilution method. This method is based on the assumption that the biodiversity of the microbial community is reduced after dilution of a soil suspension and that the reduced diversity persists after incubation of more or less diluted inocula in soil. However, little is known about how the communities develop in soil after inoculation. In this study, serial dilutions of a soil suspension were made and reinoculated into the original soil previously sterilized by gamma irradiation. We determined the structure of the microbial communities in the suspensions and in the inoculated soils using 454-pyrosequencing of 16S rRNA genes. Upon dilution, several diversity indices showed that, indeed, the diversity of the bacterial communities in the suspensions decreased dramatically, with Proteobacteria as the dominant phylum of bacteria detected in all dilutions. The structure of the microbial community was changed considerably in soil, with Proteobacteria, Bacteroidetes, and Verrucomicrobia as the dominant groups in most diluted samples, indicating the importance of soil-related mechanisms operating in the assembly of the communities. We found unique operational taxonomic units (OTUs) even in the highest dilution in both the suspensions and the incubated soil samples. We conclude that the dilution approach reduces the diversity of microbial communities in soil samples but that it does not allow accurate predictions of the community assemblage during incubation of (diluted) suspensions in soil.
| S-EPMC4475865 | biostudies-literature
Project description:We present a novel approach for computing link-based similarities among objects accurately by utilizing the link information pertaining to the objects involved. We discuss the problems with previous link-based similarity measures and propose a novel approach for computing link based similarities that does not suffer from these problems. In the proposed approach each target object is represented by a vector. Each element of the vector corresponds to all the objects in the given data, and the value of each element denotes the weight for the corresponding object. As for this weight value, we propose to utilize the probability of reaching from the target object to the specific object, computed using the "Random Walk with Restart" strategy. Then, we define the similarity between two objects as the cosine similarity of the two vectors. In this paper, we provide examples to show that our approach does not suffer from the aforementioned problems. We also evaluate the performance of the proposed methods in comparison with existing link-based measures, qualitatively and quantitatively, with respect to two kinds of data sets, scientific papers and Web documents. Our experimental results indicate that the proposed methods significantly outperform the existing measures.
| S-EPMC3948467 | biostudies-other
Project description:Adaptive therapy exploits the self-organization of tumor cells to delay the outgrowth of resistant subpopulations successfully. When the tumor has aggressive resistant subpopulations, the outcome of adaptive therapy was not superior to maximum tolerated dose therapy (MTD). To explore methods to improve the adaptive therapy's performance of this case, the tumor system was constructed by osimertinib-sensitive and resistant cell lines and illustrated by the Lotka-Volterra model in this study. Restore index proposed to assess the system reachability can predict the duration of each treatment cycle. Then the threshold of the restore index was estimated to evaluate the timing of interrupting the treatment cycle and switching to high-frequency administration. The introduced reachability-based adaptive therapy and classic adaptive therapy were compared through simulation and animal experiments. The results suggested that reachability-based adaptive therapy showed advantages when the tumor has an aggressive resistant subpopulation. This study provides a feasible method for evaluating whether to continue the adaptive therapy treatment cycle or switch to high-frequency administration. This method improves the gain of adaptive therapy by taking into account the benefits of tumor intra-competition and the tumor control of killing sensitive subpopulation.
| S-EPMC8582524 | biostudies-literature