The paper presents a novel SMT-based method for testing the satisfiability of formulae that express strategic properties of timed multi-agent systems represented by networks of timed automata. Strategic Metric Temporal Logic (SMTL) is introduced, which extends Metric Temporal Logic (MTL) with strategy operators. SMTL is interpreted over maximal continuous time runs of timed automata. We define a procedure that synthesises a model for a given SMTL formula if such a model exists. The method exploits Satisfiability Modulo Theories (SMT) techniques and Parametric Bounded Model Checking algorithms. The presented approach enables bounded satisfiability checking, where the model is partially given and needs to be completed in line with the given specification. Our method has been implemented, and its application is demonstrated through an example of the well-known dining philosophers problem extended with clocks and strategies. The experimental results are quite encouraging.

In this paper, we introduce a new method of the satisfiability (SAT) checking for Simple-Goal Strategy Logic (SL[SG]), using symbolic Boolean model encoding and the SAT Modulo Monotonic Theories techniques, which was implemented into the tool SGSAT. To the best of our knowledge, this is the only tool solving the SAT problem for SL[SG]. Its applications include process synthesis, developing controllers as well as automatic planners in multi-agent scenarios.

Synthesis of models and strategies is a very important task in software engineering. The main problem here consists in checking the satisfiability of formulae expressing the specification of a system to be implemented. This paper puts forward a novel method for deciding the satisfiability of formulae of Alternating-time Temporal Logic (ATL) under perfect and imperfect information. The synthesised models of strategic games are often minimal. The method expands the one for CTL exploiting SAT Modulo Monotonic Theories (SMMT) solvers. Our tool MsATL combines SMMT solvers with two existing ATL model checkers: MCMAS and STV. This is the first ever tool for checking the satisfiability of imperfect information ATL. The experimental results show that, similarly to the CTL case, our approach appears to be very efficient and can quickly check the satisfiability of large ATL formulae that have been out of reach of the existing approaches.

We can understand a protocol as a set of rules used by the communicating entities i.e. people or computers. These rules specify allowed interactions between them. Every day people use protocols unconsciously during their conversations since they help to achieve the goal of the conversation (e.g. a compromise, a persuasion). In the paper, we focus on argumentative dialogues in which players can perform actions representing speech acts like claim, question, scold etc. Since we consider dialogues which have an emotional undertow we want to design a system for semantic verification of properties of dialogue games with emotional reasoning. This framework is based on interpreted systems designed for a dialogue protocol in which participants have emotional skills. The GERDL language is used for a dialogue game specification. We present the idea of encoding rules describing the dialogue game given in this language. We want to verify some properties of dialogue games and we focus on the reachability property that can take into account emotions and commitments of players.

The aim of the paper is to propose a game-theoretic description of strategies available to players in dialogues. We show how existing dialogical systems can be formalized as Nash-style games, and how the game-theoretic concept of solutions (dominant strategies, Nash equilibrium) can be used to analyse these systems. Our first study, discussed in this article, describes the game DC introduced by Mackenzie.

This paper is a continuation of the work [26] in which the LND dialogue system was proposed. LND reconstructs the dialogical logic introduced by Lorenzen using the terminology of persuasion dialogue games as specified by Prakken [18]. The aim of the LND system is to recognize formal fallacies in natural dialogues and remove them. Now we extend this system to include a new protocol enabling the reconstruction of natural dialogues in which parties can commit formal fallacies. We then present the implementation of the protocols applied.

The paper proposes a dialogue system LND which brings together and unifies two traditions in studying dialogue as a game: the dialogical logic introduced by Lorenzen; and persuasion dialogue games as specified by Prakken. The first approach allows th

The aim of the paper is to extend the syntax and semantics of the AGnlogic with components allowing the representation and verification of strategies in persuasion dialogue games. The AGnlogic was introduced to express beliefs and persuasive actions of agents, and then it was used to perform model checking in persuasive inter-agent communication. In this paper, we enrich AGnby adapting strategy operators from Alternating-time Temporal Logic and adding new ones to allow reasoning about the success and persuasive power of dialogues.

The aim of the paper is to propose how to enrich a formal model of persuasion with a specification for actions which are typical for persuasion process. First, since these actions are verbal, they influence a receiver but do not change the agent’s environment. In a formal framework, we represent them as actions that change not the particular state of a model, but the whole model. Second, effects of those actions depend on how much the receiver trusts the persuader. To formally model this phenomenon, we use a trust function. Finally, we want to represent uncertainty in terms of probability. Thus far, our model did not allow to express those properties of the persuasion process. Therefore, in this paper we extend Multimodal Logic of Actions and Graded Beliefs (AG n ) with Probabilistic Dynamic Epistemic Logic (PDEL) and elements of Reputation Management framework (RM). Incorporation of PDEL into the model of persuasion requires some modifications of PDEL. Such extended model is then used to enrich Perseus – our software tool that enables to examine persuasive multi-agent systems. New components of the tool allow us to execute parametric verification of the different properties related to updating probabilistic beliefs in persuasion.

The aim of the paper is to present the software tool Perseus and show how it can be used to examine multi-agent systems where the ability to persuade is specified. Especially we want to study the issues such as: what arguments individuals use to successfully convince others, what type of a persuader guarantees a victory etc. This work describes implementation of the tool and discusses what questions about persuasion process Perseus can answer and how it is done.