Локальные свойства помеченных графов.

Здесь нужно говорить о соответствии между метамоделью и собственно графом. Например: отношение F эквивалентно направленным дугам на графе.

Опр. S = {S1, .., Sn}, F S x S, A = { …}, : F -> A – функция пометки ребер.

Локальная сходимость: , при F это частный случай, при F+ это достижимость.

Локальный детерминизм: // в автоматном смысле

Локальная коммутативность:

Локальная устойчивость:

Считается, что у Si потенциально разрешены 2 действия . Мы рассматриваем варианты когда выполняется . Выполнение одного действия не снимает разрешений с остальных действий.

Теорема(сходимости Келлера): система переходов <S, F> некоторой помеченной система <S, F, A, D> явл. Сходящейся тогда и только тогда, когда помеченная система переходов обладает свойствами локальной детерменированости, локальной коммутативности и устойчивости.