Showing 1–23 of 23 results for author: Abate, A

Distributed Markov Chain Monte Carlo Sampling based on the Alternating Direction Method of Multipliers

Authors: Alexandros E. Tzikas, Licio Romao, Mert Pilanci, Alessandro Abate, Mykel J. Kochenderfer

Abstract: Many machine learning applications require operating on a spatially distributed dataset. Despite technological advances, privacy considerations and communication constraints may prevent gathering the entire dataset in a central unit. In this paper, we propose a distributed sampling scheme based on the alternating direction method of multipliers, which is commonly used in the optimization literatur… ▽ More Many machine learning applications require operating on a spatially distributed dataset. Despite technological advances, privacy considerations and communication constraints may prevent gathering the entire dataset in a central unit. In this paper, we propose a distributed sampling scheme based on the alternating direction method of multipliers, which is commonly used in the optimization literature due to its fast convergence. In contrast to distributed optimization, distributed sampling allows for uncertainty quantification in Bayesian inference tasks. We provide both theoretical guarantees of our algorithm's convergence and experimental evidence of its superiority to the state-of-the-art. For our theoretical results, we use convex optimization tools to establish a fundamental inequality on the generated local sample iterates. This inequality enables us to show convergence of the distribution associated with these iterates to the underlying target distribution in Wasserstein distance. In simulation, we deploy our algorithm on linear and logistic regression tasks and illustrate its fast convergence compared to existing gradient-based methods. △ Less

Submitted 28 January, 2024; originally announced January 2024.

Policy Evaluation in Distributional LQR (Extended Version)

Authors: Zifan Wang, Yulong Gao, Siyi Wang, Michael M. Zavlanos, Alessandro Abate, Karl H. Johansson

Abstract: Distributional reinforcement learning (DRL) enhances the understanding of the effects of the randomness in the environment by letting agents learn the distribution of a random return, rather than its expected value as in standard reinforcement learning. Meanwhile, a challenge in DRL is that the policy evaluation typically relies on the representation of the return distribution, which needs to be c… ▽ More Distributional reinforcement learning (DRL) enhances the understanding of the effects of the randomness in the environment by letting agents learn the distribution of a random return, rather than its expected value as in standard reinforcement learning. Meanwhile, a challenge in DRL is that the policy evaluation typically relies on the representation of the return distribution, which needs to be carefully designed. In this paper, we address this challenge for the special class of DRL problems that rely on a discounted linear quadratic regulator (LQR), which we call \emph{distributional LQR}. Specifically, we provide a closed-form expression for the distribution of the random return, which is applicable for all types of exogenous disturbance as long as it is independent and identically distributed (i.i.d.). We show that the variance of the random return is bounded if the fourth moment of the exogenous disturbance is bounded. Furthermore, we investigate the sensitivity of the return distribution to model perturbations. While the proposed exact return distribution consists of infinitely many random variables, we show that this distribution can be well approximated by a finite number of random variables. The associated approximation error can be analytically bounded under mild assumptions. When the model is unknown, we propose a model-free approach for estimating the return distribution, supported by sample complexity guarantees. Finally, we extend our approach to partially observable linear systems. Numerical experiments are provided to illustrate the theoretical results. △ Less

Submitted 23 March, 2024; v1 submitted 28 November, 2023; originally announced January 2024.

Comments: This draft is an extension to our previous work https://proceedings.mlr.press/v211/wang23c/wang23c.pdf. arXiv admin note: text overlap with arXiv:2303.13657

Stability Analysis of Switched Linear Systems with Neural Lyapunov Functions

Authors: Virginie Debauche, Alec Edwards, Raphael M. Jungers, Alessandro Abate

