Автомат Бючи

Автомат Бюхи с двумя состояниями: $q_{0}$ и $q_{1}$, первое из которых является начальным состоянием, а второе — принятием. Его входные данные представляют собой бесконечные слова над символами. $\{a,b\}$. В качестве примера он принимает бесконечное слово $(ab)^{\omega }$, где $x^{\omega }$ обозначает бесконечное повторение строки. Он отвергает бесконечное слово $aaab^{\omega }$.

В информатике и теории автоматов детерминированный автомат Бюхи — это теоретическая машина, которая либо принимает, либо отклоняет бесконечные входные данные. Такая машина имеет набор состояний и функцию перехода, определяющую, в какое состояние машина должна перейти из текущего состояния при чтении следующего входного символа. Некоторые штаты являются принимающими штатами, а один штат является начальным. Машина принимает входные данные тогда и только тогда, когда она проходит через состояние принятия бесконечно много раз при чтении входных данных.

, Недетерминированный автомат Бюхи позже называемый просто автоматом Бюхи , имеет функцию перехода, которая может иметь несколько выходов, что приводит к множеству возможных путей для одного и того же входа; он принимает бесконечный ввод тогда и только тогда, когда принимает какой-то возможный путь. Детерминированные и недетерминированные автоматы Бюхи обобщают детерминированные конечные автоматы и недетерминированные конечные автоматы на бесконечные входные данные. Каждый из них является типом ω-автоматов . Автоматы Бюхи распознают ω-регулярные языки , версию регулярных языков с бесконечными словами . Они названы в честь швейцарского математика Юлиуса Рихарда Бючи , который изобрел их в 1962 году.

Автоматы Бюхи часто используются при проверке моделей как теоретико-автоматная версия формулы линейной темпоральной логики .

Формальное определение

Формально детерминированный автомат Бюхи представляет собой набор A = ( Q ,Σ,δ, q0 _, ) , F состоящий из следующих компонентов:

• Q — конечное множество . Элементы Q называются состояниями A ​ .
• конечное множество, алфавитом A. называемое Σ —
• δ: Q Σ → Q — функция, называемая функцией перехода A × .
• q ₀ является элементом Q называемым начальным состоянием A. ,
• F ⊆ Q – условие приемки . A принимает именно те прогоны, в которых хотя бы одно из бесконечно часто встречающихся состояний находится в F .

В ( недетерминированном ) автомате Бюхи функция перехода δ заменяется отношением перехода Δ, которое возвращает набор состояний, а единственное начальное состояние q ₀ заменяется набором I начальных состояний. Обычно термин «автомат Бюхи без квалификатора» относится к недетерминированным автоматам Бюхи.

Более полный формализм см. также в ω-автомате .

Свойства замыкания

Множество автоматов Бюхи замыкается при следующих операциях.

Позволять $\scriptstyle A=(Q_{A},\Sigma ,\Delta _{A},I_{A},{F}_{A})$ и $\scriptstyle B=(Q_{B},\Sigma ,\Delta _{B},I_{B},{F}_{B})$ быть автоматами Бюхи и $\scriptstyle C=(Q_{C},\Sigma ,\Delta _{C},I_{C},{F}_{C})$ быть конечным автоматом .

• Союз : Существует автомат Бючи, который распознает язык. $\scriptstyle L(A)\cup L(B).$

Доказательство: если мы предположим, что wlog , $\scriptstyle Q_{A}\cap Q_{B}$ тогда пусто $\scriptstyle L(A)\cup L(B)$ распознается автоматом Бюхи $\scriptstyle (Q_{A}\cup Q_{B},\Sigma ,\Delta _{A}\cup \Delta _{B},I_{A}\cup I_{B},{F}_{A}\cup {F}_{B}).$

• Пересечение : существует автомат Бюхи, который распознает язык. $\scriptstyle L(A)\cap L(B).$

Доказательство: автомат Бюхи. $\scriptstyle A'=(Q',\Sigma ,\Delta ',I',F')$ признает $\scriptstyle L(A)\cap L(B),$ где

