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 | Dimensione | Formato | |
|---|---|---|---|
|
prod_411542-doc_144929.pdf
accesso aperto
Descrizione: A sound and complete axiom systems for the logic ACTL
Tipologia:
Altro materiale allegato
Licenza:
Nessuna licenza dichiarata (non attribuibile a prodotti successivi al 2023)
Dimensione
1.37 MB
Formato
Adobe PDF
|
1.37 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
