Обсуждение статьи van der Hoek W., Wooldridge M. "Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and its Applications"
Мероприятие завершено
3 марта в 16:20 состоится заседание исследовательского семинара "From the Logical Point of View" Международной лаборатории логики, лингвистики и формальной философии.
В ходе семинара будет обсуждаться статья
van der Hoek W., Wooldridge M.
"Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and its Applications"
"Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and its Applications"
Аннотация:
Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as Alternating-time Temporal Logic (ATL). The key insight in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form, where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as group can cooperate to bring about iff it is common knowledge in that . The resulting logic — Alternating-time Temporal Epistemic Logic (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems.
van der Hoek W., Wooldridge M. "Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and its Applications"
Zoom
Идентификатор конференции: 951 6621 6579
Доступ к конференции по паролю, для получения пароля, пожалуйста, напишите по адресу llfp@hse.ru
Дата
3 марта
16:20
В статье упомянуты