-
Learning Robust Policies for Uncertain Parametric Markov Decision Processes
Authors:
Luke Rickard,
Alessandro Abate,
Kostas Margellos
Abstract:
Synthesising verifiably correct controllers for dynamical systems is crucial for safety-critical problems. To achieve this, it is important to account for uncertainty in a robust manner, while at the same time it is often of interest to avoid being overly conservative with the view of achieving a better cost. We propose a method for verifiably safe policy synthesis for a class of finite state mode…
▽ More
Synthesising verifiably correct controllers for dynamical systems is crucial for safety-critical problems. To achieve this, it is important to account for uncertainty in a robust manner, while at the same time it is often of interest to avoid being overly conservative with the view of achieving a better cost. We propose a method for verifiably safe policy synthesis for a class of finite state models, under the presence of structural uncertainty. In particular, we consider uncertain parametric Markov decision processes (upMDPs), a special class of Markov decision processes, with parameterised transition functions, where such parameters are drawn from a (potentially) unknown distribution. Our framework leverages recent advancements in the so-called scenario approach theory, where we represent the uncertainty by means of scenarios, and provide guarantees on synthesised policies satisfying probabilistic computation tree logic (PCTL) formulae. We consider several common benchmarks/problems and compare our work to recent developments for verifying upMDPs.
△ Less
Submitted 15 May, 2024; v1 submitted 11 December, 2023;
originally announced December 2023.
-
Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics
Authors:
Luke Rickard,
Thom Badings,
Licio Romao,
Alessandro Abate
Abstract:
Automated synthesis of provably correct controllers for cyber-physical systems is crucial for deployment in safety-critical scenarios. However, hybrid features and stochastic or unknown behaviours make this problem challenging. We propose a method for synthesising controllers for Markov jump linear systems (MJLSs), a class of discrete-time models for cyber-physical systems, so that they certifiabl…
▽ More
Automated synthesis of provably correct controllers for cyber-physical systems is crucial for deployment in safety-critical scenarios. However, hybrid features and stochastic or unknown behaviours make this problem challenging. We propose a method for synthesising controllers for Markov jump linear systems (MJLSs), a class of discrete-time models for cyber-physical systems, so that they certifiably satisfy probabilistic computation tree logic (PCTL) formulae. An MJLS consists of a finite set of stochastic linear dynamics and discrete jumps between these dynamics that are governed by a Markov decision process (MDP). We consider the cases where the transition probabilities of this MDP are either known up to an interval or completely unknown. Our approach is based on a finite-state abstraction that captures both the discrete (mode-jum**) and continuous (stochastic linear) behaviour of the MJLS. We formalise this abstraction as an interval MDP (iMDP) for which we compute intervals of transition probabilities using sampling techniques from the so-called 'scenario approach', resulting in a probabilistically sound approximation. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
△ Less
Submitted 4 August, 2023; v1 submitted 1 December, 2022;
originally announced December 2022.
-
First Light for the First Station of the Long Wavelength Array
Authors:
G. B. Taylor,
S. W. Ellingson,
N. E. Kassim,
J. Craig,
J. Dowell,
C. N. Wolfe,
J. Hartman,
G. Bernardi,
T. Clarke,
A. Cohen,
N. P. Dalal,
W. C. Erickson,
B. Hicks,
L. J. Greenhill,
B. Jacoby,
W. Lane,
J. Lazio,
D. Mitchell,
R. Navarro,
S. M. Ord,
Y. Pihlstrom,
E. Polisensky,
P. S. Ray,
L. J. Rickard,
F. K. Schinzel
, et al. (10 additional authors not shown)
Abstract:
The first station of the Long Wavelength Array (LWA1) was completed in April 2011 and is currently performing observations resulting from its first call for proposals in addition to a continuing program of commissioning and characterization observations. The instrument consists of 258 dual-polarization dipoles, which are digitized and combined into beams. Four independently-steerable dual-polariza…
▽ More
The first station of the Long Wavelength Array (LWA1) was completed in April 2011 and is currently performing observations resulting from its first call for proposals in addition to a continuing program of commissioning and characterization observations. The instrument consists of 258 dual-polarization dipoles, which are digitized and combined into beams. Four independently-steerable dual-polarization beams are available, each with two "tunings" of 16 MHz bandwidth that can be independently tuned to any frequency between 10 MHz and 88 MHz. The system equivalent flux density for zenith pointing is ~3 kJy and is approximately independent of frequency; this corresponds to a sensitivity of ~5 Jy/beam (5sigma, 1 s); making it one of the most sensitive meter-wavelength radio telescopes. LWA1 also has two "transient buffer" modes which allow coherent recording from all dipoles simultaneously, providing instantaneous all-sky field of view. LWA1 provides versatile and unique new capabilities for Galactic science, pulsar science, solar and planetary science, space weather, cosmology, and searches for astrophysical transients. Results from LWA1 will detect or tightly constrain the presence of hot Jupiters within 50 parsecs of Earth. LWA1 will provide excellent resolution in frequency and in time to examine phenomena such as solar bursts, and pulsars over a 4:1 frequency range that includes the poorly understood turnover and steep-spectrum regimes. Observations to date have proven LWA1's potential for pulsar observing, and just a few seconds with the completed 256-dipole LWA1 provide the most sensitive images of the sky at 23 MHz obtained yet. We are operating LWA1 as an open skies radio observatory, offering ~2000 beam-hours per year to the general community.
△ Less
Submitted 28 June, 2012;
originally announced June 2012.
-
The LWA1 Radio Telescope
Authors:
S. W. Ellingson,
G. B. Taylor,
J. Craig,
J. Hartman,
J. Dowell,
C. N. Wolfe,
T. E. Clarke,
B. C. Hicks,
N. E. Kassim,
P. S. Ray,
L. J. Rickard,
F. K. Schinzel,
K. W. Weiler
Abstract:
LWA1 is a new radio telescope operating in the frequency range 10-88 MHz, located in central New Mexico. The telescope consists of 258 pairs of dipole-type antennas whose outputs are individually digitized and formed into beams. Simultaneously, signals from all dipoles can be recorded using one of the instrument's "all dipoles" modes, facilitating all-sky imaging. Notable features of the instrumen…
▽ More
LWA1 is a new radio telescope operating in the frequency range 10-88 MHz, located in central New Mexico. The telescope consists of 258 pairs of dipole-type antennas whose outputs are individually digitized and formed into beams. Simultaneously, signals from all dipoles can be recorded using one of the instrument's "all dipoles" modes, facilitating all-sky imaging. Notable features of the instrument include high intrinsic sensitivity (about 6 kJy zenith system equivalent flux density), large instantaneous bandwidth (up to 78 MHz), and 4 independently-steerable beams utilizing digital "true time delay" beamforming. This paper summarizes the design of LWA1 and its performance as determined in commissioning experiments. We describe the method currently in use for array calibration, and report on measurements of sensitivity and beamwidth.
△ Less
Submitted 18 January, 2013; v1 submitted 21 April, 2012;
originally announced April 2012.
-
The First Station of the Long Wavelength Array
Authors:
Patricia Henning,
Steven W. Ellingson,
Gregory B. Taylor,
Joseph Craig,
Ylva Pihlström,
Lee J Rickard,
Tracy E. Clarke,
Namir E. Kassim,
Aaron Cohen
Abstract:
The Long Wavelength Array (LWA) will be a new multi-purpose radio telescope operating in the frequency range 10-88 MHz. Upon completion, LWA will consist of 53 phased array "stations" distributed over a region about 400 km in diameter in the state of New Mexico. Each station will consist of 256 pairs of dipole-type antennas whose signals are formed into beams, with outputs transported to a central…
▽ More
The Long Wavelength Array (LWA) will be a new multi-purpose radio telescope operating in the frequency range 10-88 MHz. Upon completion, LWA will consist of 53 phased array "stations" distributed over a region about 400 km in diameter in the state of New Mexico. Each station will consist of 256 pairs of dipole-type antennas whose signals are formed into beams, with outputs transported to a central location for high-resolution aperture synthesis imaging. The resulting image sensitivity is estimated to be a few mJy (5 sigma, 8 MHz, 2 polarizations, 1 hr, zenith) in 20-80 MHz; with resolution and field of view of (8", 8 deg) and (2",2 deg) at 20 MHz and 80 MHz, respectively. All 256 dipole antennas are in place for the first station of the LWA (called LWA-1), and commissioning activities are well underway. The station is located near the core of the EVLA, and is expected to be fully operational in early 2011.
△ Less
Submitted 3 September, 2010;
originally announced September 2010.
