A proof assistant for the action based temporal logic Actl

In this paper we present an HOL-based assistant for the mechanization of proofs in a sound and complete calculus for the branching temporal logic ACTL. This logic has action-based modalities and is interpreted over Labelled Transition Systems, so it is suitable for specifying and studying the behaviour of concurrent systems defined by process algebras terms and modelled on LTSs; moreover, ACTL can naturally describe their safety and liveness properties. The making of the axiom system was the first step in the development of this proof assistant. Our aim was to gradually develop a workbench for a proof-theoretical approach in the use of ACTL, in order to overcome the limitations of model-theoretical approach in verification.