PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Fantechi A., Gnesi S., Ristori G. Model checking for action-based logics. Internal note IEI-B4-41, 1992.
 
 
Abstract
(English)
A model checker is described which supports proving logical properties of concurrent systems. The logical properties can be described in different action based logics (variants of Hennessy-Milner Logic). The tool is based on the EMC model checker for the logic CTL. It employs therefore a set of translation functions from the considered logics to CTL, as well as a model translation function from Labelled 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, preserve satisfiability of logical formulae.
Subject


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