Pith. sign in

REVIEW 1 cited by

On flat lossy channel machines

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2007.05269 v1 pith:JAAQRCTT submitted 2020-07-10 cs.LO cs.FL

Philippe Schnoebelen This is my paper · ORCID
classification cs.LOcs.FL
keywords channellossymachinesflatreachabilityactionsacyclicalready
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Verification of Flat FIFO Systems

    cs.CC 2019-08 conditional novelty 8.0 of 10

    Reachability, non-termination, unboundedness and related verification problems are NP-complete for flat FIFO machines, and reachability is NP-complete for flat lossy and flat front-lossy FIFO machines.

Pith tools