DI-UMONS : Dépôt institutionnel de l’université de Mons

Recherche transversale
(titres de publication, de périodique et noms de colloque inclus)
2008-03-01 - Article/Dans un journal avec peer-review - Anglais - 23 page(s)

Bruyère Véronique , Dall'Olio Emmanuel, Raskin Jean-François, "Durations and Parametric Model-Checking in Timed Automata" in ACM Transactions on Computational Logic, 9, 23 pages

  • Edition : Association for Computing Machinery
  • Codes CREF : Théorie des graphes (DI1146), Informatique mathématique (DI1160)
  • Unités de recherche UMONS : Informatique théorique (S829)
Texte intégral :

Abstract(s) :

(Anglais) We consider the problem of model-checking a parametric extension of the logic TCTL over timed automata and establish its decidability. Given a timed automaton, we show that the set of durations of runs starting from a region and ending in another region is definable in Presburger arithmetic (when the time domain is discrete) or in a real arithmetic (when the time domain is dense). Using this logical definition, we show that the parametric model-checking problem for the logic TCTL can be solved algorithmically; the proof of this result is simple. More generally, we are able to effectively characterize the values of the parameters that satisfy the parametric TCTL formula with respect to the given timed automaton.

Identifiants :
  • ISSN : 1529-3785