From PSL to LTL: A formal validation in HOL

Abstract

Using the HOL theorem prover, we proved the correctness of a translation from a subset of Accellera's property specification language PSL to linear temporal logic LTL. Moreover, we extended the temporal logic hierarchy of LTL that distinguishes between safety, liveness, and more difficult properties to PSL. The combination of the translation from PSL to LTL with already available translations from LTL to corresponding classes of ω-automata yields an efficient translation from PSL to ω-automata. In particular, this translation generates liveness or safety automata for corresponding PSL fragments, which is important for several applications like bounded model checking. © Springer-Verlag Berlin Heidelberg 2005.