Action Language: a specification language for model checking reactive systems

We present a specification language called Action Language for model checking software specifications. Action Language forms an interface between transition system models that a model checker generates and high level specification languages such as Statecharts, RSML and SCR-similar to an assembly language between a microprocessor and a programming language. We show that Action Language translations of Statecharts and SCR specifications are compact and they preserve the structure of the original specification. Action Language allows specification of both synchronous and asynchronous systems. It also supports modular specifications to enable compositional model checking