In this paper we present a sound and complete axiom system for the branching temporal logics ACTL. This logic has action-based modalities and is interpreted over Labelled transition Systems, so it is suitable to specify and study the behavior of concurrent systems defined by process algebras and modelled on LTSs. ACTL is more expressive than Hennessy-Milner logic and can naturally describe safety and liveness properties. The reason we give the axiomatisaton of ACTL is to complete the characterization of such a logic; moreover, the making of the axiom system was the first step for the developement of a proof assistant based on it.
A sound and complete axiom systems for the logic ACTL
Gnesi S;
1993
Abstract
In this paper we present a sound and complete axiom system for the branching temporal logics ACTL. This logic has action-based modalities and is interpreted over Labelled transition Systems, so it is suitable to specify and study the behavior of concurrent systems defined by process algebras and modelled on LTSs. ACTL is more expressive than Hennessy-Milner logic and can naturally describe safety and liveness properties. The reason we give the axiomatisaton of ACTL is to complete the characterization of such a logic; moreover, the making of the axiom system was the first step for the developement of a proof assistant based on it.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
