Specification in CTL+Past for Verification in CTL

Barringer, 1987, Up and down the temporal way, Comput. J., 30, 134, 10.1093/comjnl/30.2.134

Burch, 1992, Symbolic model checking: 1020 states and beyond, Inform. and Comput., 98, 142, 10.1016/0890-5401(92)90017-A

Clarke, 1994, Verification tools for finite-state concurrent systems, 803

Clarke, 1997, Another look at LTL model checking, Formal Methods in System Design, 10, 47, 10.1023/A:1008615614281

Demri, 1998, The complexity of propositional linear temporal logics in simple cases (extended abstract), 1373

Emerson, 1990, Temporal and modal logic, 995

Gabbay, 1989, The declarative past and imperative future: Executable temporal logic for interactive systems, 398

Hale, 1989, Using temporal logic for prototyping: The design of a lift controller, 398

Kupferman, O. 1998, personal communication.

Kupferman, 1996, Buy one, get one free!!!, J. Logic Comput., 6, 523, 10.1093/logcom/6.4.523

Kupferman, 1995, Once and for all

Laroussinie, 1995, A hierarchy of temporal logics with past, Theoret. Comput. Sci., 148, 303, 10.1016/0304-3975(95)00035-U

Lichtenstein, 1985, The glory of the past, 193

Manna, 1989, The anchored version of the temporal framework, 354

Manna, 1990, A hierarchy of temporal properties

Manna, 1992

McMillan, 1993

Pinter, 1984, A temporal logic for reasoning about partially ordered computations (extended abstract)

Pnueli, 1977, The temporal logic of programs

Wilke, 1999, Technical Report