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

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

Brihaye Thomas , Bruyère Véronique , Raskin Jean-François, "On model-checking timed automata with stopwatch observers" in Information & Computation, 204, Issue 3, 408-433

  • Edition : Academic Press, San Diego (CA)
  • Codes CREF : Théorie des graphes (DI1146), Informatique mathématique (DI1160)
  • Unités de recherche UMONS : Mathématiques effectives (S820), Informatique théorique (S829)
Texte intégral :

Abstract(s) :

(Anglais) In this paper, we study the model-checking problem for weighted timed automata and the weighted CTL logic; we also study the finiteness of bisimulations of weighted timed automata. Weighted timed automata are timed automata extended with costs on both edges and locations. When the costs act as stopwatches, we get stopwatch automata with the restriction that the stopwatches cannot be reset nor tested. The weighted CTL logic is an extension of'TCTL that allows to reset and test the cost variables. Our main results are: (i) the undecidability of the proposed model-checking problem for discrete and dense time in general, (ii) its PSPACE-COMPLETENESS in the discrete case, and its undecidability in the dense case, for a slight restriction of the weighted CTL Logic, (iii) the precise frontier between finite and infinite bisimulations in the dense case for the subclass of stopwatch automata.

Identifiants :
  • DOI : 10.1016/j.ic.2005.12.001