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.

We present complete axiomatizations for the Priorian temporal logics of the class of all irreflexive trees, the class of all reflexive trees, as well as various classes of reflexive and irreflexive unbounded and dense trees, including trees with branches isomorphic to the rational numbers, and to the real numbers with both there strict and non-strict orderings. We introduce new model constructions including the refinement of a bidirectional transitive filtration, unfolding, and unrolling. We establish the finite model property for all logics considered and thereby prove their decidability.

This paper proposes and studies a mechanism modelling the emergence of cooperation in non-cooperative multi-player extensive form games. We consider such games enriched with additional “stage bidding actions”, where at each decision node of the game tree, before the player controlling that node makes a decision every other player may make a committed offer (‘bid’) to pay an explicitly proposed amount of utility to the controlling player if she makes the choice explicitly indicated in the bid. In this work we assume that the bids are made simultaneously by all players. The controlling player then considers all these bids and then decides on its move. The effect of each bid associated with that choice is that it modifies the payoffs in the respective subgame according to the bid by transferring the proposed amounts of utility from the bidder to the controlling player who made the choice; all other bids made at that stage become irrelevant. Thus, these stage bids serve as an incentives-based mechanism that enables reaching a mutually beneficial cooperation in extensive form games.We study the resulting multi-player extensive form games with incentive bidding, which we call incentive bidding games (IB games), and analyze the subgame perfect equilibria (SPE) in these games. We show constructively that all IB games have (possibly many) SPE, and that the SPE outcomes (i.e. payoff tuples) form a polytope in the space of all outcomes. In the case of 2-player games, we also prove for an arbitrary game tree that all the SPE are sum-maximizing and have the same outcome, thereby defining a unique “value” of the game. These results contrast some well-known drawbacks of SPE in standard extensive form games and provide a further strong motivation for studying extensive form games with incentive bidding.We also study the notion of strong SPE in the sense of Aumann for IB games. First, we show that each of these strong SPE maximizes the sum of the payoffs (thus achieving a socially optimal solution). Second, if the game tree is binary, the strong SPE outcomes form a convex polytope. Third, games with only two leaves have such strong SPE, and we conjecture that all games with binary decision trees and with the same controlling player at all decision nodes have, indeed, such strong SPE.

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 constructions, 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 construction to the general case of fibring by iterating the basic cases and mention some potential applications.

. Trees are partial orderings where every element has a linearly ordered set of smaller elements. We define and study several natural notions of completeness of trees, extending Dedekind completeness of linear orders and Dedekind-MacNeille completions of partial orders. We then define constructions of tree completions that extend any tree to a minimal one satisfying the respective completeness property.

Trees are partial orders in which every element has a linearly ordered set of predecessors. Here we initiate the exploration of the structural theory of trees with the study of different notions of branching in trees and of condensed trees, which are trees in which every node is a branching node. We then introduce and investigate two different constructions of tree condensations - one shrinking, and the other expanding, the tree to a condensed tree.

In the process of designing a computer system S and checking whether an abstract model M of S verifies a given specification property η , one might have only a partial knowledge of the model, either because M 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.

This paper is an overview of some recent and ongoing developments of formal logical systems designed for reasoning about systems of rational agents who act in pursuit of their individual and collective goals, explicitly specified in the language as arguments of the strategic operators, in a socially interactive context of collective objectives and attitudes which guide and constrain the agents’ behavior.

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.

We consider systems of rational agents who act and interact in pursuit of their individual and collective objectives. We study and formalise the reasoning of an agent, or of an external observer, about the expected choices of action of the other agents based on their objectives, in order to assess the reasoner's ability, or expectation, to achieve their own objective. To formalize such reasoning we extend Pauly's Coalition Logic with three new modal operators of conditional strategic reasoning, thus introducing the Logic for Local Conditional Strategic Reasoning ConStR. We provide formal semantics for the new conditional strategic operators in concurrent game models, introduce the matching notion of bisimulation for each of them, prove bisimulation invariance and Hennessy-Milner property for each of them, and discuss and compare briefly their expressiveness. Finally, we also propose systems of axioms for each of the basic operators of ConStR and for the full logic.

We propose and study 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. We propose a quantitative extension of the logic ATLs 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.

We introduce and study a natural extension of the Alternating time temporal logic ATL , called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features one new and quite expressive coalitional strategic operator, called the coalitional goal assignment operator ⦉ γ ⦊, where γ is a mapping assigning to each set of players in the game its coalitional goal , formalised by a path formula of the language of TLCGA, i.e., a formula prefixed with a temporal operator X , U , or G , representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. Then, the formula ⦉ γ ⦊ intuitively says that there is a strategy profile Σ for the grand coalition Agt such that for each coalition C , the restriction Σ | C of Σ to C is a collective strategy of C that enforces the satisfaction of its objective γ (C) in all outcome plays enabled by Σ | C . We establish fixpoint characterizations of the temporal goal assignments in a μ-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy–Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.

The paper deals with multiplayer normal form games which are preceded by a ‘preplay negotiation phase’ consisting of exchange of preplay offers by players for payments of utility to other players conditional on them playing designated in the offers strategies. The game-theoretic effect of such preplay offers is a transformation of the payoff matrix of the game, obtained by transferring the offered payments between the payoffs of the respective players; thus, certain groups of game matrix transformations naturally emerge. The main result is an explicit and rather transparent algebraic characterization of the possible transformations of the payoff matrix of any given N-person normal form game induced by preplay offers for transfer of payments. That result can be used to describe the ‘bargaining space’ of the game and to determine the mutually optimal game transformations that rational players can achieve by exchange of preplay offers.

I consider strategic-form games with transferable utility extended with a phase of negotiations before the actual play of the game, where players can exchange a series of alternating (turn-based) unilaterally binding offers to each other for incentive payments of utilities after the play, conditional only on the recipients playing the strategy indicated in the offer. Every such offer transforms the game payoff matrix by accordingly transferring the offered amount from the offering player's payoff to the recipient's in all outcomes where the indicated strategy is played by the latter. That exchange of offers generates an unbounded-horizon, extensive-form preplay negotiations game, which is the focus of this study. In this paper, I study the case where the players assume that their opponents can terminate the preplay negotiations phase at any stage. Consequently, in their negotiation strategies, the players are guided by myopic rationality reasoning and aim at optimising each of their offers. The main results and findings include a concrete algorithmic procedure for computing players' best offers in the preplay negotiations phase and using it to demonstrate that these negotiations can generally lead to substantial improvement of the payoffs for both players in the transformed game, but they do not always lead to optimal outcomes, as one might expect.

Reasoning is one of the most important and distinguished human activities [...]

We study the first-order theories of some natural and important classes of coloured trees, including the four classes of trees whose paths have the order type respectively of the natural numbers, the integers, the rationals, and the reals. We develop a technique for approximating a tree as a suitably coloured linear order. We then present the first-order theories of certain classes of coloured linear orders and use them, along with the approximating technique, to establish complete axiomatisations of the four classes of trees mentioned above.

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.