**Abstract:**
We define reachability logic (*RL*), a fragment of FO^{2}(TC) (with boolean variables)
that admits efficient model checking -- linear time with a small constant
-- as a function of the size of structure being checked.
*RL* is expressive enough so that modal logics PDL and
CTL^{*} can be linearly embedded in it.
The model checking algorithm is also linear in the size of the formula, but
exponential in the number of boolean variables occurring in it. In
practice this number is very small.
In particular, for CTL and PDL formulas the resulting model checking
algorithm remains linear.
For CTL^{*} the complexity of model checking --- which is PSPACE complete
in the worst case --- can be read from the face of the translated formula.

Recent Publications of Neil Immerman