Evènement pour le groupe Modélisation et Verification


Date 2010-02-04  11:30-12:45
TitreRecurrence and Transience for Probabilistic Automata 
RésuméDans le context des automates de Buchi sur les mots infinis, la condition d'acceptation classique (de Buchi) pour un run est qu'il passe infiniment souvent sur un etat acceptant. Un mot est alors accepté s'il existe un run acceptant pour ce mot. Dans un contexte d'automates probabilistes (PBA), un mot est accepté si la probabilité de l'ensemble des runs pour ce mot qui passent infiniment sur un etat acceptant est strictement positive. Avec cette definition, il devient indecidable de decider si le language d'un PBA est vide ou non. On relaxe la definition d'acceptation d'un run en demandant maintenant que la proportion du temps passé sur un des etats acceptants ne tend pas vers zero. Decider le vide du language devient alors decidable. Nous etudions la complexité du probleme de decision associé (PSPACE complet), et nous etudions les propriétés de cloture de notre nouvelle classe d'automates probabilistes. L'essentiel de l'etude se ramene à l'etude de la notion de recurrence dans le cas des chaines de Markov non-homogenes.  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurMathieu Tracol 
EmailMathieu.Tracol@lri.fr 
UrlLRI 



Aucun document lié à cet événement.

Retour
Retour à l'index