Skip to Main content Skip to Navigation
Book sections

Guarded Autonomous Transitions Increase Conciseness and Expressiveness of Timed Automata

Abstract : 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.
Complete list of metadata
Contributor : Stefan Haar Connect in order to contact the contributor
Submitted on : Wednesday, February 10, 2021 - 9:25:40 AM
Last modification on : Tuesday, January 4, 2022 - 6:46:29 AM



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⟩



Les métriques sont temporairement indisponibles