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. |