Линейная темпоральная логика к автомату Бюхи - Linear temporal logic to Büchi automaton

В формальная проверка, конечное состояние проверка модели нужно найти Büchi автомат (BA) эквивалент данной Линейная временная логика (LTL) формула, т.е. такая, что формула LTL и BA распознают одно и то же ω-язык. Есть алгоритмы, которые переводят формулу LTL в BA.^[1][2][3][4] Это преобразование обычно выполняется в два этапа. Первый шаг производит обобщенный автомат Бюхи (GBA) из формулы LTL. Второй шаг переводит этот GBA в BA, который включает относительно легкая конструкция. Поскольку LTL строго менее выразительно, чем BA, обратное построение невозможно.

Алгоритмы преобразования LTL в GBA различаются стратегиями построения, но все они имеют общий базовый принцип, т.е. каждое состояние в построенном автомате представляет собой набор формул LTL, которые ожидал быть удовлетворенным оставшимся входным словом после появления состояния во время выполнения.

Переход с LTL на GBA

Здесь представлены два алгоритма построения. Первый обеспечивает декларативную и понятную конструкцию. Второй обеспечивает алгоритмическое и эффективное построение. Оба алгоритма предполагают, что входная формула f построена с использованием набора пропозициональных переменных AP и f находится в нормальная форма отрицания.Для каждой формулы LTL f 'без верхнего символа ¬ пусть негр(f ') = ¬f', негр(¬f ') = f'. Для частного случая f '=истинный, позволять негр(истинный) = ложный.

Декларативная конструкция

Прежде чем приступить к описанию конструкции, необходимо дать несколько вспомогательных определений. Для формулы LTL ж, Позволять cl(f) наименьший набор формул, удовлетворяющий следующим условиям:

истинный ∈ cl(е) f ∈ cl(е) если f1 ∈ cl(е) тогда негр(f1) ∈ cl(е) если Икс ж1 ∈ cl(f) затем f1 ∈ cl(е)

если f1 ∧ f2 ∈ cl(f) затем f1, f2 ∈ cl(е) если f1 ∨ f2 ∈ cl(f) затем f1, f2 ∈ cl(е) если f1 U ж2 ∈ cl(f) затем f1, f2 ∈ cl(е) если f1 р ж2 ∈ cl(f) затем f1, f2 ∈ cl(е)

cl(f) является замыканием подформул f при отрицании. Отметим, что cl(f) могут содержать формулы, которые не находятся в нормальной форме отрицания. cl(f) будут служить состояниями эквивалентного GBA. Мы стремимся построить GBA так, чтобы если состояние соответствует на подмножество M ⊂ cl(f) тогда GBA выполняет приемный прогон, начиная с состояния для слова, если и только если слово удовлетворяет каждой формуле в M и нарушает каждую формулу в cl(f) / M. По этой причине мы не будем рассматривать каждое множество формул M, которое явно несовместимо или входит в строго супермножество M ', такое что M и M' эквивалентны. Множество M ⊂ cl(f) является максимально последовательный если он удовлетворяет следующим условиям:

истинный ∈ M ж1 ∈ M тогда и только тогда, когда ¬f1 ∉ M

ж1 ∧ f2 ∈ M тогда и только тогда, когда f1 ∈ M и f2 ∈ M ж1 ∨ f2 ∈ M тогда и только тогда, когда f1 ∈ M или f2 ∈ M

Позволять cs(f) множество максимально согласованных подмножеств cl(f). Мы будем использовать только cs(f) как состояния GBA.

Строительство GBA

Эквивалент GBA к f это А= ({init} ∪cs(е), 2^AP, Δ, {инициализация},F), куда

