Name
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, "$\Diamond$" and "□". An example c-ctl formula is $\Diamond$AFhappy, 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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-39860-5_2 | AT |
Keywords | Field | DocType |
multi-agent extension,intuitive syntax,well-known branching-time temporal logic,stit logic,choice ctl,choice modality,c-ctl model checking problem,temporal cooperation,example c-ctl formula | Computation tree logic,Deontic logic,Model checking,Existential quantification,Theoretical computer science,Linear temporal logic,Modal logic,Artificial intelligence,Non-monotonic logic,Temporal logic,Mathematics | Conference |
Citations | PageRank | References |
0 | 0.34 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wiebe Van Der Hoek | 1 | 2566 | 195.77 |
| Nicolas Troquard | 2 | 266 | 29.54 |
| Michael Wooldridge | 3 | 10010 | 810.27 |