Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)
Ontology highlight
ABSTRACT:
SUBMITTER: Biere A
PROVIDER: S-EPMC7480687 | biostudies-literature | 2020 Mar
REPOSITORIES: biostudies-literature
Similar Datasets
Project description:MotivationInvestigating the relation between the structure and behavior of complex biological networks often involves posing the question if the hypothesized structure of a regulatory network is consistent with the observed behavior, or if a proposed structure can generate a desired behavior.ResultsThe above questions can be cast into a parameter search problem for qualitative models of regulatory networks. We develop a method based on symbolic model checking that avoids enumerating all possible parametrizations, and show that this method performs well on real biological problems, using the IRMA synthetic network and benchmark datasets. We test the consistency between IRMA and time-series expression profiles, and search for parameter modifications that would make the external control of the system behavior more robust.AvailabilityGNA and the IRMA model are available at http://ibis.inrialpes.fr/.
| S-EPMC2935427 | biostudies-literature
Project description:Neural networks (NN) are taking over ever more decisions thus far taken by humans, even though verifiable system-level guarantees are far out of reach. Neither is the verification technology available, nor is it even understood what a formal, meaningful, extensible, and scalable testbed might look like for such a technology. The present paper is a modest attempt to improve on both the above aspects. We present a family of formal models that contain basic features of automated decision making contexts and which can be extended with further orthogonal features, ultimately encompassing the scope of autonomous driving. Due to the possibility to model random noise in the decision actuation, each model instance induces a Markov decision process (MDP) as verification object. The NN in this context has the duty to actuate (near-optimal) decisions. From the verification perspective, the externally learnt NN serves as a determinizer of the MDP, the result being a Markov chain which as such is amenable to statistical model checking. The combination of a MDP and a NN encoding the action policy is central to what we call “deep statistical model checking” (DSMC). While being a straightforward extension of statistical model checking, it enables to gain deep insight into questions like “how high is the NN-induced safety risk?”, “how good is the NN compared to the optimal policy?” (obtained by model checking the MDP), or “does further training improve the NN?”. We report on an implementation of DSMC inside TheModestToolset in combination with externally learnt NNs, demonstrating the potential of DSMC on various instances of the model family.
| S-EPMC7281856 | biostudies-literature
Project description:Semiparametric transformation models provide a very general framework for studying the effects of (possibly time-dependent) covariates on survival time and recurrent event times. Assessing the adequacy of these models is an important task because model misspecification affects the validity of inference and the accuracy of prediction. In this paper, we introduce appropriate time-dependent residuals for these models and consider the cumulative sums of the residuals. Under the assumed model, the cumulative sum processes converge weakly to zero-mean Gaussian processes whose distributions can be approximated through Monte Carlo simulation. These results enable one to assess, both graphically and numerically, how unusual the observed residual patterns are in reference to their null distributions. The residual patterns can also be used to determine the nature of model misspecification. Extensive simulation studies demonstrate that the proposed methods perform well in practical situations. Three medical studies are provided for illustrations.
| S-EPMC3276276 | biostudies-literature
Project description:Model-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as a state-transition graph satisfies a dynamical property written as a temporal logic formula. The dynamics of ecosystems have been drawn as state-transition graphs for more than a century, ranging from state-and-transition models to assembly graphs. Model-checking can provide insights into both empirical data and theoretical models, as long as they sum up into state-transition graphs. While model-checking proved to be a valuable tool in systems biology, it remains largely underused in ecology apart from precursory applications. This article proposes to address this situation, through an inventory of existing ecological STGs and an accessible presentation of the model-checking methodology. This overview is illustrated by the application of model-checking to assess the dynamics of a vegetation pathways model. We select management scenarios by model-checking Computation Tree Logic formulas representing management goals and built from a proposed catalogue of patterns. In discussion, we sketch bridges between existing studies in ecology and available model-checking frameworks. In addition to the automated analysis of ecological state-transition graphs, we believe that defining ecological concepts with temporal logics could help clarify and compare them.
| S-EPMC9203009 | biostudies-literature
Project description:Cancer cell metabolism is often deregulated as a result of adaption to meeting energy and biosynthesis demands of rapid growth or direct mutation of key metabolic enzymes. Better understanding of such deregulation can provide new insights on targetable vulnerabilities, but is complicated by the difficulty in probing cell metabolism at different levels of resolution and under different experimental conditions. We construct computational models of glucose and glutamine metabolism with focus on the effect of IDH1/2-mutations in cancer using a combination of experimental metabolic flux data and patient-derived gene expression data. Our models demonstrate the potential of computational exploration to reveal biologic behavior: they show that an exogenously-mutated IDH1 experimental model utilizes glutamine as an alternative carbon source for lactate production under hypoxia, but does not fully-recapitulate the patient phenotype under normoxia. We also demonstrate the utility of using gene expression data as a proxy for relative differences in metabolic activity. We use the approach of probabilistic model checking and the freely-available Probabilistic Symbolic Model Checker to construct and reason about model behavior.
| S-EPMC9640632 | biostudies-literature
Project description:The unpreventable connections between real networked systems have recently called for an examination of percolation, diffusion or synchronization phenomena in multilayer networks. Here we use network science and game theory to explore interactions in networks-of-networks and model these as a game for gaining importance. We propose a viewpoint where networks choose the connection strategies, in contrast with classical approaches where nodes are the active players. Specifically, we investigate how creating paths between networks leads to different Nash equilibria that determine their structural and dynamical properties. In a wide variety of cases, selecting adequate connections leads to a cooperative solution that allows weak networks to overcome the strongest opponent. Counterintuitively, each weak network can induce a global transition to such cooperative configuration regardless of the actions of the strongest network. This power of the weak reveals a critical dominance of the underdogs in the fate of networks-of-networks.
| S-EPMC5114531 | biostudies-literature
Project description:GACAL verifies C programs by searching over the space of possible invariants, using traces of the input program to identify potential invariants. GACAL uses the ACL2s theorem prover to verify these potential invariants, using an interface provided by ACL2s for connecting with external tools. GACAL iteratively searches for and proves invariants of increasing complexity until the program is verified.
| S-EPMC7480696 | biostudies-literature
Project description:A new distribution defined on (0,1) interval is introduced. Its probability density and cumulative distribution functions have simple forms. Thanks to its simple forms, the moments, incomplete moments and quantile function of the proposed distribution are derived and obtained in explicit forms. Four parameter estimation methods are used to estimate the unknown parameter of the distribution. Besides, simulation study is implemented to compare the efficiencies of these parameter estimation methods. More importantly, owing to the proposed distribution, we provide an alternative regression model for the bounded response variable. The proposed regression model is compared with the beta and unit-Lindley regression models based on two real data sets.
| S-EPMC7822343 | biostudies-literature
Project description:BackgroundMost economic theories are based on the premise that individuals maximize their own self-interest and correctly incorporate the structure of their environment into all decisions, thanks to human intelligence. The influence of this paradigm goes far beyond academia-it underlies current macroeconomic and monetary policies, and is also an integral part of existing financial regulations. However, there is mounting empirical and experimental evidence, including the recent financial crisis, suggesting that humans do not always behave rationally, but often make seemingly random and suboptimal decisions.Methods and findingsHere we propose to reconcile these contradictory perspectives by developing a simple binary-choice model that takes evolutionary consequences of decisions into account as well as the role of intelligence, which we define as any ability of an individual to increase its genetic success. If no intelligence is present, our model produces results consistent with prior literature and shows that risks that are independent across individuals in a generation generally lead to risk-neutral behaviors, but that risks that are correlated across a generation can lead to behaviors such as risk aversion, loss aversion, probability matching, and randomization. When intelligence is present the nature of risk also matters, and we show that even when risks are independent, either risk-neutral behavior or probability matching will occur depending upon the cost of intelligence in terms of reproductive success. In the case of correlated risks, we derive an implicit formula that shows how intelligence can emerge via selection, why it may be bounded, and how such bounds typically imply the coexistence of multiple levels and types of intelligence as a reflection of varying environmental conditions.ConclusionsRational economic behavior in which individuals maximize their own self interest is only one of many possible types of behavior that arise from natural selection. The key to understanding which types of behavior are more likely to survive is how behavior affects reproductive success in a given population's environment. From this perspective, intelligence is naturally defined as behavior that increases the probability of reproductive success, and bounds on rationality are determined by physiological and environmental constraints.
| S-EPMC3504016 | biostudies-literature
Project description:This article highlights some numerical challenges when implementing the bounded integer model for composite score modeling and suggests an improved implementation. The improvement is based on an approximation of the logarithm of the error function. After presenting the derivation of the improved implementation, the article compares the performance of the algorithm to a naive implementation of the log-likelihood using both simulations and a real data example. In the simulation setting, the improved algorithm yielded more precise and less biased parameter estimates when the within-subject variability was small and estimation was performed using the Laplace algorithm. The estimation results did not differ between implementations when the SAEM algorithm was used. For the real data example, bootstrap results differed between implementations with the improved implementation producing identical or better objective function values. Based on the findings in this article, the improved implementation is suggested as the new default log-likelihood implementation for the bounded integer model.
| S-EPMC8060183 | biostudies-literature