9.5. Модальная логика и анализ параллельных процессов

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

Ситуацией, или состоянием, назовем набор значений Здесь вектор значений переменных места в котором изменяется в пределах множества мест Значение переменной места указывает на место в процессе Р., которое активировано, — вектор значений распределяемых индивидуальных и пропозициональных переменных у в ситуации

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

холостой такт:

рабочий такт выбираем один из процессов Р., содержащий допустимый переход,

при некотором значении такой, что Истина. Согласно этому переходу получаем X заменой для всех имеем по команде допустимого перехода процесса Довыполняемая последовательность ситуаций о является справедливой, если для нее соблюдается сформулированное ранее по отношению к процессам требование справедливости.

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

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

означает, что в будущем будет такой такт, в котором значение переменной у будет больше на 1, чем ее текущее значение.

Для места атомарную формулу обозначим в месте т.е. Истина, если Таким образом для данной ситуации и места формула истинна в этой ситуации если процесс находится в месте т.е. . В более общем случае для множества мест с формула в месте истинна, если процесс Я находится в одном из мест, принадлежащих множеству т.е. истинна, если значение переменной места т.е. если для некоторых то будем так же записывать как Таким образом в месте в месте

Для данной совокупности параллельных процессов (программы) Р пусть будет предусловием входных переменных, задающим начальные значения и ограничения для входных переменных предусловием программных переменных, задающим начальные значения для переменных предусловием, задающим начальные значения мест программы. Начальное предусловие, ассоциируемое с допустимым вычислением, представляется формулой

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

Формула временной модальной логики является -правильной, если она истинна для всех последовательностей множества Такая формула является свойством программы Р. Нас интересуют именно формулы такого типа, выражающие правильные программные свойства. Введем обозначение которое означает, что формула является -правильной, т.е. истинна для каждого справедливого -вычисления программы Р. Иными словами, выражение означает, что формула истинна для любой допустимой выполняемой последовательности. Отметим, что когда мы говорим об истинности формулы для множества допустимых выполняемых последовательностей, то полагаем, что формула содержит условия, позволяющие проверять свойства программы, относящиеся именно только к этому множеству. Например, если речь идет о свойствах программы, касающихся только последовательностей, ведущих в терминальные состояния, то при формулировке этих свойств следует оговорить, что все допустимые выполняемые последовательности, о свойствах которых идет речь, оканчиваются именно в терминальных состояниях. Доказательство свойств ведется только для этих последовательностей. Значение формулы на остальных допустимых выполняемых последовательностях может быть несущественным.

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

Для дальнейшего рассмотрения важно следующее справедливое утверждение:

Оно означает, что если истинна для любой возможной последовательности, то она истинна также для каждого -вычисления. Это утверждение позволяет нам записать общезначимые формулы временной модальной логики с использованием введенного обозначения

Справедливым является также следующее выражение:

Оно означает: если истинна для всех -вычислений, то также всегда истинна для них.

Перейдем теперь к главной цели настоящей главы — изучению свойств, которым, как правило, должны удовлетворять программы. Естественно, эти свойства не являются всеобъемлющими, могут пополняться или модифицироваться, но являются достаточно характерными для рассматриваемого типа программ. Их классифицируют в зависимости от вида представляющих эти свойства формул. Принципы доказательства истинности формул в принципе ничем не отличаются от изложенных в главе 4, за исключением того, что в дополнение к уже изученным используются правила вывода, содержащие модальные операторы. Принципам доказательства и примерам доказательства будет посвящен отдельный параграф настоящей главы. Сначала рассмотрим только программные свойства.