Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models

Timed Automata are a well-known formalism for specifying timed behaviours. In this paper we are concerned with Timed Automata for the specification of timed behaviour of Continuous Time Markov Chains (CTMC), as used in the stochastic temporal logic CSL[Formula: see text]. A timed path formula of CSL[Formula: see text] is specified by a Deterministic Timed Automaton (DTA) that features two kinds of transitions: synchronizing transitions (triggered by CTMC transitions) and autonomous transitions (triggered when a clock reaches a given threshold). Other definitions of CSL[Formula: see text] are based on DTAs that do not include autonomous transitions. This raises the natural question: do autonomous transitions enhance expressiveness and/or conciseness of DTAs? We prove that this is the case and we provide a syntactical characterization of DTAs for which autonomous transitions do not add expressive power, but allow one to define exponentially more concise DTAs.