Michael Thielscher

KR Conference 2025 Conference Paper

Repairing General Game Descriptions

• Yifan He
• Munyque Mittelmann
• Aniello Murano
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language (GDL) is a widely used formalism for specifying the rules of general games. Writing correct GDL descriptions can be challenging, especially for non-experts. Automated theorem proving has been proposed to assist game design by verifying if a GDL description satisfies desirable logical properties. However, when a description is proved to be faulty, the repair task itself can only be done manually. Motivated by the work on repairing unsolvable planning domain descriptions, we define a more general problem of finding minimal repairs for GDL descriptions that violate formal requirements, and we provide complexity results for various computational problems related to minimal repair. Moreover, we present an Answer Set Programming-based encoding for solving the minimal repair problem and demonstrate its application for automatically repairing ill-defined game descriptions.

NMR Workshop 2025 Conference Paper

Verification of General Games with QBF Solvers

• Yifan He 0008
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language (GDL) is a lightweight formalism for representing the rules of arbitrary finite perfect information games. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Coalition Logic (CL) is a logical framework capable of expressing strategic behaviors of a set of players that involve finitely many successive game states, which can formulate important properties such as whether one player can enforce a win of the game within a certain number of steps, regardless of the actions of the other players. In this paper, we investigate how to define the CL model-checking problem in the context of GGP and how to reason about CL properties of general games using Quantified Boolean Formula (QBF) solvers. This work extends our earlier AAMAS 2024 paper [1]. We evaluate the efficiency of our approach through a case study involving two-player general games and show that it has the potential to assist general game-playing agents with endgame analysis.

AAMAS Conference 2024 Conference Paper

Solving Two-player Games with QBF Solvers in General Game Playing

• Yifan He
• Abdallah Saffidine
• Michael Thielscher

Game solving is a relatively less explored area in general game playing. This paper introduces a translation from the Game Description Language GDL to Quantified Boolean Formulas (QBF) that lets us leverage QBF solvers to compute winning strategies in two-player games described in GDL. We implement this approach and measure the computation time needed by state-of-the-art QBF solvers on a range of two-player zero-sum turn-taking games. We introduce a variety of optimizations to the translation and evaluate them experimentally. Our empirical analysis establishes that our proposed approach is suitable for solving small games and can potentially help general game players evaluate endgame positions.

KR Conference 2024 Conference Paper

Verification of General Games with Imperfect Information Using Strategy Logic

• Yifan He
• Munyque Mittelmann
• Aniello Murano
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language with Imperfect Information (GDL-II) is a lightweight formalism for representing the rules of arbitrary games, including those where players have private information. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Epistemic Strategy Logic (SLK), on the other hand, is a rich logical framework for reasoning about multi-agent systems and the strategic behavior of agents with partial observability. To enable a general game-playing system to take advantage of this rich formalism for the automatic verification of properties of games, we present a formal translation from GDL-II to SLK models. We prove the correctness of this translation and show how crucial properties of general games, including playability and the existence of Nash equilibria, can be expressed as formulas in SLK. Finally, we demonstrate the application of an existing model-checking system for SLK to verify the properties of GDL-II games.

KR Conference 2023 Conference Paper

General Game Playing With State-Independent Communication

• Sean Zammit
• Michael Thielscher

Communication actions in games are usually given meaning by either the effect they have on the game state or a possible reduction in the size of the information set of an agent. However, this precludes analysis of games involving state-independent communication, in which players are given the ability to communicate with each other but are not required to be truthful. As such, these communication actions cannot be used to reduce the size of the information set or update beliefs in states without considering the intent of the communicating agent. In this paper, we introduce a language to describe the rules of such games as an extension of the Game Description Language (GDL). We also identify a set of scenarios involving state-independent communication actions in which an effective agent should be able to derive information, and propose and evaluate strategies for reasoning about such actions in these scenarios.

IJCAI Conference 2023 Conference Paper

On Optimal Strategies for Wordle and General Guessing Games

• Michael Cunanan
• Michael Thielscher

The recent popularity of Wordle has revived interest in guessing games. We develop a general method for finding optimal strategies for guessing games while avoiding an exhaustive search. Our main contribution are several theorems that build towards a general theory to prove optimality of a strategy for a guessing game. This work is developed to apply to any guessing game, but we use Wordle as an example to present concrete results.

AIJ Journal 2021 Journal Article

Game description language and dynamic epistemic logic compared

• Thorsten Engesser
• Robert Mattmüller
• Bernhard Nebel
• Michael Thielscher

Several different frameworks have been proposed to model and reason about knowledge in dynamic multi-agent settings, among them the logic-programming-based game description language GDL-III and dynamic epistemic logic (DEL). GDL-III and DEL have complementary strengths and weaknesses in terms of ease of modeling and simplicity of semantics. In this paper, we formally study the expressiveness of GDL-III vs. DEL. We clarify the commonalities and differences between those languages, demonstrate how to bridge the differences where possible, and identify large fragments of GDL-III and DEL that are equivalent in the sense that they can be used to encode games or planning tasks that admit the same legal action sequences. We prove the latter by providing translations between those fragments of GDL-III and DEL.

