Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Zeno, Hercules and the Hydra
du groupe Modélisation et Verification

Date 2014-10-16  11:00-12:00
TitreZeno, Hercules and the Hydra 
RésuméMetric temporal logic (MTL) is one of the most prominent specification formalisms for real-time systems. Over infinite timed words, full MTL is undecidable, but satisfiability for its safety fragment was proved decidable several years ago. The problem is also known to be equivalent to a fair termination problem for a class of channel machines with insertion errors. However, the complexity has remained elusive, except for a non-elementary lower bound. Via another equivalent problem, namely termination for a class of rational relations, we show that satisfiability for safety MTL is not primitive recursive, yet is Ackermannian, i.e., among the simplest non-primitive recursive problems. This is surprising since decidability was originally established using Higman's Lemma, suggesting a much higher non-multiply recursive complexity. Joint work with Joel Ouaknine and James Worrell.  
Lieu076 
OrateurRanko Lazic 
Emaillazic@dcs.warwick.ac.uk 
UrlUniv. Warwick 



Aucun document lié à cet événement.

Retour
Retour à l'index