Housing Agency Workflow

This is an exercise to build a Workflow Net


Housing Agency


  • potential tenants indicate their interests:
    • certain criteria: price, size, location, etc
  • the interests are entered into some database


  • after the registration, the agency sends an offer when a suitable apartment is found
  • customer decides to accept or decline the offer
  • if he declines, the agency continues to look for another flat
  • if the customer doesn't respond in 2 weeks, it's assumed he has declined the offer
  • if the customer declines two offers in a row, the process ends automatically


  • if the customer accepts the offer, he has to sign a contract
  • after signing he has to send the signed copy
  • and pay 1000 USD deposit
  • once it's done, the tenants receive the keys


  • they pay of the monthly basis
  • every two months the finance department checks the payment history
  • if everything is alright - no further action is needed
  • if not, then a warning is sent
  • then the payment is checked 2 months later: if there are still problems, the eviction process starts
  • and then the process ends

Annual inspection

  • the flat is checked annually
  • ok - no actions needed
  • if problems (damages) - tenants have to solve them in 4 weeks
  • second inspection: if the problems solved - no actions are needed
  • if not, the damage must be paid by the tenants
  • if payment is not received in 3 weeks, the eviction process starts
  • and the process ends

Workflow Net Model

To model this in Petri Nets, PNEditor was used

Obtained model:


Bad sides of the model:

  • lack of parallelism
  • the model is too restrictive

YAWL Model

The main flow:

Initiate Renting flow:

  • yawl-housing-agency3.png

Check Payment flow

  • yawl-housing-agency4.png

Annual Check flow:

  • yawl-housing-agency2.png

In this model:

  • the issue with the lack of parallelism was fixed

Re-discovering the Model

Using the $\alpha^+$ algorithm


  • first of all, the transitions were renamed to letters
  • petri-net-housing-agency-ren.png
  • to obtain the possible sequences we construct the following graph:
  • petri-net-housing-agency-firing.png
  • then we execute Breadth-First Search restricting the traversal of each node to 2 visits
  • and get a log with the following possible firing sequences: http://pastebin.com/kSyhR9uK
  • then the $\alpha^+$ algorithm is applied to these sequences using EMiT
  • and the following workflow net is rediscovered:
  • petri-net-housing-agency-redisc.png