文章基本信息

标题：Safety Verification of Communicating One-Counter Machines
本地全文：下载
作者：Alexander Heu{\ss}ner ; Tristan Le Gall ; Gr{\'e}goire Sutre 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2012
卷号：18
页码：224-235
DOI：10.4230/LIPIcs.FSTTCS.2012.224
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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