KR Conference 2021 Conference Paper

Representing and Reasoning with Event Models for Epistemic Planning

• David Rajaratnam
• Michael Thielscher

The standard representation formalism for multi-agent epistemic planning has one central disadvantage: When you use event models in dynamic epistemic logic (DEL) to describe the action of one agent, the model must specify not only the actual change and the change of that agent's knowledge. Also required is the epistemic change of any agents that may be observing the first agent performing the action, plus the epistemic change for any further agents that failed to observe that anything had taken place. To overcome the gap between this complex DEL notion of events and a more commonsense notion of actions, we propose a simple high-level action description language for multi-agent epistemic planning domains with just one type of effect laws: a causes x if y. Effect x can either be a physical effect, or an observation from an independent set that is specific to individual agents. We formally prove that any DEL event model can be described in this way. We show how this language provides a framework for expressing a variety of executability and action models; such as describing actions that are both ontic and epistemic, partially observable, or nondeterministic. We further combine our representation of event models with a description language for finitary initial epistemic theories, and we show how this allows us to reason about the effects of a sequence of actions in a multi-agent epistemic domain by updating a single multi-pointed epistemic model.

AAAI Conference 2020 Conference Paper

Deep Reinforcement Learning for General Game Playing

• Adrian Goldwaser
• Michael Thielscher

General Game Playing agents are required to play games they have never seen before simply by looking at a formal description of the rules of the game at runtime. Previous successful agents have been based on search with generic heuristics, with almost no work done into using machine learning. Recent advances in deep reinforcement learning have shown it to be successful in some two-player zero-sum board games such as Chess and Go. This work applies deep reinforcement learning to General Game Playing, extending the AlphaZero algorithm and finds that it can provide competitive results.

JAIR Journal 2019 Journal Article

General Game Playing with Imperfect Information

• Michael Schofield
• Michael Thielscher

General Game Playing is a field which allows the researcher to investigate techniques that might eventually be used in an agent capable of Artificial General Intelligence. Game playing presents a controlled environment in which to evaluate AI techniques, and so we have seen an increase in interest in this field of research. Games of imperfect information offer the researcher an additional challenge in terms of complexity over games with perfect information. In this article, we look at imperfect-information games: their expression, their complexity, and the additional demands of their players. We consider the problems of working with imperfect information and introduce a technique called HyperPlay, for efficiently sampling very large information sets, and present a formalism together with pseudo code so that others may implement it. We examine the design choices for the technique, show its soundness and completeness then provide some experimental results and demonstrate the use of the technique in a variety of imperfect-information games, revealing its strengths, weaknesses, and its efficiency against randomly generating samples. Improving the technique, we present HyperPlay-II, capable of correctly valuing information-gathering moves. Again, we provide some experimental results and demonstrate the use of the new technique revealing its strengths, weaknesses and its limitations.

IJCAI Conference 2018 Conference Paper

Game Description Language and Dynamic Epistemic Logic Compared

• Thorsten Engesser
• Robert Mattmüller
• Bernhard Nebel
• Michael Thielscher

Several different frameworks have been proposed to model and reason about knowledge in dynamic multi-agent settings, among them the logic-programming-based game description language GDL-III, and dynamic epistemic logic (DEL), based on possible-worlds semantics. GDL-III and DEL have complementary strengths and weaknesses in terms of ease of modeling and simplicity of semantics. In this paper, we formally study the expressiveness of GDL-III vs. DEL. We clarify the commonalities and differences between those languages, demonstrate how to bridge the differences where possible, and identify large fragments of GDL-III and DEL that are equivalent in the sense that they can be used to encode games or planning tasks that admit the same legal action sequences. We prove the latter by providing compilations between those fragments of GDL-III and DEL.

IJCAI Conference 2017 Conference Paper

GDL-III: A Description Language for Epistemic General Game Playing

• Michael Thielscher

GDL-III, a description language for general game playing with imperfect information and introspection, supports the specification of epistemic games. These are characterised by rules that depend on the knowledge of players. GDL-III provides a simpler language for representing actions and knowledge than existing formalisms: domain descriptions require neither explicit axioms about the epistemic effects of actions, nor explicit specifications of accessibility relations. We develop a formal semantics for GDL-III and demonstrate that this language, despite its syntactic simplicity, is expressive enough to model the famous Muddy Children domain. We also show that it significantly enhances the expressiveness of its predecessor GDL-II by formally proving that termination of games becomes undecidable, and we present experimental results with a reasoner for GDL-III applied to general epistemic puzzles.

AAAI Conference 2017 Conference Paper

The Efficiency of the HyperPlay Technique Over Random Sampling

• Michael Schofield
• Michael Thielscher

We show that the HyperPlay technique, which maintains a bag of updatable models for sampling an imperfect-information game, is more efficient than taking random samples of play sequences. Also, we demonstrate that random sampling may become impossible under the practical constraints of a game. We show the HyperPlay sample can become biased and not uniformly distributed across an information set and present a remedy for this bias, showing the impact on game results for biased and unbiased samples. We extrapolate the use of the technique beyond General Game Playing and in particular for enhanced security games with ingame percepts to facilitate a flexible defense response.

