Темпоральная логика

Темпоральная логика [1, 4, 5] состоит из пропозициональной логики и темпоральных операторов. Приведём определение линейной темпоральной логики(LTL), которая используется в настоящей работе.

Пусть AP- множество атомарных предложений. Тогда:

• pявляется формулой для всех pє AP.

• Если φ- формула, то -φ- формула.

• Если φи ψ- формулы, то φ v ψ- формула.

• Если φ- формула, то X φ- формула.

• Если φи ψ- формулы, то φ U ψ- формула.

Множество формул, построенных в соответствии с этими правилами, называется формулами LTL. X (neXt, «в следующем состоянии») и U (Until, «пока не») называются темпоральными операторами.

Синтаксис LTL может быть задан и в нотации Бэкуса-Наура. Для pє AP множество LTL-формул определяется следующим образом:

φ ■■=p^|-φ^{| (}ф^vφ) ^{| χ}φ^{| (}ф^uφ).

Темпоральные операторыG (Globally, «всегда») и F (Future, «когда- нибудь») определяются следующим образом:

F φ = true U φ,

G φ = -F -φ.

Приведём неформальное определение семантики LTL-формул:

• φ U ψозначает, что свойство ψдолжно выполниться в будущем, а до тех пор, пока оно не выполнилось, должно выполняться φ;

• X φозначает, что в следующем состоянии должно выполниться φ;

• F φозначает, что φдолжно выполниться когда-нибудь в будущем;

• G φозначает, что φдолжно выполниться в текущем состоянии и во всех следующих.

1.6.