30
Oct

Conference paper: Model Checking for Reasoning About Incomplete Information Games

Title: Model Checking for Reasoning About Incomplete Information Games

Authors: Xiaowei Huang, Ji Ruan, Michael Thielscher

Abstract. GDL-II is a logic-based knowledge representation formalism used in general game playing to describe the rules of arbitrary games, in particular those with incomplete information. In this paper, we use model checking to automatically verify that games specified in GDL-II satisfy desirable temporal and knowledge conditions. We present a systematic translation of GDL-II to a model check- ing language, prove the translation to be correct, and demonstrate the feasibility of applying model checking tools for GDL-II games by four case studies.

To be presented at the 26th Australasian Joint Conference on Artificial Intelligence in December 2013 (Dunedin, New Zealand).

Short URL:
14
May

FWD: The European Master’s Program in Computational Logic (deadline 31 May)

The European Master’s Program in Computational Logic

We are glad to announce to you the possibility to join our European
Master’s Program of Computational Logic. This program is offered
jointly at the Free-University of Bozen-Bolzano in Italy, the
Technische Universität Dresden in Germany, the Universidade Nova de
Lisboa in Portugal and the Technische Universität Wien in
Austria. Within this program you have the choice to study at two
/three of the four European universities. In addition you can do your
project work at the National ICT of Australia (NICTA). You will
graduate with a MSc in Computer Science and obtain a multiple
degree. Information on the universities and the program is provided
here:

http://www.emcl-study.eu/home.html