IJCAI Conference 2016 Conference Paper

A Framework for Integrating Symbolic and Sub-Symbolic Representations

• Keith Clark
• Bernhard Hengst
• Maurice Pagnucco
• David Rajaratnam
• Peter Robinson
• Claude Sammut
• Michael Thielscher

This paper establishes a framework that hierarchically integrates symbolic and sub-symbolic representations in an architecture for cognitive robotics. It is formalised abstractly as nodes in a hierarchy, with each node a sub-task that maintains its own belief-state and generates behaviour. An instantiation is developed for a real robot building towers of blocks, subject to human interference; this hierarchy uses a node with a concurrent multitasking teleo-reactive program, a node embedding a physics simulator to provide spatial knowledge, and nodes for sensor processing and robot control.

ECAI Conference 2016 Conference Paper

GDL-III: A Proposal to Extend the Game Description Language to General Epistemic Games

• Michael Thielscher

We propose an extension of the standard game description language for general game playing to include epistemic games, which are characterised by rules that depend on the knowledge of players. A single additional keyword suffices to define GDL-III, a general description language for games with imperfect information and introspection. We present an Answer Set Program for automatically reasoning about GDL-III games. Our extended language along with a suitable basic reasoning system can also be used to formalise and solve general epistemic puzzles.

AAAI Conference 2016 Conference Paper

Nested Monte Carlo Search for Two-Player Games

• Tristan Cazenave
• Abdallah Saffidine
• Michael Schofield
• Michael Thielscher

The use of the Monte Carlo playouts as an evaluation function has proved to be a viable, general technique for searching intractable game spaces. This facilitate the use of statistical techniques like Monte Carlo Tree Search (MCTS), but is also known to require significant processing overhead. We seek to improve the quality of information extracted from the Monte Carlo playout in three ways. Firstly, by nesting the evaluation function inside another evaluation function; secondly, by measuring and utilising the depth of the playout; and thirdly, by incorporating pruning strategies that eliminate unnecessary searches and avoid traps. Our experimental data, obtained on a variety of two-player games from past General Game Playing (GGP) competitions and others, demonstrate the usefulness of these techniques in a Nested Player when pitted against a standard, optimised UCT player.

IJCAI Conference 2016 Conference Paper

Sampling-Based Belief Revision

• Michael Thielscher

Model sampling has proved to be a practically viable method for decision-making under uncertainty, for example in imperfect-information games with large state spaces. In this paper, we examine the logical foundations of sampling-based belief revision. We show that it satisfies six of the standard AGM postulates but not Vacuity nor Subexpansion. We provide a corresponding representation theorem that generalises the standard result from a single to a family of faithful assignments for a given belief set. We also provide a formal axiomatisation of sampling-based belief revision in the Situation Calculus as an alternative way of reasoning about actions, sensing, and beliefs.

AAAI Conference 2015 Conference Paper

A Logic for Reasoning About Game Strategies

• Dongmo Zhang
• Michael Thielscher

This paper introduces a modal logic for reasoning about game strategies. The logic is based on a variant of the well-known game description language for describing game rules and further extends it with two modalities for reasoning about actions and strategies. We develop an axiomatic system and prove its soundness and completeness with respect to a specific semantics based on the state transition model of games. Interestingly, the completeness proof makes use of forgetting techniques that have been widely used in the KR&R literature. We demonstrate how general game-playing systems can apply the logic to develop game strategies.

IJCAI Conference 2015 Conference Paper

Execution Monitoring as Meta-Games for General Game-Playing Robots

• David Rajaratnam
• Michael Thielscher

General Game Playing aims to create AI systems that can understand the rules of new games and learn to play them effectively without human intervention. The recent proposal for general game-playing robots extends this to AI systems that play games in the real world. Execution monitoring becomes a necessity when moving from a virtual to a physical environment, because in reality actions may not be executed properly and (human) opponents may make illegal game moves. We develop a formal framework for execution monitoring by which an action theory that provides an axiomatic description of a game is automatically embedded in a meta-game for a robotic player — called the arbiter — whose role is to monitor and correct failed actions. This allows for the seamless encoding of recovery behaviours within a meta-game, enabling a robot to recover from these unexpected events.

AAAI Conference 2015 Conference Paper

Lifting Model Sampling for General Game Playing to Incomplete-Information Models

• Michael Schofield
• Michael Thielscher

General Game Playing is the design of AI systems able to understand the rules of new games and to use such descriptions to play those games effectively. Games with incomplete information have recently been added as a new challenge for general game-playing systems. The only published solutions to this challenge are based on sampling complete information models. In doing so they ground all of the unknown information, thereby making information gathering moves of no value; a well-known criticism of such sampling based systems. We present and analyse a method for escalating reasoning from complete information models to incomplete information models and show how this enables a general game player to correctly value information in incomplete information games. Experimental results demonstrate the success of this technique over standard model sampling.

ECAI Conference 2014 Conference Paper

