Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Larosa S. A sound and complete axiom systems for the logic ACTL. Internal note IEI-B4-53, 1993.
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.
Subject Temporal Logic
D.2.4 Software/Program Verification. Formal methods

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional