On termination and invariance for faulty channel machines

A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper we focus on channel machines with insertion errors , i.e., machines in whose channels messages can spontaneously appear. We consider the invariance problem: does a given insertion channel machine have an infinite computation all of whose configurations satisfy a given predicate? We show that this problem is primitive-recursive if the predicate is closed under message losses. We also give a non-elementary lower bound for the invariance problem under this restriction. Finally, using the previous result, we show that the satisfiability problem for the safety fragment of Metric Temporal Logic is non-elementary.