7.Теория взаимодействующих процессов. Основные принципы и определения.

Процесс с заданным алфавитом определяется множеством следов, символы которых принадлежат этому алфавиту. Каждый след описывает возможную последовательность событий, в которых процесс может участвовать в определенный момент времени. Формально процесс P - это любое множество следов в алфавите A, для которого выполняются следующие аксиомы: P0. P A ^{* ;} P1. <>  P ^; P2. st  P => s  P ^;

Каждый процесс будет определяться парой (A,P) , где A- алфавит процесса , а P - множество следов в алфавите A. Выделим следующие процессы - примитивы :

FAIL_A = _df (A,{<>}) - пустой процесс в алфавите A , который никогда "ничего не делает";

(A , A ^*)- универсальный процесс в алфавите A , который " все делает".

В дальнейшем для удобства процесс P будем рассматривать просто как множество следов, выделяя его алфавит лишь в тех случаях, когда это необходимо, обозначая через P алфавит процесса P .

Примеры процессов в алфавите{a, b}:{<>},{<>,< b >},{<>,< a >,< a, b>},{<>,< a >,< a, b>,< b>,<b, a >}.Для процессов-примитивов справедливы следующие ниже свойства.

P3. FAIL_A является процессом в алфавите A.

P4. A ^* является процессом в алфавите A.

P5. P= A => FAIL_A  P.

8. Теория взаимодействующих процессов. Определения операций над следами.

Многие свойства процессов можно доказать, рассматривая соответствующие свойства следов - последовательностей событий из заданного алфавита A .

Пусть A^* означает множество всевозможных следов в алфавите A . Пустой след обозначается как <>, а выражение (c->s ) означает результат приписывания символа (события) c к следу s. Базисные свойства следов определяются следующими:

Ax1. <>  A ^*

Ax2. (c  A) & (s  A ^*)  (c->s)  A ^*

Ax3. (c->s )= (d-> t)  c = d & s = t

Ax4. (c->s )  <>

Ax5. ((<>  S) & ( c A . s S . (c -> s)  S)) => S  A ^*

В дальнейшем будем буквами a, b, c, d обозначать события, буквами s, t ,u, v - следы, буквами P ,Q, R, S ,T - процессы. Например , s=< a,b,c,d > - обозначает след s , состоящий из событий

a,b,c,d ; ( c-> <>)= < c > ; ( a ->< b,c,d > ) = < a,b,c,d >. Аксиома Ax5 обосновывает корректность применения метода структурной индукции при доказательстве свойств следов. Ниже

приводится суть этого метода.

Пусть требуется доказать утверждение (s, t ,u ,…) для любых s  A ^* .

Доказательство строится из следующих шагов (индукция по длине cледа s).

B(базис индукции) . Доказываем (<>, t , u ,…) для всех t , u ,… I(индукционная гипотеза). Предполагаем, что  (s, t ,u ,…) истинно для некоторого s  A^* и для всех t , u ,… . S (шаг индукции). Доказываем  ( c->s, t , u ,…) для всех с A. В результате заключаем, что утверждение  (s, t ,u ,…) истинно для всех s  A ^*. Аналогично проводится процесс доказательства для всех остальных переменных t ,u ,…

Пример доказательства. Докажем свойство Ax6.(c-> s) <> методом структурной индукции по s.

B(базис индукции). Согласно Ax4 имеем ( c-> <> )  <> для всех с A .

I (индукционная гипотеза). ( c-> s)  <> для всех с A.

S (шаг индукции). Согласно Ax3 и индукционной гипотезе имеем

( c-> (c-> s ) )  ( c-> s ) ; кроме того, для всех d , где d  c , по Ax3 имеем ( d-> ( c-> s ) )  ( c-> s ) . Таким образом, последнее соотношение имеет место независимо от того ,c=d или c  d , и свойство Ax6 доказано. Если s  <> , то будем обозначать через s₀ первый символ, а через s' - результат удаления первого символа из следа s.

Формально это определяется так: Ax7. ( c-> s )₀ =c Ax8. ( c-> s )' =s. Отсюда можно вывести свойство: Ax9. ( c-> s ) = t  ( t  <> ) & ( t₀ = c & t' = s)

Конкатенация. Через st обозначается результат конкатенации следов s и t .

Формально это определяется следующим образом :

c1. <> t = t ,

c2. ( c-> s) t = c-> ( st )

Префикс. След s является префиксом следа t (обозначается , как s  t ), если

t начинается с копии s . Формально это определяется так :

p1 . s  t = _df  u (su=t ) .

Операция "после".

Пусть s  t . Тогда операция t/s ( читается t после s) определяется

следующими аксиомами :

a1. t/<> = t ;

a2. ( c-> t )/ (c->s) =t/s

Пример . < a,b,c,d >/< a,b > = < c,d >

Проекция .

Пусть B -множество символов , а s -след . Тогда проекция следа s на множество B ( обозначение s  B) получается удалением из следа s

всех символов , не принадлежащих множеству B . Формально эта операция определяется следующими аксиомами :

r1. <>  B = <> ; r2. c  B => (c-s)  B =c->(s  B) ; r3. c  B => (c-s)  B =c->(s  B) ;

Последовательная композиция . Будем использовать специальный символ  для обозначения успешного завершения следа . Тогда через ( s ; t ) обозначается след , получившийся в результате подстановки следа t вместо первого вхождения символа  в s и удаления остатка следа s (то есть той части следа s , которая следует после символа  ) . Если s не содержит  , то s ; t = s .Формально эту операцию можно определить так :

s1. <> ; t=<> ; s2. (< >s ) ;t = t ; s3. ( c->s );t = c-> (s;t) , c .

Поскольку символ  является признаком успешного завершения следа ,то будем исключать из рассмотрения случаи , когда  появляется внутри

следа ( например , <a,b, ,c > ) , то есть в любом случае имеет место соотношение s <  > t = s .

Переименование . Пусть f - функция , отображающая один алфавит в другой . Если s - след , построенный из символов , входящих в область определения функции f , то определим функцию f ^*(s) как след , получающийся из следа s путем применения функции f к каждому из его символов .Формально :

f1. f ^*(<>) = <> ;

f2. f ^*(c-> s) = f(c) -> f ^*(s) .

Аналогично , если B - множество символов из области определения

Функции f , то f ^*(B) = _df { f^*(B) | b B } .

Условимся , что :

f3. f^*(c) =   c= .