Линейно ограниченный автомат
| Определение: | 
| Линейно ограниченный автомат (англ. linear bounded automata, lba) — недетерминированная одноленточная машина Тьюринга, которая никогда не покидает те ячейки, на которых размещен ее ввод. | 
Более формально:
| Определение: | 
| Линейно ограниченный автомат — формальная система , в которой 
 | 
Из определения следует, что языком, принимаемым линейно ограниченным автоматом , называется множество 
Связь линейно ограниченных автоматов с контекстно-зависимыми языками
| Теорема: | 
| Если  — контекстно-зависимый язык, то язык  принимается некоторым линейно ограниченным автоматом. | 
| Доказательство: | 
| Пусть — контекстно-зависимая грамматика. Мы построим линейный ограниченный автомат , такой, что язык, принимаемый , есть . Входная лента будет иметь две дорожки. Первая дорожка будет содержать входную строку с концевыми маркерами. Вторая дорожка будет использоваться для работы. На первом шаге помещает символ в крайнюю левую ячейку второй дорожки. Затем автомат входит в порождающую подпрограмму, которая выполняет следующие шаги: 
 | 
| Теорема: | 
| Если язык  принимается линейно ограниченным автоматом, то  — контекстно-зависимый язык. | 
| Доказательство: | 
| Доказательство схоже с доказательством теоремы о формальной грамматике, генерирующая язык, распознаваемый МТ. Для доказательства этой теоремы построим контекстно-зависимую грамматику, которая моделирует линейно ограниченный автомат. Нетерминалы контекстно-зависимой грамматики должны указывать не только первоначальное содержание некоторой ячейки ленты линейно ограниченного автомата, но также и то, является ли эта ячейка смежной с концевым маркером слева или справа. Такие ячейки в обозначении нетерминалов мы будем снабжать маркерами и , обозначающими, что ячейка граничит соответственно с левым, правым или обоими концевыми маркерами. В обозначении нетерминала состояние линейно ограниченного автомата должно также комбинироваться с символом, находящимся под головкой ленты. Контекстно-зависимая грамматика не может иметь отдельных символов для концевых маркеров и состояния линейно ограниченного автомата, потому что эти символы должны были бы заменяться на пустые цепочки, когда строка превращается в терминальную, а -порождения в контекстно-зависимой грамматике запрещены. В грамматике необходимо поддерживать три типа операций: 
 | 