• $\scriptstyle Q'=Q_{A}\times Q_{B}\times \{1,2\}$
• $\scriptstyle \Delta '=\Delta _{1}\cup \Delta _{2}$
  • $\scriptstyle \Delta _{1}=\{((q_{A},q_{B},1),a,(q'_{A},q'_{B},i))|(q_{A},a,q'_{A})\in \Delta _{A}{\text{ and }}(q_{B},a,q'_{B})\in \Delta _{B}{\text{ and if }}q_{A}\in F_{A}{\text{ then }}i=2{\text{ else }}i=1\}$
  • $\scriptstyle \Delta _{2}=\{((q_{A},q_{B},2),a,(q'_{A},q'_{B},i))|(q_{A},a,q'_{A})\in \Delta _{A}{\text{ and }}(q_{B},a,q'_{B})\in \Delta _{B}{\text{ and if }}q_{B}\in F_{B}{\text{ then }}i=1{\text{ else }}i=2\}$
• $\scriptstyle I'=I_{A}\times I_{B}\times \{1\}$
• $\scriptstyle F'=\{(q_{A},q_{B},2)|q_{B}\in F_{B}\}$

По конструкции, $\scriptstyle r'=(q_{A}^{0},q_{B}^{0},i^{0}),(q_{A}^{1},q_{B}^{1},i^{1}),\dots$ является запуском автомата A' по входному слову w, если $\scriptstyle r_{A}=q_{A}^{0},q_{A}^{1},\dots$ является запуском A на w и $\scriptstyle r_{B}=q_{B}^{0},q_{B}^{1},\dots$ это запуск B на w . $\scriptstyle r_{A}$ принимает и $\scriptstyle r_{B}$ является приемлемым, если r' представляет собой объединение бесконечной серии конечных сегментов 1-состояний (состояний с третьим компонентом 1) и 2-состояний (состояний с третьим компонентом 2) попеременно. Существует такая серия отрезков г', если г' принимается А'.

• Конкатенация : существует автомат Бюхи, который распознает язык. $\scriptstyle L(C)\cdot L(A).$

Доказательство: если мы предположим, что wlog , $\scriptstyle Q_{C}\cap Q_{A}$ пусто, то автомат Бюхи $\scriptstyle A'=(Q_{C}\cup Q_{A},\Sigma ,\Delta ',I',F_{A})$ признает $\scriptstyle L(C)\cdot L(A)$, где

• $\scriptstyle \Delta '=\Delta _{A}\cup \Delta _{C}\cup \{(q,a,q')|q'\in I_{A}{\text{ and }}\exists f\in F_{C}.(q,a,f)\in \Delta _{C}\}$
• $\scriptstyle {\text{ if }}I_{C}\cap F_{C}{\text{ is empty then }}I'=I_{C}{\text{ otherwise }}I'=I_{C}\cup I_{A}$

• ω-замыкание : если $\scriptstyle L(C)$ не содержит пустого слова, то существует автомат Бюхи, распознающий язык $\scriptstyle L(C)^{\omega }.$

