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.@en

Formal 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 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 models of the given stochastic systems. Symbolic models are finite 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. Such discretization generally 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.

@en