Safety Verification of Communicating One-Counter Machines

Authors Alexander Heußner, Tristan Le Gall, Grégoire Sutre

Thumbnail PDF


  • Filesize: 0.5 MB
  • 12 pages

Document Identifiers

Author Details

Alexander Heußner
Tristan Le Gall
Grégoire Sutre

Cite AsGet BibTex

Alexander Heußner, Tristan Le Gall, and Grégoire Sutre. Safety Verification of Communicating One-Counter Machines. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 224-235, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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.
  • Counter Machines
  • FIFO Channels
  • Reachability Problem
  • Data Words


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads