Bounded Model Checking of CTL^*

Bounded Model Checking has been recently introduced as an efficientverification method for reactive systems. This technique reduces modelchecking of linear temporal logic to propositional satisfiability. Inthis paper we first present how quantified Boolean decision procedurescan replace BDDs. We introduce a bounded model checking procedure fortemporal logic CTL* which reduces model checking to the satisfiabilityof quantified Boolean formulas. Our new technique avoids the space blowup of BDDs, and extends the concept of bounded model checking.