Структура КрипкеСтруктура Крипке имеет конечное множество состояний и (непомеченных) переходов между ними, причем каждое состояние помечено множеством истинных в этом состоянии атомарных предикатов.
Структура Крипке M — это пятерка M = (S, S0,R, AP, L) , где:
• S — конечное непустое множество состояний;
• S0 ⊆S — непустое множество начальных состояний;
• R⊆S ×S — тотальное отношение на S , т. е. множество переходов, удовлетворяющее требованию: (∀s∈S )(∃s '∈S )( s, s ')∈R (из любого состояния есть переход);
• AP — конечное множество атомарных предикатов;
• L:S → 2 в степени AP — функция пометок (каждому состоянию отображение L сопоставляет множество истинных в нем атомарных предикатов).
Вычислением структуры Крипке M называется любая бесконечная цепочка σ = q0 q1 q2 q3... , такая, что q0∈S0 и (qi, qi+1) ∈ R.
Формально вычисление структуры Крипке M можно представить как отображение σ :N →S , где N — множество натуральных чисел, т. е. σ(i ) — это некоторое состояние структуры Крипке.
Траекторией структуры Крипке M , индуцированной вычислением σ = q0 q1 q2 q3 ... называется бесконечная цепочка L(σ) = L(q0) L(q1) L(q2) L(q3) ... , т. е. бесконечная цепочка подмножеств атомарных предикатов, истинных в соответствующих состояниях вычисления σ .
Формально, траектория — это отображение натурального ряда в множество 2 в степени AP.
Траектории структуры Крипке иногда называют трассами. Траектории являются последовательностями подмножеств атомарных предикатов — наблюдаемых свойств (событий, соотношений между переменными и т. п.), которые могут выполниться (произойти) в анализируемых системах. Именно эти последовательности являются важными для анализа. Формулы темпоральной логики описывают свойства траекторий.
В структуре Крипке в каждом состоянии указаны атомарные предикаты из конечного множества AP атомарных предикатов, которые истинны (выполняются) в этом состоянии. Каждое такое подмножество атомарных предикатов можно считать символом, помечающим состояние структуры Крипке.
Слова - в теории формальных языков конечные цепочки, построенные над конечным словарем.
ω-слова - бесконечные цепочки называются.
Поэтому траектории структуры Крипке называются также ее ω-словами.
Множество всех ω-слов структуры Крипке M называется
ω-языком, допускаемым M .
Рис. 2.12, а задает структуру Крипке с четырьмя состояниями {s0, s1, s2, s3} , одним начальным состоянием s0 , множеством атомарных предикатов { p, q, r} и функцией пометок L : L(s0) = {p,q} , L( s1) ={q, r} , L( s2) ={r} , L(s3) = { } .
Одно из вычислений структуры Крипке рис. 2.12, а — s0 s3 s1 s2 s2 s3... .
Траекторией структуры Крипке рис. 2.12, а при вычислении s0 s3 s1s2 s2 s3... является следующая цепочка: {p,q} {} {q,r} {r} {r}... .
Вычисления, показанные на рис. 2.12, в индуцируют следующие траектории (ω-слова) — бесконечные цепочки подмножеств множества атомарных предикатов, которые выполняются в последовательно проходимых состояниях:
п1 = {p,q} {q,r} {r} {} ... ;
п2 = {p,q} {q,r} {r} {r}... ;
п3 = {p,q} {} {q,r} {r} {} ... ;
п4 = {p,q} {} {q,r} {r} {r} ... .
В структуре Крипке мы не рассматриваем причины переходов — конкретные внешние события, существенные в модели конечного автомата. Такие события легко могут быть учтены в модели Крипке, но
при верификации нам чаще всего важно проверить, существует ли некорректное поведение системы при любых последовательностях внешних событий, и только когда такое некорректное поведение найдено, мы можем искать и его причину.
Model Checking и структура КрипкеСтандартными шагами доказательства того, что поведение реагирующей системы обладает некоторым свойством, являются следующие:
1. Для верифицируемой системы строится адекватная модель Крипке M, т. е. система переходов с конечным числом состояний. Поведения реальной системы представляются разверткой (деревом вычислений) построенной структуры Крипке.
2. С помощью переменных и параметров верифицируемой системы выражаются интересующие разработчика атомарные предикаты структуры Крипке — логические выражения, которые могут принимать значения "истина" или "ложь" в каждом состоянии системы.
3. Проверяемое свойство выражается формулой ϕ темпоральной логики с использованием атомарных утверждений, темпоральных операторов и кванторов пути.
4. Проверяется истинность утверждения M |= ϕ (т. е. утверждения, что структура Крипке является моделью формулы ϕ ) с помощью полностью автоматизированной процедуры.
Метод верификации, реализующий эти шаги, и называется model checking.