文章基本信息

标题：On Flat Lossy Channel Machines
本地全文：下载
作者：Philippe Schnoebelen
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：183
页码：37:1-37:22
DOI：10.4230/LIPIcs.CSL.2021.37
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We show that reachability, repeated reachability, nontermination and unboundedness are NP-complete for Lossy Channel Machines that are flat, i.e., with no nested cycles in the control graph. The upper complexity bound relies on a fine analysis of iterations of lossy channel actions and uses compressed word techniques for efficiently reasoning with paths of exponential lengths. The lower bounds already apply to acyclic or single-path machines.
关键词：Infinite state systems; Automated verification; Flat systems; Lossy channels