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: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: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: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: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
Project description:MOTIVATION: The increasing number and complexity of biomodels makes automatic procedures for checking the models' properties and quality necessary. Approaches like elementary mode analysis, flux balance analysis, deficiency analysis and chemical organization theory (OT) require only the stoichiometric structure of the reaction network for derivation of valuable information. In formalisms like Systems Biology Markup Language (SBML), however, information about the stoichiometric coefficients required for an analysis of chemical organizations can be hidden in kinetic laws. RESULTS: First, we introduce an algorithm that uncovers stoichiometric information that might be hidden in the kinetic laws of a reaction network. This allows us to apply OT to SBML models using modifiers. Second, using the new algorithm, we performed a large-scale analysis of the 185 models contained in the manually curated BioModels Database. We found that for 41 models (22%) the set of organizations changes when modifiers are considered correctly. We discuss one of these models in detail (BIOMD149, a combined model of the ERK- and Wnt-signaling pathways), whose set of organizations drastically changes when modifiers are considered. Third, we found inconsistencies in 5 models (3%) and identified their characteristics. Compared with flux-based methods, OT is able to identify those species and reactions more accurately [in 26 cases (14%)] that can be present in a long-term simulation of the model. We conclude that our approach is a valuable tool that helps to improve the consistency of biomodels and their repositories. AVAILABILITY: All data and a JAVA applet to check SBML-models is available from http://www.minet.uni-jena.de/csb/prj/ot/tools. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.
| S-EPMC2712341 | biostudies-literature
Project description:A key question of theoretical ecology is which properties of ecosystems favour their stability and help maintaining biodiversity. This question recently reconsidered mutualistic systems, generating intense controversy about the role of mutualistic interactions and their network architecture. Here we show analytically and verify with simulations that reducing the effective interspecific competition and the propagation of perturbations positively influences structural stability against environmental perturbations, enhancing persistence. Noteworthy, mutualism reduces the effective interspecific competition only when the direct interspecific competition is weaker than a critical value. This critical competition is in almost all cases larger in pollinator networks than in random networks with the same connectance. Highly connected mutualistic networks reduce the propagation of environmental perturbations, a mechanism reminiscent of MacArthur's proposal that ecosystem complexity enhances stability. Our analytic framework rationalizes previous contradictory results, and it gives valuable insight on the complex relationship between mutualism and biodiversity.
| S-EPMC5512850 | biostudies-other