Guarded Autonomous Transitions Increase Conciseness and Expressiveness of Timed Automata - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Chapitre D'ouvrage Année : 2020

Guarded Autonomous Transitions Increase Conciseness and Expressiveness of Timed Automata

Résumé

Timed Automata (TA) are an appropriate model for specifying timed requirements for Continuous Time Markov Chains (CTMC). However in order to keep tractable the model checking of a TA over a CTMC, temporal logics based on TA, like CSL TA , restrict TA to have a single clock and to be deterministic (DTA). Different variants of DTAs have been proposed to address the issue of their expressiveness and conciseness. Here we study the effect of two possible features: (1) autonomous transitions which are triggered by time elapsing in addition to synchronized transitions and (2) transitions guarded by propositional formulas instead of propositional formulas guarding locations. We first show that autonomous guarded transitions increase the expressiveness of DTAs (as already shown for guarded locations). Then we identify a hierarchy of DTAs subclasses all equivalent to DTAs without guarded autonomous transitions and we analyze their respective conciseness. In particular we show that eliminating resets in autonomous transitions implies an exponential blow-up, while eliminating autonomous transitions without reset can be performed in polynomial time if decision diagrams are used. Finally we compare TA with guarded transitions to TA with guarded locations showing that the former model is exponentially more concise than the latter one.
main-guardedTemporarySubmission.pdf (375.45 Ko) Télécharger le fichier

Dates et versions

hal-03136066 , version 1 (10-02-2021)

Identifiants

Citer

Susanna Donatelli, Serge Haddad. Guarded Autonomous Transitions Increase Conciseness and Expressiveness of Timed Automata. FORMATS 2020: Formal Modeling and Analysis of Timed Systems, pp.215 - 230, 2020, ⟨10.1007/978-3-030-57628-8_13⟩. ⟨hal-03136066⟩
40 Consultations
54 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More