This paper introduces a class of graphs associated to linear bounded machines. It is shown that this class is closed, up to observational equivalence, under synchronized product. The first-order theory of these graphs is investegated and shown to be undecidable. The latter result extends to any logic in which the existence of sinks may be stated.