Сходимость

Теорема Рассела-Черча: Если метамодель обладает свойством сходимости, то такая система порождает процессы, приводящие к одному результату.

Эта теорема объясняет, зачем вообще нужно это свойство сходимости: процессы, порождаемые системой, обладающей этим св-вом, приводят к 1-му результату.

Теорема (Келлер): Если асинхронные процессы, порождаемые некоторой метамоделью, обладают локальными свойствами детерминированности, коммутативности и устойчивости, то такая метамодель обладает свойством сходимости.

1. Св-во лок. детерминированности:
s_i, s_j, s_k Î S σ Î A [ s_i (σ) s_j & s_i (σ) s_k → s_j = s_k ]

т.к. σ Î A, то это локальное свойство. s_i (σ) s_j можно записать s_i → ^σ s_j

2. Св-во лок. коммутативности:
s_i, s_j, s_k Î S σ, π Î A [ s_i (σ π) s_j Î F⁺ & s_i (π σ) s_k Î F⁺ → s_j = s_k ]

3. Св-во устойчивости:
s_i, s_j, s_k Î S σ, π Î A s_m Î S [ s_i (σ) s_j Î F & s_i (π) s_k Î F → s_i (π σ) s_m Î F⁺ ]

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

Теорема (сходимости Келлера):

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