Exact acceleration of complex real-time model checking based on overlapping cycle.
Ontology highlight
ABSTRACT:
SUBMITTER: Wang G
PROVIDER: S-EPMC7924618 | biostudies-literature |
REPOSITORIES: biostudies-literature
Similar Datasets
Project description:Although electro-holography can reconstruct three-dimensional (3D) motion pictures, its computational cost is too heavy to allow for real-time reconstruction of 3D motion pictures. This study explores accelerating colour hologram generation using light-ray information on a ray-sampling (RS) plane with a graphics processing unit (GPU) to realise a real-time holographic display system. We refer to an image corresponding to light-ray information as an RS image. Colour holograms were generated from three RS images with resolutions of 2,048?×?2,048; 3,072?×?3,072 and 4,096?×?4,096 pixels. The computational results indicate that the generation of the colour holograms using multiple GPUs (NVIDIA Geforce GTX 1080) was approximately 300-500 times faster than those generated using a central processing unit. In addition, the results demonstrate that 3D motion pictures were successfully reconstructed from RS images of 3,072?×?3,072 pixels at approximately 15 frames per second using an electro-holographic reconstruction system in which colour holograms were generated from RS images in real time.
| S-EPMC5784160 | biostudies-literature
Project description:Recurrent events are the natural outcome in many medical and epidemiology studies. To assess covariate effects on the gaps between consecutive recurrent events, the Cox proportional hazards model is frequently employed in data analysis. The validity of statistical inference, however, depends on the appropriateness of the Cox model. In this paper, we propose a class of graphical techniques and formal tests for checking the Cox model with recurrent gap time data. The building block of our model checking method is an averaged martingale-like process, based on which a class of multiparameter stochastic processes is proposed. This maneuver is very general and can be used to assess different aspects of model fit. Numerical simulations are conducted to examine finite-sample performance, and the proposed model checking techniques are illustrated with data from the Danish Psychiatric Central Register.
| S-EPMC3138070 | 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:Traffic problems often occur due to the traffic demands by the outnumbered vehicles on road. Maximizing traffic flow and minimizing the average waiting time are the goals of intelligent traffic control. Each junction wants to get larger traffic flow. During the course, junctions form a policy of coordination as well as constraints for adjacent junctions to maximize their own interests. A good traffic signal timing policy is helpful to solve the problem. However, as there are so many factors that can affect the traffic control model, it is difficult to find the optimal solution. The disability of traffic light controllers to learn from past experiences caused them to be unable to adaptively fit dynamic changes of traffic flow. Considering dynamic characteristics of the actual traffic environment, reinforcement learning algorithm based traffic control approach can be applied to get optimal scheduling policy. The proposed Sarsa(λ)-based real-time traffic control optimization model can maintain the traffic signal timing policy more effectively. The Sarsa(λ)-based model gains traffic cost of the vehicle, which considers delay time, the number of waiting vehicles, and the integrated saturation from its experiences to learn and determine the optimal actions. The experiment results show an inspiring improvement in traffic control, indicating the proposed model is capable of facilitating real-time dynamic traffic control.
| S-EPMC3922017 | biostudies-other
Project description:We derive and validate a novel and analytic method for estimating the probability that an epidemic has been eliminated (i.e. that no future local cases will emerge) in real time. When this probability crosses 0.95 an outbreak can be declared over with 95% confidence. Our method is easy to compute, only requires knowledge of the incidence curve and the serial interval distribution, and evaluates the statistical lifetime of the outbreak of interest. Using this approach, we show how the time-varying under-reporting of infected cases will artificially inflate the inferred probability of elimination, leading to premature (false-positive) end-of-epidemic declarations. Contrastingly, we prove that incorrectly identifying imported cases as local will deceptively decrease this probability, resulting in delayed (false-negative) declarations. Failing to sustain intensive surveillance during the later phases of an epidemic can therefore substantially mislead policymakers on when it is safe to remove travel bans or relax quarantine and social distancing advisories. World Health Organisation guidelines recommend fixed (though disease-specific) waiting times for end-of-epidemic declarations that cannot accommodate these variations. Consequently, there is an unequivocal need for more active and specialised metrics for reliably identifying the conclusion of an epidemic.
| S-EPMC7717584 | biostudies-literature
Project description:A synaptic theory of Working Memory (WM) has been developed in the last decade as a possible alternative to the persistent spiking paradigm. In this context, we have developed a neural mass model able to reproduce exactly the dynamics of heterogeneous spiking neural networks encompassing realistic cellular mechanisms for short-term synaptic plasticity. This population model reproduces the macroscopic dynamics of the network in terms of the firing rate and the mean membrane potential. The latter quantity allows us to gain insight of the Local Field Potential and electroencephalographic signals measured during WM tasks to characterize the brain activity. More specifically synaptic facilitation and depression integrate each other to efficiently mimic WM operations via either synaptic reactivation or persistent activity. Memory access and loading are related to stimulus-locked transient oscillations followed by a steady-state activity in the β-γ band, thus resembling what is observed in the cortex during vibrotactile stimuli in humans and object recognition in monkeys. Memory juggling and competition emerge already by loading only two items. However more items can be stored in WM by considering neural architectures composed of multiple excitatory populations and a common inhibitory pool. Memory capacity depends strongly on the presentation rate of the items and it maximizes for an optimal frequency range. In particular we provide an analytic expression for the maximal memory capacity. Furthermore, the mean membrane potential turns out to be a suitable proxy to measure the memory load, analogously to event driven potentials in experiments on humans. Finally we show that the γ power increases with the number of loaded items, as reported in many experiments, while θ and β power reveal non monotonic behaviours. In particular, β and γ rhythms are crucially sustained by the inhibitory activity, while the θ rhythm is controlled by excitatory synapses.
| S-EPMC7771880 | biostudies-literature
Project description:Tracking and manipulating deformable linear objects (DLOs) has great potential in the industrial world. However, estimating the object's state is crucial and challenging, especially when dealing with heavy occlusion situations and physical properties of different objects. To address these problems, we introduce a novel tracking algorithm to observe and estimate the states of DLO. The proposed tracking algorithm is based on the Coherent Point Drift (CPD), which registers the observed point cloud, and the finite element method (FEM) model encodes physical properties. The Gaussian mixture model with CPD regularization generates constraints to deform a given FEM model into desired shapes. The FEM model encodes the local structure, the global topology, and the material property to better approximate the deformation process in the real world without using simulation software. A series of simulations and real data tracking experiments have been conducted on deformable objects, such as rope and iron wire, to demonstrate the robustness and accuracy of our method in the presence of occlusion.
| S-EPMC9136076 | biostudies-literature
Project description:Mapping the longitudinal relaxation time T1 has widespread applications in clinical MRI as it promises a quantitative comparison of tissue properties across subjects and scanners. Due to the long scan times of conventional methods, however, the use of quantitative MRI in clinical routine is still very limited. In this work, an acceleration of Inversion-Recovery Look-Locker (IR-LL) T1 mapping is presented. A model-based algorithm is used to iteratively enforce an exponential relaxation model to a highly undersampled radially acquired IR-LL dataset obtained after the application of a single global inversion pulse. Using the proposed technique, a T1 map of a single slice with 1.6mm in-plane resolution and 4mm slice thickness can be reconstructed from data acquired in only 6s. A time-consuming segmented IR experiment was used as gold standard for T1 mapping in this work. In the subsequent validation study, the model-based reconstruction of a single-inversion IR-LL dataset exhibited a T1 difference of less than 2.6% compared to the segmented IR-LL reference in a phantom consisting of vials with T1 values between 200ms and 3000ms. In vivo, the T1 difference was smaller than 5.5% in WM and GM of seven healthy volunteers. Additionally, the T1 values are comparable to standard literature values. Despite the high acceleration, all model-based reconstructions were of a visual quality comparable to fully sampled references. Finally, the reproducibility of the T1 mapping method was demonstrated in repeated acquisitions. In conclusion, the presented approach represents a promising way for fast and accurate T1 mapping using radial IR-LL acquisitions without the need of any segmentation.
| S-EPMC4393277 | biostudies-literature
Project description:Multipath and off-axis scattering are two of the primary mechanisms for ultrasound image degradation. To address their impact, we have proposed Aperture Domain Model Image REconstruction (ADMIRE). This algorithm utilizes a model-based approach in order to identify and suppress sources of acoustic clutter. The ability of ADMIRE to suppress clutter and improve image quality has been demonstrated in previous works, but its use for real-time imaging has been infeasible due to its significant computational requirements. However, in recent years, the use of graphics processing units (GPUs) for general-purpose computing has enabled the significant acceleration of compute-intensive algorithms. This is because many modern GPUs have thousands of computational cores that can be utilized to perform massively parallel processing. Therefore, in this work, we have developed a GPU-based implementation of ADMIRE. The implementation on a single GPU provides a speedup of two orders of magnitude when compared to a serial CPU implementation, and additional speedup is achieved when the computations are distributed across two GPUs. In addition, we demonstrate the feasibility of the GPU implementation to be used for real-time imaging by interfacing it with a Verasonics Vantage 128 ultrasound research system. Moreover, we show that other beamforming techniques, such as delay-and-sum (DAS) and short-lag spatial coherence (SLSC), can be computed and simultaneously displayed with ADMIRE. The frame rate depends upon various parameters, and this is exhibited in the multiple imaging cases that are presented. An open-source code repository containing CPU and GPU implementations of ADMIRE is also provided.
| S-EPMC8532145 | 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