A Systematic Solution to the (De-)Composition Problem in General Game Playing

• Timothy Joseph Cerexhe
• David Rajaratnam
• Abdallah Saffidine
• Michael Thielscher

General game players can drastically reduce the cost of search if they are able to solve smaller subproblems individually and synthesise the resulting solutions. To provide a systematic solution to this (de-)composition problem, we start off with generalising the standard decomposition problem in planning by allowing the composition of individual solutions to be further constrained by domain-dependent requirements of the global planning problem. We solve this generalised problem based on a systematic analysis of composition operators for transition systems, and we demonstrate how this solution can be further generalised to general game playing.

KR Conference 2014 Conference Paper

Forgetting in Action

• David Rajaratnam
• Hector Levesque
• Maurice Pagnucco
• Michael Thielscher

A further motivation for the concept of forgetting is evident in the formal analysis of security and cryptographic protocols. Cryptographic protocols have previously been analysed using the Situation Calculus equipped with a notion of the knowledge of agents (Delgrande, Hunter, and Grote 2010). However, such an encoding cannot always represent the class of nonmonotonic cryptographic protocols (Rubin and Honeyman 1994), where a notion of forgetting can be important. For example, in the analysis of credit card protocols it is a critical requirement to model vendors that forget (i. e., not retain) customer credit card details. In order to illustrate our approach to forgetting we consider the following running example. A robot needs to enter a room that is protected by a closed door with a keypad lock. When the robot senses that the door is closed, it needs to download the key combination from an external data source (e. g., the cloud or a database). It can then use this key combination to open the door and enter the room. Furthermore, since the door will now be open, the robot no longer needs the key combination, so is free to forget this information. The rest of the paper proceeds as follows. First we introduce the Situation Calculus (McCarthy 1963; Reiter 2001) and its epistemic extension (Lesperance et al. 1995) that allows for knowledge acquisition without forgetting. We then present our approach that handles both knowledge acquisition and forgetting and perform an extensive analysis of its properties and the conditions under which both knowledge acquisition and forgetting can occur. Having established our approach to forgetting, we then place it within the broader context of two of the main models that have been developed within the literature: AGM belief revision (Alchourrón, Gärdenfors, and Makinson 1985) and logical forgetting (Lin and Reiter 1994). In particular, we show that our approach is well-behaved with respect to the AGM belief contraction postulates, but is distinct from that of logical forgetting since knowledge forgetting can provide for more fine-grained control over what is forgotten. Finally, we provide some concluding remarks and discuss directions for future research. In this paper we develop a general framework that allows for both knowledge acquisition and forgetting in the Situation Calculus. Based on the Scherl and Levesque (Scherl and Levesque 1993) possible worlds approach to knowledge in the Situation Calculus, we allow for both sensing as well as explicit forgetting actions. This model of forgetting is then compared to existing frameworks. In particular we show that forgetting is well-behaved with respect to the contraction operator of the well-known AGM theory of belief revision (Alchourrón, Gärdenfors, and Makinson 1985) but that knowledge forgetting is distinct from the more commonly known notion of logical forgetting (Lin and Reiter 1994).

AAAI Conference 2014 Conference Paper

Solving the Inferential Frame Problem in the General Game Description Language

• Javier Romero Davila
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language GDL is the standard input language for general game-playing systems. While players can gain a lot of traction by an efficient inference algorithm for GDL, state-of-the-art reasoners suffer from a variant of a classical KR problem, the inferential frame problem. We present a method by which general game players can transform any given game description into a representation that solves this problem. Our experimental results demonstrate that with the help of automatically generated domain knowledge, a significant speedup can thus be obtained for the majority of the game descriptions from the AAAI competition.

AAAI Conference 2013 Conference Paper

Filtering With Logic Programs and Its Application to General Game Playing

• Michael Thielscher

Motivated by the problem of building a basic reasoner for general game playing with imperfect information, we address the problem of filtering with logic programs, whereby an agent updates its incomplete knowledge of a program by observations. We develop a filtering method by adapting an existing backward-chaining and abduction method for so-called open logic programs. Experimental results show that this provides a basic effective and efficient “legal” player for general imperfect-information games.

KR Conference 2012 Conference Paper

Automated Verification of Epistemic Properties for General Game Playing

• Sebastian Haufe
• Michael Thielscher

(Thielscher 2010) poses new challenges to both designer and player of a general game. Fundamental issues such as the knowledge of a player about its legal moves, game termination, or its opponents’ viewpoints are no longer obvious. The designer of a game must endow players with sufficient information to guarantee that the game is playable, and players themselves require reliable information about the game state to maximise their utility. Gaining this knowledge is an intricate reasoning task over the game rules, and its automation is of major assistance for the game designer and essential for a successful general game-playing program. In this paper, we provide such an automated reasoning method for epistemic properties by fundamentally extending our proof method for state sequence invariants. To this end, we specify syntax and semantics of a formula language for the expression of epistemic game knowledge; we develop an inductive proof theory that allows to verify “positive” epistemic formulas against a given game specification without analysis of the entire game tree; we prove the correctness of our proof theory; and we demonstrate its efficiency by reporting on experiments with a practical implementation. Automatically deriving properties of new games is one of the fundamental challenges for general game-playing systems, whose task is to learn to play any previously unknown game solely by being given the rules of that game. A recently developed method uses Answer Set Programming for verifying finitely-bounded temporal invariance properties against a given game description by structural induction. Addressing the new challenge posed by the recent extension of the general Game Description Language to include games with imperfect information and randomness, we extend this method to epistemic properties about games. We formally prove this extension to be correct, and we report on experiments that show its practical applicability.