• Δ = Δ₁ ∪ Δ₂
  • (M, a, M ') ∈ Δ₁ если и только если (M '∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M '} и:
    • Икс ж₁ ∈ M тогда и только тогда, когда f₁ ∈ M ';
    • ж₁ U ж₂ ∈ M тогда и только тогда, когда f₂ ∈ M или (f₁ ∈ M и f₁ U ж₂ ∈ M ');
    • ж₁ р ж₂ ∈ M тогда и только тогда, когда f₁ ∧ f₂ ∈ M или (f₂ ∈ M и f₁ р ж₂ ∈ M ')
  • Δ₂ = {(init, a, M ') | (M '∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M '} и f ∈ M'}
• Для каждого f₁ U ж₂ ∈ cl(f), {M ∈ cs(е) | ж₂ ∈ M или ¬ (f₁ U ж₂) ∈ M} ∈ F

Три условия в определении Δ₁ гарантировать, что любой запуск А не нарушает семантику временных операторов. Обратите внимание, что F - набор наборов состояний. F определены для захвата свойства оператора U что не может быть проверено путем сравнения двух последовательных состояний в серии, т. е. если f₁ U ж₂ верно в каком-то состоянии, то в конечном итоге f₂ верно в каком-то состоянии позже.

Доказательство правильности приведенной выше конструкции

Пусть ω-слово ш= а₁, а₂, ... по алфавиту 2^AP. Позволять ш^я = а_я, а_{я + 1}, ... .Пусть M_ш = {f '∈ cl(е) | ш ${\displaystyle \vDash }$ f '}, который мы называем удовлетворение set. В соответствии с определением cs(е), М_ш ∈ cs(f). Можно определить последовательность ρ_ш = init, M_ш¹, М_ш², .... Благодаря определению А, если w ${\displaystyle \vDash }$ f, то ρ_ш должен быть приемлемый пробег А над ш.

И наоборот, допустим А принимает ш.Пусть ρ = init, M₁, М₂, ... быть бегом А над шСледующая теорема завершает оставшееся доказательство корректности.

Теорема 1: Для всех i> 0 M_ш^я = M_я.

Доказательство: Доказательство проводится индукцией по структуре f '∈ cl(е).

• Базовые случаи:
  • f '= истинный. По определениям f '∈ M_ш^я и f '∈ M_я.
  • f '= p. По определению А, p ∈ M_я тогда и только тогда, когда p ∈ a_я тогда и только тогда, когда p ∈ M_ш^я.
• Шаги индукции:
  • f '= f₁ ∧ f₂. Согласно определению согласованных множеств, f₁ ∧ f₂ ∈ M_я если и только тогда₁ ∈ M_я и е₂ ∈ M_я. По предположению индукции f₁ ∈ M_ш^я и е₂ ∈ M_ш^я. В силу определения удовлетворяющего множества f₁ ∧ f₂ ∈ M_ш^я.
  • f '= ¬f₁, f '= f₁ ∨ f₂, f '= Икс ж₁ или f '= f₁ р ж₂. Доказательства очень похожи на предыдущее.
  • f '= f₁ U ж₂. Доказательство равенства разделено на два доказательства вывода.
    • Если f₁ U ж₂ ∈ M_я, то f₁ U ж₂ ∈ M_ш^я. По определению переходов А, возможны следующие два случая.
      • ж₂ ∈ M_я. По предположению индукции f₂ ∈ M_ш^я. Итак, f₁ U ж₂ ∈ M_ш^я.
      • ж₁ ∈ M_я и е₁ U ж₂ ∈ M_{я + 1}. И в связи с условием приемки А, существует хотя бы один индекс j ≥ i такой, что f₂ ∈ M_j. Пусть j 'наименьший из этих индексов. Докажем результат индукцией по k = {j ', j'-1, ..., i + 1, i}. Если k = j ', то f₂ ∈ M_k, мы применяем те же рассуждения, что и в случае f₂ ∈ M_я. Если i ≤ k 2 ∉ M_k, и так f₁ ∈ M_k и е₁ U ж₂ ∈ M_{к + 1}. По предположению индукции относительно f 'имеем f₁ ∈ M_ш^k. В силу предположения индукции об индексах также имеем f₁ U ж₂ ∈ M_{ш^{к + 1}}. В силу определения семантики LTL, f₁ U ж₂ ∈ M_ш^k.
    • Если f₁ U ж₂ ∈ M_ш^я, то f₁ U ж₂ ∈ M_я. Из-за семантики LTL мы можем иметь следующие два случая.
      • ж₂ ∈ M_ш^я. По предположению индукции f₂ ∈ M_я. Итак, f₁ U ж₂ ∈ M_я.
      • ж₁ ∈ M_ш^я и е₁ U ж₂ ∈ M_{ш^{я + 1}}. В силу семантики LTL существует хотя бы один индекс j ≥ i такой, что f₂ ∈ M_j. Пусть j 'наименьший из этих индексов. Действуйте, как при доказательстве обратного следствия.

По приведенной теореме M_ш¹ = M₁. Благодаря определению переходов А, f ∈ M₁. Следовательно, f ∈ M_ш¹ и ш ${\displaystyle \vDash }$ f.

Gerth et al. алгоритм

Следующий алгоритм принадлежит Герту, Пеледу, Варди, и Wolper.^[3] Также доступен проверенный конструктивный механизм от Schimpf, Merz и Smaus.^[5] Предыдущая конструкция заранее создает экспоненциально много состояний, и многие из этих состояний могут быть недоступны. Следующий алгоритм избегает этой предварительной конструкции и состоит из двух этапов. На первом этапе он постепенно создает ориентированный граф. На втором этапе он строит помеченный обобщенный автомат Бюхи (LGBA), определяя узлы графа как состояния и направленные ребра как переходы. Этот алгоритм учитывает достижимость и может производить меньший автомат, но сложность наихудшего случая остается той же.

Узлы графа помечены наборами формул и получаются путем декомпозиции формул в соответствии с их булевой структурой и путем расширения временных операторов, чтобы отделить то, что должно быть истинным немедленно, от того, что должно быть истинным, начиная со следующего состояния. . Например, предположим, что формула LTL f₁ U ж₂ появляется в метке узла. f₁ U ж₂ эквивалентно f₂ ∨ (f₁ ∧ Икс(f₁ U ж₂Эквивалентное разложение предполагает, что f₁ U ж₂ верно в одном из следующих двух условий.

1. ж₁ выполняется в текущий момент и (f₁ U ж₂) выполняется на следующем временном шаге, или
2. ж₂ удерживается на текущем временном шаге

Два случая могут быть закодированы путем создания двух состояний (узлов) автомата, и автомат может недетерминированно перейти к любому из них. В первом случае мы сняли часть бремени доказательства на следующем временном шаге, поэтому мы также создайте другое состояние (узел), которое будет нести обязательство для следующего временного шага в своей метке.

Также необходимо учитывать темпоральный оператор р что может вызвать такой случай split.f₁ р ж₂ эквивалентно (f₁ ∧ f₂) ∨ (f₂ ∧ Икс(f₁ р ж₂)) и это эквивалентное разложение предполагает, что f₁ р ж₂ верно в одном из следующих двух условий.

1. ж₂ выполняется в текущий момент и (f₁ р ж₂) выполняется на следующем временном шаге, или
2. (f₁ ∧ f₂) выполняется на текущем временном шаге.

Чтобы избежать многих случаев в следующем алгоритме, определим функции curr1, следующий1 и curr2 которые кодируют вышеуказанные эквиваленты в следующей таблице.

ж	curr1 (f)	next1 (f)	curr2 (f)
ж1 U ж2	{f1}	{f1 U ж2 }	{f2}
ж1 р ж2	{f2}	{f1 р ж2 }	{f1, f2}
ж1 ∨ f2	{f2}	∅	{f1}

Мы также добавили регистр дизъюнкции в приведенную выше таблицу, так как он также вызывает разделение регистра в автомате.

Ниже приведены два шага алгоритма.

Шаг 1. create_graph

В следующем окне мы представляем первую часть алгоритма построения ориентированного графа. create_graph - функция входа, которая ожидает входную формулу f в нормальная форма отрицания. Вызывает рекурсивную функцию расширять который строит график, заполняя глобальные переменные Узлы, Входящий, Сейчас же, и Следующий.Набор Узлы хранит набор узлов в графе. Карта Входящий отображает каждый узел Узлы к подмножеству Узлы ∪ {init}, который определяет набор входящих ребер. Входящий узла может также содержать специальный символ init, который используется в конечной конструкции автомата для определения набора начальных состояний.Сейчас же и Следующий сопоставить каждый узел Узлы к набору формул LTL. для узла q Сейчас же(q) обозначает набор формул, которым должна удовлетворять остальная часть входного слова, если автомат в настоящее время находится в узле (состоянии) q.Следующий(q) обозначает набор формул, которым должна удовлетворять остальная часть входного слова, если автомат в настоящее время находится в следующем узле (состоянии) после q.

typedefs     LTL: Формулы LTL LTLSet: Наборы формул LTL NodeSet: Наборы узлов графа ∪ {init} глобалы         Узлы : набор узлов графа: = ∅ Входящий: Узлы → NodeSet := ∅         Сейчас же    : Узлы → LTLSet := ∅         Следующий   : Узлы → LTLSet := ∅        функция create_graph(LTL е) {развернуть ({f}, ∅, ∅, {init}) возвращаться (Узлы, Сейчас же, Входящий)      }

 функция расширять(LTLSet curr, LTLSet Старый, LTLSet следующий, NodeSet входящий) {1: если curr = ∅ тогда 2:    если ∃q ∈ Узлы: Следующий(q) = следующий ∧ Сейчас же(q) = старый тогда 3:       Входящий(q): = Входящий(q) ∪ входящие 4: еще 5: q: = new_node() 6:       Узлы := Узлы ∪ {q} 7: Входящий(q): = входящий 8: Сейчас же(q): = старый 9: Следующий(q): = next10: expand (Следующий(q), ∅, ∅, {q}) 11: еще12: f ∈ curr13: curr: = curr  {f} 14: old: = old ∪ {f} 15: матч ж с16:     | истинный, ложный, p или ¬p, где p ∈ AP  →17:       если f = ложный ∨ негр(f) ∈ old тогда18:          пропускать19:       еще20: развернуть (текущее, старое, следующее, входящее) 21: | ж1 ∧ f2 → 22: развернуть (curr ∪ ({f1, f2}  old), old, next, incoming) 23: | Икс g → 24: expand (curr, old, next ∪ {g}, incoming) 25: | ж1 ∨ f2, f1 U ж2, или f1 р ж2 → 26: развернуть (curr ∪ (curr1(е)  старый), старый, следующий ∪ следующий1(f), входящий) 27: expand (curr ∪ (curr2(е)  старый), старый, следующий, входящий) 28: возвращаться }

Кодекс расширять помечены номерами строк для удобства. расширять стремится добавить узел и его последующие узлы в граф. Параметры вызова описывают потенциальный новый узел.

• Первый параметр curr содержит набор формул, которые еще предстоит расширить.
• Второй параметр Старый содержит набор уже развернутых формул.
• Третий параметр следующий - набор формулы, с помощью которой будет создан узел-преемник.
• Четвертый параметр входящий определяет набор входящих ребер, когда узел добавляется к графу.

В строке 1 если условие проверяет, если curr содержит любую формулу, которую нужно раскрыть. curr пусто, то в строке 2 если condition проверяет, существует ли уже состояние q 'с таким же набором расширенных формул. Если это так, то мы не добавляем избыточный узел, а добавляем параметр входящий в Входящий(q ') в строке 3. В противном случае мы добавляем новый узел q, используя параметры в строках 5–9, и начинаем расширять узел-последователь q, используя следующий(q) в виде нерасширенного набора формул в строке 10.

В случае curr не пусто, тогда у нас есть больше формул для раскрытия и управления переходами со строки 1 на 12. В строках 12–14 формула f из curr выбран и перемещен в Старый. В зависимости от структуры f выполняется остальная часть функции.

• Если f - литерал, то раскрытие продолжается в строке 20, но если Старый уже содержит негр(f) или f =ложный, тогда Старый содержит противоречивую формулу, и мы отбрасываем этот узел, не делая никакой рекурсии в строке 18.
• Если f = f₁ ∧ f₂, то f₁ и е₂ добавлены к curr и делается рекурсивный вызов для дальнейшего расширения в строке 22.
• Если f = Икс ж₁, то f₁ добавлен к следующий для преемника текущего рассматриваемого узла в строке 24.
• Если f = f₁ ∨ f₂, f = f₁ U ж₂, или f = f₁ р ж₂ затем текущий узел делится на два узла, и для каждого узла выполняется рекурсивный вызов.

Для рекурсивных вызовов curr и следующий изменяются с помощью функций curr1, следующий1, и curr2 которые были определены в приведенной выше таблице.

Шаг 2. Конструирование ЛГБА

Позволять (Узлы, Сейчас же, Входящий) = create_graph (f). Эквивалент LGBA f - А=(Узлы, 2^AP, L, Δ, Q₀, F), куда

• L = {(q, a) | q ∈ Узлы и (Сейчас же(д) ∩ AP) ⊆ a ⊆ {p ∈ AP | ¬p ∉ Сейчас же(q)}}
• Δ = {(q, q ') | q, q '∈ Nodes и q ∈ Incoming (q')}
• Q₀ = {q ∈ Nodes | init ∈ Входящий(q)}
• Для каждой подформулы g = g₁ U грамм₂, пусть F_грамм = {q ∈ Nodes | грамм₂ ∈ Сейчас же(q) или g ∉ Сейчас же(q)}, то F = {F_грамм | g ∈ cl(f)}

Обратите внимание, что метки узлов в алгоритмической конструкции не содержат отрицания подформул f. В декларативном построении узел имеет набор формул, которые должны быть истинными. Алгоритмическое построение гарантирует правильность без необходимости присутствия всех истинных формул в метке узла.

Инструменты

• СПОТ LTL2TGBA - Транслятор LTL2TGBA включен в библиотеку проверки объектно-ориентированных моделей SPOT. Доступен онлайн-переводчик.
• LTL2BA - Быстрый переводчик LTL в BA через чередующиеся автоматы. Доступен онлайн-переводчик.
• LTL3BA - Актуальное улучшение LTL2BA.

Рекомендации

1. МОЙ. Варди и П. Вольпер, Рассуждения о бесконечных вычислениях, Информация и вычисления, 115 (1994), 1–37.
2. Ю. Кестен, З. Манна, Х. Макгуайр, А. Пнуели, Алгоритм принятия решений для полной временной логики высказываний, CAV’93, Элунда, Греция, LNCS 697, Springer – Verlag, 97-109.
3. Р. Герт, Д. Пелед, М.Ю. Варди и П. Вольпер, "Простая автоматическая проверка линейной темпоральной логики на лету", Proc. IFIP / WG6.1 Symp. Спецификация протокола, тестирование и проверка (PSTV95), стр. 3-18, Варшава, Польша, Chapman & Hall, июнь 1995 г.
4. П. Гастин и Д. Одду, Быстрый перевод LTL в автомат Бюхи, Тринадцатая конференция по компьютерной проверке (CAV '01), номер 2102 в LNCS, Springer-Verlag (2001), стр. 53–65.
5. А. Шимпф, С. Мерц и Дж. Г. Смаус, "Построение автоматов Bu¨chi для проверки моделей LTL, проверенных в Isabelle / HOL", Proc. Международная конференция по доказательству теорем в логиках высшего порядка (TPHOLs 2009), стр. 424-439, Мюнхен, Германия, Springer, август 2009 г.