Hello,

I'm now taking a seminar course and my report topic is model checking. I've done some literature research and figured out that in the original model checking and symbolic checking, they use CTL to describe the properties/formulae.

But in the first bounded model checking paper (A. Biere et al., “Symbolic model checking without BDDs,) they first emphasized that they concentrate on LTL model checking because it can "reduces model checking to propositional satisfiability", while in later sections they introuduced path quantifiers again (A and E), which is not allowed in LTL. And in later bounded model checking papers (e.g., E. Clarke et al., “Bounded model checking using satisfiability solving,”) they once again focused on CTL model checking.

As far as I know, the major difference between CTL and LTL is their expression power. But is there any other reason that makes bounded model checking originally "focused" on LTL model checking?

Many thanks in advance.