У нас есть несколько определений и обозначений, давайте сначала рассмотрим go:
Нам дан набор атомов c предложений AP. Здесь не сказано явно, но обычно это означает, что мы заинтересованы в языках, которые имеют в качестве алфавита набор мощностей AP. Таким образом, для AP = {a, b, c} наш алфавит будет Sigma = {{}, {a}, {b}, {c}, {a, b}, {a, c}, {b, c }, {a, b, c}}.
Как вы можете видеть, написание этого алфавита набора мощности может быть большой работой. По этой причине существует альтернативное обозначение, основанное на формулах высказываний. Рассмотрим пропозициональную формулу phi над переменными AP. Мы можем взять символ x из Sigma и установить в phi все предложения атоми c, содержащиеся в x, в true, а все остальные предложения атоми c в false. Затем мы оцениваем фи, и оно становится истинным или ложным. Мы можем понимать фи, чтобы ссылаться на все те x из Sigma, для которых фи оценивается как истинное.
Например, формула phi = "a, а не b" относится к символам {a} и {a, c }. Формула phi = "a" относится к символам {a}, {a, b}, {a, c}, {a, b, c}. Формула phi = "not a" относится к символам {}, {b}, {c}, {b, c}. Формула phi = "не а и не б и не c" относится только к символу {}. Формула phi = "true" относится ко всем символам из сигмы. Формула phi = "false" относится к отсутствию символа (не путать с символом {}). И так далее ...
Эта логика c - это обозначение, используемое на ребрах NFA в вашем примере.
Мы называем язык L над конечными словами " обычный «если есть NFA, который принимает L.
Мы называем язык L над бесконечными трассами« свойством безопасности », если каждая трасса, не входящая в L, имеет плохой префикс, означающий конечную префикс w, такой, что в L. нет бесконечного продолжения w.
Мы называем свойство безопасности "регулярным", если язык его плохих префиксов является регулярным. Обратите внимание, что здесь мы имеем дело с двумя различными понятиями «обычного», одно для языков конечных слов и одно для свойств безопасности по бесконечным следам.
Общий подход
Вы имеем дело с проблемой перехода от неформального описания свойства безопасности к формальному описанию языка его плохих префиксов. Не существует общего правила, как это сделать, но помните, что на интуитивном уровне свойство безопасности означает «какое-то плохое событие никогда не случится». Язык плохих префиксов - это как раз те конечные слова, для которых «плохое событие происходит в какой-то момент». Поэтому ваш подход заключается в том, чтобы проанализировать, что такое «плохое событие».
(Конечно, это общая проблема при проверке модели, когда при переходе от неформальных описаний к формальной модели существует риск не совсем улавливания исходное описание.)
Рассмотрим P1: плохое событие: «a становится действительным, а после b действует только конечное число шагов и становится ложным до того, как c становится истинным». Мы можем превратить это в несколько более подробное описание: «a становится действительным, после этого мы видим некоторые b, но не c, и затем мы не видим b и нет c». Мы можем использовать это описание, чтобы получить формальное определение «плохое событие происходит в какой-то момент». Я лично нахожу регулярные выражения более интуитивно понятными, чем NFA, поэтому я сначала попытался бы создать регулярное выражение, а затем построить NFA из этого:
(true)* a (b and not c)* (not b and not c) (true)*
Это регулярное выражение описывает все конечные слова, где в какой-то момент случается плохое событие Мы используем (true) * в начале и в конце, потому что нам все равно, что произойдет до или после плохого события. Регулярное выражение уже очень близко к NFA в вашем примере, в общем, должно быть легко построить NFA из таких регулярных выражений. Вы можете видеть, что обозначения, основанные на формулах высказываний, делают это намного более компактным по сравнению с явным написанием символов, например, написание «a» короче, чем написание полного регулярного выражения ({a} + {a, b} + {a, c} + {a, b, c}).
Это не единственное решение, вместо того, чтобы требовать видеть (b и не c) * перед просмотром (не b и не c), достаточно также потребовать увидеть (не c) * до просмотра (не б и не c). Это привело бы к регулярному выражению:
(true)* a (not c)* (not b and not c) (true)*
Единственное отличие первого решения состоит в том, что вместо того, чтобы требовать совпадения с первым (не b и не c), которое мы видим, мы могли бы также пропустить по некоторым (не b и не c), потому что они также совпадают (не c), если мы в конечном итоге сопоставим a (не b и не c). Таким образом, в некотором смысле первое решение является лучшим, потому что результирующий NFA является более детерминированным c.
Рассмотрим P2: плохое событие будет иметь два a, таких, что между ними в некоторой точке b не выполняется , Превратив это в немного более подробное описание, мы получили бы «мы видим a, после чего мы видим некоторые b, не видя a, затем мы достигаем точки, где мы не видим ни b, ни a, после чего мы видим любые символы, пока не достигнем закрытия a ». Превращение этого в регулярное выражение для «плохое событие происходит в какой-то момент» дает нам:
(true)* a (b and not a)* (not b and not a) (true)* a (true)*
Опять же, это очень похоже на NFA в вашем примере, должно быть легко увидеть, как построить Нфа от такого выражения. Как и раньше, мы могли бы также получить альтернативное решение, уменьшив (b и не a) * до (не a) *, единственное отличие состояло бы в том, что это позволило бы пропускать некоторые (не b и не a), пока как мы сопоставим один в конце концов. Кроме того, мы могли бы усилить среднее (true) * до (не a) *, требуя от нас совпадать с первым закрывающим a вместо того, чтобы пропустить некоторые a перед соответствием закрывающему a:
(true)* a (not a)* (not b and not a) (not a)* a (true)*
Относительно количество штатов
Поскольку вы спрашивали о том, как узнать количество штатов: сначала я бы попытался получить NFA, а затем проверить, можно ли его упростить. Для NFA в вашем примере я не вижу способа дальнейшего уменьшения количества состояний, но в целом сведение к минимуму NFA является сложной проблемой ( reference ), поэтому для этого нет эффективного алгоритма. Конечно, если вы получаете полностью детерминированный c автомат, вы можете применить стандартный алгоритм минимизации DFA.