Nicolas Markey

Résumé

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.

@article{fac24(4-6)-BMOSW,
  author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Schnoebelen, {\relax Ph}ilippe and
                         Worrell, James},
  title =               {On Termination and Invariance for Faulty Channel
                         Systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Aspects of Computing},
  volume =              {24},
  number =              {4-6},
  pages =               {595-607},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/s00165-012-0234-7},
  abstract =            {A~\emph{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
                         \emph{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.},
}