Верификация недетерминированных и параллельных программ {P} A {Q} D=cobegin B1 || B2 … || Bn coend D=resource r cobegin B1 || B2 … || Bn coend F=with r when do B inv r
Процессы
Классификация процессов
Сети Петри С=(P, T, I, O) P={p 1, p 2, …, p n } T={t 1, t 2, …, t m } Пример: C={P, T, I, O} P={p 1, p 2, p 3, p 4, p 5 } T={t 1, t 2, t 3, t 4 } I(t 1 )={p 1 }O(t 1 )={p 2, p 3, p 4 } I(t 2 )={p 2, p 3, p 4 }O(t 2 )={p 2 } I(t 3 )={p 4 }O(t 3 )={p 5 } I(t 4 )={p 5 }O(t 4 )={p 3, p 4 }
C=(P, T, I, O) С=(P, T, I, O) M= (P, T, I, O, ) =(1, 0, 0, 2, 1)
t j (, t j )= ( 0, 1, 2, …) (t j0, t j1, t j2, …) ( k, t jk )= k+1 C=(P, T, I, O) t j T (, t j )= R(C, )