Anzeige
Erschienen in:
2020 | OriginalPaper | Buchkapitel
Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models
verfasst von : Susanna Donatelli, Serge Haddad
Erschienen in: Language and Automata Theory and Applications
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
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\(^{\!\text {TA}}\). A timed path formula of CSL\(^{\!\text {TA}}\) 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\(^{\!\text {TA}}\) 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.