Доказательство: автомат Бюхи, распознающий $\scriptstyle L(C)^{\omega }$ строится в два этапа. Сначала построим конечный автомат А' такой, что А' также распознает $\scriptstyle L(C)$ но входящих переходов в начальные состояния А' нет. Так, $\scriptstyle A'=(Q_{C}\cup \{q_{\text{new}}\},\Sigma ,\Delta ',\{q_{\text{new}}\},F_{C}),$ где $\scriptstyle \Delta '=\Delta _{C}\cup \{(q_{\text{new}},a,q')|\exists q\in I_{C}.(q,a,q')\in \Delta _{C}\}.$ Обратите внимание, что $\scriptstyle L(C)=L(A')$ потому что $\scriptstyle L(C)$ не содержит пустой строки. Во-вторых, мы построим автомат Бюхи А", распознающий $\scriptstyle L(C)^{\omega }$ путем добавления цикла возврата в исходное состояние A'. Так, $\scriptstyle A''=(Q_{C}\cup \{q_{\text{new}}\},\Sigma ,\Delta '',\{q_{\text{new}}\},\{q_{\text{new}}\})$, где $\scriptstyle \Delta ''=\Delta '\cup \{(q,a,q_{\text{new}})|\exists q'\in F_{C}.(q,a,q')\in \Delta '\}.$

• Дополнение : существует автомат Бюхи, распознающий язык. $\scriptstyle \Sigma ^{\omega }/L(A).$

Доказательство: Доказательство представлено здесь .

Узнаваемые языки

Автоматы Бюхи распознают ω-регулярные языки . Используя определение ω-регулярного языка и приведенные выше свойства замыкания автоматов Бюхи, можно легко показать, что автомат Бюхи можно построить так, чтобы он распознавал любой заданный ω-регулярный язык. Обратное см. построение ω-регулярного языка для автомата Бюхи.

Детерминированные и недетерминированные автоматы Бюхи

Недетерминированный автомат Бюхи, распознающий ⁠ $(0\cup 1)^{*}0^{\omega }$⁠

Класса детерминированных автоматов Бюхи недостаточно, чтобы охватить все омега-регулярные языки. В частности, не существует детерминированного автомата Бюхи, распознающего язык ⁠ $(0\cup 1)^{*}0^{\omega }$⁠ , который содержит ровно слова, в которых 1 встречается только конечное число раз. Мы можем продемонстрировать от противного, что такого детерминированного автомата Бюхи не существует. Предположим, что A — детерминированный автомат Бюхи, распознающий ⁠ $(0\cup 1)^{*}0^{\omega }$⁠ с набором конечных состояний F . А принимает ⁠ $0^{\omega }$⁠ . Итак, A посетит какое-то состояние в F после прочтения некоторого конечного префикса ⁠. $0^{\omega }$⁠ , скажем после ⁠ $i_{0}$⁠- я буква. A также принимает ω-слово $0^{i_{0}}10^{\omega }.$ Следовательно, для некоторых ⁠ $i_{1}$⁠ , после префикса $0^{i_{0}}10^{i_{1}}$ автомат посетит некоторое состояние в F . Продолжая эту конструкцию, ω-слово $0^{i_{0}}10^{i_{1}}10^{i_{2}}\dots$ генерируется, что заставляет A бесконечно часто посещать какое-то состояние в F , а слова нет в ⁠ $(0\cup 1)^{*}0^{\omega }.$⁠ Противоречие.

Класс языков, распознаваемых детерминированными автоматами Бюхи, характеризуется следующей леммой.

Лемма: ω-язык распознаётся детерминированным автоматом Бюхи, если он является предельным языком некоторого регулярного языка .

Доказательство: любой детерминированный автомат Бюхи A можно рассматривать как детерминированный конечный автомат A' , и наоборот, поскольку оба типа автоматов определяются как набор из пяти одних и тех же компонентов, различается только интерпретация условия приемки. Мы это покажем ⁠ $L(A)$⁠ — предельный язык ⁠ $L(A')$⁠ . ω-слово принимается A , если оно заставит A бесконечно часто посещать конечные состояния. будет принимать бесконечное число конечных префиксов этого ω-слова Таким образом, A' . Следовательно, ⁠ $L(A)$⁠ — предельный язык ⁠ $L(A')$⁠ .

Алгоритмы

Проверка модели конечных систем часто может быть переведена в различные операции над автоматами Бюхи. Помимо операций закрытия, представленных выше, Ниже приведены некоторые полезные операции для применения автоматов Бюхи.

Определение

Поскольку детерминированные автоматы Бюхи строго менее выразительны, чем недетерминированные автоматы, не может быть алгоритма детерминизации автоматов Бюхи. Но теорема Макнотона и конструкция Сафры предоставляют алгоритмы, которые могут преобразовать автомат Бюхи в детерминированный автомат Мюллера или детерминированный автомат Рабина .

Проверка пустоты

Язык, распознаваемый автоматом Бюхи, непуст тогда и только тогда, когда существует конечное состояние, которое одновременно достижимо из начального состояния и лежит в цикле.

Эффективный алгоритм проверки пустоты автомата Бюхи:

1. Рассмотрим автомат как ориентированный граф и разложим его на сильно связные компоненты (СКС).
2. Запустите поиск (например, поиск в глубину ), чтобы определить, какие SCC достижимы из исходного состояния.
3. Проверьте, существует ли нетривиальный SCC, достижимый и содержащий конечное состояние.

Каждый из шагов этого алгоритма может быть выполнен за время, линейное по размеру автомата, поэтому алгоритм явно оптимален.

Минимизация

Минимизация детерминированных автоматов Бюхи (т. е. при наличии детерминированного автомата Бюхи поиск детерминированного автомата Бюхи, распознающего тот же язык с минимальным числом состояний) является NP-полной задачей. В этом отличие от минимизации DFA , которую можно выполнить за полиномиальное время.

