Stochastic systems have been widely investigated and employed in numerous
applications in different areas such as finance, biology and engineering as
they allow accounting for imprecisions so often faced in every practical tasks. Often that task would require to find the best action sequence in order to optimize the outcome. When the model is small, one can efficiently employ algorithmic techniques to synthesize such a control policy. Hence, in case of more complex models, instead of solving control tasks there directly, one may want to approximate them with simpler ones and then use those algorithms. This method is called abstraction for it abstracts the original “physical” model to an “abstract” one, only needed to ease the computations. Ideally, this abstract model is somewhat similar to the original one, as we want to extrapolate results achieved over the former to the setting of the latter. One way this similarity can be ensured is by means of the (bi)simulation methods, that give sufficient conditions to the closeness of behaviors of the two systems being compared. Such techniques became popular in discrete non-stochastic models, then advanced to continuous ones and started making steps to discrete stochastic systems. Yet, definite results were not achieved for abstractions of continuous stochastic models. There were trials to extend ideas from continuous non-stochastic framework, or discrete stochastic one, but they were mostly fragmentary. This thesis brings those methods together to build a unified framework and shows immediate benefits of doing this.
To define the closeness between the systems we look at their path-wise properties, which cover most of the tasks whose relevance was praised in the literature. That comprises both additive cost-like criteria and formal specifications, e.g. encoded by LTL formulae of the kind “reach the goal set through the safe set while avoiding dangerous states”. We derive guarantees on the approximation error and suggest how to build an abstraction for a given tolerance level. These guarantees work mostly for the finite time horizon properties, hence for the rest we develop task-dependent solution methods, further connecting with the existing literature. Besides those concrete results, we also put some effort in developing the conceptual side of the bisimulation framework for stochastic systems. For example, we know how important it is to choose a definition of behavior here, since bisimiliarity is useful as long as it guarantees closeness of behaviors one is interested in.
We hence stress the importance of keeping in mind the final goal while extrapolating abstract solution methods, and show which issues may arise when this goal is forgotten. We also extend the framework we deal with beyond bisimulation of stochastic systems only, providing a formalization of approximate relations and their connections with pseudo-metrics, proving several theorems in probabilistic approximation, whose generality is greater than the scope of this thesis, and also provide a category-theoretical basis for bisimulations of stochastic systems, hence opening one more door from which this problem can be approached.