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 metadatas

https://hal.inria.fr/hal-02306021
Contributor : Serge Haddad <>
Submitted on : Friday, October 4, 2019 - 5:36:31 PM
Last modification on : Wednesday, December 4, 2019 - 1:26:02 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02306021, version 1

Citation

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⟩

Share

Metrics

Record views

16

Files downloads

186