|
• если р является n-местным предикатным символом, a ei,...,en термы, то р (ej,...>en ) временной атом. Такие формулы будем н а з ы в а т ь ч и с т ы м и временными атомами; • если А временной атом, то временными атомами являются также first А, next А. Определение 2. Правильно построенная формула (ППФ) определяется рекурсивно следующим образом: • все временные атомы суть ппф. • если А и В ппф, то ппф будут также и A, first A, next А, □ А. • если А и В ппф, то ппф будет также и (А л В). • если А ппф, х переменная, свободная в А, то ппф будет также и (V x) А. Логические связки v , -> , о и квантор существования 3 могут быть получены из примитивных связок и универсального квантора обычным путём. Для временного оператора Ф (иногда) также используется обычное определение: dcf ФА = -н и ^ А . Кроме того, может использоваться нотация next [п] для обозначения п применений оператора next, где п натуральное число. Если n=0, next [п] означает пустую строку. Используются также аббревиатуры: п л л next [i] A , v next [i] A i-0 HI для записи формул А л next А л ... л next [n] А и A v next A v...v next [n] А соответственно. Исчисление часов вводится следующим образом. Пусть со обозначает множество натуральных чисел {0, 1, 2,...}. В TLC часы определяются как последовательности над ш. |
Словарь TLC включает помимо констант, переменных, функциональных и предикатных символов примитивные пропозициональные связки 1 и л, универсальный квантор V и три временных оператора: first (начальный момент времени), next (следующий момент времени) и □ (всегда). Термы в TLC определяются как обычно в логике первого порядка. Определения правильно построенной формулы (ппф) начнём с определения временного атома. Определение 1. Временной атом определяется рекурсивно следующим образом: • если р является n-местным предикатным символом, a ei,...,en термы, то р (еь...,е„ ) временной атом. Такие формулы будем называтсь чистыми временными атомами; • если А временной атом, то временными атомами являются также first A, next А. Определение 2. Правильно построенная формула (ППФ) определяется рекурсивно следующим образом: • все временные атомы суть ппф. • если А и В ппф, то ппф будут также и -> A, first A, next А, □ А. • если А и В ппф, то ппф будет также и (А д В). • если А ппф, х переменная, свободная в А, то ппф будет также и (Vx ) А. Логические связки v , — > , о и квантор существования 3 могут быть получены из примитивных связок и универсального квантора обычным путём. Для временного оператора 0 (иногда) также используется обычное определение: dcf ОА “ — I [] — IА . 87 Кроме того, может использоваться нотация next [п] для обозначения п применений оператора next, где п натуральное число. Если п=0, next [п] означает пустую строку. Используются также аббревиатуры П П л next [i] А , v next [i] А ¡=0 ¡=0 для записи формул А л next А л ... л next [п] А и A v next A v...v next [п] А соответственно. Исчисление часов вводится следующим образом. Пусть со обозначает множество натуральных чисел {0, 1, 2,...}. В TLC часы определяются как последовательности над со. Определение 3. Глобальными часами называется возрастающая последовательность натуральных чисел, т.е., <0, 1, 2, ...>. Локальные часы это подпоследовательность глобальных часов, т.е. ограниченно возрастающая последовательность натуральных чисел, конечная В частности, глобальные часы и пустые часы, обозначаемые, соответственно, gck и < > также являются локальными часами. Пусть t е ckj означает факт, что t является моментом времени на часах ckj, СК означает множество всех часов, R отношение порядка, заданное на элементах СК2 (здесь 2 показатель декартовой степени множества СК) таким образом, что для любых скь ск2 е СК, имеет место ск) R ск2 , если и только если для всех t е ckt имеет место t е ск2 . Очевидно, что структура (СК, R) является полной решёткой, что позволяет определить две операции, аналогичные теоретикомножественным операциям пересечения и объединения: 88 |