DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2012.224

Safety Verification of Communicating One-Counter Machines

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

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{heuner_et_al:LIPIcs.FSTTCS.2012.224,
  author =	{Heu{\ss}ner, Alexander and Le Gall, Tristan and Sutre, Gr\'{e}goire},
  title =	{{Safety Verification of Communicating One-Counter Machines}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{224--235},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.224},
  URN =		{urn:nbn:de:0030-drops-38614},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.224},
  annote =	{Keywords: Counter Machines, FIFO Channels, Reachability Problem, Data Words}
}

Search Results

Documents authored by Le Gall, Tristan

Safety Verification of Communicating One-Counter Machines

Abstract

Cite as

Thanks for your feedback!

Could not send message