TABLE OF CONTENTS Below we give a brief history of PSL. Our aim is not to give a complete chronicle of the history of temporal logic, nor a full accounting of the history of assertions in hardware design. Furthermore, we will not list each of the many people who participated in one or more of the Accellera and IEEE committees involved in the development of PSL their names appear in the Accellera and IEEE standards. Rather, our aim is to touch on the major milestones in the development of the language, and the main personalities and ideas that have influenced PSL from its beginnings as syntactic sugaring of the temporal logic CTL, through the move to an LTL-based paradigm, and concluding with the IEEE standardization in October 2005. For background, we include a few words about the temporal logics CTL and LTL as well.
We have made every effort to refer to all the main relevant works, however we may have missed something. If so, we apologize in advance for the omission and would welcome any corrections and/or comments.
The linear time logic LTL was introduced as propositional temporal logic, or PTL, by Amir Pnueli in 1977 [41], and the computation tree logic CTL was first presented by Ed Clarke and Allen Emerson in 1981 [14]. For many years, a debate as to the relative merits of each was conducted in the literature. Moshe Vardi was one of the main players in that debate ...
