On the fly verification of networks of automata

In this paper we present an "on the fly model checker" for the action based branching time temporal logic mu -ACTL. The model checker allows a logic formula to be evaluated directly on the network representing a concurrent system as a collection of synchronized agents working in parallel without generating the global model of the system. It is possible in this way to verify interesting properties also an systems for which the state explosion problem makes other verification tools inapplicable.