AIJ Journal 2012 Journal Article

Automated verification of state sequence invariants in general game playing

• Sebastian Haufe
• Stephan Schiffel
• Michael Thielscher

A general game player is a system that can play previously unknown games given nothing but their rules. Many of the existing successful approaches to general game playing require to generate some form of game-specific knowledge, but when current systems establish knowledge they rely on the approximate method of playing random sample matches rather than formally proving knowledge. In this paper, we present a theoretically founded and practically viable method for automatically verifying properties of games whose rules are given in the general Game Description Language (GDL). We introduce a simple formal language to describe game-specific knowledge as state sequence invariants, and we provide a proof theory for verifying these invariants with the help of Answer Set Programming. We prove the correctness of this method against the formal semantics for GDL, and we report on extensive experiments with a practical implementation of this proof system, which show that our method of formally proving knowledge is viable for the practice of general game playing.

AAAI Conference 2012 Conference Paper

HyperPlay: A Solution to General Game Playing with Imperfect Information

• Michael Schofield
• Timothy Cerexhe
• Michael Thielscher

General Game Playing is the design of AI systems able to understand the rules of new games and to use such descriptions to play those games effectively. Games with imperfect information have recently been added as a new challenge for existing general game-playing systems. The HyperPlay technique presents a solution to this challenge by maintaining a collection of models of the true game as a foundation for reasoning, and move selection. The technique provides existing game players with a bolt-on solution to convert from perfectinformation games to imperfect-information games. In this paper we describe the HyperPlay technique, show how it was adapted for use with a Monte Carlo decision making process and give experimental results for its performance.

ECAI Conference 2012 Conference Paper

Strategic and Epistemic Reasoning for the Game Description Language GDL-II

• Ji Ruan
• Michael Thielscher

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 to describe nondeterministic games with any number of players who may have incomplete, asymmetric information. In this paper, we show how the well-known Alternating-time Temporal Epistemic Logic (ATEL) can be adapted for strategic and epistemic reasoning about general games described in GDL-II. We provide a semantic characterisation of GDL-II descriptions in terms of ATEL models. We also provide a syntactic translation of GDL-II descriptions into ATEL formulas, and we prove that these two characterisations are equivalent. We show that model checking in this setting is decidable by giving an algorithm, and we demonstrate how our results can be used to verify strategic and epistemic properties of games described in GDL-II.

AIJ Journal 2011 Journal Article

A unifying action calculus

• Michael Thielscher

McCarthy's Situation Calculus is arguably the oldest special-purpose knowledge representation formalism, designed to axiomatize knowledge of actions and their effects. Four decades of research in this area have led to a variety of alternative formalisms: While some approaches can be considered instances or extensions of the classical Situation Calculus, like Reiter's successor state axioms or the Fluent Calculus, there are also special planning languages like ADL and approaches based on a linear (rather than branching) time structure like the Event Calculus. The co-existence of many different calculi has two main disadvantages: The formal relations among them is a largely open issue, and a lot of today's research concerns the transfer of specific results from one approach to another. In this paper, we present a unifying action calculus, which encompasses (well-defined classes of) all of the aforementioned formalisms. Our calculus not only facilitates comparisons and translations between specific approaches, it also allows to solve interesting problems for various calculi at once. We exemplify this by providing a general, calculus-independent solution to a problem of practical relevance, which is intimately related to McCarthy's quest for elaboration tolerant formalisms: the modularity of domain axiomatizations.

AAAI Conference 2011 Conference Paper

Reasoning About General Games Described in GDL-II

• Stephan Schiffel
• Michael Thielscher

Recently the general Game Description Language (GDL) has been extended so as to cover arbitrary games with incomplete/imperfect information. Learning—without human intervention—to play such games poses a reasoning challenge for general game-playing systems that is much more intricate than in case of complete information games. Action formalisms like the Situation Calculus have been developed for precisely this purpose. In this paper we present a full embedding of the Game Description Language into the Situation Calculus (with Scherl and Levesque’s knowledge fluent). We formally prove that this provides a sound and complete reasoning method for players’ knowledge about game states as well as about the knowledge of the other players.

AAAI Conference 2011 Conference Paper

The Epistemic Logic Behind the Game Description Language

• Ji Ruan
• Michael Thielscher

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 game description language GDL, a variant of Datalog with function symbols and a few known keywords. In its latest version GDL allows to describe nondeterministic games with any number of players who may have imperfect, asymmetric information. We analyse the epistemic structure and expressiveness of this language in terms of epistemic modal logic and present 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) multiagent epistemic model.

