Go backward to Non-Laws
Go up to Top
Go forward to Equivalence of Agents

The Expansion Law

The Expansion Law
- Let $P$ $<=>$ $(P$ ₁[f₁] | ...| P_n[f_n])\ $L$
- $P$ = sum{ $f$ ₁(alpha $).(P$ ₁[f₁] | ...| P_i'[f_i] | ...| P_n[f_n])\ $L$ :
  $P$ _i ->^alpha $P$ _i', $f$ _i(alpha) not in $L$ unionL}
  + sum{tau.( $P$ ₁[f₁] | ...| P_i'[f_i] | ...| P_j'[f_j] | ...| P_n[f_n])\ $L$ :
  $P$ _i ->^l_1 $P$ _i', $P$ _j ->^l_2 $P$ _j', $f$ _i( $l$ ₁) = $f$ _i(l₂), $i < j$ }
Corollary
- Let $P$ $<=>$ $(P$ ₁ | ...| P_n)\ $L$
- $P$ = sum{alpha.( $P$ ₁ | ...| P_i' | ...| P_n)\ $L$ :
  $P$ _i ->^alpha $P$ _i', alphanot in $L$ union $L'$ }
  + sum{tau.( $P$ ₁ | ...| P_i' | ...| P_j' | ...P_n)\ $L$ :
  $P$ _i ->^l $P$ _i', $P$ _j ->^l $P$ _j', $i < j$ }
Example
- $P$ ₁ = $a.P$ ₁' + b.P₁"
- $P$ ₂ = $a$ . $P$ ₂' + c.P₂"
- ( $P$ ₁|P₂)\ $a$ = $b.(P$ ₁"|P₂)\ $a$ + $c.(P$ ₁|P₂")\ $a$ + tau. $(P$ ₁'|P₂')\ $a$

Id: ccs2.tex,v 1.1 1996/06/12 15:55:52 schreine Exp schreine