9.2. Язык временной модальной логики

Язык временной модальной логики основан на языке логики предикатов первого порядка и использует множество индивидуальных (объектных) и пропозициональных переменных и констант, функциональных и предикатных символов. Множество всех переменных разбивается на два подмножества: глобальных и локальных переменных.

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

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

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