A key aspect of many probabilistic systems such as continuous-time Markov chains is that of time: time passes as the system moves from state to state, and many properties of interest, such as safety properties, are concerned with time, e.g. “the airbag has a probability of 0.99 or greater of being deployed before 0.1 seconds”.

We therefore propose a natural and intuitive way of comparing such probabilistic systems with respect to time by way of a faster-than relation. This relation is trace-based and requires that for any word and time bound, the faster process has a higher probability of producing a trace that begins with that word within the time bound. This means that time is accumulated along the trace, and it allows for the faster process to be slower than the slower process in some states along the trace, as long as the overall trace is faster. Our investigation of the faster-than relation is carried out in the context of semi-Markov processes, where the time behaviour can be governed by probability distributions other than the exponential distribution, since many systems encountered in practice do not have exponential time behaviour.

We investigate the computational complexity of the proposed relation, and show that is a difficult problem. Through a connection to probabilistic automata, we show that the relation in general is undeciable, and that if we restrict to only a single output label, the problem remains as hard as the Positivity problem for linear recurrence sequences, which has remained an open problem in number theory for many decades. Exploiting the connection to probabilistic automata further, we also show that the relation can not even be approximated.

Although the problem is a difficult one, we also obtain some decidability results. If we restrict ourselves to unambiguous processes, where every output label leads to a unique successor state, then the problem becomes decidable in coNP. If we instead restrict the time so that we only want the faster process to be faster up to a given time bound, then we are able to approximate the relation under the assumption that all timing distributions are slow, meaning that they must take some amount of time to fire a transition.

In this work we have investigated the computational complexity of the faster-than relation, but there are many other interesting aspects of the relation that we hope to investigate in future work, such as logical and compositional aspects.

Authors: Mathias Ruggaard Pedersen, NathanaĆ«l Fijalkow, Giorgio Bacci, Kim Guldstrand Larsen, and Radu Mardare.

This extended abstract is based on a paper that has been accepted for LATA 2018, a preprint of which can be found on arXiv here.