IJCAI Conference 2011 Conference Paper

The General Game Playing Description Language Is Universal

• Michael Thielscher

The Game Description Language is a high-level, rule-based formalisms for communicating the rules of arbitrary games to general game-playing systems, whose challenging task is to learn to play previously unknown games without human intervention. Originally designed for deterministic games with complete information about the game state, the language was recently extended to include randomness and imperfect information. However, determining the extent to which this enhancement allows to describe truly arbitrary games was left as an open problem. We provide a positive answer to this question by relating the extended Game Description Language to the universal, mathematical concept of extensive-form games, proving that indeed just any such game can be described faithfully.

AAAI Conference 2010 Conference Paper

A General Game Description Language for Incomplete Information Games

• Michael Thielscher

A General Game Player is a system that can play previously unknown games given nothing but their rules. The Game Description Language (GDL) has been developed as a highlevel knowledge representation formalism for axiomatising the rules of any game, and a basic requirement of a General Game Player is the ability to reason logically about a given game description. In this paper, we address the fundamental limitation of existing GDL to be confined to deterministic games with complete information about the game state. To this end, we develop an extension of GDL that is both simple and elegant yet expressive enough to allow to formalise the rules of arbitrary (discrete and finite) n-player games with randomness and incomplete state knowledge. We also show that this extension suffices to provide players with all information they need to reason about their own knowledge as well as that of the other players up front and during game play.

AAAI Conference 2010 Conference Paper

A Temporal Proof System for General Game Playing

• Michael Thielscher
• Sebastian Voigt

A general game player is a system that understands the rules of unknown games and learns to play these games well without human intervention. A major challenge for research in General Game Playing is to endow a player with the ability to extract and prove game-specific knowledge from the mere game rules. We define a formal language to express temporally extended—yet local—properties of games. We also develop a provably correct proof theory for this language using the paradigm of Answer Set Programming, and we report on experiments with a practical implementation of this proof system in combination with a successful general game player.

KR Conference 2010 Conference Paper

Integrating Action Calculi and AgentSpeak: Closing the Gap

• Michael Thielscher

Existing action calculi provide rich, declarative formalisms for reasoning about actions. BDI-based programming languages like AgentSpeak, on the other hand, are procedural and geared towards practical applications of cognitive agents. In this paper, we close the gap between these two lines of research by integrating action calculi and AgentSpeak programs. Specifically, we develop a new and purely declarative semantics for AgentSpeak, which paves the way for combining this language with any suitable action calculus in a strictly modular fashion. As the main technical result, we prove that the new declarative semantics is correct wrt. the standard operational semantics for AgentSpeak. This provides the basis for a modular integration of a BDIbased agent programming language with sophisticated methods for reasoning about actions.

KR Conference 2010 Conference Paper

State Defaults and Ramifications in the Unifying Action Calculus

• Ringo Baumann
• Gerhard Brewka
• Hannes Strass
• Michael Thielscher
• Vadim Zaslawski

We present a framework for reasoning about actions that not only solves the frame and ramification problems, but also the state default problem—the problem to determine what normally holds at a given time point. Yet, the framework is general enough not to be tied to a specific time structure. This is achieved as follows: We use effect axioms that draw ideas both from Reiter’s successor state axioms and the nonmonotonic causal theories by Giunchiglia et al. These axioms are formulated in a recently proposed unifying action calculus to guarantee independence of a specific underlying notion of time. Reiter’s default logic is then wrapped around the resulting calculus and plays a key role in solving the ramification as well as the state default problem.

IJCAI Conference 2009 Conference Paper

• Stephan Schiffel
• Michael Thielscher

A general game player is a system that understands the rules of an unknown game and learns to play this game well without human intervention. To succeed in this endeavor, systems need to be able to extract and prove game-specific knowledge from the mere game rules. We present a practical approach to this challenge with the help of Answer Set Programming. The key idea is to reduce the automated theorem proving task to a simple proof of an induction step and its base case. We prove correctness of this method and report on experiments with an offthe-shelf Answer Set Programming system in combination with a successful general game player.

ICAART Conference 2009 Conference Paper

Specifying Multiagent Environments Systems in the Game Description Language

• Stephan Schiffel
• Michael Thielscher

The Game Description Language (GDL) has been developed for the purpose of formalizing game rules. It serves as the input language for general game players, which are systems that learn to play previously unknown games without human intervention. In this paper, we show that GDL can be readily used as a specification language for a large class of multiagent environments. The resulting specifications are declarative, compact, and easy to understand and maintain. At the same time they can be fully automatically understood and used by autonomous agents who intend to participate in these environments. Our main result is a formal characterization of the class of multiagent environments that can be described in GDL.

JELIA Conference 2008 Conference Paper

A Fluent Calculus Semantics for ADL with Plan Constraints

• Conrad Drescher
• Michael Thielscher

Abstract Plan constraints are the most recent addition to the ever growing Planning Domain Definition Language (PDDL). In this work we consider the PDDL fragment consisting of basic ADL extended by plan constraints. We provide a purely declarative semantics for this fragment by interpreting it in the basic Fluent Calculus. We thus obtain a logical semantics for this fragment of PDDL instead of the usual meta-theoretical state transition semantics.

