PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Ristori G. Model checking for action-based logics. In: Formal Methods in System Design, vol. 4 (2) pp. 187 - 203. Kluwer, 1994.
 
 
Abstract
(English)
A model checker is described that supports proving logical properties of concurrent systems. The logical properties can be described in different action-based logics (variants of Hennessy-Milner logic). The tools is based on the EMC model checker for the logic CTL. It therefore employs a set of translation functions from the considered logics to CTL, as well as a model translation function from labeled transition systems (models of the action-based logics) to Kripke structures (models for CTL). The obtained tool performs model checking in linear time complexity, and its correctness is guaranteed by the proof that the set of translation functions, coupled with the model translation function, preserves satisfiability of logical formulae.
Subject Action-based logics
Concurrent systems
Model checking
D.2.4 Software/Program Verification. Model checking


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