This paper proposes criteria for metrics between stochastic systems with a focus on the task of linear temporal model-checking. It explicitly puts forward two metrics which partially satisfy those criteria, and discusses their connection with other metrics studied in the literature. In particular, the notion of coupling between stochastic processes is shown to be crucial: omitting the explicit choice of coupling may lead to conservative results. The theoretical claims in the paper are supported by numerical examples.

In the past few years different techniques have been developed for constructively deriving symbolic abstractions of (stochastic) control systems. The obtained symbolic models allow us to leverage the apparatus of finite-state reactive synthesis towards the problem of designing hybrid controllers enforcing rich logic specifications over the concrete models. Unfortunately, most of the existing techniques severely suffer from the curse of dimensionality due to the need to discretize state and input sets. In this paper we provide a symbolic abstraction technique for incrementally stable stochastic control systems, which only requires discretizing input sets. We show that for every incrementally stable stochastic control system, and for every given positive precision ε, the discretization of exclusively the input set allows constructing a symbolic model which is ε-approximate bisimilar (in moments) to the original stochastic control system. The details of the proposed technique are elucidated by synthesizing a control policy for a 6-dimensional linear stochastic control system satisfying some logic specifications, which would not be tractable using existing approaches based on state-space discretization.

Results on approximate model-checking of Stochastic Hybrid Systems (SHS) against general temporal specifications lead to abstractions that structurally depend on the given specification or with a state cardinality that crucially depends on the size of the specification. In order to cope with the associated issues of generality and scalability, we propose a specification-free abstraction approach that is general, namely it allows constructing a single abstraction to be then used for a whole cohort of problems. It furthermore computationally outperforms specification-dependent abstractions over linear temporal properties, such as bounded LTL (BLTL). The proposed approach unifies techniques for the approximate abstraction of SHS over different classes of properties by explicitly relating the error introduced by the approximation to the distance between transition kernels of abstract and concrete models, and by propagating the error in time over the horizon of the specification. The new technique is compared over a case study to related results in the literature.

This work deals with Markov processes that are defined over an uncountable state space (possibly hybrid) and embedding non-determinism in the shape of a control structure. The contribution looks at the problem of optimization, over the set of allowed controls, of probabilistic specifications defined by automata - in particular, the focus is on deterministic finite-state automata. This problem can be reformulated as an optimization of a probabilistic reachability property over a product process obtained from the model for the specification and the model of the system. Optimizing over automata-based specifications thus leads to maximal or minimal probabilistic reachability properties. For both setups, the contribution shows that these problems can be sufficiently tackled with history-independent Markov policies. This outcome has relevant computational repercussions: in particular, the work develops a discretization procedure leading into standard optimization problems over Markov decision processes. Such procedure is associated with exact error bounds and is experimentally tested on a case study.

This work studies Bellman integral equations arising in infinite-horizon probabilistic verification problems for discrete time homogeneous Markov processes over general state spaces. The problems of interest are expressed via specifications such as probabilistic reachability, invariance, reach-avoid and mean exit time. The contribution shows that the uniqueness of the solutions of the corresponding Bellman equations depends on the presence of absorbing sets within the state space. Furthermore, the work puts forward methods to modify the integral equations to obtain unique solutions for them, techniques to compute such solutions with explicit bounds on the approximation error, and conditions to characterize the possible presence of absorbing sets over the state space.