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é:   
Safety Verification of Communicating One-Counter Machines
du groupe Modélisation et Verification

Date 2012-11-29  11:30-12:30
TitreSafety Verification of Communicating One-Counter Machines 
RésuméIn order to verify protocols that tag messages with integer values, we investigate the decidability of the reachability problem for systems of communicating one-counter machines. These systems consist of local one-counter machines that asynchronously communicate by exchanging the value of their counters via, a priori unbounded, FIFO channels. This model extends communicating finite-state machines (CFSM) by infinite-state local processes and an infinite message alphabet. The main result of the paper is a complete characterization of the communication topologies that have a solvable reachability question. As already CFSM exclude the possibility of automatic verification in presence of mutual communication, we also consider an under-approximative approach to the reachability problem, based on rendezvous synchronization. Joint work with Alexander Heußner and Tristan Le Gall. 
Lieu076 
OrateurGrégoire Sutre 
Emailsutre@labri.fr 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index