Modelling transition systems within an action based logic

In this paper we study the ability of a logic to finitely characterize the complete behaviour of a system. Given a Labelled Transition System, we look for a formula of the logic that is satisfied by all and only the Labelled Transition Systems that are equivalent to it. The main result is that we are able to finitely characterize finite state Labelled Transition Systems, with respect to the classical notion of strong bisimulation equivalence, in a completely syntax driven way and using a logic without fixed points. The logic we have chosen is the action based version of CTL, known as ACTL, which is strictly less expressive than CTL