PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Larosa S. A proof assistant for the action based temporal logic Actl. Internal note IEI-B4-50, 1995.
 
 
Abstract
(English)
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.
Subject Model cheking
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