The Glory of the Past. - Orna Lichtenstein; Amir Pnueli; Lenore D. Zuck (Logic of Programs, 1985)

Checking That Finite State Concurrent Programs Satisfy Their Linear Specification. - Orna Lichtenstein; Amir Pnueli (POPL, 1985)

Explicit Clock Temporal Logic - Eyal Harel; Orna Lichtenstein; Amir Pnueli (LICS, 1990)

Propositional Temporal Logics: Decidability and Completeness. - Orna Lichtenstein; Amir Pnueli (Log. J. IGPL, 2000)