Alternating-time Temporal Logic and jMocha

Sebastian Wandelt

Alternating-time Temporal Logic (ATL) is an extension of the Computation
Tree Logic (CTL). jMocha is an interactive verification environment for
the modular verification of heterogeneos systems.

This project tries to apply the logic ATL and its extension ATEL to
so-called mix networks. For doing so, a model checking algorithm for ATEL is
presented. Furthermore, a specification of a general mix network is given and
some simple properties are checked.

Finally the applicability of jMocha will be discussed and some
alternatives will be raised.