Valentin Goranko

I&C Journal 2026 Journal Article

Complete axiomatization and decidability of the logic of two-agent cooperative strategic interaction

• Valentin Goranko

The multi-agent Socially Friendly Coalition Logic SFCL was introduced in [1]. The present paper focuses on the two-agent fragment SFCL ( 2 ) of SFCL. We illustrate the use of SFCL ( 2 ) for formalising reasoning about two-agent interactions enabling cooperative strategic behaviour. Then we prove completeness of an axiomatic system for the 2-agent case SFCL ( 2 ) essentially extracted from the one for SFCL presented in [1]. The proof method is fully constructive and produces finite tree-like models for all consistent SFCL ( 2 ) -formulae, thus also implying decidability of that logic. The proof method is, in principle, generically extendable to the full SFCL and to various other logics for local strategic reasoning.

FLAP Journal 2025 Journal Article

Combining Tableaux for Combinations of Logics. I. Generic Fibring of Tableaux

• Valentin Goranko

This is the first paper in a series exploring the following generic question for a given type of combination of logics: Given tableaux systems for two logics and a combination of these logics of a given type, how to combine systematically and uniformly the tableaux systems for component logics into a tableaux system for the combined logic by preserving important properties of the components? Here I consider the case of general fibring of logics, introduced by Dov Gab- bay. Starting with the basic cases of propositional merger and simple nesting of logics, I present natural generic versions of fibring of tableaux for these construc- tions, illustrate them with some examples, and establish respective results on preservation of soundness, completeness, and termination from the component tableaux to the combined tableau. Then I extend the combined tableau con- struction to the general case of fibring by iterating the basic cases and mention some potential applications.

Highlights Conference 2025 Conference Abstract

Local Basic Strategy Logic

• Valentin Goranko

LAMAS&SR Workshop 2024 Workshop Paper

Local Basic Strategy Logic: A Unifying Formalism for Local Strategic Reasoning

• Valentin Goranko

FSCD Conference 2023 Conference Paper

Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach

• Serenella Cerrito
• Valentin Goranko
• Sophie Paillocher

In the process of designing a computer system S and checking whether an abstract model ℳ of S verifies a given specification property η, one might have only a partial knowledge of the model, either because ℳ has not yet been completely defined (constructed) by the designer, or because it is not completely observable by the verifier. This leads to new verification problems, subsuming satisfiability and model checking as special cases. We state and discuss these problems in the case of LTL specifications, and develop a uniform tableau-based approach for their solutions.

AAMAS Conference 2022 Conference Paper

Combining Quantitative and Qualitative Reasoning in Concurrent Multi-player Games

• Nils Bulling
• Valentin Goranko

We propose and study a general framework for modelling and formal reasoning about multi-agent systems and, in particular, multistage games where both quantitative and qualitative objectives and constraints are involved. Our models enrich concurrent game models with payoffs and guards on actions associated with each state of the model. We propose a quantitative extension of the logic ATL∗ that enables combination of quantitative and qualitative reasoning. We illustrate the framework with some examples and then consider the model-checking problems arising in it and establish some general undecidability and decidability results for them.

AIJ Journal 2022 Journal Article

Knowledge-based strategies for multi-agent teams playing against Nature

• Dilian Gurov
• Valentin Goranko
• Edvin Lundberg

We study teams of agents that play against Nature towards achieving a common objective. The agents are assumed to have imperfect information due to partial observability, and have no communication during the play of the game. We propose a natural notion of higher-order knowledge of agents. Based on this notion, we define a class of knowledge-based strategies, and consider the problem of synthesis of strategies of this class. We introduce a multi-agent extension, MKBSC, of the well-known knowledge-based subset construction applied to such games. Its iterative applications turn out to compute higher-order knowledge of the agents. We show how the MKBSC can be used for the design of knowledge-based strategy profiles, and investigate the transfer of existence of such strategies between the original game and in the iterated applications of the MKBSC, under some natural assumptions. We also relate and compare the “intensional” view on knowledge-based strategies based on explicit knowledge representation and update, with the “extensional” view on finite memory strategies based on finite transducers and show that, in a certain sense, these are equivalent.

LAMAS&SR Workshop 2022 Workshop Paper

Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems

• Riccardo De Masellis
• Valentin Goranko

LAMAS&SR Workshop 2022 Workshop Paper

Multi-stage Blotto Games

• Nicolas Dumange
• Valentin Goranko

JAAMAS Journal 2021 Journal Article

Combining quantitative and qualitative reasoning in concurrent multi-player games

• Nils Bulling
• Valentin Goranko

Abstract We propose a general framework for modelling and formal reasoning about multi-agent systems and, in particular, multi-stage games where both quantitative and qualitative objectives and constraints are involved. Our models enrich concurrent game models with payoffs and guards on actions associated with each state of the model and propose a quantitative extension of the logic \({\textsf {ATL}}^{*}\) that enables the combination of quantitative and qualitative reasoning. We illustrate the framework with some detailed examples. Finally, we consider the model-checking problems arising in our framework and establish some general undecidability and decidability results for them.

I&C Journal 2021 Journal Article

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

• Valentin Goranko
• Antti Kuusisto
• Raine Rönnholm

We develop a game-theoretic semantics ( GTS ) for the fragment AT L + of the alternating-time temporal logic AT L ⁎, thereby extending the recently introduced GTS for ATL. We show that the game-theoretic semantics is equivalent to the standard compositional semantics of AT L + with perfect-recall strategies. Based on the new semantics, we provide an analysis of the memory and time resources needed for model checking AT L + 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 AT L + and identify a natural hierarchy of tractable fragments of AT L + that substantially extend ATL.

LAMAS&SR Workshop 2021 Workshop Paper

Knowledge-Based Strategies for Multi-Agent Teams Playing Against Nature

• Dilian Gurov
• Valentin Goranko
• Edvin Lundberg

AAMAS Conference 2021 Conference Paper

Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems

• Riccardo De Masellis
• Valentin Goranko

ECAI Conference 2020 Conference Paper

Gradual Guaranteed Coordination in Repeated Win-Lose Coordination Games

• Valentin Goranko
• Antti Kuusisto
• Raine Rönnholm

We investigate repeated win-lose coordination games and analyse when and how rational players can guarantee eventual coordination in such games. Our study involves both the setting with a protocol shared in advance as well as the scenario without an agreed protocol. In both cases, we focus on the case without any communication amongst the players once the particular game to be played has been revealed to them. We identify classes of coordination games in which coordination cannot be guaranteed in a single round, but can eventually be achieved in several rounds by following suitable coordination protocols. In particular, we study coordination using protocols invariant under structural symmetries of games under some natural assumptions, such as: priority hierarchies amongst players, different patience thresholds, use of focal groups, and gradual coordination by contact.

JAAMAS Journal 2020 Journal Article

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

• Riccardo De Masellis
• Valentin Goranko

