|
Для любой формулы А ее локальные часы при данном присваивании часов определяются, исходя из ее синтаксической структуры и часов предикатных символов, ассоциированных с ними. Определение 5. Пусть А формула и ск присваивание часов. Локальные часы, ассоциированные с А, обозначаются скд и определяются рекурсивно следующим образом: • если А есть временной атом р(хь ..., хп), то скд = ск (р ); • если А = first В, -IВ , □ В или (Vx) В, то скд = скв ♦если А = (В л С), то скд = скв ^ скс* если А next В, то ( 1 ) скд = В дальнейшем для простоты представления будемиспользовать нотацию скдв для скд 4 скв и ск$д для скпе« д . Из определений1-5 следует, что сквvc = скв-*с ~ скв«с = сквс и для квантора существования 3 имеем ck(3x)D~ скц. Справедливо утверждение» что каждое присваивание часов индуцирует однозначное соответствие каждой формулы TLC некоторым конкретным локальным часам [1 0 1]. Определение 6 . Для данных локальных часов cki = Инверсно, можно записать tn = ckj(n>, что означает, что tn является моментом времени на локальных часах ск,, имеющим ранг п. Для глобальных часов gck имеем: rank (t, gck) = t и gckw= t. Интерпретация формул (семантика) вводится следующим образом. В TLC значением любого предикатного n-местного символа р фактически является частичное отображение из <ов P(Dom"), |
89 def cki I ck2 = g.l.b.{ ck, ck2}, def cki T ck2 = l.u.b. { ck, ck2}, где скь ck2 e CK, g.l.b., l.u.b. соответствуют “ наибольшей нижней грани” и “наименьшей верхней грани” для отношения R. По определению cki 4 ск2 есть локальные часы, состоящие из тех моментов времени, которые появляются как на скь так и на ck2 , а ск t ск2 локальные часы, состоящие из моментов времени, появляющиеся либо на ck i, либо на ск2 , либо на обоих. Определение 4. Присваиванием часов ск называется отображение из множества LP предикатных символов в множество часов СК, т.е. ск е [LP -> СК]. Нотация ск(р) означает часы, ассоциированные с предикатным символом р при данном присваивании часов ск. Для любой формулы А ее локальные часы при данном присваивании часов определяются, исходя из ее синтаксической структуры и часов предикатных символов, ассоциированных с ними. Определение 5. Пусть А формула и ск присваивание часов. Локальные часы, ассоциированные с А, обозначаются скл и определяются рекурсивно следующим образом: • если А есть временной атом p(xi,..., х„ ),то скА = ск (р ); • если А = first В, 1 В , □ В или (Vx) В, тоскЛ= скв • если А = (В д С), то скА= скц 4скс. • если А = next В, то (1 ) скА = В дальнейшем для простоты представления будем использовать нотацию скА в для скЛ i скв и ск^д для cknextа • Из определений 1-5 следует, что ckBvc = скв_>с = скВос = сквс и для квантора существования 3 имеем ск(ЗХ )В= скв. Справедливо утверждение, что каждое присваивание часов индуцирует однозначное соответствие каждой формулы TLC некоторым конкретным локальным часам [167]. Определение 6. Для данных локальных часов ck¡ Инверсно, можно записать t„ ~ ck,(n), что означает, что tn является моментом времени на локальных часах ck¡, имеющим ранг п. Для глобальных часов gck имеем: rank (t, gck) = t и gck(t)= t. Интерпретация формул (семантика) вводится следующим образом. В TLC значением любого предикатного n-местного символа р фактически является частичное отображение из со в P(Domn), где Dora область интерпретации, Dom" n-я декартова степень множества Dom и P(Dom") множество всех подмножеств множества Dom". Таким образом, при любом конкретном присваивании часов, для любого t е ск (р) в соответствии с данным частичным отображением найдётся некоторое подмножество множества Dom", между тем, как для моментов времени, не входящих в ск (р), образ не определён. Формула определяется только на моменты времени, появляющиеся на ее часах при данном присваивании часов. Поэтому для данных часов te w значение формулы может быть истина , ложно или неопределено в зависимости от локальных часов, ассоциированных с ней в соответствии с определением 5. 90 |