Multi-agent systems often involve multi-level interactions that make strategic reasoning hard to scale. To capture such systems, we introduce hierarchical concurrent game models (HCGMs) that allow embedding of (sub)systems into other systems. We define the semantics of ATL on HCGMs by an unfolding of an HCGM into a standard (flat) concurrent game model. Building on this semantics, we provide a model checking algorithm for ATL interpreted over HCGMs and discuss its complexity.

We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, ie STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for STCTLir is of the same complexity as for ATLir, the model checking problem for STCTLir is of the same complexity as for TCTL, while for STCTLiR it is undecidable as for ATLiR. The above results suggest to use STCTLir and STCTLir in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTLir.

Multi-agent systems (MAS) often include multiple layers of uncertainty. One source comes from agents' limited ability to observe their environment, while another arises from the unpredictability of natural events and the actions of other agents, which, though uncertain, can be estimated through experiments or past experiences. A central focus in MAS is the agents' ability to achieve their goals.For intelligent agents, these goals are often epistemic, involving the acquisition of partial or complete knowledge about a crucial fact A. Many such properties can be expressed using PATLK, an extension of probabilistic alternating-time temporal logic (PATL) with knowledge operators, or PATLC that extends PATL with probabilistic beliefs. In many scenarios, however, the goal of the players is not to achieve high confidence about A being true, but rather to reduce their uncertainty about A (be it true or false). Similarly, in scenarios where the goal is to keep A secret, the outsiders' uncertainty about A should be maintained above a certain threshold. To capture such properties, we introduce PATLH, a logic extending PATL with information-theoretic modalities based on Shannon entropy.The logic enables the specification of agents' capabilities concerning the uncertainty of a player about a given set of facts. We define it over multi-agent systems with stochastic transitions and probabilistic imperfect information, capturing two key uncertainties: the agents' partial observability of their environment and the stochastic nature of state transitions. As technical results, we compare the epistemic and information-theoretic extensions of PATL with respect to their expressiveness, succinctness, and complexity of model checking.

We present NatSTV, a tool for approximate verification of natural strategic ability in multi-agent systems. The tool builds on our model checker STV (STrategic Verifier), and implements heuristic synthesis of natural strategies for asynchronous agents with imperfect information and recall. All of that is available through a web interface, with no need to install or configure the software by the user.

Verification of strategic ability under imperfect information is challenging, with complexity ranging from NP-complete to undecidable. This is partly because traditional fixpoint equivalences fail in this setting. Some years ago, an interesting idea of fixpoint approximation was proposed for model checking of ATL_ir, i.e., the logic of strategic ability for agents with imperfect information and imperfect recall. In this paper, we propose a new variant of the approximation, that uses the agent's local model rather than the global model of the system. We prove correctness of the construction, and demonstrate its effectiveness through experimental results on scalable models of voting.

In this paper, we present a substantially enhanced version of our software tool STV (STrategic Verifier), dedicated to strategy synthesis and model checking of strategic abilities in multi-agent systems. The new extension, called STV+FLY, incorporates an advanced strategy synthesis algorithm that enables model checking with on-the-fly generation of the global model. This innovative approach allows for the verification of some strategic properties without generating the entire global state space, thus avoiding an important bottleneck and significantly improving the efficiency.

The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle this issue but at the expense of expressiveness. In this paper, we propose a three-valued semantics for Strategy Logic upon which we define an abstraction method. We show that the latter semantics is an approximation of the classic two-valued one for Strategy Logic. Furthermore, we extend MCMAS, an open-source model checker for multi-agent specifications, to incorporate our abstraction method and present some promising experimental results.

Formal verification of intelligent agents is often computationally infeasible due to state-space explosion. We present a tool for reducing the impact of the explosion by means of state abstraction that is (a) easy to use and understand by non-experts, and (b) agent-based in the sense that it operates on a modular representation of the system, rather than on its huge explicit state model.

In this paper, we investigate the probabilistic variants of the strategy logics ATL and ATL* under imperfect information. Specifically, we present novel decidability and complexity results when both the model transitions and the strategies played by agents are stochastic. That is, the semantics of the logics are based on multi-agent, stochastic transition systems with imperfect information, which combine two sources of uncertainty, namely, the partial observability agents have on the environment, and the likelihood of transitions to occur from a system state. Since the model checking problem is undecidable in general in this setting, we restrict our attention to agents with memoryless (positional) strategies. The resulting setting captures the situation in which agents have qualitative uncertainty of the local state and quantitative uncertainty about the occurrence of future events. We illustrate the usefulness of this setting with meaningful examples.

