A Branching Time Variant of CaRet.

A shortcoming of traditional logics like LTL and CTL on Pushdown Systems is their inability to express specifications about the call-/return-behavior or the stack content. A natural approach to this problem is the logic CaRet. CaRet adds modalities to LTL that allow specifications to navigate over calls and returns of procedures. In this paper, BranchCaRet, a natural CTL-like variant of CaRet is defined that provides existentially and universally quantified CaRet modalities. We prove that BranchCaRet model checking is decidable and EXPTIME-complete by extending a known CTL model checking algorithm for Pushdown Systems based on Alternating Buchi Pushdown Systems.