An official website of the United States government
We study the problem of covering barrier points by mobile sensors. Each sensor is represented by a point in the plane with the same covering range [Formula: see text] so that any point within distance [Formula: see text] from the sensor can be covered by the sensor. Given a set [Formula: see text] of [Formula: see text] points (called “barrier points”) and a set [Formula: see text] of [Formula: see text] points (representing the “sensors”) in the plane, the problem is to move the sensors so that each barrier point is covered by at least one sensor and the maximum movement of all sensors is minimized. The problem is NP-hard. In this paper, we consider two line-constrained variations of the problem and present efficient algorithms that improve the previous work. In the first problem, all sensors are given on a line [Formula: see text] and are required to move on [Formula: see text] only while the barrier points can be anywhere in the plane. We propose an [Formula: see text] time algorithm for the problem. We also consider the weighted case where each sensor has a weight; we give an [Formula: see text] time algorithm for this case. In the second problem, all barrier points are on [Formula: see text] while all sensors are in the plane but are required to move onto [Formula: see text] to cover all barrier points. We also solve the weighted case in [Formula: see text] time.
more »
« less
Formal Safety Envelopes for Provably Accurate State Classification by Data-Driven Flight Models
Aerospace systems are inherently stochastic and increasingly data-driven, thus hard to formally verify. Data-driven statistical models can be used to estimate the state and classify potentially anomalous conditions of aerospace systems from multiple heterogeneous sensors with high accuracy. In this paper, we consider the problem of precisely bounding the regions in the sensor input space of a stochastic system in which safe state classification can be formally proven. As an archetypal application, we consider a statistical model created to detect aerodynamic stall in a prototype wing retrofitted with piezoelectric sensors and used to generate data in a wind tunnel for different flight states. We formally define safety envelopes as regions parameterized by [Formula: see text] and [Formula: see text], to respectively capture how model-predictable observed sensor values are, and given these values, how likely the model’s accurate state classification is. Safety envelopes are formalized in the Agda proof assistant, used to also generate formally verified runtime monitors for sensor data stream analyses in the Haskell programming language. We further propose a new metric for model classification quality, evaluate it on our wing prototype model, and compare it to the model restricted to two different fixed airspeeds, and enhanced to a continuous Gaussian process regression model. Safety envelopes are an important step in formally verifying precise probabilistic properties of data-driven models used in stochastic aerospace systems and could be used by advanced control algorithms to maintain these systems well within safe operation boundaries.
more »
« less
- Award ID(s):
- 1816307
- PAR ID:
- 10469147
- Publisher / Repository:
- AIAA
- Date Published:
- Journal Name:
- Journal of Aerospace Information Systems
- Volume:
- 20
- Issue:
- 1
- ISSN:
- 1940-3151
- Page Range / eLocation ID:
- 3 to 16
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)Consider a fractional Brownian motion (fBM) [Formula: see text] with Hurst index [Formula: see text]. We construct a probability space supporting both B H and a fully simulatable process [Formula: see text] such that[Formula: see text] with probability one for any user-specified error bound [Formula: see text]. When [Formula: see text], we further enhance our error guarantee to the α-Hölder norm for any [Formula: see text]. This enables us to extend our algorithm to the simulation of fBM-driven stochastic differential equations [Formula: see text]. Under mild regularity conditions on the drift and diffusion coefficients of Y, we construct a probability space supporting both Y and a fully simulatable process [Formula: see text] such that[Formula: see text] with probability one. Our algorithms enjoy the tolerance-enforcement feature, under which the error bounds can be updated sequentially in an efficient way. Thus, the algorithms can be readily combined with other advanced simulation techniques to estimate the expectations of functionals of fBMs efficiently.more » « less
-
We provide a simple extension of Bolthausen’s Morita-type proof of the replica symmetric formula [E. Bolthausen, “A Morita type proof of the replica-symmetric formula for SK,” in Statistical Mechanics of Classical and Disordered Systems, Springer Proceedings in Mathematics and Statistics (Springer, Cham., 2018), pp. 63–93; arXiv:1809.07972] for the Sherrington–Kirkpatrick model and prove the replica symmetry for all ( β, h) that satisfy [Formula: see text], where [Formula: see text]. Compared to the work of Bolthausen [“A Morita type proof of the replica-symmetric formula for SK,” in Statistical Mechanics of Classical and Disordered Systems, Springer Proceedings in Mathematics and Statistics (Springer, Cham., 2018), pp. 63–93; arXiv:1809.07972], the key of the argument is to apply the conditional second moment method to a suitably reduced partition function.more » « less
-
In this paper, we present a homotopical framework for studying invertible gapped phases of matter from the point of view of infinite spin lattice systems, using the framework of algebraic quantum mechanics. We define the notion of quantum state types. These are certain lax-monoidal functors from the category of finite-dimensional Hilbert spaces to the category of topological spaces. The universal example takes a finite-dimensional Hilbert space [Formula: see text] to the pure state space of the quasi-local algebra of the quantum spin system with Hilbert space [Formula: see text] at each site of a specified lattice. The lax-monoidal structure encodes the tensor product of states, which corresponds to stacking for quantum systems. We then explain how to formally extract parametrized phases of matter from quantum state types, and how they naturally give rise to [Formula: see text]-spaces for an operad we call the “multiplicative” linear isometry operad. We define the notion of invertible quantum state types and explain how the passage to phases for these is related to group completion. We also explain how invertible quantum state types give rise to loop-spectra. Our motivation is to provide a framework for constructing Kitaev’s loop-spectrum of bosonic invertible gapped phases of matter. Finally, as a first step toward understanding the homotopy types of the loop-spectra associated to invertible quantum state types, we prove that the pure state space of any UHF algebra is simply connected.more » « less
-
Control barrier functions are mathematical constructs used to guarantee safety for robotic systems. When integrated as constraints in a quadratic programming optimization problem, instantaneous control synthesis with real-time performance demands can be achieved for robotics applications. Prevailing use has assumed full knowledge of the safety barrier functions, however there are cases where the safe regions must be estimated online from sensor measurements. In these cases, the corresponding barrier function must be synthesized online. This paper describes a learning framework for estimating control barrier functions from sensor data. Doing so affords system operation in unknown state space regions without compromising safety. Here, a support vector machine classifier provides the barrier function specification as determined by sets of safe and unsafe states obtained from sensor measurements. Theoretical safety guarantees are provided. Experimental ROS-based simulation results for an omnidirectional robot equipped with LiDAR demonstrate safe operation.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.2514/1.I011073