Model checking of multi-agent systems (MAS) is known to be hard, both theoretically and in practice. A smart abstraction of the state space may significantly reduce the model,and facilitate the verification. In this paper, we propose and study an intuitive agent-based abstraction scheme, based on the removal of variables in the representation of a MAS. This allows to achieve a desired reduction of a state space without generating the global model of the system. Moreover, the process is easy to understand and control even for domain experts with little knowledge of computer science. We formally prove the correctness of the approach, and evaluate the gains experimentally on a family of a postal voting models.

Formal analysis of security is often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the relevant security properties. In real life, this cannot be taken for granted. In particular, security mechanisms that are difficult and costly to use are often ignored by the users, and do not really defend the system against possible attacks. Here, we propose a graded notion of security based on the complexity of the user’s strategic behavior. More precisely, we suggest that the level to which a security property φ is satisfied can be defined in terms of: (a) the complexity of the strategy that the user needs to execute to make φ true, and (b) the resources that the user must employ on the way. The simpler and cheaper to obtain φ, the higher the degree of security. We demonstrate how the idea works in a case study based on an electronic voting scenario. To this end, we model the vVote implementation of the Prêt à Voter voting protocol for coercion-resistant and voter-verifiable elections. Then, we identify “natural” strategies for the voter to obtain voter-verifiability, and measure the voter’s effort that they require. We also consider the dual view of graded security, measured by the complexity of the attacker’s strategy to compromise the relevant properties of the election.

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems (MAS), together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.

Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic ( mv-ATL → ∗ ), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branchingtime logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL → ∗ . We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL → ∗ . We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL → ∗ and motivate its use for model checking multi-agent systems.

We propose a general semantics for strategic abilities of agents in asynchronous systems, with and without perfect information. Based on the semantics, we show some general complexity results for verification of strategic abilities in asynchronous interaction. More importantly, we develop a methodology for partial order reduction in verification of agents with imperfect information. We show that the reduction preserves an important subset of strategic properties, with as well as without the fairness assumption. We also demonstrate the effectiveness of the reduction on a number of benchmarks. Interestingly, the reduction does not work for strategic abilities under perfect information.

In this paper we introduce Strategy Logic with simple goals (SL[SG]), a fragment of Strategy Logic that strictly extends the well-known Alternating-time Temporal Logic ATL by introducing arbitrary quantification over the agents' strategies. Our motivation comes from game-theoretic applications, such as expressing Stackelberg equilibria in games, coercion in voting protocols, as well as module checking for simple goals. Most importantly, we prove that the model checking problem for SL[SG] is PTIME-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned.

Model checking strategic abilities in multi-agent systems is hard, especially for agents with partial observability of the state of the system. In that case, it ranges from NP-complete to undecidable, depending on the precise syntax and the semantic variant. That, however, is the worst case complexity, and the problem might as well be easier when restricted to particular subclasses of inputs. In this paper, we look at the verification of models with "extreme" epistemic structure, and identify several special cases for which model checking is easier than in general. We also prove that, in the other cases, no gain is possible even if the agents have almost full (or almost nil) observability. To prove the latter kind of results, we develop generic techniques that may be useful also outside of this study.

In this paper we investigate the Timed Alternating-Time Temporal Logic (TATL), a discrete-time extension of ATL. In particular, we propose, systematize, and further study semantic variants of TATL, based on different notions of a strategy. The notions are derived from different assumptions about the agents’ memory and observational capabilities, and range from timed perfect recall to untimed memoryless plans. We also introduce a new semantics based on counting the number of visits to locations during the play. We show that all the semantics, except for the untimed memoryless one, are equivalent when punctuality constraints are not allowed in the formulae. In fact, abilities in all those notions of a strategy collapse to the “counting” semantics with only two actions allowed per location. On the other hand, this simple pattern does not extend to the full TATL. As a consequence, we establish a hierarchy of TATL semantics, based on the expressivity of the underlying strategies, and we show when some of the semantics coincide. In particular, we prove that more compact representations are possible for a reasonable subset of TATL specifications, which should improve the efficiency of model checking and strategy synthesis.

In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the nested game again from scratch, thus, effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past. In this article, we investigate the alternative semantics for ATL*where the past is not forgotten in nested games. We show that the standard semantics of ATL*coincides with the “truly perfect recall” semantics for agents with perfect information and in case of so-called “objective” abilities under uncertainty. On the other hand, the two semantics differ significantly for the most popular (“subjective”) notion of ability under imperfect information. The same applies to the standard vs. “truly perfect recall” semantics of ATL*with persistent strategies. We compare the relevant variants of ATL*by looking at their expressive power, sets of validities, and tractability of model checking.

