Model checking for action-based logics

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.