Game-theoretic semantics for ATL(+) with applications to model checking

2021. Valentin Goranko, Antti Kuusisto, Raine Rönnholm. Information and Computation 276

Article

We develop a game-theoretic semantics (GTS) for the fragment ATL(+) of the alternating-time temporal logic ATL*, thereby extending the recently introduced GTS for ATL. We show that the game-theoretic semantics is equivalent to the standard compositional semantics of ATL(+) with perfect-recall strategies. Based on the new semantics, we provide an analysis of the memory and time resources needed for model checking ATL(+) and show that strategies of the verifier that use only a very limited amount of memory suffice. Furthermore, using the GTS, we provide a new algorithm for model checking ATL(+) and identify a natural hierarchy of tractable fragments of ATL(+) that substantially extend ATL.

Rational coordination with no communication or conventions

2020. Valentin Goranko, Antti Kuusisto, Raine Rönnholm. Journal of logic and computation (Print) 30 (6), 1183-1211

Article

We study pure coordination games where in every outcome, all players have identical payoffs, ‘win’ or ‘lose’. We identify and discuss a range of ‘purely rational principles’ guiding the reasoning of rational players in such games and compare the classes of coordination games that can be solved by such players with no preplay communication or conventions. We observe that it is highly nontrivial to delineate a boundary between purely rational principles and other decision methods, such as conventions, for solving such coordination games.

Temporal Logic

2020. Valentin Goranko, Antje Rumberg. Stanford Encyclopedia of Philosophy

Article

Logic-based specification and verification of homogeneous dynamic multi-agent systems

2020. Riccardo De Masellis, Valentin Goranko. Autonomous Agents and Multi-Agent Systems 34 (2)

Article

We develop a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems. Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. The state transitions are therefore determined only by the vector of numbers of agents performing each action and are specified symbolically, by means of conditions on these numbers definable in Presburger arithmetic. The agents are divided into controllable (by the system supervisor/controller) and uncontrollable, representing the environment or adversary. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a language for formal specification we use a suitably extended version of Alternating-time Temporal Logic, where one can specify properties of the type a coalition of (at least) n controllable agents can ensure against (at most) m uncontrollable agents that any possible evolution of the system satisfies a given objective ., where is specified again as a formula of that language and each of n and m is either a fixed number or a variable that can be quantified over. We provide formal semantics to our logic L HDMAS and define normal form of its formulae. We then prove that every formula in L HDMAS is equivalent in the finite to one in a normal form and develop an algorithm for global model checking of formulae in normal form in finite HDMAS models, which invokes model checking truth of Presburger formulae. We establish worst case complexity estimates for the model checking algorithm and illustrate it on a running example.

Hybrid Deduction–Refutation Systems

2019. Valentin Goranko. Axioms 8 (4)

Article

Hybrid deduction–refutation systems are deductive systems intended to derive both valid and non-valid, i.e., semantically refutable, formulae of a given logical system, by employing together separate derivability operators for each of these and combining ‘hybrid derivation rules’ that involve both deduction and refutation. The goal of this paper is to develop a basic theory and ‘meta-proof’ theory of hybrid deduction–refutation systems. I then illustrate the concept on a hybrid derivation system of natural deduction for classical propositional logic, for which I show soundness and completeness for both deductions and refutations.

Towards a Logic for Conditional Local Strategic Reasoning

2019. Valentin Goranko, Fengkui Ju. Logic, Rationality, and Interaction, 112-125

Conference

We consider systems of rational agents who act in pursuit of their individual and collective objectives and we study the reasoning of an agent or an external observer about the consequences from the expected choices of action of the other agents based on their objectives, in order to assess the reasoner’s ability to achieve his own objective.

To formalize such reasoning we introduce new modal operators of conditional strategic reasoning and use them to extend Coalition Logic in order to capture variations of conditional strategic reasoning. We provide formal semantics for the new conditional strategic operators, introduce the matching notion of bisimulation for each of them and discuss and compare briefly their expressiveness.

A logic for temporal conditionals and a solution to the Sea Battle Puzzle

2018. Fengkui Ju, Gianluca Grilletti, Valentin Goranko. Advances in Modal Logic, 379-398

Conference

