## On termination and invariance for faulty channel machines

*Patricia Bouyer*, *Nicolas Markey*,
*Joël
Ouaknine*, *Philippe Schnoebelen*, and *James Worrell*
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.

*Formal Aspects of Computing* 24(4-6), 2012. 13 pages.

PDF
© 2012 Springer.

Imprint / Data Protection