Verified Certification of Reachability Checking for Timed Automata
Ontology highlight
ABSTRACT:
SUBMITTER: Biere A
PROVIDER: S-EPMC7439749 | biostudies-literature | 2020 Mar
REPOSITORIES: biostudies-literature
Similar Datasets
Project description:We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin’s
| S-EPMC7439748 | biostudies-literature
Project description:The heart rhythm of a person following heart transplantation (HTX) is assumed to display an intrinsic cardiac rhythm because it is significantly less influenced by the autonomic nervous system-the main source of heart rate variability in healthy people. Therefore, such a rhythm provides evidence for arrhythmogenic processes developing, usually silently, in the cardiac tissue. A model is proposed to simulate alterations in the cardiac tissue and to observe the effects of these changes on the resulting heart rhythm. The hybrid automata framework used makes it possible to represent reliably and simulate efficiently both the electrophysiology of a cardiac cell and the tissue organization. The curve fitting method used in the design of the hybrid automaton cycle follows the well-recognized physiological phases of the atrial myocyte membrane excitation. Moreover, knowledge of the complex architecture of the right atrium, the ability of the almost free design of intercellular connections makes the automata approach the only one possible. Two particular aspects are investigated: impairment of the impulse transmission between cells and structural changes in intercellular connections. The first aspect models the observed fatigue of cells due to specific cardiac tissue diseases. The second aspect simulates the increase in collagen deposition with aging. Finally, heart rhythms arising from the model are validated with the sinus heart rhythms recorded in HTX patients. The modulation in the impairment of the impulse transmission between cells reveals qualitatively the abnormally high heart rate variability observed in patients living long after HTX.
| S-EPMC6340163 | biostudies-literature
Project description:Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class which still captures useful behaviors. In this paper, we propose a new class of bounded underapproximations for multi-pushdown systems, which subsumes most existing classes. We develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fix-point computations. We implement it in our tool BHIM and illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway BHIM solves the binary reachability problem in pushdown automata. To show the versatility of our approach, we then extend our algorithm to the timed setting and provide the first implementation that can handle timed multi-pushdown automata with closed guards.
| S-EPMC7439744 | 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:Modelled as finite homogeneous Markov chains, probabilistic cellular automata with local transition probabilities in (0, 1) always posses a stationary distribution. This result alone is not very helpful when it comes to predicting the final configuration; one needs also a formula connecting the probabilities in the stationary distribution to some intrinsic feature of the lattice configuration. Previous results on the asynchronous cellular automata have showed that such feature really exists. It is the number of zero-one borders within the automaton's binary configuration. An exponential formula in the number of zero-one borders has been proved for the 1-D, 2-D and 3-D asynchronous automata with neighborhood three, five and seven, respectively. We perform computer experiments on a synchronous cellular automaton to check whether the empirical distribution obeys also that theoretical formula. The numerical results indicate a perfect fit for neighbourhood three and five, which opens the way for a rigorous proof of the formula in this new, synchronous case.
| S-EPMC4182702 | 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:We argue in favor of representing living cells as automata and review demonstrations that autonomous cells can form patterns by responding to local variations in the strain fields that arise from their individual or collective motions. An autonomous cell's response to strain stimuli is assumed to be effected by internally-generated, internally-powered forces, which generally move the cell in directions other than those implied by external energy gradients. Evidence of cells acting as strain-cued automata have been inferred from patterns observed in nature and from experiments conducted in vitro. Simulations that mimic particular cases of pattern forming share the idealization that cells are assumed to pass information among themselves solely via mechanical boundary conditions, i.e., the tractions and displacements present at their membranes. This assumption opens three mechanisms for pattern formation in large cell populations: wavelike behavior, kinematic feedback in cell motility that can lead to sliding and rotational patterns, and directed migration during invasions. Wavelike behavior among ameloblast cells during amelogenesis (the formation of dental enamel) has been inferred from enamel microstructure, while strain waves in populations of epithelial cells have been observed in vitro. One hypothesized kinematic feedback mechanism, "enhanced shear motility", accounts successfully for the spontaneous formation of layered patterns during amelogenesis in the mouse incisor. Directed migration is exemplified by a theory of invader cells that sense and respond to the strains they themselves create in the host population as they invade it: analysis shows that the strain fields contain positional information that could aid the formation of cell network structures, stabilizing the slender geometry of branches and helping govern the frequency of branch bifurcation and branch coalescence (the formation of closed networks). In simulations of pattern formation in homogeneous populations and network formation by invaders, morphological outcomes are governed by the ratio of the rates of two competing time dependent processes, one a migration velocity and the other a relaxation velocity related to the propagation of strain information. Relaxation velocities are approximately constant for different species and organs, whereas cell migration rates vary by three orders of magnitude. We conjecture that developmental processes use rapid cell migration to achieve certain outcomes, and slow migration to achieve others. We infer from analysis of host relaxation during network formation that a transition exists in the mechanical response of a host cell from animate to inanimate behavior when its strain changes at a rate that exceeds 10-4-10-3s-1. The transition has previously been observed in experiments conducted in vitro.
| S-EPMC6550492 | biostudies-literature
Project description:Stochastic computing has a broad range of applications, yet electronic computers realize its basic step, stochastic choice between alternative computation paths, in a cumbersome way. Biomolecular computers use a different computational paradigm and hence afford novel designs. We constructed a stochastic molecular automaton in which stochastic choice is realized by means of competition between alternative biochemical pathways, and choice probabilities are programmed by the relative molar concentrations of the software molecules coding for the alternatives. Programmable and autonomous stochastic molecular automata have been shown to perform direct analysis of disease-related molecular indicators in vitro and may have the potential to provide in situ medical diagnosis and cure.
| S-EPMC454388 | biostudies-literature