StarMC: an automata based CTL* model checker.
Ontology highlight
ABSTRACT:
SUBMITTER: Amparore EG
PROVIDER: S-EPMC9044404 | biostudies-literature | 2022
REPOSITORIES: biostudies-literature
Publications
starMC: an automata based CTL* model checker.
Amparore Elvio Gilberto EG Donatelli Susanna S Gallà Francesco F
PeerJ. Computer science 20220224
Model-checking of temporal logic formulae is a widely used technique for the verification of systems. CTL ∗ is a temporal logic that allows to consider an intermix of both branching behaviours (like in CTL) and linear behaviours (LTL), overcoming the limitations of LTL (that cannot express "possibility") and CTL (cannot fully express fairness). Nevertheless CTL ∗ model-checkers are uncommon. This paper presents (1) the algorithms for a <i>fully symbolic automata-based</i> approach for CTL ∗ ...[more]
Similar Datasets
Project description:Intrathymic T cell development is an important process necessary for the normal formation of cell-mediated immune responses. Importantly, such a process depends on interactions of developing thymocytes with cellular and extracellular elements of the thymic microenvironment. Additionally, it includes a series of oriented and tunely regulated migration events, ultimately allowing mature cells to cross endothelial barriers and leave the organ. Herein we built a cellular automata-based mathematical model for thymocyte migration and development. The rules comprised in this model take into account the main stages of thymocyte development, two-dimensional sections of the normal thymic microenvironmental network, as well as the chemokines involved in intrathymic cell migration. Parameters of our computer simulations with further adjusted to results derived from previous experimental data using sub-lethally irradiated mice, in which thymus recovery can be evaluated. The model fitted with the increasing numbers of each CD4/CD8-defined thymocyte subset. It was further validated since it fitted with the times of permanence experimentally ascertained in each CD4/CD8-defined differentiation stage. Importantly, correlations using the whole mean volume of young normal adult mice revealed that the numbers of cells generated in silico with the mathematical model fall within the range of total thymocyte numbers seen in these animals. Furthermore, simulations made with a human thymic epithelial network using the same mathematical model generated similar profiles for temporal evolution of thymocyte developmental stages. Lastly, we provided in silico evidence that the thymus architecture is important in the thymocyte development, since changes in the epithelial network result in different theoretical profiles for T cell development/migration. This model likely can be used to predict thymocyte evolution following therapeutic strategies designed for recovery of the thymus in diseases coursing with thymus involution, such as some primary immunodeficiencies, acute infections, and malnutrition.
| S-EPMC2784945 | biostudies-literature
Project description:With the rise of new technologies such as the Internet of Vehicles and the Internet of Things, research on the intelligent connected vehicle has become a hot topic in contemporary times. The modeling and simulation of traffic flow are mainly used to analyze the characteristics of traffic flow and study the formation and dissipation mechanism of traffic congestion to better guide the real traffic. Cellular automata are suitable for the simulation of complex giant systems. Because of the randomness and discreteness of vehicle driving, cellular automata are often used to model and analyze traffic flow. This article mainly studies the traffic flow formed by intelligent connected vehicles. Based on the traditional NaSch model, the producer-consumer algorithm is introduced to form a multi-buffer vehicle information access mode, and an improved cellular automata model with random updates is constructed. The simulation results show that the improved cellular automata model improves the traffic congestion significantly compared with the original NaSch model in the intelligent network environment, which is consistent with the actual traffic situation. Therefore, the algorithm proposed in this article can effectively simulate the traffic flow characteristics of intelligent connected vehicles, and provide a theoretical basis for solving traffic problems.
| S-EPMC9575854 | biostudies-literature
Project description:The authorship attribution is a problem of considerable practical and technical interest. Several methods have been designed to infer the authorship of disputed documents in multiple contexts. While traditional statistical methods based solely on word counts and related measurements have provided a simple, yet effective solution in particular cases; they are prone to manipulation. Recently, texts have been successfully modeled as networks, where words are represented by nodes linked according to textual similarity measurements. Such models are useful to identify informative topological patterns for the authorship recognition task. However, there is no consensus on which measurements should be used. Thus, we proposed a novel method to characterize text networks, by considering both topological and dynamical aspects of networks. Using concepts and methods from cellular automata theory, we devised a strategy to grasp informative spatio-temporal patterns from this model. Our experiments revealed an outperformance over structural analysis relying only on topological measurements, such as clustering coefficient, betweenness and shortest paths. The optimized results obtained here pave the way for a better characterization of textual networks.
| S-EPMC5863954 | biostudies-literature
Project description:BACKGROUND: In Thomas' formalism for modeling gene regulatory networks (GRNs), branching time, where a state can have more than one possible future, plays a prominent role. By representing a certain degree of unpredictability, branching time can model several important phenomena, such as (a) asynchrony, (b) incompletely specified behavior, and (c) interaction with the environment. Introducing more than one possible future for a state, however, creates a difficulty for ordinary simulators, because infinitely many paths may appear, limiting ordinary simulators to statistical conclusions. Model checkers for branching time, by contrast, are able to prove properties in the presence of infinitely many paths. RESULTS: We have developed Antelope ("Analysis of Networks through TEmporal-LOgic sPEcifications", http://turing.iimas.unam.mx:8080/AntelopeWEB/), a model checker for analyzing and constructing Boolean GRNs. Currently, software systems for Boolean GRNs use branching time almost exclusively for asynchrony. Antelope, by contrast, also uses branching time for incompletely specified behavior and environment interaction. We show the usefulness of modeling these two phenomena in the development of a Boolean GRN of the Arabidopsis thaliana root stem cell niche.There are two obstacles to a direct approach when applying model checking to Boolean GRN analysis. First, ordinary model checkers normally only verify whether or not a given set of model states has a given property. In comparison, a model checker for Boolean GRNs is preferable if it reports the set of states having a desired property. Second, for efficiency, the expressiveness of many model checkers is limited, resulting in the inability to express some interesting properties of Boolean GRNs.Antelope tries to overcome these two drawbacks: Apart from reporting the set of all states having a given property, our model checker can express, at the expense of efficiency, some properties that ordinary model checkers (e.g., NuSMV) cannot. This additional expressiveness is achieved by employing a logic extending the standard Computation-Tree Logic (CTL) with hybrid-logic operators. CONCLUSIONS: We illustrate the advantages of Antelope when (a) modeling incomplete networks and environment interaction, (b) exhibiting the set of all states having a given property, and (c) representing Boolean GRN properties with hybrid CTL.
| S-EPMC3316443 | biostudies-other
Project description:Background and objective Many countries around the world experienced a high increase in the number of COVID-19 cases after a few weeks of the first case, and along with it, excessive pressure on the healthcare systems. While medicines, drugs, and vaccines against the COVID-19 are being developed, social isolation has become the most used method for controlling the virus spreading. With the social isolation, authorities aimed to slow down the spreading, avoiding saturation of the healthcare system, and allowing that all critical COVID-19 cases could be appropriately treated. By tuning the proposed model to fit Brazil's initial COVID-19 data, the objectives of the paper are to analyze the impact of the social isolation features on the population dynamics; simulate the number of deaths due to COVID-19 and due to the lack of healthcare infrastructure; study combinations of the features for the healthcare system does not collapse; and analyze healthcare system responses for the crisis. Methods In this paper, a Susceptible-Exposed-Infected-Removed model is described in terms of probabilistic cellular automata and ordinary differential equations for the transmission of COVID-19, flexible enough for simulating different scenarios of social isolation according to the following features: the start day for the social isolation after the first death, the period for the social isolation campaign, and the percentage of the population committed to the campaign. Results Results showed that efforts in the social isolation campaign must be concentrated both on the isolation percentage and campaign duration to delay the healthcare system failure. For the hospital situation in Brazil at the beginning of the pandemic outbreak, a rate of 200 purchases per day of intensive care units and mechanical ventilators is the minimum rate to prevent the collapse of the healthcare system. Conclusions By using the model for different scenarios, it is possible to estimate the impact of social isolation campaign adhesion. For instance, if the social isolation percentage increased from 40% to 50% in Brazil, the purchase rate of 150 intensive care units and mechanical ventilators per day would be enough to prevent the healthcare system to collapse. Moreover, results showed that a premature relaxation of the social isolation campaign can lead to subsequent waves of contamination.
| S-EPMC7836885 | biostudies-literature
Project description:Symptom checkers are increasingly used to assess new symptoms and navigate the health care system. The aim of this study was to compare the accuracy of an artificial intelligence (AI)-based symptom checker (Ada) and physicians regarding the presence/absence of an inflammatory rheumatic disease (IRD). In this survey study, German-speaking physicians with prior rheumatology working experience were asked to determine IRD presence/absence and suggest diagnoses for 20 different real-world patient vignettes, which included only basic health and symptom-related medical history. IRD detection rate and suggested diagnoses of participants and Ada were compared to the gold standard, the final rheumatologists' diagnosis, reported on the discharge summary report. A total of 132 vignettes were completed by 33 physicians (mean rheumatology working experience 8.8 (SD 7.1) years). Ada's diagnostic accuracy (IRD) was significantly higher compared to physicians (70 vs 54%, p = 0.002) according to top diagnosis. Ada listed the correct diagnosis more often compared to physicians (54 vs 32%, p < 0.001) as top diagnosis as well as among the top 3 diagnoses (59 vs 42%, p < 0.001). Work experience was not related to suggesting the correct diagnosis or IRD status. Confined to basic health and symptom-related medical history, the diagnostic accuracy of physicians was lower compared to an AI-based symptom checker. These results highlight the potential of using symptom checkers early during the patient journey and importance of access to complete and sufficient patient information to establish a correct diagnosis.
| S-EPMC9548469 | biostudies-literature
Project description:Obtaining a minimal automaton is a fundamental issue in the theory and practical implementation of deterministic finite automatons (DFAs). A minimization algorithm is presented in this paper that consists of two main phases. In the first phase, the backward depth information is built, and the state set of the DFA is partitioned into many blocks. In the second phase, the state set is refined using a hash table. The minimization algorithm has a lower time complexity O(n) than a naive comparison of transitions O(n2). Few states need to be refined by the hash table, because most states have been partitioned by the backward depth information in the coarse partition. This method achieves greater generality than previous methods because building the backward depth information is independent of the topological complexity of the DFA. The proposed algorithm can be applied not only to the minimization of acyclic automata or simple cyclic automata, but also to automata with high topological complexity. Overall, the proposal has three advantages: lower time complexity, greater generality, and scalability. A comparison to Hopcroft's algorithm demonstrates experimentally that the algorithm runs faster than traditional algorithms.
| S-EPMC5091862 | biostudies-literature
Project description:Background and objectiveCOVID-19 pandemic continues unabated due to the rapid spread of new mutant strains of the virus. Decentralized cluster containment is an efficient approach to manage the pandemic in the long term, without straining the healthcare system and economy. In this study, the objective is to forecast the peak and duration of COVID-19 spread in a cluster under different conditions, using a probabilistic cellular automata configuration designed to include the observed characteristics of the pandemic with appropriate neighbourhood schemes and transition rules.MethodsThe cellular automata, initially configured to have only susceptible and exposed states, enlarges and evolves in discrete time steps to different infection states of the COVID-19 pandemic. The transition rules take into account the probability and proximity of contact between infected hosts and susceptible individuals. A transmittable and transition neighbourhoods are defined to identify the most probable individuals infected from a single host in a time step.ResultsThe model with novel neighbourhood schemes and transition rules reproduce the macroscopic behaviour of infection and recovery observed in pandemics. The temporal evolution of the pandemic trajectory is sensitive to lattice size, range, latent and recovery periods but has constraints in capturing the changes in the infectious period. A study of lockdown and migration scenarios shows strict social isolation is crucial in controlling the pandemic. The simulations also indicate that earlier vaccination with a higher capacity and rate is essential to mitigate the pandemic. A comparison of simulated and actual data shows a good match.ConclusionsThe study concludes that social isolation during movement and interaction of people can limit the spread of new infections. Vaccinating a large proportion of the population reduces new cases in subsequent waves of the pandemic. The model and algorithm with real-world data as input can quickly forecast the trajectory of the pandemic, for effective response in cluster containment.
| S-EPMC8423711 | biostudies-literature
Project description:BackgroundThe Institute of Medicine has identified patient safety as a key goal for health care in the United States. Detecting vaccine adverse events is an important public health activity that contributes to patient safety. Reports about adverse events following immunization (AEFI) from surveillance systems contain free-text components that can be analyzed using natural language processing. To extract Unified Medical Language System (UMLS) concepts from free text and classify AEFI reports based on concepts they contain, we first needed to clean the text by expanding abbreviations and shortcuts and correcting spelling errors. Our objective in this paper was to create a UMLS-based spelling error correction tool as a first step in the natural language processing (NLP) pipeline for AEFI reports.MethodsWe developed spell checking algorithms using open source tools. We used de-identified AEFI surveillance reports to create free-text data sets for analysis. After expansion of abbreviated clinical terms and shortcuts, we performed spelling correction in four steps: (1) error detection, (2) word list generation, (3) word list disambiguation and (4) error correction. We then measured the performance of the resulting spell checker by comparing it to manual correction.ResultsWe used 12,056 words to train the spell checker and tested its performance on 8,131 words. During testing, sensitivity, specificity, and positive predictive value (PPV) for the spell checker were 74% (95% CI: 74-75), 100% (95% CI: 100-100), and 47% (95% CI: 46%-48%), respectively.ConclusionWe created a prototype spell checker that can be used to process AEFI reports. We used the UMLS Specialist Lexicon as the primary source of dictionary terms and the WordNet lexicon as a secondary source. We used the UMLS as a domain-specific source of dictionary terms to compare potentially misspelled words in the corpus. The prototype sensitivity was comparable to currently available tools, but the specificity was much superior. The slow processing speed may be improved by trimming it down to the most useful component algorithms. Other investigators may find the methods we developed useful for cleaning text using lexicons specific to their area of interest.
| S-EPMC1805499 | 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