Temporal reasoning with conditionals is more complex than both classical temporal reasoning and reasoning with timeless conditionals, and can lead to some rather counter-intuitive conclusions. For instance, Aristotle’s famous “Sea Battle Tomorrow” puzzle leads to a fatalistic conclusion: whether there will be a sea battle tomorrow or not, but that is necessarily the case now. We propose a branching-time logic LTC to formalise reasoning about temporal conditionals and provide that logic with adequate formal semantics. The logic LTC extends the Nexttime fragment of CTL∗ , with operators for model updates, restricting the domain to only future moments where antecedent is still possible to satisfy. We provide formal semantics for these operators that implements the restrictor interpretation of antecedents of temporalized conditionals, by suitably restricting the domain of discourse. As a motivating example, we demonstrate that a naturally formalised in our logic version of the ‘Sea Battle’ argument renders it unsound, thereby providing a solution to the problem with fatalist conclusion that it entails, because its underlying reasoning per cases argument no longer applies when these cases are treated not as material implications but as temporal conditionals. On the technical side, we analyze the semantics of LTC and provide a series of reductions of LTC-formulae, first recursively eliminating the dynamic update operators and then the path quantifiers in such formulae. Using these reductions we obtain a sound and complete axiomatization for LTC, and reduce its decision problem to that of the modal logic KD.

LOGICS FOR PROPOSITIONAL DETERMINACY AND INDEPENDENCE

2018. Valentin Goranko, Antti Kuusisto. The Review of Symbolic Logic 11 (3), 470-506

Article

We introduce and study formal logics for reasoning about propositional determinacy and independence. These relate naturally with the philosophical concept of supervenience, which can also be regarded as a generalisation of logical consequence. Propositional Dependence Logic D, and Propositional Independence Logic I are recently developed logical systems, based on team semantics, that provide a framework for such reasoning tasks. We introduce two new logics L_D and L_I, based on Kripke semantics, and propose them as alternatives for D and I, respectively. We analyse and compare the relative expressive powers of these four logics and also discuss how they relate to the natural language use and meaning of the concepts of determinacy and independence. We argue that L_D and L_I naturally resolve a range of interpretational problems that arise in D and I. We also obtain sound and complete axiomatizations for L_D and L_I and relate them with the recently studied inquisitive logics and their semantics.

Socially Friendly and Group Protecting Coalition Logics

2018. Valentin Goranko, Sebastian Enqvist. Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2018), 372-380

Conference

We consider extensions of Coalition Logic (CL) which can express statements about inter-related powers of coalitions to achieve their respective goals. In particular, we introduce and study two new extensions of CL. One of them is the “Socially Friendly Coalition Logic” SFCL, which is also a multi-agent extension of the recently introduced “Instantial Neighborhood Logic” INL. SFCL can express the claim that a coalition has a collective strategy to guarantee achieving its explicitly stated goal while acting in a ‘socially friendly way’, by enabling the remaining agents to achieve other (again, explicitly stated) goals of their choice. The other new extension is the “Group Protecting Coalition Logic” GPCL which enables reasoning about entire coalitional goal assignments, in which every group of agents has its own specified goal. GPCL can express claims to the effect that there is an action profile of the grand coalition such that, by playing it, every sub-coalition of agents can guarantee satisfaction of its own private goal (and thus, protect its own interests) while acting towards achievement of the common goal of the grand coalition. For each of these logics, we discuss its expressiveness, introduce the respective notion of bisimulation and prove bisimulation invariance and Hennessy-Milner property. We then also present sound and complete axiomatic systems and prove decidability for both logics.

Logic as a Tool

2016. Valentin Goranko.

Book

The book explains the grammar, semantics and use of classical logical languages and teaches the reader how grasp the meaning and translate them to and from natural language. It illustrates with extensive examples the use of the most popular deductive systems -- axiomatic systems, semantic tableaux, natural deduction, and resolution -- for formalising and automating logical reasoning both on propositional and on first-order level, and provides the reader with technical skills needed for practical derivations in them. Systematic guidelines are offered on how to perform logically correct and well-structured reasoning using these deductive systems and the reasoning techniques that they employ.

Big Brother Logic

2016. Olivier Gasquet, Valentin Goranko, François Schwarzentruber. Autonomous Agents and Multi-Agent Systems 30 (5), 793-825

Article

