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

LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to a DFA game. In this paper, we propose a symbolic framework for LTLf synthesis based on this technique, by performing the computation over a representation of the DFA as a boolean formula rather than as an explicit graph. Read More

Computational cognitive modeling investigates human cognition by building detailed computational models for cognitive processes. Adaptive Control of Thought - Rational (ACT-R) is a rule-based cognitive architecture that offers a widely employed framework to build such models. There is a sound and complete embedding of ACT-R in Constraint Handling Rules (CHR). Read More

We develop a coalgebraic generalization of the classical Paige-Tarjan algorithm for efficient bisimilarity checking. Coalgebraic generality implies that our algorithm applies to systems beyond the standard relational setup, in particular various flavours of weighted systems. The specific requirements of the algorithm force rather strong assumptions on the coalgebraic type functors, but by using modularity principles in multi-sorted coalgebra and generalizing our methods beyond the category of sets, we nevertheless arrive at covering not just the known examples (transition systems and Markov chains) but also systems with mixed transition types, such as Segala-style probabilistic automata. Read More

We introduce loose graph simulations (LGS), a new notion about labelled graphs which subsumes in an intuitive and natural way subgraph isomorphism (SGI), regular language pattern matching (RLPM) and graph simulation (GS). Being an unification of all these notions, LGS allows us to express directly also problems which are "mixed" instances of previous ones, and hence which would not fit easily in any of them. After the definition and some examples, we show that the problem of finding loose graph simulations is NP-complete, we provide formal translation of SGI, RLPM, and GS into LGSs, and we give the representation of a problem which extends both SGI and RLPM. Read More

We consider the synthesis of distributed implementations for specifications in parameterized temporal logics such as PROMPT-LTL, which extends LTL by temporal operators equipped with parameters that bound their scope. For single process synthesis it is well-established that such parametric extensions do not increase worst-case complexities. For synchronous distributed systems we show that, despite being more powerful, the realizability problem for PROMPT-LTL is not harder than its LTL counterpart. Read More

We study the properties of the language of Stratified Sets (first-order logic with $\in$ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to $\beta$-conversion. Read More

String diagrams provide a convenient graphical framework which may be used for equational reasoning about morphisms of monoidal categories. However, unlike term rewriting, rewriting string diagrams results in shorter equational proofs, because the string diagrammatic representation allows us to formally establish equalities modulo any rewrite steps which follow from the monoidal structure. Manipulating string diagrams by hand is a time-consuming and error-prone process, especially for large string diagrams. Read More

In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 theorem prover, with some improvements and new theorems. Three deduction systems (Syntactic Calculus, Natural Deduction and Sequent Calculus) of Lambek Calculus are defined with many related theorems proved. The equivalance between these systems are formally proved. Read More

An old formalization of the Process Algebra CCS (no value passing, with explicit relabeling operator) on has been ported from HOL88 theorem prover to HOL4 (Kananaskis-11 and later). Transitions between CCS processes are defined by SOS (Structured Operational Semantics) inference rules, then all algebaric laws (including the expansion theorem) were proved upon SOS transition rules. We have used HOL4's new co-inductive relation support to re-define strong and weak bisimulation equivalances, and shows that the new definitions are equivalent with old ones. Read More

Homomorphisms between relational structures play a central role in finite model theory, constraint satisfaction and database theory. A central theme in quantum computation is to show how quantum resources can be used to gain advantage in information processing tasks. In particular, non-local games have been used to exhibit quantum advantage in boolean constraint satisfaction, and to obtain quantum versions of graph invariants such as the chromatic number. Read More