Trace Expressiveness of Timed and Probabilistic Automata

TL;DR

This paper introduces a new measure called trace expressiveness to compare the modeling capabilities of timed, probabilistic, stochastic timed automata, and a new model of timed automata with polynomial delay.

Contribution

It presents a novel measure of automata expressiveness and characterizes the relative expressiveness of various automata models, including a new timed automata variant.

Findings

Trace expressiveness effectively compares automata models.

Timed automata with polynomial delay offer unique expressiveness features.

The relative expressiveness of models is formally characterized.

Abstract

Automata expressiveness is an essential feature in understanding which of the formalisms available should be chosen for modelling a particular problem. Probabilistic and stochastic automata are suitable for modelling systems exhibiting probabilistic behavior and their expressiveness has been studied relative to non-probabilistic transition systems and Markov chains. In this paper, we consider previous formalisms of Timed, Probabilistic and Stochastic Timed Automata, we present our new model of Timed Automata with Polynomial Delay, we introduce a measure of expressiveness for automata we call trace expressiveness and we characterize the expressiveness of these models relative to each other under this new measure.