Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Abstract State Machines

  • Basic ASM are finite sets of conditional state transition rules of the form:
    if Condition then Updates
  • A state is represented by a first order structure; a set with relations and functions
  • Every algorithm can be rewritten as a finite number of transition rules
  • Signature is a finite collection of function names
    • each name comes with an indication of its arity
      \[ f(t_{1},...,t_{n}):=t \]
  • Updates is a finite set of assignments of the form
  • Execution can be understood as changing (or defining, if there was none) in parallel the value of the occurring functions f at the indicated arguments to the indicated value 
  • A guarded rule is a transition
    if Condition then Updates
    where Condition is the guard under which a rule is applied
  • A set of guarded updates are written usually as a list 
  • They are executed in parallel, so order is immaterial
  • All guarded updates on the list are performed simultaneously
  • Execution of an ASM
    • Check which rules apply
    • Randomly select a/all rule(s)
    • Perform update

Speaker notes:

Content Tools


There are currently no sources for this slide.