# 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

Yoshida demonstrated how to eliminate the bound names coming from the input prefix in the asynchronous pi calculus, but her combinators still depend on the "new" operator to bind names. We modify Yoshida's combinators by replacing "new" and replication with reflective operators to provide the first combinator calculus with no bound names into which the asynchronous pi calculus has a faithful embedding. We also show that multisorted Lawvere theories enriched over graphs suffice to capture the operational semantics of the calculus. Read More

Existing logical models do not fairly represent epistemic situations with fallible justifications, e.g., Russell's Prime Minister example, though such scenarios have long been at the center of epistemic studies. Read More

In process algebras such as ACP, parallel processes are considered to be interleaved in an arbitrary way. In the case of multi-threading as found in contemporary programming languages, parallel processes are actually interleaved according to some interleaving strategy. Interleaving strategies are also known as process-scheduling policies. Read More

**Affiliations:**

^{1}SEECS, NUST, Islamabad, Pakistan,

^{2}SEECS, NUST, Islamabad, Pakistan

Cell injection is a technique in the domain of biological cell micro-manipulation for the delivery of small volumes of samples into the suspended or adherent cells. It has been widely applied in various areas, such as gene injection, in-vitro fertilization (IVF), intracytoplasmic sperm injection (ISCI) and drug development. However, the existing manual and semi-automated cell injection systems require lengthy training and suffer from high probability of contamination and low success rate. Read More

We present a term rewrite system that formally models the Message Authenticator Algorithm (MAA), which was one of the first cryptographic functions for computing a Message Authentication Code and was adopted, between 1987 and 2001, in international standards (ISO 8730 and ISO 8731-2) to ensure the authenticity and integrity of banking transactions. Our term rewrite system is large (13 sorts, 18 constructors, 644 non-constructors, and 684 rewrite rules), confluent, and terminating. Implementations in thirteen different languages have been automatically derived from this model and used to validate 200 official test vectors for the MAA. Read More

**Affiliations:**

^{1}University of the South Pacific,

^{2}University of Twente,

^{3}University of the South Pacific

This paper considers on a network routing protocol known as Better Approach to Mobile Ad hoc Networks (B.A.T. Read More

**Affiliations:**

^{1}Data61, CSIRO,

^{2}Data61, CSIRO

We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an in-built mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming. Read More

**Affiliations:**

^{1}University of the South Pacific,

^{2}University of Twente

The Stream Control Transmission Protocol (SCTP) is a Transport Layer protocol that has been proposed as an alternative to the Transmission Control Protocol (TCP) for the Internet of Things (IoT). SCTP, with its four-way handshake mechanism, claims to protect the Server from a Denial-of-Service (DoS) attack by ensuring the legitimacy of the Client, which has been a known issue pertaining to the three-way handshake of TCP. This paper compares the handshakes of TCP and SCTP to discuss its shortcomings and strengths. Read More

We identify multirole logic as a new form of logic in which conjunction/disjunction is interpreted as an ultrafilter on the power set of some underlying set (of roles) and the notion of negation is generalized to endomorphisms on this underlying set. We formalize both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively, and also present a filter-based interpretation for intuitionism in multirole logic. Among various meta-properties established for MRL and LMRL, we obtain one named multiparty cut-elimination stating that every cut involving one or more sequents (as a generalization of a (binary) cut involving exactly two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen. Read More

We present two fully mechanized proofs of Dilworths and Mirskys theorems in the Coq proof assistant. Dilworths Theorem states that in any finite partially ordered set (poset), the size of a smallest chain cover and a largest antichain are the same. Mirskys Theorem is a dual of Dilworths Theorem. Read More