AIJ Journal 2007 Journal Article

Iterated belief revision, revised

• Yi Jin
• Michael Thielscher

The AGM postulates for belief revision, augmented by the DP postulates for iterated belief revision, provide widely accepted criteria for the design of operators by which intelligent agents adapt their beliefs incrementally to new information. These postulates alone, however, are too permissive: They support operators by which all newly acquired information is canceled as soon as an agent learns a fact that contradicts some of its current beliefs. In this paper, we present a formal analysis of the deficiency of the standard postulates alone, and we show how to solve the problem by an additional postulate of independence. We give a representation theorem for this postulate and prove that it is compatible with AGM and DP.

AAAI Conference 2006 Conference Paper

Reconciling Situation Calculus and Fluent Calculus

• Stephan Schiffel
• Michael Thielscher

The Situation Calculus and the Fluent Calculus are successful action formalisms that share many concepts. But until now there is no formal relation between the two calculi that would allow to formally analyze the relationship between the two approaches as well as between the programming languages based on them, Golog and FLUX. Furthermore, such a formal relation would allow to combine Golog and FLUX and to analyze which of the underlying computation principles is better suited for different classes of programs. We develop a formal translation between domain axiomatizations of the Situation Calculus and the Fluent Calculus and present a Fluent Calculus semantics for Golog programs. For domains with deterministic actions our approach allows an automatic translation of Golog domain descriptions and execution of Golog programs with FLUX.

KR Conference 2006 Conference Paper

The Features-and-Fluents Semantics for the Fluent Calculus

• Michael Thielscher
• Thomas Witkowski

Based on an elaborate ontological taxonomy, the Features-and-Fluents framework provides an independent action semantics for assessing the range of applicability of action calculi. In this paper, we show how the fluent calculus can be used to capture the full range of phenomena in K-IA, the broadest ontological class that has been fully formalized in (Sandewall 1994). To this end, we develop a significant extension of the fluent calculus for modeling actions with durations and with specific trajectories of changes. We present a provably correct translation of scenario descriptions from the Features-and-Fluents semantics into fluent calculus axiomatizations.

KR Conference 2004 Conference Paper

Knowledge of Other Agents and Communicative Actions in the Fluent Calculus

• Yves Martin
• Iman Narasamdya
• Michael Thielscher

The Fluent Calculus has largely been focused on building agents that work individually. However, agents often need to interact with each other to learn more about their environment as well as to achieve their goals. One form of interaction is by means of communication. Effective, goal--oriented communication requires knowledge of other agents. This paper studies the problem of endowing agents with the ability to reason about the knowledge of other agents and with communication skills. Our formalism for the knowledge of other agents generalizes the existing notion of knowledge in the Fluent Calculus. Communication is treated as actions which are called communicative actions. The specification of communicative actions is based on the formalism for the knowledge of other agents. We have also developed an implementation of the theory as an extension to FLUX, which is a programming method that allows to design intelligent agents based on the Fluent Calculus.

ICAPS Conference 2004 Conference Paper

Knowledge of Other Agents and Communicative Actions in the Fluent Calculus

• Yves Martin
• Iman Narasamdya
• Michael Thielscher

The Fluent Calculus has largely been focused on building agents that work individually. However, agents often need to interact with each other to learn more about their environment as well as to achieve their goals. One form of interaction is by means of communication. Effective, goal-oriented communication requires knowledge of other agents. This paper studies the problem of endowing agents with the ability to reason about the knowledge of other agents and with communication skills. Our formalism for the knowledge of other agents generalizes the existing notion of knowledge in the Fluent Calculus. Communication is treated as actions which are called communicative actions. The specification of communicative actions is based on the formalism for the knowledge of other agents. We have also developed an implementation of the theory as an extension to FLUX, which is a programming method that allows to design intelligent agents based on the Fluent Calculus.

ECAI Conference 2004 Conference Paper

Representing Beliefs in the Fluent Calculus

• Yi Jin 0006
• Michael Thielscher

KR Conference 2002 Conference Paper

Programming of Reasoning and Planning Agents with FLUX

• Michael Thielscher

AIJ Journal 2001 Journal Article

The Qualification Problem: A solution to the problem of anomalous models

• Michael Thielscher

Intelligent agents in open environments inevitably face the Qualification Problem: The executability of an action can never be predicted with absolute certainty; unexpected circumstances, albeit unlikely, may at any time prevent the successful performance of an action. Reasoning agents in real-world environments rely on a solution to the Qualification Problem in order to make useful predictions but also to explain and recover from unexpected action failures. Yet the main theoretical result known today in this context is a negative one: While a solution to the Qualification Problem requires to assume away by default abnormal qualifications of actions, straightforward minimization of abnormality falls prey to the production of anomalous models. We present an approach to the Qualification Problem which resolves this anomaly. Anomalous models are shown to arise from ignoring causality, and they are avoided by appealing to just this concept. Our theory builds on the established predicate logic formalism of the Fluent Calculus as a solution to the Frame Problem and to the Ramification Problem in reasoning about actions. The monotonic Fluent Calculus is enhanced by a default theory in order to obtain the nonmonotonic approach called for by the Qualification Problem. The approach has been implemented in an action programming language based on the Fluent Calculus and successfully applied to the high-level control of robots.

