Skip to Main content Skip to Navigation

Autonomous Transitions Enhance CSLTA Expressiveness and Conciseness

Abstract : CSLTA is a stochastic temporal logic for continuous-time Markov chains (CTMC) where formulas similarly to those of CTL* are inductively defined by nesting of timed path formulas and state formulas. In particular a timed path formula of CSLTA is specified by a single-clock Deterministic Timed Automaton (DTA). Such a DTA features two kinds of transitions: synchronizing transitions triggered by CTMC transitions and autonomous transitions triggered by time elapsing that change the location of the DTA when the clock reaches a given threshold. It has already been shown that CSLTA strictly includes stochastic logics like CSL and asCSL. An interesting variant of CSLTA consists in equipping transitions rather than locations by boolean formulas. Here we answer the following question: do autonomous transitions and/or boolean guards on transitions enhance expressiveness and/or conciseness of DTAs? We show that this is indeed the case. In establishing our main results we also identify an accurate syntactical characterization of DTAs for which the autonomous transitions do not add expressive power but lead to exponentially more concise DTAs.
Complete list of metadata
Contributor : Serge Haddad Connect in order to contact the contributor
Submitted on : Friday, October 4, 2019 - 5:36:31 PM
Last modification on : Friday, April 30, 2021 - 10:05:17 AM


Files produced by the author(s)


  • HAL Id : hal-02306021, version 1


Susanna Donatelli, Serge Haddad. Autonomous Transitions Enhance CSLTA Expressiveness and Conciseness. [Research Report] Inria Saclay Ile de France; LSV, ENS Cachan, CNRS, INRIA, Université Paris-Saclay, Cachan (France); Universita degli Studi di Torino. 2019. ⟨hal-02306021⟩



Record views


Files downloads