Abstract: Neural-based, data-driven analysis and control of dynamical systems have been recently investigated and have shown great promise, e.g. for safety verification or stability analysis. Indeed, not only do neural networks allow for an entirely model-free, data-driven approach, but also for handling arbitrary complex functions via their power of representation (as opposed to, e.g. algebraic optimizatio… ▽ More Neural-based, data-driven analysis and control of dynamical systems have been recently investigated and have shown great promise, e.g. for safety verification or stability analysis. Indeed, not only do neural networks allow for an entirely model-free, data-driven approach, but also for handling arbitrary complex functions via their power of representation (as opposed to, e.g. algebraic optimization techniques that are restricted to polynomial functions). Whilst classical Lyapunov techniques allow to provide a formal and robust guarantee of stability of a switched dynamical system, very little is yet known about correctness guarantees for Neural Lyapunov functions, nor about their performance (amount of data needed for a certain accuracy). We thus formally introduce neural Lyapunov functions for the stability analysis of switched linear systems: we benchmark them on this paradigmatic problem, which is notoriously difficult (and in general Turing-undecidable), but which admits recently-developed technologies and theoretical results. Inspired by switched systems theory, we provide theoretical guarantees on the representative power of neural networks, leveraging recent results from the ML community. We additionally experimentally display how neural Lyapunov functions compete with state-of-the-art results and techniques, while admitting a wide range of improvement, both in theory and in practice. This study intends to improve our understanding of the opportunities and current limitations of neural-based data-driven analysis and control of complex dynamical systems. △ Less

Submitted 13 December, 2023; originally announced December 2023.

Comments: 13 pages, 8 figures

Learning-based Rigid Tube Model Predictive Control

Authors: Yulong Gao, Shuhao Yan, Jian Zhou, Mark Cannon, Alessandro Abate, Karl H. Johansson

Abstract: This paper is concerned with model predictive control (MPC) of discrete-time linear systems subject to bounded additive disturbance and mixed constraints on the state and input, whereas the true disturbance set is unknown. Unlike most existing work on robust MPC, we propose an algorithm incorporating online learning that builds on prior knowledge of the disturbance, i.e., a known but conservative… ▽ More This paper is concerned with model predictive control (MPC) of discrete-time linear systems subject to bounded additive disturbance and mixed constraints on the state and input, whereas the true disturbance set is unknown. Unlike most existing work on robust MPC, we propose an algorithm incorporating online learning that builds on prior knowledge of the disturbance, i.e., a known but conservative disturbance set. We approximate the true disturbance set at each time step with a parameterised set, which is referred to as a quantified disturbance set, using disturbance realisations. A key novelty is that the parameterisation of these quantified disturbance sets enjoys desirable properties such that the quantified disturbance set and its corresponding rigid tube bounding disturbance propagation can be efficiently updated online. We provide statistical gaps between the true and quantified disturbance sets, based on which, probabilistic recursive feasibility of MPC optimisation problems is discussed. Numerical simulations are provided to demonstrate the effectiveness of our proposed algorithm and compare with conventional robust MPC algorithms. △ Less

Submitted 21 May, 2024; v1 submitted 11 April, 2023; originally announced April 2023.

Comments: 8 pages

Policy Evaluation in Distributional LQR

Authors: Zifan Wang, Yulong Gao, Siyi Wang, Michael M. Zavlanos, Alessandro Abate, Karl H. Johansson

Abstract: Distributional reinforcement learning (DRL) enhances the understanding of the effects of the randomness in the environment by letting agents learn the distribution of a random return, rather than its expected value as in standard RL. At the same time, a main challenge in DRL is that policy evaluation in DRL typically relies on the representation of the return distribution, which needs to be carefu… ▽ More Distributional reinforcement learning (DRL) enhances the understanding of the effects of the randomness in the environment by letting agents learn the distribution of a random return, rather than its expected value as in standard RL. At the same time, a main challenge in DRL is that policy evaluation in DRL typically relies on the representation of the return distribution, which needs to be carefully designed. In this paper, we address this challenge for a special class of DRL problems that rely on linear quadratic regulator (LQR) for control, advocating for a new distributional approach to LQR, which we call \emph{distributional LQR}. Specifically, we provide a closed-form expression of the distribution of the random return which, remarkably, is applicable to all exogenous disturbances on the dynamics, as long as they are independent and identically distributed (i.i.d.). While the proposed exact return distribution consists of infinitely many random variables, we show that this distribution can be approximated by a finite number of random variables, and the associated approximation error can be analytically bounded under mild assumptions. Using the approximate return distribution, we propose a zeroth-order policy gradient algorithm for risk-averse LQR using the Conditional Value at Risk (CVaR) as a measure of risk. Numerical experiments are provided to illustrate our theoretical results. △ Less

Submitted 23 March, 2023; originally announced March 2023.

Comments: 12pages

Markov Chain Approximations to Stochastic Differential Equations by Recombination on Lattice Trees

Authors: Francesco Cosentino, Harald Oberhauser, Alessandro Abate

Abstract: We revisit the classical problem of approximating a stochastic differential equation by a discrete-time and discrete-space Markov chain. Our construction iterates Caratheodory's theorem over time to match the moments of the increments locally. This allows to construct a Markov chain with a sparse transition matrix where the number of attainable states grows at most polynomially as time increases.… ▽ More We revisit the classical problem of approximating a stochastic differential equation by a discrete-time and discrete-space Markov chain. Our construction iterates Caratheodory's theorem over time to match the moments of the increments locally. This allows to construct a Markov chain with a sparse transition matrix where the number of attainable states grows at most polynomially as time increases. Moreover, the MC evolves on a tree whose nodes lie on a "universal lattice" in the sense that an arbitrary number of different SDEs can be approximated on the same tree. The construction is not tailored to specific models, we discuss both the case of uni-variate and multi-variate case SDEs, and provide an implementation and numerical experiments. △ Less

Submitted 5 November, 2021; originally announced November 2021.

Grid-Free Computation of Probabilistic Safety with Malliavin Calculus

Authors: Francesco Cosentino, Harald Oberhauser, Alessandro Abate

Abstract: This work concerns continuous-time, continuous-space stochastic dynamical systems described by stochastic differential equations (SDE). It presents a new approach to compute probabilistic safety regions, namely sets of initial conditions of the SDE associated to trajectories that are safe with a probability larger than a given threshold. The approach introduces a functional that is minimised at th… ▽ More This work concerns continuous-time, continuous-space stochastic dynamical systems described by stochastic differential equations (SDE). It presents a new approach to compute probabilistic safety regions, namely sets of initial conditions of the SDE associated to trajectories that are safe with a probability larger than a given threshold. The approach introduces a functional that is minimised at the border of the probabilistic safety region, then solves an optimisation problem using techniques from Malliavin Calculus, which computes such region. Unlike existing results in the literature, the new approach allows one to compute probabilistic safety regions without gridding the state space of the SDE. △ Less

Submitted 10 January, 2023; v1 submitted 29 April, 2021; originally announced April 2021.

Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems

Authors: Muhammad Syifa'ul Mufid, Dieky Adzkiya, Alessandro Abate

Abstract: This work discusses the reachability analysis (RA) of Max-Plus Linear (MPL) systems, a class of continuous-space, discrete-event models defined over the max-plus algebra. Given the initial and target sets, we develop algorithms to verify whether there exist trajectories of the MPL system that, starting from the initial set, eventually reach the target set. We show that RA can be solved symbolicall… ▽ More This work discusses the reachability analysis (RA) of Max-Plus Linear (MPL) systems, a class of continuous-space, discrete-event models defined over the max-plus algebra. Given the initial and target sets, we develop algorithms to verify whether there exist trajectories of the MPL system that, starting from the initial set, eventually reach the target set. We show that RA can be solved symbolically by encoding the MPL system, as well as initial and target sets into difference logic, and then checking the satisfaction of the resulting logical formula via an off-the-shelf satisfiability modulo theories (SMT) solver. The performance and scalability of the developed SMT-based algorithms are shown to clearly outperform state-of-the-art RA algorithms for MPL systems, newly allowing to investigate RA of high-dimensional MPL systems: the verification of models with more than 100 continuous variables shows the applicability of these techniques to MPL systems of industrial relevance. △ Less

Submitted 8 July, 2020; originally announced July 2020.

Comments: 7 pages, accepted in International Workshop on Discrete Event Systems (WODES) 2020

Carathéodory Sampling for Stochastic Gradient Descent

Authors: Francesco Cosentino, Harald Oberhauser, Alessandro Abate

Abstract: Many problems require to optimize empirical risk functions over large data sets. Gradient descent methods that calculate the full gradient in every descent step do not scale to such datasets. Various flavours of Stochastic Gradient Descent (SGD) replace the expensive summation that computes the full gradient by approximating it with a small sum over a randomly selected subsample of the data set th… ▽ More Many problems require to optimize empirical risk functions over large data sets. Gradient descent methods that calculate the full gradient in every descent step do not scale to such datasets. Various flavours of Stochastic Gradient Descent (SGD) replace the expensive summation that computes the full gradient by approximating it with a small sum over a randomly selected subsample of the data set that in turn suffers from a high variance. We present a different approach that is inspired by classical results of Tchakaloff and Carathéodory about measure reduction. These results allow to replace an empirical measure with another, carefully constructed probability measure that has a much smaller support, but can preserve certain statistics such as the expected gradient. To turn this into scalable algorithms we firstly, adaptively select the descent steps where the measure reduction is carried out; secondly, we combine this with Block Coordinate Descent so that measure reduction can be done very cheaply. This makes the resulting methods scalable to high-dimensional spaces. Finally, we provide an experimental validation and comparison. △ Less

Submitted 25 November, 2020; v1 submitted 2 June, 2020; originally announced June 2020.

A Randomized Algorithm to Reduce the Support of Discrete Measures

Authors: Francesco Cosentino, Harald Oberhauser, Alessandro Abate

Abstract: Given a discrete probability measure supported on $N$ atoms and a set of $n$ real-valued functions, there exists a probability measure that is supported on a subset of $n+1$ of the original $N$ atoms and has the same mean when integrated against each of the $n$ functions. If $ N \gg n$ this results in a huge reduction of complexity. We give a simple geometric characterization of barycenters via ne… ▽ More Given a discrete probability measure supported on $N$ atoms and a set of $n$ real-valued functions, there exists a probability measure that is supported on a subset of $n+1$ of the original $N$ atoms and has the same mean when integrated against each of the $n$ functions. If $ N \gg n$ this results in a huge reduction of complexity. We give a simple geometric characterization of barycenters via negative cones and derive a randomized algorithm that computes this new measure by "greedy geometric sampling". We then study its properties, and benchmark it on synthetic and real-world data to show that it can be very beneficial in the $N\gg n$ regime. A Python implementation is available at \url{https://github.com/FraCose/Recombination_Random_Algos}. △ Less

Submitted 26 November, 2020; v1 submitted 2 June, 2020; originally announced June 2020.

Journal ref: 34th Conference on Advances in Neural Information Processing Systems, 2020

Tropical Abstractions of Max-Plus-Linear Systems

Authors: Muhammad Syifa'ul Mufid, Dieky Adzkiya, Alessndro Abate

Abstract: This paper describes the development of finite abstractions of Max-Plus-Linear (MPL) systems using tropical operations. The idea of tropical abstraction is inspired by the fact that an MPL system is a discrete-event model updating its state with operations in the tropical algebra. The abstract model is a finite-state transition system: we show that the abstract states can be generated by operation… ▽ More This paper describes the development of finite abstractions of Max-Plus-Linear (MPL) systems using tropical operations. The idea of tropical abstraction is inspired by the fact that an MPL system is a discrete-event model updating its state with operations in the tropical algebra. The abstract model is a finite-state transition system: we show that the abstract states can be generated by operations on the tropical algebra, and that the generation of transitions can be established by tropical multiplications of matrices. The complexity of the algorithms based on tropical algebra is discussed and their performance is tested on a numerical benchmark against an existing alternative abstraction approach. △ Less

Submitted 12 June, 2018; originally announced June 2018.

Comments: 20 pages including 5 pages Appendix. The paper is accepted in FORMATS'2018. We submit the longer version

Temporal logic control of general Markov decision processes by approximate policy refinement

Authors: Sofie Haesaert, Sadegh Soudjani, Alessandro Abate

Abstract: The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between… ▽ More The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between the original model and its abstraction. We newly work with a robust satisfaction for the construction and verification of control strategies, which allows for both deviations in the outputs of the gMDPs and in the probabilistic transitions. The computation is done over the reduced or abstracted models, such that when a property is robustly satisfied on the abstract model, it is also satisfied on the original model with respect to a refined control strategy. △ Less

Submitted 27 November, 2018; v1 submitted 20 December, 2017; originally announced December 2017.

Comments: 22 pages, 3 figures, Short version presented at the ADHS conference 2018 in Oxford

MSC Class: 93E03; 93E20; 68W25

Safety Verification of Output Feedback Controllers for Nonlinear Systems

Authors: Kendra Lesser, Alessandro Abate

Abstract: A high-gain observer is used for a class of feedback linearisable nonlinear systems to synthesize safety-preserving controllers over the observer output. A bound on the distance between trajectories under state and output feedback is derived, and shown to converge to zero as a function of the gain parameter of an observer. We can therefore recover safety properties under output feedback and contro… ▽ More A high-gain observer is used for a class of feedback linearisable nonlinear systems to synthesize safety-preserving controllers over the observer output. A bound on the distance between trajectories under state and output feedback is derived, and shown to converge to zero as a function of the gain parameter of an observer. We can therefore recover safety properties under output feedback and control saturation constraints by synthesizing a controller as if the full state were available. We specifically design feedback linearising controllers that satisfy certain properties, such as stability, and then construct the associated maximal safety-invariant set, namely the largest set of all initial states that are guaranteed to produce safe trajectories over a given (possibly infinite) time horizon. △ Less

Submitted 21 March, 2016; originally announced March 2016.

Comments: Extended version of European Control Conference 2016 submission

Towards Scalable Synthesis of Stochastic Control Systems

Authors: Majid Zamani, Ilya Tkachev, Alessandro Abate

Abstract: Formal control synthesis approaches over stochastic systems have received significant attention in the past few years, in view of their ability to provide provably correct controllers for complex logical specifications in an automated fashion. Examples of complex specifications of interest include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. A… ▽ More Formal control synthesis approaches over stochastic systems have received significant attention in the past few years, in view of their ability to provide provably correct controllers for complex logical specifications in an automated fashion. Examples of complex specifications of interest include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. A general methodology to synthesize controllers for such properties resorts to symbolic abstractions of the given stochastic systems. Symbolic models are discrete abstractions of the given concrete systems with the property that a controller designed on the abstraction can be refined (or implemented) into a controller on the original system. Although the recent development of techniques for the construction of symbolic models has been quite encouraging, the general goal of formal synthesis over stochastic control systems is by no means solved. A fundamental issue with the existing techniques is the known "curse of dimensionality," which is due to the need to discretize state and input sets and that results in an exponential complexity over the number of state and input variables in the concrete system. In this work we propose a novel abstraction technique for incrementally stable stochastic control systems, which does not require state-space discretization but only input set discretization, and that can be potentially more efficient (and thus scalable) than existing approaches. We elucidate the effectiveness of the proposed approach by synthesizing a schedule for the coordination of two traffic lights under some safety and fairness requirements for a road traffic model. Further we argue that this 5-dimensional linear stochastic control system cannot be studied with existing approaches based on state-space discretization due to the very large number of generated discrete states. △ Less

Submitted 3 February, 2016; originally announced February 2016.

Comments: 22 pages, 3 figures. arXiv admin note: text overlap with arXiv:1407.2730

MSC Class: 93E03; 68Q60; 93C10 ACM Class: D.2.4; B.1.2; B.5.2; I.2.8

Quantitative model-checking of controlled discrete-time Markov processes

Authors: Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate

Abstract: This paper focuses on optimizing probabilities of events of interest defined over general controlled discrete-time Markov processes. It is shown that the optimization over a wide class of $ω$-regular properties can be reduced to the solution of one of two fundamental problems: reachability and repeated reachability. We provide a comprehensive study of the former problem and an initial characterisa… ▽ More This paper focuses on optimizing probabilities of events of interest defined over general controlled discrete-time Markov processes. It is shown that the optimization over a wide class of $ω$-regular properties can be reduced to the solution of one of two fundamental problems: reachability and repeated reachability. We provide a comprehensive study of the former problem and an initial characterisation of the (much more involved) latter problem. A case study elucidates concepts and techniques. △ Less

Submitted 21 July, 2014; originally announced July 2014.

Symbolic Models for Stochastic Switched Systems: A Discretization and a Discretization-Free Approach

Authors: Majid Zamani, Alessandro Abate, Antoine Girard

Abstract: Stochastic switched systems are a relevant class of stochastic hybrid systems with probabilistic evolution over a continuous domain and control-dependent discrete dynamics over a finite set of modes. In the past few years several different techniques have been developed to assist in the stability analysis of stochastic switched systems. However, more complex and challenging objectives related to t… ▽ More Stochastic switched systems are a relevant class of stochastic hybrid systems with probabilistic evolution over a continuous domain and control-dependent discrete dynamics over a finite set of modes. In the past few years several different techniques have been developed to assist in the stability analysis of stochastic switched systems. However, more complex and challenging objectives related to the verification of and the controller synthesis for logic specifications have not been formally investigated for this class of systems as of yet. With logic specifications we mean properties expressed as formulae in linear temporal logic or as automata on infinite strings. This paper addresses these complex objectives by constructively deriving approximately equivalent (bisimilar) symbolic models of stochastic switched systems. More precisely, this paper provides two different symbolic abstraction techniques: one requires state space discretization, but the other one does not require any space discretization which can be potentially more efficient than the first one when dealing with higher dimensional stochastic switched systems. Both techniques provide finite symbolic models that are approximately bisimilar to stochastic switched systems under some stability assumptions on the concrete model. This allows formally synthesizing controllers (switching signals) that are valid for the concrete system over the finite symbolic model, by means of mature automata-theoretic techniques in the literature. The effectiveness of the results are illustrated by synthesizing switching signals enforcing logic specifications for two case studies including temperature control of a six-room building. △ Less

Submitted 10 July, 2014; originally announced July 2014.

Comments: 25 pages, 4 figures. arXiv admin note: text overlap with arXiv:1302.3868

Symbolic Abstractions of Networked Control Systems

Authors: Majid Zamani, Manuel Mazo Jr, Mahmoud Khaled, Alessandro Abate

Abstract: The last decade has witnessed significant attention on networked control systems (NCS) due to their ubiquitous presence in industrial applications, and, in the particular case of wireless NCS, because of their architectural flexibility and low installation and maintenance costs. In wireless NCS the communication between sensors, controllers, and actuators is supported by a communication channel th… ▽ More The last decade has witnessed significant attention on networked control systems (NCS) due to their ubiquitous presence in industrial applications, and, in the particular case of wireless NCS, because of their architectural flexibility and low installation and maintenance costs. In wireless NCS the communication between sensors, controllers, and actuators is supported by a communication channel that is likely to introduce variable communication delays, packet losses, limited bandwidth, and other practical non-idealities leading to numerous technical challenges. Although stability properties of NCS have been investigated extensively in the literature, results for NCS under more complex and general objectives, and in particular results dealing with verification or controller synthesis for logical specifications, are much more limited. This work investigates how to address such complex objectives by constructively deriving symbolic models of NCS, while encompassing the mentioned network non-idealities. The obtained abstracted (symbolic) models can then be employed to synthesize hybrid controllers enforcing rich logical specifications over the concrete NCS models. Examples of such general specifications include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. We thus provide a general synthesis framework that can be flexibly adapted to a number of NCS setups. We illustrate the effectiveness of the results over some case studies. △ Less

Submitted 21 November, 2016; v1 submitted 24 January, 2014; originally announced January 2014.

Comments: 22 pages, 8 figures, 1 table

MSC Class: 93C57; 93C85; 68M10 ACM Class: D.2.4; B.1.2; C.2.1

On the Optimal Solutions of the Infinite-Horizon Linear Sensor Scheduling Problem

Authors: Lin Zhao, Wei Zhang, Jianghai Hu, Alessandro Abate, Claire J. Tomlin

Abstract: This paper studies the infinite-horizon sensor scheduling problem for linear Gaussian processes with linear measurement functions. Several important properties of the optimal infinite-horizon schedules are derived. In particular, it is proved that under some mild conditions, both the optimal infinite-horizon average-per-stage cost and the corresponding optimal sensor schedules are independent of t… ▽ More This paper studies the infinite-horizon sensor scheduling problem for linear Gaussian processes with linear measurement functions. Several important properties of the optimal infinite-horizon schedules are derived. In particular, it is proved that under some mild conditions, both the optimal infinite-horizon average-per-stage cost and the corresponding optimal sensor schedules are independent of the covariance matrix of the initial state. It is also proved that the optimal estimation cost can be approximated arbitrarily closely by a periodic schedule with a finite period. Moreover, it is shown that the sequence of the average-per-stage costs of the optimal schedule must converge. These theoretical results provide valuable insights into the design and analysis of various infinite-horizon sensor scheduling algorithms. △ Less

Submitted 20 March, 2014; v1 submitted 30 November, 2013; originally announced December 2013.

Comments: 6 pages, 1 figure

On the effect of perturbation of conditional probabilities in total variation

Authors: Alessandro Abate, Frank Redig, Ilya Tkachev

Abstract: A celebrated result by A. Ionescu Tulcea provides a construction of a probability measure on a product space given a sequence of regular conditional probabilities. We study how the perturbations of the latter in the total variation metric affect the resulting product probability measure. A celebrated result by A. Ionescu Tulcea provides a construction of a probability measure on a product space given a sequence of regular conditional probabilities. We study how the perturbations of the latter in the total variation metric affect the resulting product probability measure. △ Less

Submitted 13 November, 2013; originally announced November 2013.

MSC Class: 60G99; 28A35

Journal ref: Statistics & Probability Letters 88 (2014), pp. 1-8

Computation of ruin probabilities for general discrete-time Markov models

Authors: Ilya Tkachev, Alessandro Abate

Abstract: We study the ruin problem over a risk process described by a discrete-time Markov model. In contrast to previous studies that focused on the asymptotic behaviour of ruin probabilities for large values of the initial capital, we provide a new technique to compute the quantity of interest for any initial value, and with any given precision. Rather than focusing on a particular model for risk process… ▽ More We study the ruin problem over a risk process described by a discrete-time Markov model. In contrast to previous studies that focused on the asymptotic behaviour of ruin probabilities for large values of the initial capital, we provide a new technique to compute the quantity of interest for any initial value, and with any given precision. Rather than focusing on a particular model for risk processes, we give a general characterization of the ruin probability by providing corresponding recursions and fixpoint equations. Since such equations for the ruin probability are ill-posed in the sense that they do not allow for unique solutions, we approximate the ruin probability by a two-barrier ruin probability, for which fixpoint equations are well-posed. We also show how good the introduced approximation is by providing an explicit bound on the error and by characterizing the cases when the error converges to zero. The presented technique and results are supported by two computational examples over models known in the literature, one of which is extremely heavy-tailed. △ Less

Submitted 23 August, 2013; originally announced August 2013.

Aggregation and Control of Populations of Thermostatically Controlled Loads by Formal Abstractions

Authors: Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate

Abstract: This work discusses a two-step procedure, based on formal abstractions, to generate a finite-space stochastic dynamical model as an aggregation of the continuous temperature dynamics of a homogeneous population of Thermostatically Controlled Loads (TCL). The temperature of a single TCL is described by a stochastic difference equation and the TCL status (ON, OFF) by a deterministic switching mechan… ▽ More This work discusses a two-step procedure, based on formal abstractions, to generate a finite-space stochastic dynamical model as an aggregation of the continuous temperature dynamics of a homogeneous population of Thermostatically Controlled Loads (TCL). The temperature of a single TCL is described by a stochastic difference equation and the TCL status (ON, OFF) by a deterministic switching mechanism. The procedure is formal as it allows the exact quantification of the error introduced by the abstraction -- as such it builds and improves on a known, earlier approximation technique in the literature. Further, the contribution discusses the extension to the case of a heterogeneous population of TCL by means of two approaches resulting in the notion of approximate abstractions. It moreover investigates the problem of global (population-level) regulation and load balancing for the case of TCL that are dependent on a control input. The procedure is tested on a case study and benchmarked against the mentioned alternative approach in the literature. △ Less

Submitted 30 July, 2013; v1 submitted 25 July, 2013; originally announced July 2013.

Comments: 40 pages, 21 figures; the paper generalizes the result of conference publication: S. Esmaeil Zadeh Soudjani and A. Abate, "Aggregation of Thermostatically Controlled Loads by Formal Abstractions," Proceedings of the European Control Conference 2013, pp. 4232-4237. version 2: added references for section 1

MSC Class: 60J05; 68Q60; 93E20

Symbolic control of stochastic systems via approximately bisimilar finite abstractions

Authors: Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, John Lygeros

Abstract: Symbolic approaches to the control design over complex systems employ the construction of finite-state models that are related to the original control systems, then use techniques from finite-state synthesis to compute controllers satisfying specifications given in a temporal logic, and finally translate the synthesized schemes back as controllers for the concrete complex systems. Such approaches… ▽ More Symbolic approaches to the control design over complex systems employ the construction of finite-state models that are related to the original control systems, then use techniques from finite-state synthesis to compute controllers satisfying specifications given in a temporal logic, and finally translate the synthesized schemes back as controllers for the concrete complex systems. Such approaches have been successfully developed and implemented for the synthesis of controllers over non-probabilistic control systems. In this paper, we extend the technique to probabilistic control systems modeled by controlled stochastic differential equations. We show that for every stochastic control system satisfying a probabilistic variant of incremental input-to-state stability, and for every given precision $\varepsilon>0$, a finite-state transition system can be constructed, which is $\varepsilon$-approximately bisimilar (in the sense of moments) to the original stochastic control system. Moreover, we provide results relating stochastic control systems to their corresponding finite-state transition systems in terms of probabilistic bisimulation relations known in the literature. We demonstrate the effectiveness of the construction by synthesizing controllers for stochastic control systems over rich specifications expressed in linear temporal logic. The discussed technique enables a new, automated, correct-by-construction controller synthesis approach for stochastic control systems, which are common mathematical models employed in many safety critical systems subject to structured uncertainty and are thus relevant for cyber-physical applications. △ Less

Submitted 15 February, 2013; originally announced February 2013.

Comments: 27 pages, 4 figures

Characterization and computation of infinite horizon specifications over Markov processes

Authors: Ilya Tkachev, Alessandro Abate

Abstract: This work is devoted to the formal verification of specifications over general discrete-time Markov processes, with an emphasis on infinite-horizon properties. These properties, formulated in a modal logic known as PCTL, can be expressed through value functions defined over the state space of the process. The main goal is to understand how structural features of the model (primarily the presence o… ▽ More This work is devoted to the formal verification of specifications over general discrete-time Markov processes, with an emphasis on infinite-horizon properties. These properties, formulated in a modal logic known as PCTL, can be expressed through value functions defined over the state space of the process. The main goal is to understand how structural features of the model (primarily the presence of absorbing sets) influence the uniqueness of the solutions of corresponding Bellman equations. Furthermore, this contribution shows that the investigation of these structural features leads to new computational techniques to calculate the specifications of interest: the emphasis is to derive approximation techniques with associated explicit convergence rates and formal error bounds. △ Less

Submitted 22 July, 2014; v1 submitted 19 November, 2012; originally announced November 2012.

MSC Class: 60J05; 68Q60

Journal ref: Theoretical Computer Science 515 (2014), pp. 1-18