{a, b, c} = {1, 0, 1}, активны атомарные предложения a и c, а
предложение b не активно.
Среди этих вершин оставим только те, у которых соответствующий
двоичный набор удовлетворяет формуле q (делает ее значение
истинным). Остальные вершины удалим, так как q должна
выполняться всегда. Далее, для любых двоичных наборов x и y
добавляем ребро из «вершины» x в «вершину» y, если и только если
для любого i от 1 до n выполняется импликация r
i
(x) s
i
(y). Это
ребро соответствует условию (r
1
X s
1
) … (r
n
X s
n
) и означает,
что для любого i «если сейчас выполнено r
i
, то на следующем шаге
будет выполнено s
i
».
Далее, отметим в качестве стартовых состояний (их может быть
несколько) те, у которых соответствующий двоичный набор
удовлетворяет формуле p. Это соответствует условию, что формула p
верна «в момент времени 0».
Последний этап называется «чисткой таблицы» и является
необязательным. Он предназначен для более эффективной работы с
моделью. На этом этапе обеспечим требование, состоящее в том, что
все пути в графе должны быть бесконечными и что отовсюду должны
быть пути в вершины, в которых выполняются формулы t
j
(j от 1 до
m). Делается это «рекурсивным» удалением из модели всех вершин, у
которых нет ни одного потомка, и всех таких вершин, из которых для
какого-то j нет пути ни в одну вершину, в которой выполняется
формула t
j
. Проще говоря, в таблице следует оставить только те
состояния, из которых существует хотя бы один бесконечный путь,
удовлетворяющий условиям справедливости (это значит, что все t
j
выполняются на таком пути бесконечно часто). Алгоритм,
позволяющий проделать это эффективно (работающий за линейное
время от размера таблицы), будет обсуждаться в контексте поиска
справедливых путей в разд. 2.4.
После всех этих действий следует оставить в таблице только те
вершины, которые достижимы из начальных, а остальные – удалить.
Полученная таблица естественным образом отражает смысл формулы,
а ее бесконечные пути удовлетворяют двум свойствам:
1. Пусть σ – некоторый абстрактный путь (последовательность
двоичных наборов, соответствующих атомарным предложениям).
Если рассматриваемая формула верна для пути σ, то в таблице
присутствует экземпляр этого пути, стартующий в начальном
состоянии.
2. Пусть σ – путь в построенной таблице (стартующий в начальном
состоянии) такой, что каждая пропозициональная формула t
j
(при j