Automated verification of discrete-state systems has been a hot topic in computer science for over 35 years. Model checking of temporal and strategic properties is one of the most prominent and most successful approaches here. In this talk, I present a brief introduction to the topic, and mention some relevant properties that one might like to verify this way. Then, I describe some recent results on approximate model checking and model reductions, which can be applied to facilitate verification of notoriously hard cases.

A possible purpose of performing an action is to gather information. Such information-collecting actions are usually resource-consuming. The resources needed for performing them can be for example time or memory, but also money, specialized equipment, etc. In this work, we propose a formal framework to study how the ability of an agent to improve its knowledge changes as a result of changing the available resources. We introduce a model for resource-consuming information-collecting actions, and show how the process of accumulating knowledge can be modelled. Based on this model, we propose a modal logic for reasoning about the epistemic abilities of agents. We present some validities of the logic, and show that the model-checking problem sits in the first level of polynomial hierarchy. We also discuss the connection between our framework and classic information theory. More specifically, we show that the notion of uncertainty given by Hartley measure can be seen as a special case of an agent's ability to improve its knowledge using information-collecting actions.

We introduce a substructural modal logic of utility that can be used to reason aboutoptimality with respect to properties of states. Our notion of state is quite general, and is able to represent resource allocation problems in distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on resource semantics, which is closely related to concurrent separation logic. We consider a labelled transition semantics and establish conditions under which Hennessy—Milner soundness and completeness hold. By considering notions of cost, strategy and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics. We also show that our logic is able to serve as a logic for a fully featured process algebra and explain the interaction between utility and the structure of processes.

Judgment aggregation problems form a class of collective decision-making problems represented in an abstract way, subsuming some well known problems such as voting. A collective decision can be reached in many ways, but a direct one-step aggregation of individual decisions is arguably most studied. Another way to reach collective decisions is by iterative consensus building – allowing each decision-maker to change their individual decision in response to the choices of the other agents until a consensus is reached. Iterative consensus building has so far only been studied for voting problems. Here we propose an iterative judgment aggregation algorithm, based on movements in an undirected graph, and we study for which instances it terminates with a consensus. We also compare the computational complexity of our itterative procedure with that of related judgment aggregation operators.

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.

In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the nested game again from scratch, thus effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past.

Alternating-time temporal logic (ATL) is a wellknown logic for reasoning about strategic abilities of agents. An important feature that distinguishes variants of ATL for imperfect information scenarios is that the standard fixed point characterizations of temporal modalities do not hold anymore. In this paper, we show that adding explicit fixed point operators to the “next-time ” fragment of ATL already allows to capture abilities that could not be expressed in ATL. We also illustrate that the new language allows to specify important kinds of abilities, namely ones where the agents can always recompute their strategy while executing it. Thus, the agents are not assumed to remember their strategy by definition, like in the existing variants of ATL. Last but not least, we show that verification of such abilities can be cheaper than for all the variants of “ATL with imperfect information ” considered so far. 1

In agent-oriented programming and planning, agents ’ actions are typically specified in terms of postconditions, and the model of execution assumes that the environment carries the actions out exactly as specified. That is, it is assumed that the state of the environment after an action has been executed will satisfy its postcondition. In reality, however, such environments are rare: the actual execution of an action may fail, and the envisaged outcome is not met. We provide a conceptual framework for reasoning about success and failure of agents’ behaviours. In particular, we propose a measure that reflects how ”good” an environment is with respect to agent’s capabilities and a given goal it might pursue. We also discuss which types of goals are worth pursuing, depending on the type of environment the agent is acting in.

Alternating-time Temporal Logic (ATL) is probably themost influential logic of strategic ability that has emerged in recent years. The idea of ATL is centered around cooperation modalities: ≪A≫γ is satisfied if the group A of agents has a collective strategy to enforce temporal property γ against the worst possible response from the other agents. So, the semantics of ATL shares the "all-or-nothing" attitude of many logical approaches to computation. Such an assumption seems appropriate in some application areas (life-critical systems, security protocols, expensive ventures like space missions). In many cases, however, one might be satisfied if the goal is achieved with reasonable likelihood. In this paper, we try to soften the rigorous notion of success that underpins ATL.

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.