Варианты

• Автомат Ко-Бюхи
• Слабый автомат Бюхи
• Полудетерминированный автомат Бюхи
• Обобщенный автомат Бюхи

Переход от других моделей описания к недетерминированным автоматам Бюхи

Из обобщенных автоматов Бюхи (GBA).

Несколько наборов состояний в условии приемки можно перевести в один набор состояний с помощью автоматной конструкции, известной как «счетная конструкция». Допустим, A = (Q,Σ,∆,q ₀ ,{F ₁ ,...,F _n }) — GBA, где F ₁ ,...,F _n — множества принимающих состояний, тогда эквивалентный автомат Бюхи есть A' = (Q', Σ, ∆',q' ₀ ,F'), где

• Q' = Q × {1,...,n}
• q' ₀ знак равно ( q ₀ ,1 )
• ∆' знак равно { ( (q,i), a, (q',j) ) | (q,a,q') ∈ ∆, и если q ∈ F _i, то j=((i+1) mod n) else j=i }
• Ф'=Ф ₁ × {1}

Из линейной темпоральной логики формулы

дан перевод формулы линейной темпоральной логики в обобщенный автомат Бюхи Здесь . А перевод от обобщенного автомата Бюхи к автомату Бюхи представлен выше.

Из автоматов Мюллера

Данный автомат Мюллера можно преобразовать в эквивалентный автомат Бюхи с помощью следующей конструкции автомата. Предположим, что A = (Q,Σ,∆,Q ₀ ,{F ₀ ,...,F _n }) — автомат Мюллера, где F ₀ ,...,F _n — множества принимающих состояний. Эквивалентным автоматом Бюхи является A' = (Q', Σ, ∆',Q ₀ ,F'), где

