Reasoning about Choice

We present a logic for reasoning about choice. Choice CTL (C-CTL) extends the well-known branching-time temporal logic CTL with choice modalities, “3” and “2”. An example C-CTL formula is 3AFhappy, 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 multiagent extensions to the logic.

• Type: Journal
• Year: 2013
• Where: AT
• Authors: Wiebe van der Hoek, Nicolas Troquard, Michael Wooldridge
• Keywords: AT 2013, Hardware