Learning One-Clock Timed Automata
Ontology highlight
ABSTRACT:
SUBMITTER: Biere A
PROVIDER: S-EPMC7439748 | biostudies-literature | 2020 Mar
REPOSITORIES: biostudies-literature
Similar Datasets
Project description:We study a variant of the classical membership problem in automata theory, which consists of deciding whether a given input word is accepted by a given automaton. We do so through the lenses of parameterized dynamic data structures: we assume that the automaton is fixed and its size is the parameter, while the input word is revealed as in a stream, one symbol at a time following the natural order on positions. The goal is to design a dynamic data structure that can be efficiently updated upon revealing the next symbol, while maintaining the answer to the query on whether the word consisting of symbols revealed so far is accepted by the automaton. We provide complexity bounds for this dynamic acceptance problem for timed automata that process symbols interleaved with time spans. The main contribution is a dynamic data structure that maintains acceptance of a fixed one-clock timed automaton A with amortized update time 2O(|A|) per input symbol.
| S-EPMC9596569 | 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: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:We introduce the notion of reinforcement quantum annealing (RQA) scheme in which an intelligent agent searches in the space of Hamiltonians and interacts with a quantum annealer that plays the stochastic environment role of learning automata. At each iteration of RQA, after analyzing results (samples) from the previous iteration, the agent adjusts the penalty of unsatisfied constraints and re-casts the given problem to a new Ising Hamiltonian. As a proof-of-concept, we propose a novel approach for casting the problem of Boolean satisfiability (SAT) to Ising Hamiltonians and show how to apply the RQA for increasing the probability of finding the global optimum. Our experimental results on two different benchmark SAT problems (namely factoring pseudo-prime numbers and random SAT with phase transitions), using a D-Wave 2000Q quantum processor, demonstrated that RQA finds notably better solutions with fewer samples, compared to the best-known techniques in the realm of quantum annealing.
| S-EPMC7224393 | biostudies-literature
Project description:Deep learning is one of the most advanced forms of machine learning. Most modern deep learning models are based on an artificial neural network, and benchmarking studies reveal that neural networks have produced results comparable to and in some cases superior to human experts. However, the generated neural networks are typically regarded as incomprehensible black-box models, which not only limits their applications, but also hinders testing and verifying. In this paper, we present an active learning framework to extract automata from neural network classifiers, which can help users to understand the classifiers. In more detail, we use Angluin's L* algorithm as a learner and the neural network under learning as an oracle, employing abstraction interpretation of the neural network for answering membership and equivalence queries. Our abstraction consists of value, symbol and word abstractions. The factors that may affect the abstraction are also discussed in the paper. We have implemented our approach in a prototype. To evaluate it, we have performed the prototype on a MNIST classifier and have identified that the abstraction with interval number 2 and block size 1 × 28 offers the best performance in terms of F1 score. We also have compared our extracted DFA against the DFAs learned via the passive learning algorithms provided in LearnLib and the experimental results show that our DFA gives a better performance on the MNIST dataset.
| S-EPMC8064235 | biostudies-literature
Project description:We characterize the class of nondeterministic
| S-EPMC7439745 | biostudies-literature
Project description:Timed daily access to a running-wheel (scheduled voluntary exercise; SVE) synchronizes rodent circadian rhythms and promotes stable, 24h rhythms in animals with genetically targeted impairment of neuropeptide signaling (Vipr2 -/- mice). Here we used RNA-seq and/or qRT-PCR to assess how this neuropeptide signaling impairment as well as SVE shapes molecular programs in the brain clock (suprachiasmatic nuclei; SCN) and peripheral tissues (liver and lung). Compared to Vipr2 +/+ animals, the SCN transcriptome of Vipr2 -/- mice showed extensive dysregulation which included core clock components, transcription factors, and neurochemicals. Furthermore, although SVE stabilized behavioral rhythms in these animals, the SCN transcriptome remained dysregulated. The molecular programs in the lung and liver of Vipr2 -/- mice were partially intact, although their response to SVE differed to that of these peripheral tissues in the Vipr2 +/+ mice. These findings highlight that SVE can correct behavioral abnormalities in circadian rhythms without causing large scale alterations to the SCN transcriptome.
| S-EPMC9971895 | biostudies-literature
Project description:Circadian clocks impose daily periodicities to behavior, physiology, and metabolism. This control is mediated by a central clock and by peripheral clocks, which are synchronized to provide the organism with a unified time through mechanisms that are not fully understood. Here, we characterized in Drosophila the cellular and molecular mechanisms involved in coupling the central clock and the peripheral clock located in the prothoracic gland (PG), which together control the circadian rhythm of emergence of adult flies. The time signal from central clock neurons is transmitted via small neuropeptide F (sNPF) to neurons that produce the neuropeptide Prothoracicotropic Hormone (PTTH), which is then translated into daily oscillations of Ca2+ concentration and PTTH levels. PTTH signaling is required at the end of metamorphosis and transmits time information to the PG through changes in the expression of the PTTH receptor tyrosine kinase (RTK), TORSO, and of ERK phosphorylation, a key component of PTTH transduction. In addition to PTTH, we demonstrate that signaling mediated by other RTKs contributes to the rhythmicity of emergence. Interestingly, the ligand to one of these receptors (Pvf2) plays an autocrine role in the PG, which may explain why both central brain and PG clocks are required for the circadian gating of emergence. Our findings show that the coupling between the central and the PG clock is unexpectedly complex and involves several RTKs that act in concert and could serve as a paradigm to understand how circadian clocks are coordinated.
| S-EPMC10945756 | biostudies-literature
Project description:The brain’s suprachiasmatic nucleus (SCN) is the master clock driving circadian rhythms in mammals. Vasoactive intestinal polypeptide (VIP) and its cognate receptor, VPAC2, are expressed in SCN neurons and mice with genetically targeted deletion of VPAC2 (Vipr2 -/-animals) show aberrant resetting to light, abnormal behavioral rhythms, and diminished SCN clock gene expression. Timed daily access to a running-wheel (scheduled voluntary exercise; SVE) promotes Vipr2 -/- SCN clock cell synchrony and 24h behavioral rhythms. We hypothesized that timed exercise alters the SCN transcriptome. Here, in control (Vipr2+/+) and Vipr2-/- mice under freely exercising and SVE conditions, RNAseq and qRT-PCR were used to measured gene expression of laser-dissected SCN. Compared to Vipr2+/+ mice, hundreds of genes were differentially expressed in the SCN from Vipr2-/- mice rhythmic in the freely exercising condition. Unexpectedly, SVE did not promote a Vipr2+/+-like SCN transcriptome in Vipr2-/- mice and many transcripts involved in SCN function including Avp, C1ql3, Gpr176, Prok2, Sst, Per2, and Nr1d1 remained dysregulated in the SVE condition. By contrast, circadian oscillators in the liver and lung were mostly intact in Vipr2-/- mice. This study indicates that marked molecular deficits in the SCN are sustained in behaviorally rhythmic Vipr2-/- mice, raising the possibility that a minimal functional SCN circadian clock can underpin whole animal rhythms.
2023-01-20 | GSE207992 | GEO
Project description:The sleep duration of adolescents has continued to decline over the past 20 years. Sleep insufficiency is one of the most important risk factors for obesity, but the mechanisms underlying the association are unclear. Therefore, the hypothalamic-regulated mechanisms of appetite and the circadian clock gene expression were examined in sleep-restricted rats. Rats aged 7 weeks were randomly divided into two groups: the control group and sleep restriction group (7 rats/group) rats were sleep-restricted for 4 weeks. Body weight gain and amount of food/water consumption were quantified. The expression of genes or proteins which regulated appetite and energy metabolism via leptin receptor signaling and the circadian clock in the hypothalamus were assessed. Chronic sleep restriction induced increased food intake and weight gain in adolescent and young adult rats from the second week of initiation of sleep restriction. Phosphorylation of Janus kinase 2 (JAK2)/signal transducer and activator of transcription 3 (STAT3) was decreased, although levels of circulating leptin or leptin receptor expression were unaltered. Furthermore, insulin receptor substrate (IRS)/phosphoinositide 3-kinase (PI3K)/AKT/mTOR and forkhead box O1 (FoxO1) signaling pathways were also compromised. Moreover, core circadian clock genes were also decreased in the sleep restriction group compared with the control. Chronic timed sleep restriction induced hyperphagic behaviors, attenuated leptin receptor-mediated signaling pathways, and depleted the expression of circadian clock gene in the hypothalamus of adolescent and young adult rats.
| S-EPMC7507490 | biostudies-literature