• Using Sorted First Order Action Logic.
  
  
  
• Can explicitly represent:
  - operators and their actions;
  - synchronisation and concurrency.
  
  
  
• For example...