Go backward to Reformulations Go up to Top Go forward to Action and Transition

Equality of Agents

• Five basic operators:
  • Prefix: alpha.P
  • Summation: P + Q
  • Composition: P | Q
  • Restriction: P\{l₁,...,l_n}
  • Relabelling: P[l'₁/l₁,...,l'_n/l_n]
• Strongjobber only needs hands:
  • Strongjobber :=
    in(job).out(done(job)).Strongjobber
• Claim:
  • Jobshop = Strongjobber | Strongjobber
  • Specification of system Jobshop
  • Proof of equality required.