• Q' = Q ∪ ∪ ^н _{я = 0} {я} × F _я × 2 ^{Ф _я}
• ∆'= ∆ ∪ ∆ ₁ ∪ ∆ ₂ , где
  • ∆ ₁ = { ( q, a, (i,q',∅) ) | (q, a, q') ∈ ∆ и q' ∈ F _i }
  • ∆ ₂ = { ( (i,q,R), a, (i,q',R') ) | (q,a,q')ε∆ и q,q' ∈ F _i, и если R=F _i, то R'= ∅, иначе R'=R∪{q} }
• F'= ∪ ^н _{я = 0} {я} × F _я × {F _я }

A' сохраняет исходный набор состояний из A и добавляет к ним дополнительные состояния. Автомат Бюхи A' моделирует автомат Мюллера A следующим образом: в начале входного слова выполнение A' следует за выполнением A , поскольку начальные состояния одинаковы и ∆' содержит ∆. В некоторой недетерминированно выбранной позиции во входном слове A' решает перейти во вновь добавленные состояния посредством перехода в ∆ ₁ . Затем переходы в ∆ ₂ пытаются посетить все состояния Fi _и продолжать расти R . Как только R становится равным F _i , оно сбрасывается в пустое множество, и ∆ ₂ пытается снова и снова посетить все состояния состояний F _i . Итак, если состояния R = F _i посещаются бесконечно часто, то A' тоже принимает соответствующие входные данные, и A . Эта конструкция близко следует первой части доказательства теоремы Макнотона .

Из структур Крипке

Пусть данная структура Крипке определяется формулой M = ⟨ Q , I , R , L , AP ⟩ , где Q — множество состояний, I — множество начальных состояний, R — отношение между двумя состояниями, также интерпретируемое как ребро, L — это метка состояния, а AP — это набор атомарных предложений, которые L. образуют

Автомат Бюхи будет иметь следующие характеристики:

$Q_{\text{final}}=Q\cup \{{\text{init}}\}$

$\Sigma =2^{AP}$

$I=\{{\text{init}}\}$

$F=Q\cup \{{\text{init}}\}$

$\delta =q{\overrightarrow {a}}p$ если ( q , p ) принадлежит R и L ( p ) = a

и инициализировать ${\overrightarrow {a}}$ q, если q принадлежит I и L ( q ) знак равно a .

Однако обратите внимание, что существует разница в интерпретации структур Крипке и автоматов Бюхи. В то время как первый явно называет полярность каждой переменной состояния для каждого состояния, второй просто объявляет текущий набор переменных верным или неверным. Это абсолютно ничего не говорит о других переменных, которые могут присутствовать в модели.

Дополнение

В теории автоматов дополнением автомата Бюхи называется задача дополнения автомата Бюхи, т. е. построения другого автомата, распознающего дополнение к ω-регулярному языку, распознаваемое данным автоматом Бюхи. Существование алгоритмов этой конструкции доказывает, что множество ω-регулярных языков замкнуто относительно дополнений.

Эта конструкция особенно сложна по сравнению с конструкциями для других свойств замыкания автоматов Бюхи . Первую конструкцию Бючи представил в 1962 году. Позже были разработаны другие конструкции, обеспечивающие эффективное и оптимальное дополнение.

Строительство Бючи

Бючи ​​представил конструкция двояко экспоненциального дополнения в логической форме. Здесь мы имеем его конструкцию в современных обозначениях, используемых в теории автоматов. Пусть A = ( Q ,Σ,Δ, , _Q0 F ) — автомат Бюхи . Пусть ~ _A — отношение эквивалентности над элементами из Σ ⁺ такой, что для каждого v,w ∈ Σ ⁺ , v ~ _A   w тогда и только тогда, когда для всех p,q ∈ Q , A имеет пробег от p до q по v тогда и только тогда, когда это возможно по w. и более того A имеет путь через F от p к q по v тогда и только тогда, когда это возможно по w . Каждый класс ~ _A определяет отображение f : Q → 2 ^вопрос × 2 ^вопрос следующим образом: для каждого состояния p ∈ Q имеем ( Q ₁ , Q ₂ ) = f ( p ), где Q ₁ знак равно { q ∈ Q | w может переместить автомат A из p к q } и Q ₂ знак равно { q ∈ Q | w может переместить автомат A из p в q через состояние в F }. Заметим Q2 _, ⊆ Q1 _что . Если f — отображение, определяемое таким образом, мы обозначаем (уникальный) класс, определяющий f, через L _f .

Следующие три теоремы дают конструкцию дополнения к A используя классы эквивалентности ~ _A .

Теорема 1: ~ _A имеет конечное число эквивалентных классов, и каждый класс является регулярным языком .
Доказательство: Поскольку существует конечное число f : Q → 2 ^вопрос × 2 ^вопрос отношение С _А имеет конечное число классов эквивалентности. Теперь мы покажем, что L _f — ​​регулярный язык. Для p , q ∈ Q и i ∈ {0,1}, пусть A _{i , p , q} = ( {0,1}× Q , Σ, Δ ₁ ∪Δ ₂ , {(0, p )}, {( i , q )} ) быть недетерминированным конечным автоматом , где Δ ₁ = { ((0, q ₁ ), (0, q ₂ )) | ( q ₁ , q ₂ ) ∈ Δ} ∪ { ((1, q ₁ ), (1, q ₂ )) | ( q ₁ , q ₂ ) ∈ ∆}, и Δ ₂ = { ((0, q ₁ ), (1, q ₂ )) | q ₁ ∈ F ∧ ( q ₁ , q ₂ ) ∈ ∆ }. Пусть Q' ⊆ Q . Пусть α _{p ,Q'} = ∩{ L ( A _{1, p , q} ) | q ∈ Q'}, который представляет собой набор слов, которые могут переместить A из p во все состояния в Q' через некоторое состояние в F . Пусть βp _{, Q'} = ∩{ L ( A0 _{, p , q} ) -L ( A1 _{, p , q} )-{ε} | q ∈ Q'}, который представляет собой набор непустых слов, которые могут переместить A из p во все состояния в Q'. и не имеет пробега, проходящего через какое-либо состояние в F . Пусть γ _{p ,Q'} = ∩{ Σ ⁺ - L ( А _{0, п , q} ) | q ∈ Q'}, который представляет собой набор непустых слов, которые не могут переместить A из p в любой из говорится в Q'. Поскольку регулярные языки замкнуты относительно конечных пересечений и относительных дополнений, любые αp _{, Q'} , βp _{, Q'} и γp _{, Q'} регулярны. По определениям, L ж _знак равно ∩{ α _{п , Q 2} ∩ β _{п , Q 1 - Q 2} ∩ γ _{п , Q - Q 1} | ( Q ₁ , Q ₂ ) = ж ( п ) ∧ р ∈ Q }.

Теорема 2: Для каждого w ∈ Σ ^ой , существуют ~ _{классов} Lf и _что Lg такие _А , ш ∈ L _ж ( L _г ) ^ой .
Доказательство: Мы воспользуемся бесконечной теоремой Рамсея. доказать эту теорему. Пусть w = a ₀ a ₁ ... и w ( i , j ) = a _i ... a _{j -1} . Рассмотрим набор натуральных N. чисел Пусть классы эквивалентности ~ _A — цвета подмножеств N размера 2. Цвета назначаем следующим образом. Для каждого i < j , пусть цвет { i , j } будет классом эквивалентности, в котором встречается w ( i , j ). По бесконечной теореме Рамсея мы можем найти бесконечное множество X ⊆ N так, что каждое подмножество X размера 2 имеет одинаковый цвет. Пусть 0 < я ₀ < я ₁ < я ₂ .... ∈ X . Пусть f — определяющее отображение класса эквивалентности такое, что ш (0, я ₀ ) ∈ L _ж . Пусть g — определяющее отображение класса эквивалентности такое, что для каждого j >0 w ( i _{j -1} , i _j ) ∈ L _g . Тогда w ∈ L _f ( L _g ) ^ой .

Теорема 3. Пусть L _f и L _g — классы эквивалентности. ~ _А . Тогда L _f ( L _g ) ^ой является либо подмножеством L ( A ), либо не пересекается с L ( A ).
Доказательство: Предположим, существует слово w ∈ L ( A ) ∩ L _f ( L _g ) ^ой , в противном случае теорема выполняется тривиально. Пусть r — принимающий прогон A по входному сигналу w . Нам нужно показать, что каждое слово w' ∈ L _f ( L _g ) ^ой также находится в L ( A ), т. е. существует серия r' A по входу w' такая, что состояние в F возникает в r' бесконечно часто. Поскольку w ∈ L _f ( L _g ) ^ой , пусть w ₀ w ₁ w ₂ ... = w такой, что w ₀ ∈ L _f и для каждого i > 0 w _i ∈ L _g . Пусть s _i будет состоянием в r после потребления w ₀ ... w _i . Пусть I — набор индексов такой, что i ∈ I тогда и только тогда, когда беговой сегмент в r от s _i до s _{i +1} содержит состояние из F . Я должен быть бесконечным множеством. Аналогично мы можем разделить слово w'. Пусть w' ₀ w' ₁ w' ₂ ... = w' такой, что w' ₀ ∈ L _f и для каждого i > 0 w' _i ∈ L _g . Построим r' индуктивно следующим образом. Пусть первое состояние r' будет таким же, как r . По определению L _f , мы можем выбрать сегмент пробега в слове w' _0, чтобы достичь s ₀ . По предположению индукции, у нас есть пробег по w' ₀ ...w'i _, который достигает s _i . По определению L _g , мы можем продолжить пробег вдоль отрезка слова w' _{i +1} так, что расширение достигает s _i+1 и посещает состояние в F, если i ∈ I . R', полученный в результате этого процесса, будет иметь бесконечное количество сегментов выполнения. содержащие состояния из F , поскольку I бесконечно. Следовательно, r' — принимающая серия и w' ∈ L ( A ).

По приведенным выше теоремам мы можем представить Σ ^ой - Л ( А ) как конечное объединение ω-регулярных языков вида L _f ( L _g ) ^ой , где L _f и L _g — классы эквивалентности ~ _A . Следовательно, Σ ^ой - L ( A ) — ω-регулярный язык. Мы можем перевести этот язык в автомат Бюхи. Эта конструкция является дважды экспоненциальной по размеру A .

Ссылки

• Бахадыр Хусаинов; Анил Нероде (6 декабря 2012 г.). Теория автоматов и ее приложения . Springer Science & Business Media. ISBN  978-1-4612-0171-7 .
• Томас, Вольфганг (1990). «Автоматы на бесконечных объектах». В Ван Леувене (ред.). Справочник по теоретической информатике . Эльзевир. стр. 133–164.

Внешние ссылки

• «Конечные автоматы на бесконечных входах» (PDF) .
• Варди, Моше Ю. «Теоретико-автоматный подход к линейной темпоральной логике». CiteSeerX   10.1.1.125.8126 .