AAAI Conference 2000 Conference Paper

Modeling Actions with Ramifications in Nondeterministic, Concurrent, and Continuous Domains and a Case Study

• Michael Thielscher

Combining into a consistent theory co-existing models for different phenomena in reasoning about actions can be a problem as challenging as addressing new aspects. We present a uniform theory for reasoning about actions with indirect effects in nondeterministic, concurrent, and continuous domains. We report on a case study to which our theory has been successfully applied.

AIJ Journal 1999 Journal Article

From situation calculus to fluent calculus: State update axioms as a solution to the inferential frame problem

• Michael Thielscher

Successor state axioms provide a solution to the famous Frame Problem as far as the representational aspect is concerned. Solving in classical, monotonic logic the additional inferential Frame Problem, on the other hand, was the major motivation for the development of the Fluent Calculus a decade or so ago. Yet the expressiveness of the latter in comparison to the Situation Calculus remained a largely open question until today. In this note, we derive a novel version of the Fluent Calculus by gradually applying the principle of reification to successor state axioms in order to address the inferential Frame Problem without losing the representational merits. Our approach results in a fully mechanic method for the generation of state update axioms from any collection of Situation Calculus-style effect axioms for deterministic actions, provided the actions do not have potentially infinitely many effects. The axiomatization thus obtained is proved essentially equivalent to the corresponding axiomatization which uses successor state axioms.

AIJ Journal 1998 Journal Article

Reasoning about actions: steady versus stabilizing state constraints

• Michael Thielscher

In formal approaches to commonsense reasoning about actions, the Ramification Problem denotes the problem of handling indirect effects which implicitly derive from so-called state constraints. We pursue a new distinction between two kinds of state constraints which will be proved crucially important for solving the general Ramification Problem. Steady constraints never, not even for an instant, cease being in force. As such they give rise to truly instantaneous indirect effects of actions. Stabilizing state constraints, on the other hand, may be suspended for a short period of time after an action has occurred. Indirect effects deriving from these constraints materialize with a short lag. This hitherto neglected distinction is shown to have essential impact on the Ramification Problem: if stabilizing state constraints interact, then approaches not based on so-called causal propagation prove defective. But causal propagation, too, is shown to risk producing anomalous models, in case steady and stabilizing indirect effects are propagated indiscriminately. Motivated by these two observations, we improve the theory of causal relationships and its Fluent Calculus axiomatization, which both are methods of causal propagation, so as to properly handle the distinction between steady and stabilizing constraints.

AAAI Conference 1997 Conference Paper

Qualified Ramifications

• Michael Thielscher

We consider the problem of ramifications, i. e. , indirect effects of actions, having exceptions. It is argued that straightforward minimization of abnormality is insufficient in this context. Taking a recent causality-based solution to the plain Ramification Problem as starting point, we develop an action theory that is shown to successfully address this amalgamation of Ramification and Qualification Problem.

AIJ Journal 1997 Journal Article

Ramification and causality

• Michael Thielscher

In formal systems for reasoning about actions, the ramification problem denotes the problem of handling indirect effects. These effects are not explicitly represented in action specifications but follow from general laws describing dependencies among components of the world state. An adequate treatment of indirect effects requires a suitably weakened version of the general law of persistence. It also requires a method to avoid unintuitive changes suggested by the aforementioned dependency laws. We propose a solution to the ramification problem that uses directed relations between two single effects, stating the circumstances under which the occurrence of the first causes the second. We argue for the necessity of an approach based on causality by elaborating the limitations of common paradigms employed to handle ramifications—the principle of categorization and the policy of minimal change. Our abstract solution is realized on the basis of a particular action calculus, namely, the fluent calculus.

LOPSTR Conference 1996 Conference Paper

Solving Deductive Planning Problems Using Program Analysis and Transformation

• D. Andre de Waal
• Michael Thielscher

Abstract Two general, problematic aspects of deductive planning, namely, detecting unsolvable planning problems and solving a certain kind of postdiction problem, are investigated. The work is based on a resource oriented approach to reasoning about actions and change using a logic programming paradigm. We show that ordinary resolution methods are insufficient for solving these problems and propose program analysis and transformation as a more promising and successful way to solve them.

IJCAI Conference 1995 Conference Paper

Computing Ramifications by Post processing

• Michael Thielscher

AIJ Journal 1993 Journal Article

On prediction in theorist

• Michael Thielscher

Theorist is a well-known framework and system for nonmonotonic reasoning which provides mechanisms for dealing with both explanations for observations and skeptical prediction. Its current implementation, developed by David Poole and co-workers, uses an algorithm for prediction which holds for a restricted part of Theorist. In more general cases, the system produces incorrect results in the case of prediction. In this note, we present an algorithm for prediction which is shown to be correct within the entire Theorist framework.