Language of instruction is English. Tuition fees are 3.000 EUR (for
non-European students) and 1.000 (for European students) per year. The
ERASMUS-MUNDUS consortium offers tuition fee waivers and small grants
(http://www.emcl-study.eu/grants.html). (more…)

Short URL:
07
Aug

新南威尔士大学计算机科学和工程学院的逻辑研究介绍

新南威尔士大学计算机科学和工程学院是澳大利亚最好的计算机研究所之一,其中有两个研究组做逻辑相关的研究:人工智能组和理论组。人工智能组和逻辑相关的研究大方向是知识的表示与推理以及在机器人学中的应用。这个组做逻辑的学者主要有Michael Thielscher教授,Maurice Pagnucco(副)教授,和Wayne Wobcke(副)教授。其中Thielscher教授的主要领域有:知识表示,认知主体和机器人学,通用游戏竞赛和约束逻辑编程,主要学术专著有《行动编程语言》,《机器人推理》。他的团队开发的FLUXPLAYER在2006年获得AAAI通用游戏竞赛的冠军。Pagnucco教授的主要领域有:认知机器人学、信念修正和基于行动的推理;他和多伦多大学Hector Levesque教授共同开发了基于逻辑变成语言Prolog的Legolog系统。Wobcke教授的主要领域是智能主体的逻辑基础、信念修正和非单调推理。

理论组的主方向是程序的形式化验证。这个组做逻辑的主要学者有:Carroll Morgan教授,Ron van der Meyden教授,Rob van Glabbeek教授和Kai Engelhardt博士。其中Morgan教授的主要领域是程序验证的概率模型,专著有《概率系统的抽象、改善与证明》。Van der Meyden教授的主要领域是:知识推理、分布式系统的形式化方法、计算机安全协议,以及逻辑编程;他领导的团队开发了MCK模型检测工具。Van Glabbeek教授的主要领域有:并行计算模型,进程代数,线性逻辑的证明网,时间逻辑等;他同时也是NICTA(澳大利亚国家信息和通信研究中心)在新南威尔士大学分部的首席研究员之一。Engelhardt博士的主要领域是程序验证的形式化方法,认知时间逻辑,计算机安全理论等。

另外同时在本院和NICTA任职的Toby Walsh教授也做一部分和逻辑相关的工作,主要研究领域有:约束编程,调度,以及计算社会选择理论,主要学术专著有《可满足性手册》,《约束编程手册》等。

本院的研究生奖学金主要在这个网站上公布:

https://www.cse.unsw.edu.au/scholarships/postgraduate_research.html

和英国类似,这里的讲师到教授都有资格指导博士研究生。有些研究者可能有来自研究项目的博士奖学金。申请者需要做的是了解研究者的工作(例如阅读其学术论文和著作),并在邮件中写上自己的个人简介以及希望做的研究。

新南威尔士大学计算机科学和工程学院网址 www.cse.unsw.edu.au

 

Short URL:
06
Aug

利物浦大学计算机系的逻辑研究介绍

利物浦大学计算机系在英国计算机系最新排名中名列第九(共103个*),在计算逻辑研究领域拥有世界一流的水准。该系有两个研究组进行逻辑相关的研究:主体系统研究组(Agent ART Group),以及逻辑与计算研究组(Logic and Computation Group)。

主体系统研究组主要对智能自治主体,多主体系统进行基础和应用的研究。这个组做逻辑研究的学者主要有:Wiebe van der Hoek教授,Michael Wooldridge教授(2012年6月成为牛津大学的教授),和Davide Grossi博士。其中van der Hoek教授的方向是模态逻辑,动态认知逻辑和多主体系统逻辑,主要学术专著有:《计算机科学和人工智能中的认知逻辑》,《动态认知逻辑》。Wooldridge教授是多主体系统研究的奠基人之一,研究方向是多主体系统逻辑,计算复杂性,博弈论,主要学术专著有:《多主体系统入门》,《理性主体的推理》等。

逻辑与计算研究组主要专注于三类课题的研究:(1)时态逻辑、多模态逻辑和描述逻辑的推理技术,(2)基于主体系统的形式化验证和高级程序语言验证,(3)网络数据库的形式化建模和分布式证明技术。这个组的研究者有:Michael Fisher教授,Frank Wolter教授,Clare Dixon博士,Ullrich Hustadt博士,Boris Konev博士,Alexei Lisitsa博士,Grant Malcolm博士,Vladimir Sazonov博士,和Sven Schewe博士。其中Fisher教授是这个组的领头人,方向是形式化验证技术(包括模型检测), 专著有《基于时态逻辑的实用形式化方法入门》。Wolter教授的方向是:模态逻辑,时态逻辑,描述逻辑和空间推理,主要专著有《多维模态逻辑:理论和应用》,《模态逻辑手册》等。

在英国的高校,一般奖学金有三种来源:大学奖学金,院系内部的奖学金,以及导师项目的资金。大学的奖学金一般公布在网站上,例如在利物浦大学给研究生的奖学金网站是http://pgf.liv.ac.uk/,其中特别对中国学生开放的有Hong Kong Graduate Association Awards,Liverpool China Scholarship Council (CSC) Award。其它两种奖学金有可能在院系网站上找到。有时候在研究者的网站上也能够发现招生信息。一般申请奖学金的方式是直接和研究者(从讲师到教授都有指导博士的资格)进行联系,若他或她有意招收你为学生,则会告诉你如何申请奖学金。联系之前需要做的是了解这位研究者的研究(通过发表的文章或者专著),并在信中写上自己的个人简介以及希望做的研究。

利物浦大学计算机系网址 www.csc.liv.ac.uk
注解*Liverpool scores 9th out of 103 Computer Science departments in the Guardian University guide 2013 subject table http://www.guardian.co.uk/education/table/2012/may/22/university-guide-computer-sciences-it

Short URL:
03
Aug

Journal paper: Logical-Epistemic Foundations of General Game Descriptions

Title: Logical-Epistemic Foundations of General Game Descriptions

Authors:
Ji Ruan and Michael Thielscher
School of Computer Science and Engineering The University of New South Wales, Australia

Abstract:
A general game player automatically learns to play arbitrary new games solely by being told their rules. For this purpose games are specified in the general Game Description Language (GDL), a variant of Datalog with function symbols that uses a few game-specific keywords. A recent extension of basic GDL allows the description of nondeterministic games with any number of players who may have incomplete, asymmetric information. In this paper, we analyse the epistemic structure and expressiveness of this language in terms of modal epistemic logic and prove two main results: (1) The operational semantics of GDL entails that the situation at any stage of a game can be characterised by a multi-agent epistemic (i.e., S5-) model; (2) GDL is sufficiently expressive to model any situation that can be described by a (finite) multi-agent epistemic model.

Acknowledgements:
A preliminary version of this paper has been published in the Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI’11). We thank Jerome Lang for suggesting the example for the paper, the anonymous reviewers from AAAI’11 and Studia Logica for their helpful comments. This research was supported under Australian Research Council’s (ARC) Discovery Projects funding scheme (project DP120102023). The second author is the recipient of an Australian Research Council Future Fellowship (project FT0991348) and is also affiliated with the University of Western Sydney.

Status:

It was accepted by the Special Issue of Studia Logica on Logic and Games in July 2012.

Download: Pre-publication version.

Short URL:
06
Jul

Workshop Paper: Model Checking Games in GDL-II

Title: Model Checking Games in GDL-II

Authors: Ji Ruan and Michael Thielscher
School of Computer Science and Engineering, The University of New South Wales, Australia

Abstract:The game description language GDL has been developed as a logic-based formalism for representing the rules of arbitrary games in general game playing. A recent language extension called GDL-II allows the description of nondeterministic games with any number of players who may have incomplete, asymmetric information. In this paper, we apply model checking to address the problem of verifying that games specified in GDL-II satisfy appropriate temporal and knowledge conditions. We present a systematic translation of a GDL-II description to a model checking tool, and show the feasibility by two case studies.

Accepted by the Computer Games Workshop at ECAI 2012.

Acknowledgements:
We thank Xiaowei Huang, Ron van der Meyden and two anonymous reviewers for their helpful comments. This research was supported under Australian Research Council’s (ARC) Discovery Projects funding scheme (DP120102023).

Short URL: http://goo.gl/tGcwJ
Page 1 of 23123451020...Last »

    RSS Subscribe

    Navigation

    Vistors

    Locations of visitors to this page