We propose Boolean Negotiation Games, a computationally grounded model to investigate strategic aspects of negotiations. Our model is inspired by the popular Boolean Game framework and Rubinstein’s bargaining model of alternating offers. We analyse restrictions on negotiation protocols and investigate properties of agreements. We propose and investigate protocols that do not allow repeating offers. In the context of Boolean Games we then naturally obtain finite games, which arise in many practical negotiation contexts. We show that Boolean negotiation games (BNGs) can yield agreements which are more beneficial than the stable solutions (i.e. Nash equilibria) of the underlying Boolean game, and propose an algorithm to compute stable negotiation strategies.

The increasing presence of autonomous (software) systems in open environments in general, and the complex interactions taking place among them in particular, require flexible control and coordination mechanisms to guarantee desirable overall system level properties without limiting the autonomy of the involved systems. In artificial intelligence, and in particular in the multi-agent systems research field, social laws, norms, and sanctions have been widely proposed as flexible means for coordinating the behaviour of autonomous agents in multi-agent settings. Recently, many languages have been proposed to specify and implement norm-based environments where the behaviour of autonomous agents is monitored, evaluated based on norms, and possibly sanctioned if norms are violated. In this paper, we first introduce a formal setting of multi-agent environments based on concurrent game structures which abstracts from concrete specification languages. We extend this formal setting with norms and sanctions, and show how concepts from mechanism design can be used to formally analyse and verify whether a specific behaviour can be enforced (or implemented) if agents follow their subjective preferences. We relate concepts from mechanism design to our setting, where agents' preferences are modelled by linear time temporal logic (LTL) formulae. This proposal bridges the gap between norms and mechanism design allowing us to formally study and analyse the effect of norms and sanctions on the behaviour of rational agents. The proposed machinery can be used to check whether specific norms and sanctions have the designer's expected effect on the rational agents' behaviour or if a set of norms and sanctions that realise the effect exists at all. We investigate the computational complexity of our framework, focusing on its implementation in Nash equilibria and we show that it is located at the second and third level of the polynomial hierarchy. Despite this high complexity, on the positive side, these results are in line with existing complexity results of related problems. Finally, we propose a concrete executable specification language that can be used to implement multi-agent environments. We show that the proposed specification language generates specific concurrent game structures and that the abstract multi-agent environment setting can be applied to study and analyse the behaviour of multi-agent programs with and without norms.

We propose a new strategic model of negotiation, called Boolean negotiation games. Our model is inspired by Boolean games and the alternating offers model of bargaining. It offers a computationally grounded model for studying properties of negotiation protocols in a qualitative setting. Boolean negotiation games can yield agreements that are more beneficial than stable solutions (Nash equilibria) of the underlying Boolean game.