Efficient model checking of properties of a distributed application: a multimedia case study