From Quantified CTL to QBF

Akash Hossain, Francois Laroussinie

QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over…