Abstract 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 \(\gamma\) ″, where \(\gamma\) 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 \({\mathcal {L}}_{\textsc {hdmas}}\) and define normal form of its formulae. We then prove that every formula in \({\mathcal {L}}_{\textsc {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.

TCS Journal 2019 Journal Article

Alternating-time temporal logic ATL with finitely bounded semantics

• Valentin Goranko
• Antti Kuusisto
• Raine Rönnholm

We study a variant ATL FB of the alternating-time temporal logic ATL with a non-standard, ‘finitely bounded’ semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL FB differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL FB. The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL FB and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL FB and prove its soundness and completeness.

TIME Conference 2019 Conference Paper

Minimisation of Models Satisfying CTL Formulas

• Serenella Cerrito
• Amélie David 0001
• Valentin Goranko

We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.

LORI Conference 2019 Conference Paper

Towards a Logic for Conditional Local Strategic Reasoning

• Valentin Goranko
• Fengkui Ju

Abstract 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.

EUMAS Conference 2018 Conference Paper

Generalising the Dining Philosophers Problem: Competitive Dynamic Resource Allocation in Multi-agent Systems

• Riccardo De Masellis
• Valentin Goranko
• Stefan Gruner
• Nils Timm

Abstract We consider a new generalisation of the Dining Philosophers problem with a set of agents and a set of resource units which can be accessed by them according to a fixed graph of accessibility between agents and resources. Each agent needs to accumulate a certain (fixed for the agent) number of accessible resource units to accomplish its task, and once it is accomplished the agent releases all resources and starts accumulating them again. All this happens in succession of discrete ‘rounds’ and yields a concurrent game model of ‘dynamic resource allocation’. We use the Alternating time Temporal Logic (ATL) to specify important properties, such as goal achievability, fairness, deadlock, starvation, etc. These can be formally verified using the efficient model checking algorithm for ATL. However, the sizes of the resulting explicit concurrent game models are generally exponential both in the number of resources and the number of agents, which makes the ATL model checking procedure generally intractable on such models, especially when the number of resources is large. That is why we also develop an abstract representation of the dynamic resource allocation models and develop a symbolic version of the model checking procedure for ATL. That symbolic procedure reduces the time complexity of model checking to polynomial in the number of resources, though it can take a worst-case double exponential time in the number of agents.

AAMAS Conference 2018 Conference Paper

Socially Friendly and Group Protecting Coalition Logics

• Valentin Goranko
• Sebastian Enqvist

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.

TIME Conference 2017 Conference Paper

CTL with Finitely Bounded Semantics

• Valentin Goranko
• Antti Kuusisto
• Raine Rönnholm

We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property. We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.

AAMAS Conference 2017 Conference Paper

Game-Theoretic Semantics for ATL+ with Applications to Model Checking

• Valentin Goranko
• Antti Kuusisto
• Raine Rö nnholm

We develop a game-theoretic semantics (GTS) for the fragment ATL+ of the Alternating-time Temporal Logic ATL∗, essentially extending a recently introduced GTS for ATL. We show that the new game-theoretic semantics is equivalent to the standard compositional semantics of ATL+ (with perfectrecall 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 extend ATL.

EUMAS Conference 2017 Conference Paper

Rational Coordination in Games with Enriched Representations

• Valentin Goranko
• Antti Kuusisto
• Raine Rönnholm

Abstract We consider pure win-lose coordination games where the representation of the game structure has additional features that are commonly known to the players, such as colouring, naming, or ordering of the available choices or of the players. We study how the information provided by such enriched representations affects the solvability of these games by means of principles of rational reasoning in coordination scenarios with no prior communication or conventions.

LORI Conference 2017 Conference Paper

Rational Coordination with no Communication or Conventions

• Valentin Goranko
• Antti Kuusisto
• Raine Rönnholm

Abstract 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 analyse which classes of coordination games 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.

Highlights Conference 2016 Conference Abstract

Game-Theoretic Semantics for Alternating-Time Temporal Logic

• Valentin Goranko

We introduce several versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level, in the standard semantics of the strategic operators, and on the meta-level, where game-theoretic logical semantics can be applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL, based on limiting the time resources available to the verifier and falsier in the semantic evaluation game. We introduce and analyse unbounded and bounded GTS and prove these to be equivalent to the standard (Tarski style) compositional semantics. We also introduce a non-equivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

AAMAS Conference 2016 Conference Paper

Game-Theoretic Semantics for Alternating-Time Temporal Logic

• Valentin Goranko
• Antti Kuusisto
• Raine Rönnholm

We introduce versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level, in the standard semantics of the strategic operators, and on the meta-level, where gametheoretic logical semantics can be applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The novel game-theoretic perspective enables us to identify new variants of the semantics of ATL, based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game; we introduce and analyse an unbounded and bounded GTS and prove these to be equivalent to the standard (Tarskistyle) compositional semantics. We also introduce a nonequivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

TIME Conference 2016 Conference Paper

On the Length and Depth of Temporal Formulae Distinguishing Non-bisimilar Transition Systems

• Valentin Goranko
• Louwe B. Kuijer

We investigate the minimal length and nesting depth of temporal formulae that distinguish two given non-bisimilar finite pointed transition systems. We show that such formula can always be constructed in length at most exponential in the combined number of states of both transition systems, and give an example with exponential lower bound, for several common temporal languages. We then show that by using renamings of subformulae or explicit assignments the length of the distinguishing formula can always be reduced to one that is bounded above by a cubic polynomial on the combined size of both transition systems. This is also a bound for the size obtained by using DAG representation of formulae. We also prove that the minimal nesting depth for such formula is less than the combined size of the two state spaces and obtain some tight upper bounds.

JAAMAS Journal 2015 Journal Article

Big Brother Logic: visual-epistemic reasoning in stationary multi-agent systems

• Olivier Gasquet
• Valentin Goranko
• François Schwarzentruber

Abstract 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.

JAAMAS Journal 2015 Journal Article

State and path coalition effectivity models of concurrent multi-player games

• Valentin Goranko
• Wojciech Jamroga

Abstract We consider models of multi-player games where abilities of players and coalitions are defined in terms of sets of outcomes which they can effectively enforce. We extend the well-studied state effectivity models of one-step games in two different ways. On the one hand, we develop multiple state effectivity functions associated with different long-term temporal operators. On the other hand, we define and study coalitional path effectivity models where the outcomes of strategic plays are infinite paths. For both extensions we obtain representation results with respect to concrete models arising from concurrent game structures. We also apply state and path coalitional effectivity models to provide alternative, arguably more natural and elegant semantics to the alternating-time temporal logic ATL*, and discuss their technical and conceptual advantages.

LORI Conference 2013 Conference Paper

An Offer You Cannot Refuse: Obtaining Efficiency and Fairness in Preplay Negotiation Games with Conditional Offers

• Valentin Goranko
• Paolo Turrini

Abstract We study a recently introduced extension of normal form games with a phase before the actual play of the game, where each player can make binding offers for payments of utility to the other players after the play of the game, contingent on the recipient playing the strategy indicated in the offer. Such offers transform the payoff matrix of the original game and allow for some degree of cooperation between rational players while preserving the non-cooperative nature of the game. We focus on 2-player negotiations games arising in the preplay phase when offers for payments are made conditional on a suggested matching offer of the same kind being made in return by the receiver. We study and analyze such bargaining games, obtain results describing their possible solutions and discuss the degrees of efficiency and fairness that can be achieved in such negotiation process depending on whether time is valuable or not.

Highlights Conference 2013 Conference Abstract

Combining quantitative and qualitative strategic reasoning in concurrent multi-player games

• Nils Bulling
• Valentin Goranko

We propose a logical modeling framework, combining a game-theoretic study of the abilities of players to achieve quantitative objectives in multi-player games (optimizing payoffs or preferences on outcomes) with a logical analysis of the abilities of players for achieving qualitative objectives (reaching or maintaining game states with desired properties). We enrich concurrent game models with payoffs for the normal form games associated with each state of the model and propose a quantitative extension of the logic ATL* enabling combination of quantitative and qualitative reasoning.

Highlights Conference 2013 Conference Abstract

Strategic games and truly playable effectivity functions

• Valentin Goranko
• Wojtek Jamroga
• Paolo Turrini

A well-known result states that every strategic game generates a playable effectivity function, and every playable effectivity function can be implemented with a strategic game. We show that the latter does not hold for infinite games. We identify the error in the proof, and present examples of playable effectivity functions for which no equivalent strategic game exists. Then, we characterize the class of *truly playable* functions that do correspond to strategic games. We also show that Coalition Logic cannot distinguish between the two classes, and we extend it to a logic that is expressive enough.

AAMAS Conference 2012 Conference Paper

State and Path Coalition Effectivity Models for Logics of Multi-Player Games

• Valentin Goranko
• Wojciech Jamroga

We consider models of multi-player games where abilities of players and coalitions are defined in terms of sets of outcomes which they can effectively enforce. We extend the well studied state effectivity models of one-step games in two different ways. On the one hand, we develop multiple state effectivity functions associated with different long-term temporal operators. On the other hand, we define and study coalitional path effectivity models where the outcomes of strategic play are infinite paths. For both extensions we obtain representation results with respect to concrete models arising from concurrent game structures. We also apply state and path coalitional effectivity models to provide alternative, arguably more natural and elegant semantics to alternating-time temporal logic ATL*, and discuss their technical and conceptual advantages.

JAAMAS Journal 2012 Journal Article

Strategic games and truly playable effectivity functions

• Valentin Goranko
• Wojciech Jamroga
• Paolo Turrini

Abstract A well-known result in the logical analysis of cooperative games states that the so-called playable effectivity functions exactly correspond to strategic games. More precisely, this result states that for every playable effectivity function E there exists a strategic game that assigns to coalitions of players exactly the same power as E, and every strategic game generates a playable effectivity function. While the latter direction of the correspondence is correct, we show that the former does not hold for a number of infinite state games. We point out where the original proof of correspondence goes wrong, and we present examples of playable effectivity functions for which no equivalent strategic game exists. Then, we characterize the class of truly playable effectivity functions, that do correspond to strategic games. Moreover, we discuss a construction that transforms any playable effectivity function into a truly playable one while preserving the power of most (but not all) coalitions. We also show that Coalition Logic (CL), a formalism used to reason about effectivity functions, is not expressive enough to distinguish between playable and truly playable effectivity functions, and we extend it to a logic that can make that distinction while still enjoying the good meta-logical properties of CL, such as finite axiomatization and decidability via finite model property.

TIME Conference 2012 Invited Paper

Undecidability and Temporal Logic: Some Landmarks from Turing to the Present

• Valentin Goranko

This is a selective survey and discussion of some of the landmark undecidability results in temporal logic, beginning with Turing's undecidability of the Halting problem which, in retrospect, can be regarded as the historically first undecidability result for a suitable temporal logic over configuration graphs of Turing machines. I will discuss some of the natural habitats of undecidable temporal logics, such as first-order, interval-based and real time temporal logics, as well as some extensions that often lead to undecidability, such as two-dimensional temporal logics and temporal-epistemic logics.

IJCAI Conference 2011 Conference Paper

Expressiveness of the Interval Logics of Allen's Relations on the Class of All Linear Orders: Complete Classification

• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

We compare the expressiveness of the fragments of Halpern and Shoham's interval logic (HS), i. e. , of all interval logics with modal operators associated with Allen's relations between intervals in linear orders. We establish a complete set of inter-definability equations between these modal operators, and thus obtain a complete classification of the family of 212 fragments of HS with respect to their expressiveness. Using that result and a computer program, we have found that there are 1347 expressively different such interval logics over the class of all linear orders.

AAMAS Conference 2011 Conference Paper

Strategic Games and Truly Playable Effectivity Functions

• Valentin Goranko
• Wojciech Jamroga
• Paolo Turrini

A well known (and often used) result by Marc Pauly states that for every playable effectivity function E there exists a strategic game that assigns to coalitions exactly the same power as E, and vice versa. While the latter direction of the correspondence is correct, we show that the former does not always hold in the case of infinite game models. We point out where the proof of correspondence goes wrong, and we present examples of playable effectivity functions in infinite models for which no equivalent strategic game exists. Then, we characterize the class of truly playable effectivity functions, that does correspond to strategic games. Moreover, we discuss a construction that transforms any playable effectivity function into a truly playable one while preserving the power of most (but not all) coalitions. We also show that Coalition Logic is not expressive enough to distinguish between playable and truly playable effectivity functions, and we extend it to a logic that can make this distinction while enjoying finite axiomatization and finite model property.

TIME Conference 2011 Conference Paper

The Dark Side of Interval Temporal Logic: Sharpening the Undecidability Border

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

Unlike the Moon, the dark side of interval temporal logics is the one we usually see: their ubiquitous undesirability. Identifying minimal undecidable interval logics is thus a natural and important issue in the research agenda in the area. The decidability status of a logic often depends on the class of models (in our case, the class of interval structures)in which it is interpreted. In this paper, we have identified several new minimal undecidable logics amongst the fragments of Halpern-Shoham logic HS, including the logic of the overlaps relation, over the classes of all and finite linear orders, as well as the logic of the meet and subinterval relations, over the class of dense linear orders. Together with previous undecid ability results, this work contributes to delineate the border of the dark side of interval temporal logics quite sharply.

ECAI Conference 2010 Conference Paper

Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

Interval temporal logics formalize reasoning about interval structures over (usually) linearly ordered domains, where time intervals are the primitive ontological entities and truth of formulae is defined relative to time intervals, rather than time points. In this paper, we introduce and study Metric Propositional Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval that is "met by" the current one and to an interval that "meets" the current one, plus an infinite set of length constraints, regarded as atomic propositions, to constrain the lengths of intervals. We argue that MPNL can be successfully used in different areas of artificial intelligence to combine qualitative and quantitative interval temporal reasoning, thus providing a viable alternative to well-established logical frameworks such as Duration Calculus. We show that MPNL is decidable in double exponential time and expressively complete with respect to a well-defined subfragment of the two-variable fragment FO2[N, =, <, s] of first-order logic for linear orders with successor function, interpreted over natural numbers. Moreover, we show that MPNL can be extended in a natural way to cover full FO2[N, =, <, s], but, unexpectedly, the latter (and hence the former) turns out to be undecidable.

AAMAS Conference 2009 Conference Paper

Tableau-Based Decision Procedure for Full Coalitional Multiagent Temporal-Epistemic Logic of Linear Time

• Valentin Goranko
• Dmitry Shkatov

We develop a tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT). It extends LTL with operators of common and distributed knowledge for all coalitions of agents. The tableau procedure runs in exponential time, matching the lower bound obtained by Halpern and Vardi for a fragment of our logic, thus providing a complexity-optimal decision procedure for CMATEL(CD+LT). General Terms Theory

TIME Conference 2009 Conference Paper

Undecidability of Interval Temporal Logics with the Overlap Modality

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

We investigate fragments of Halpern-Shoham's interval logic HS involving the modal operators for the relations of left or right overlap of intervals. We prove that most of these fragments are undecidable, by employing a non-trivial reduction from the octant tiling problem.

LPAR Conference 2008 Conference Paper

Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

Abstract Interval temporal logics are based on temporal structures where time intervals, rather than time instants, are the primitive ontological entities. They employ modal operators corresponding to various relations between intervals, known as Allen’s relations. Technically, validity in interval temporal logics translates to dyadic second-order logic, thus explaining their complex computational behavior. The full modal logic of Allen’s relations, called HS, has been proved to be undecidable by Halpern and Shoham under very weak assumptions on the class of interval structures, and this result was discouraging attempts for practical applications and further research in the field. A renewed interest has been recently stimulated by the discovery of interesting decidable fragments of HS. This paper contributes to the characterization of the boundary between decidability and undecidability of HS fragments. It summarizes known positive and negative results, it describes the main techniques applied so far in both directions, and it establishes a number of new undecidability results for relatively small fragments of HS.

TARK Conference 2007 Conference Paper

Alternating-time temporal logics with irrevocable strategies

• Thomas Ågotnes
• Valentin Goranko
• Wojciech Jamroga

In Alternating-time Temporal Logic (atl), one can express statements about the strategic ability of an agent (or a coalition of agents) to achieve a goal φ such as: “agent i can choose a strategy such that, if i follows this strategy then, no matter what other agents do, φ will always be true”. However, strategies in atl are revocable in the sense that in the evaluation of the goal φ the agent i is no longer restricted by the strategy she has chosen in order to reach the state where the goal is evaluated. In this paper we consider alternative variants of atl where strategies, on the contrary, are irrevocable. The difference between revocable and irrevocable strategies shows up when we consider the ability to achieve a goal which, again, involves (nested) strategic ability. Furthermore, unlike in the standard semantics of atl, memory plays an essential role in the semantics based on irrevocable strategies.

TCS Journal 2006 Journal Article

Complete axiomatization and decidability of Alternating-time temporal logic

• Valentin Goranko
• Govert van Drimmelen

Alternating-time Temporal Logic (ATL), introduced by Alur, Henzinger and Kupferman, is a logical formalism for the specification and verification of open systems involving multiple autonomous players (agents, components). In particular, this logic allows for the explicit expression of coalition abilities in such systems, modelled as infinite transition games between the coalition and its complement. Formally, ATL is a non-normal multi-modal extension of CTL (regarded as a one-player fragment of ATL) with temporal operators indexed by coalitions of players, and thus expressing selective quantification over those paths which can be effected as outcomes of infinite transition games between the coalition and its complement. We present a sound and complete axiomatization of the logic ATL, based on Pauly's axiomatization of his Coalition Logic, augmented with axioms and rules for fixed point formulae characterizing the temporal operators. The completeness proof is by construction of a bounded branching tree model for each ATL-consistent formula. These models can be folded into finite models, thus rendering the finite model property for ATL. We also describe an automata-based decision procedure for ATL by translating the satisfiability problem to the nonemptiness problem for alternating automata on infinite trees. When considering formulae over a fixed finite set of players the decidability problem is shown to be EXPTIME-complete.

TIME Conference 2001 Conference Paper

Hybrid Ockhamist Temporal Logic

• Patrick Blackburn
• Valentin Goranko

We introduce hybrid Ockhamist temporal logic, which combines the mechanisms of hybrid logic with Ockhamist semantics by employing nominals, satisfaction operators, binders, and quantifiers over branches. We provide a complete (with respect to bundled trees semantics) axiomatic system for the basic hybrid Ockhamist temporal logic (HOT) and for some of its extensions including the full hybrid Ockhamist temporal logic. The fill system is expressively equivalent to the first-order logic over trees extended with branch quantifiers which was proved decidable previously.