An Algorithm to Translate PARADIGM specifications to PLTL

PARADIGM has recently emerged as a new language to design cooperative object-oriented systems. To our knowledge, PARADIGM temporal aspects have not been studied before. Here we describe a polynomial algorithm to translate PARADIGM models to Propositional Linear Temporal Logic programs. The resulting program is an executable specification of the modelled system, suitable for verifying model properties. It is also a declarative view of the model. Therefore we provide a temporal framework to understand and reason about PARADIGM models behavior, and system development in general. Finally, we believe this work provides further evidence on the benefits that PARADIGM has to offer to the Software Engineering community. We complement a previous conference paper which introduced the main concepts behind the translation process and its application to system verification.