When are Stochastic Transition Systems Tameable?

A decade ago, Abdulla et al introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Denumerable Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs) are needed. In this paper, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. We first define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and explicit the relationships between them. Then we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. Then we focus on qualitative analysis. Beyond (repeated) reachability properties for which our technics are strongly inspired by [1], we use abstractions to design algorithms for the qualitative model-checking of arbitrary omega-regular properties, when the STS admits a denumerable (sound and complete) abstraction with a finite attractor. We further design generic approximation procedures for quantitative analysis; in addition to extensions of [1] for general STSs, we design approximation algorithms for omega-regular properties (once again by means of specific abstractions). Last we instantiate our framework with stochastic timed automata and generalized semi-Markov processes, two models combining dense-time and probabilities. This allows to derive decidability and approximability results for those models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework. We also derive interesting new approximability results.

Comments: 63 pages

Similar Publications

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. Read More


Weighted labelled transition systems (WLTSs) are an established meta-model aiming to provide general results and tools for a wide range of systems such as non-deterministic, stochastic, and probabilistic systems. In order to encompass processes combining several quantitative aspects, extensions of the WLTS framework have been further proposed, state-to-function transition systems (FuTSs) and uniform labelled transition systems (ULTraSs) being two prominent examples. In this paper we show that this hierarchy of meta-models collapses when studied under the lens of bisimulation-coherent encodings. Read More


This paper positively solves an open problem if it is possible to provide a Hilbert system to Epistemic Logic of Friendship (EFL) by Seligman, Girard and Liu. To find a Hilbert system, we first introduce a sound, complete and cut-free tree (or nested) sequent calculus for EFL, which is an integrated combination of Seligman's sequent calculus for basic hybrid logic and a tree sequent calculus for modal logic. Then we translate a tree sequent into an ordinary formula to specify a Hilbert system of EFL and finally show that our Hilbert system is sound and complete for the intended two-dimensional semantics. Read More


Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for certain stylized, and widely used, multi-view architectures by suitably interpreting and fusing sub-models from different UML diagrams. Read More


This paper presents a symmetric monoidal and compact closed bicategory that categorifies the zx-calculus developed by Coecke and Duncan. The $1$-cells in this bicategory are certain graph morphisms that correspond to the string diagrams of the zx-calculus, while the $2$-cells are rewrite rules. Read More


We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods. Read More


We show that by restricting the degrees of the vertices of a graph to an arbitrary set $ \Delta $, the threshold point $ \alpha(\Delta) $ of the phase transition for a random graph with $ n $ vertices and $ m = \alpha(\Delta) n $ edges can be either accelerated (e.g., $ \alpha(\Delta) \approx 0. Read More


Markov automata combine non-determinism, probabilistic branching, and exponentially distributed delays. This compositional variant of continuous-time Markov decision processes is used in reliability engineering, performance evaluation and stochastic scheduling. Their verification so far focused on single objectives such as (timed) reachability, and expected costs. Read More


We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdzi\'nski et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwi\'nski, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). Read More


In this extended abstract we present the GUBS Upper Bound Solver. GUBS is a dedicated constraint solver over the naturals for inequalities formed over uninterpreted function symbols and standard arithmetic operations. GUBS now forms the backbone of HoSA, a tool for analysing space and time complexity of higher-order functional programs automatically. Read More