SYMay 31, 2016
Verification of general Markov decision processes by approximate similarity relations and policy refinementS. Haesaert, S. Esmaeil Zadeh Soudjani, A. Abate
In this work we introduce new approximate similarity relations that are shown to be key for policy (or control) synthesis over general Markov decision processes. The models of interest are discrete-time Markov decision processes, endowed with uncountably-infinite state spaces and metric output (or observation) spaces. The new relations, underpinned by the use of metrics, allow in particular for a useful trade-off between deviations over probability distributions on states, and distances between model outputs. We show that the new probabilistic similarity relations, inspired by a notion of simulation developed for finite-state models, can be effectively employed over general Markov decision processes for verification purposes, and specifically for control refinement from abstract models.
SYApr 23, 2018
Approximate Abstractions of Markov Chains with Interval Decision Processes (Extended Version)Y. Zacchia Lun, J. Wheatley, A. D'Innocenzo et al.
This work introduces a new abstraction technique for reducing the state space of large, discrete-time labelled Markov chains. The abstraction leverages the semantics of interval Markov decision processes and the existing notion of approximate probabilistic bisimulation. Whilst standard abstractions make use of abstract points that are taken from the state space of the concrete model and which serve as representatives for sets of concrete states, in this work the abstract structure is constructed considering abstract points that are not necessarily selected from the states of the concrete model, rather they are a function of these states. The resulting model presents a smaller one-step bisimulation error, when compared to a like-sized, standard Markov chain abstraction. We outline a method to perform probabilistic model checking, and show that the computational complexity of the new method is comparable to that of standard abstractions based on approximate probabilistic bisimulations.
SYMar 7, 2019
Linear quadratic regulation of polytopic time-inhomogeneous Markov jump linear systems (extended version)Y. Zacchia Lun, A. Abate, A. D'Innocenzo
In most real cases transition probabilities between operational modes of Markov jump linear systems cannot be computed exactly and are time-varying. We take into account this aspect by considering Markov jump linear systems where the underlying Markov chain is polytopic and time-inhomogeneous, i.e. its transition probability matrix is varying over time, with variations that are arbitrary within a polytopic set of stochastic matrices. We address and solve for this class of systems the infinite-horizon optimal control problem. In particular, we show that the optimal controller can be obtained from a set of coupled algebraic Riccati equations, and that for mean square stabilizable systems the optimal finite-horizon cost corresponding to the solution to a parsimonious set of coupled difference Riccati equations converges exponentially fast to the optimal infinite-horizon cost related to the set of coupled algebraic Riccati equations. All the presented concepts are illustrated on a numerical example showing the efficiency of the provided solution.