We consider multi-agent scenarios where each agent controls a surveillance camera in the plane, with fixed position and angle of vision, but rotating freely. The agents can thus observe the surroundings and each other. They can also reason about each other’s observation abilities and knowledge derived from these observations. We introduce suitable logical languages for reasoning about such scenarios which involve atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of cameras to turn around in order to reach positions satisfying formulae in the language. We also consider effects of public announcements. We introduce several different but equivalent versions of the semantics for these languages, discuss their expressiveness and provide translations in PDL style. Using these translations we develop algorithms and obtain complexity results for model checking and satisfiability testing for the basic logic BBL that we introduce here and for some of its extensions. Notably, we show that even for the extension with common knowledge, model checking and satisfiability testing remain in PSPACE. We also discuss the sensitivity of the set of validities to the admissible angles of vision of the agents’ cameras. Finally, we discuss some further extensions: adding obstacles, positioning the cameras in 3D or enabling them to change positions. Our work has potential applications to automated reasoning, formal specification and verification of observational abilities and knowledge of multi-robot systems.

Temporal logics in computer science

2016. Stephane Demri, Valentin Goranko, Martin Lange.

Book

This comprehensive text provides a modern and technically precise exposition of the fundamental theory and applications of temporal logics in computer science. Part I presents the basics of discrete transition systems, including constructions and behavioural equivalences. Part II examines the most important temporal logics for transition systems and Part III looks at their expressiveness and complexity. Finally, Part IV describes the main computational methods and decision procedures for model checking and model building - based on tableaux, automata and games - and discusses their relationships. The book contains a wealth of examples and exercises, as well as an extensive annotated bibliography. Thus, the book is not only a solid professional reference for researchers in the field but also a comprehensive graduate textbook that can be used for self-study as well as for teaching courses.

Knowledge and Ability

2015. Thomas Ågotnes (et al.). Handbook of Epistemic Logic, 543-589

Chapter

In this chapter we relate epistemic logics with logics for strategic ability developed and studied in computer science, artificial intelligence and multi-agent systems. We discuss approaches from philosophy and artificial intelligence to modelling the interaction of agents’ knowledge and abilities and then focus on concurrent game models and the alternating-time temporal logic ATL. We show how ATL enables reasoning about agents’ coalitional abilities to achieve qualitative objectives in concurrent game models, first assuming complete information and then under incomplete information and uncertainty about the structureof the game model. We then discuss epistemic extensions of ATL enabling explicit reasoning about the interaction of knowledge and strategic abilities on different epistemic levels, leading inter alia to the notion of constructive knowledge.

Logic and Discrete Mathematics

2015. Willem Conradie, Valentin Goranko.

Book

This book features a unique combination of comprehensive coverage of logic with a solid exposition of the most important fields of discrete mathematics, presenting material that has been tested and refined by the authors in university courses taught over more than a decade.

The chapters on logic - propositional and first-order - provide a robust toolkit for logical reasoning, emphasizing the conceptual understanding of the language and the semantics of classical logic as well as practical applications through the easy to understand and use deductive systems of Semantic Tableaux and Resolution. The chapters on set theory, number theory, combinatorics and graph theory combine the necessary minimum of theory with numerous examples and selected applications. Written in a clear and reader-friendly style, each section ends with an extensive set of exercises, most of them provided with complete solutions which are available in the accompanying solutions manual.

Logics for reasoning about strategic abilities in multi-player games

2015. Nils Bulling, Valentin Goranko, Wojciech Jamroga. Models of strategic reasoning, 93-136

Chapter

We introduce and discuss basic concepts, ideas, and logical formalisms used for reasoning about strategic abilities in multi-player games. In particular, we present concurrent game models and the alternating time temporal logic ATL∗ and its fragment ATL. We discuss variations of the language and semantics of ATL∗ that take into account the limitations and complications arising from incomplete information, perfect or imperfect memory of players, reasoning within dynamically changing strategy contexts, or using stronger, constructive concepts of strategy. Finally, we briefly summarize some technical results regarding decision problems for some variants of ATL.

Valentin Goranko

About me

Teaching

Research

Publications

Game-theoretic semantics for ATL(+) with applications to model checking

Rational coordination with no communication or conventions

Temporal Logic

Logic-based specification and verification of homogeneous dynamic multi-agent systems

Hybrid Deduction–Refutation Systems

Towards a Logic for Conditional Local Strategic Reasoning

A logic for temporal conditionals and a solution to the Sea Battle Puzzle

LOGICS FOR PROPOSITIONAL DETERMINACY AND INDEPENDENCE

Socially Friendly and Group Protecting Coalition Logics

Logic as a Tool

Big Brother Logic

Temporal logics in computer science

Knowledge and Ability

Logic and Discrete Mathematics

Logics for reasoning about strategic abilities in multi-player games