Abstract
We present a logic for reasoning about choice. Choice CTL (C-CTL) extends the well-known branching-time temporal logic ctl with choice modalities, "◇" and "□". An example C-CTL formula is ◇ AF happy, asserting that there exists a choice that will lead to happiness. C-CTL is related to both STIT logics and temporal cooperation logics such as ATL, but has a much simpler and (we argue) more intuitive syntax and semantics. After presenting the logic, we investigate the properties of the language. We characterise the complexity of the C-CTL model checking problem, investigate some validities, and propose multi-agent extensions to the logic. © 2013 Springer-Verlag.