Reasoning about Cognitive Trust in Stochastic Multiagent Systems
Xiaowei Huang, Marta Kwiatkowska, Maciej Olejnik
TL;DR
This paper introduces a formal framework for modeling and verifying human-like trust in stochastic multiagent systems using an extended probabilistic logic that captures mental attitudes and social trust concepts.
Contribution
It proposes PRTL*, a novel probabilistic logic that incorporates mental attitudes and social trust, enabling automated reasoning about trust in multiagent systems.
Findings
The logic can express trust-related properties like probability thresholds for agent behavior.
The general verification problem is undecidable, but certain restrictions lead to decidable or tractable cases.
The framework advances formal analysis of trust in complex multiagent interactions.
Abstract
We consider the setting of stochastic multiagent systems modelled as stochastic multiplayer games and formulate an automated verification framework for quantifying and reasoning about agents' trust. To capture human trust, we work with a cognitive notion of trust defined as a subjective evaluation that agent A makes about agent B's ability to complete a task, which in turn may lead to a decision by A to rely on B. We propose a probabilistic rational temporal logic PRTL*, which extends the probabilistic computation tree logic PCTL* with reasoning about mental attitudes (beliefs, goals and intentions), and includes novel operators that can express concepts of social trust such as competence, disposition and dependence. The logic can express, for example, that `agent A will eventually trust agent B with probability at least p that B will behave in a way that ensures the successful…
Click any figure to enlarge with its caption.
Figure 1
Figure 2| share | keep | |
|---|---|---|
| invest | ||
| withhold |
| Strategy | ||||
|---|---|---|---|---|
| 0.7 | 0.3 | |||
| 0.1 | 0.9 | |||
| 0.0 | 1.0 | |||
| 1.0 | 0.0 |
| share | keep | |
|---|---|---|
| invest | (20,20+5) | (0,40-20) |
| withhold | (10,5) | (10,5) |
| PCTL | PTIME-complete |
| PCTL∗ | PSPACE-complete |
| BPRTL∗ | PSPACE-hard |
|---|---|
| PRTL | PSPACE-complete |
| PQRTL | PTIME |
| BPRTL∗ | PRTL | PQRTL |
|---|---|---|
| no or operators | is trivial | |
| all preceded by , or | , for single only | or |
| constant depth of , nesting | no nesting of and | |
| no or in scope of | ||
| constant # of and | ||
| “expanded system restriction” |
| 1. Deterministic Behaviour Assumption (Assumption 2) |
| 2. Uniformity Assumptions (Assumptions 1, 3) |
| 3. Transition Type Distinguishability Assumption (Assumption 4) |
| 4. Synchronous perfect recall (Remark 2) |
| 5. PCTL∗ formulas are evaluated in induced SMGs (Remark 7) |
| 6. Constraints on the language |
| 7. Seriality of legal goal and intention functions |
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
11institutetext: University of Oxford, Oxford, UK
11email: [email protected]
Reasoning about Cognitive Trust in Stochastic Multiagent Systems
Xiaowei Huang
Marta Kwiatkowska
Maciej Olejnik
Abstract
We consider the setting of stochastic multiagent systems modelled as stochastic multiplayer games and formulate an automated verification framework for quantifying and reasoning about agents’ trust. To capture human trust, we work with a cognitive notion of trust defined as a subjective evaluation that agent makes about agent ’s ability to complete a task, which in turn may lead to a decision by to rely on . We propose a probabilistic rational temporal logic PRTL∗, which extends the probabilistic computation tree logic PCTL∗ with reasoning about mental attitudes (beliefs, goals and intentions), and includes novel operators that can express concepts of social trust such as competence, disposition and dependence. The logic can express, for example, that “agent will eventually trust agent with probability at least that B will behave in a way that ensures the successful completion of a given task”. We study the complexity of the automated verification problem and, while the general problem is undecidable, we identify restrictions on the logic and the system that result in decidable, or even tractable, subproblems.
Keywords:
multi-agent systems stochastic games cognitive trust quantitative reasoning probabilistic temporal logic
1 Introduction
Mobile autonomous robots are rapidly entering the fabric of our society, to mention driverless cars and home assistive robots. Since robots are expected to work with or alongside humans in our society, they need to form partnerships with humans, as well as other robots, understand the social context, and behave, and be seen to behave, according to the norms of that context. Human partnerships such as cooperation are based on trust, which is influenced by a range of subjective factors that include subjective preferences and experience. As the degree of autonomy of mobile robots increases and the nature of partnerships becomes more complex, to mention shared autonomy, understanding and reasoning about social trust and the role it plays in decisions whether to rely on autonomous systems is of paramount importance. A pertinent example is the recent Tesla fatal car accident while on autopilot mode [38], which is a result of over-reliance (“overtrust”) by the driver, likely influenced through his personal motivation and preferences.
Trust is a complex notion, viewed as a belief, attitude, intention or behaviour, and is most generally understood as a subjective evaluation of a truster on a trustee about something in particular, e.g., the completion of a task [24]. A classical definition from organisation theory [40] defines trust as the willingness of a party to be vulnerable to the actions of another party based on the expectation that the other will perform a particular action important to the trustor, irrespective of the ability to monitor or control that party. The importance of being able to correctly evaluate and calibrate trust to guide reliance on automation was recognised in [39]. Trust (and trustworthiness) have also been actively studied in many application contexts such as security [31] and e-commerce [14]. However, in this paper we are interested in trust that governs social relationships between humans and autonomous systems, and to this end consider cognitive trust that captures the human notion of trust. By understanding how human trust in an autonomous system evolves, and being able to quantify it and reason about it, we can offer guidance for selecting an appropriate level of reliance on autonomy.
The goal of this paper is therefore to develop foundations for automated, quantitative reasoning about cognitive trust between (human and robotic) agents, which can be employed to support decision making in dynamic, uncertain environments. The underlying model is that of multiagent systems, where agents are autonomous and endowed with individual goals and preferences in the style of BDI logic [45]. To capture uncertainty, we work in the setting of stochastic multiagent systems, represented concretely in terms of concurrent stochastic multiplayer games, where stochasticity can be used to model, e.g., component failure or environmental uncertainty. This also allows us to represent agent beliefs probabilistically. Inspired by the concepts of social trust in [17], we formulate a probabilistic rational temporal logic PRTL∗ as an extension of the probabilistic temporal logic PCTL∗ [23] with cognitive aspects. PCTL∗ allows one to express temporal properties pertaining to system execution, for example “with probability , agent A will eventually complete a given task”. PRTL∗ includes, in addition, mental attitude operators (belief, goal, intention and capability), together with a collection of novel trust operators (competence, disposition and dependence), in turn expressed using beliefs. The logic PRTL∗ is able to express properties such as “agent A will eventually trust agent B with probability at least that B will behave in a way that ensures the successful completion of a given task” that are informally defined in [17]. PRTL∗ is interpreted over a stochastic multiagent system, where the cognitive reasoning processes for each agent can be modelled based on a cognitive mechanism that describes his/her mental state (a set of goals and an intention, referred to as pro-attitudes) and subjective preferences.
Since we wish to model dynamic evolution of beliefs and trust, the mechanisms are history-dependent, and thus the underlying semantics is an infinite branching structure, resulting in undecidability of the general model checking problem for PRTL∗. In addition, there are two types of nondeterministic choices available to the agents, those made along the temporal or the cognitive dimension. By convention, the temporal nondeterminism is resolved using the concept of adversaries and quantifying over them to obtain a fully probabilistic system [22], as is usual for models combining probability and nondeterminism. We use a similar approach for the cognitive dimension, instead of the classical accessibility relation employed in logics for agency, and resolve cognitive nondeterminism by preference functions, given as probability distributions that model subjective knowledge about other agents. Also, in contrast to defining beliefs in terms of knowledge [16] and probabilistic knowledge [22] operators, which are based solely on agents’ (partial) observations, we additionally allow agents’ cognitive changes and subjective preferences to influence their belief.
This paper makes the following original contributions.
We introduce autonomous stochastic multiagent systems as an extension of stochastic multiplayer games with a cognitive mechanism for each agent (a set of goals and intentions).
We provide a mechanism for reasoning about agent’s cognitive states based on preference functions that enables a sound formulation of probabilistic beliefs.
We formalise a collection of trust operators (competence, disposition and dependence) informally introduced in [17] in terms of probabilistic beliefs.
We formulate a novel probabilistic rational temporal logic PRTL∗ that extends the logic PCTL∗ [23] with mental attitude and trust operators.
We study the complexity of the automated verification problem for PRTL∗ and, while the general problem is undecidable, we identify restrictions on the logic and the system that result in decidable, or even tractable, subproblems.
The structure of the paper is as follows. Section 2 gives an overview of related work, and in Section 3 we discuss the concept of cognitive trust. Section 4 presents stochastic multiplayer games and strategic reasoning on them. Section 5 introduces autonomous stochastic multiagent systems, an extension of stochastic multiplayer games with a cognitive mechanism. Section 6 introduces preference functions and derives the semantics of the subjective, probabilistic belief operator. Section 7 defines how beliefs vary with respect to agents’ observations. In Section 8 we define trust operators and the logic PRTL∗. We consider the interactions of beliefs and pro-attitudes in Section 9 via pro-attitude synthesis. Section 10 gives the undecidable complexity result for the general PRTL∗ model checking problem and Section 11 presents several decidable logic fragments. We conclude the paper in Section 12.
A preliminary version of this work appeared as [29]. This extended version includes detailed derivations of the concepts, illustrative examples and full proofs of the complexity results omitted from [29].
2 Related Work
The notion of trust has been widely studied in management, psychology, philosophy and economics (see [37] for an overview). Recently, the importance of trust in human-robot cooperation was highlighted in [35]. Trust in the context of human-technology relationships can be roughly classified into three categories: credentials-based, experience-based, and cognitive trust. Credentials-based trust is used mainly in security, where a user must supply credentials in order to gain access. Experience-based trust, which includes reputation-based trust in peer-to-peer and e-commerce applications, involves online evaluation of a trust value for an agent informed by experiences of interaction with that agent. A formal foundation for quantitative reputation-based trust has been proposed in [33]. In contrast, we focus on (quantitative) cognitive trust, which captures the social (human) notion of trust and, in particular, trust-based decisions between humans and robots. The cognitive theory of [17], itself founded on organisational trust of [40], provides an intuitive definition of complex trust notions but lacks rigorous semantics. Several papers, e.g., [41, 30, 25, 26], have formalised the theory of [17] using modal logic, but none are quantitative and automatic verification is not considered. Of relevance are recent approaches [49, 48] that model the evolution of trust in human-robot interactions as a dynamical system; instead, our formalism supports evolution of trust through events and agent interactions.
A number of logic frameworks have been proposed that develop the theory of human decisions [6] for artificial agents, see [42] for a recent overview. The main focus has been on studying the relationships between modalities with various axiomatic systems, but their amenability to automatic verification is arguable because of a complex underlying possible world semantics, to mention the sub-tree relation of BDI logic [45]. The only attempt at model checking such logics [47] ignores the internal structure of the possible worlds to enable a reduction to temporal logic model checking.
The distinctive aspects of our work is thus a quantitative formalisation of cognitive trust in terms of probabilistic temporal logic, based on a probabilistic notion of belief, together with algorithmic complexity of the corresponding model checking problem.
3 Cognitive Theory of Social Trust
In the context of automation, trust is understood as delegation of responsibility for actions to the autonomous system and willingness to accept risk (possible harm) and uncertainty. The decision to delegate is based on a subjective evaluation of the system’s capabilities for a particular task, informed by factors such as past experience, social norms and individual preferences. Moreover, trust is a dynamic concept which evolves over time, influenced by events and past experience. The cognitive processes underpinning trust are captured in the influential theory of social trust by [17], which is particularly appropriate for human-robot relationships and serves as an inspiration for this work.
The theory of [17] views trust as a complex mental attitude that is relative to a set of goals and expressed in terms of beliefs, which in turn influence decisions about agent’s future behaviour. They consider agent ’s trust in agent for a specific goal (goals may be divided into tasks), and distinguish the following core concepts: competence trust, where believes that is able to perform , and disposition trust, where believes that is willing to perform . The decision to delegate or rely on involves a complex notion of trust called dependence: believes that needs, depends, or is at least better off to rely on to achieve , which has two forms, strong ( needs or depends on ) and weak (for , it is better to rely than not to rely on ). [17] also identify fulfilment belief arising in the truster’s mental state, which we do not consider.
We therefore work in a stochastic setting (to represent uncertainty), aiming to quantify belief probabilistically and express trust as a subjective, belief-weighted expectation, informally understood as a degree of trust.
4 Stochastic Multiagent Systems and Temporal Reasoning
A multiagent system comprises a set of agents (humans, robots, components, processes, etc.) running in an environment [16]. To capture random events such as failure and environmental uncertainty that are known to influence trust, we work with stochastic multiagent systems, concretely represented using concurrent stochastic multiplayer games, where each agent corresponds to a player. Taking such models as a starting point, in this section we gradually extend them to autonomous multiagent systems that support cognitive reasoning.
4.1 Stochastic Multiplayer Games
Given a finite set , we denote by the set of probability distributions on and by the power set of . Given a probability distribution over a set , we denote by the support of , i.e., the set of elements of which have positive probability. We call a Dirac distribution if for some .
We now introduce concurrent stochastic games, in which several players repeatedly make choices simultaneously to determine the next state of the game.
Definition 1.
A stochastic multiplayer game (SMG) is a tuple , where:
is a finite set of players called agents, ranged over by , , …
is a finite set of states,
is a set of initial states,
is a finite set of actions for the agent ,
is a (partial) probabilistic transition function, where ,
is a labelling function mapping each state to a set of atomic propositions taken from a set .
We assume that each (global) state of the system includes a local state of each agent and an (optional) environment state. In every state of the game, each player selects a local action independently and the next state of the game is chosen by the environment according to the probability distribution where is the joint action. In other words, the probability of transitioning from state to state when action is taken is . In this paper we will usually omit the environment part of the state.
In concurrent games players perform their local actions simultaneously. Turn-based games are a restricted class of SMGs whose states are partitioned into subsets, each of which is controlled by a single agent, meaning that only that agent can perform an action in any state in the partition. Turn-based games can be simulated by concurrent games by requiring that, in states controlled by agent , performs an action and the other agents perform a distinguished silent action .
Let denote agent ’s action in the joint action . We let be the set of valid joint actions in state , and be the set of valid actions in state for agent . is called serial (or total) if, for any state and joint action , is defined. We often write for a transition from to via action , provided that .
Paths
A path is a finite or infinite sequence of states induced from the transition probability function , i.e., satisfying for some , for all . Paths generated by are viewed as occurring in the temporal dimension. We denote the set of finite (resp. infinite) paths of starting in by (resp. ), and the set of paths starting from any state by (resp. ). We may omit if clear from the context. For any path we write for its -th state, for the prefix , and for the suffix when is infinite. If is finite then we write for its last state and for its length, i.e., the number of states in . Given two paths and , we write when for their concatenation by an overlapping state, and for the regular concatenation.
Strategies
A (history-dependent and stochastic) action strategy of agent in an SMG is a function , such that for all and finite paths it holds that only if . We call a strategy pure if is a Dirac distribution for any . A strategy profile for a set of agents is a vector of action strategies , one for each agent . We let be the set of agent ’s strategies, be the set of strategy profiles for the set of agents , and be the set of strategy profiles for all agents.
Probability space
In order to reason formally about a given SMG we need to quantify the probabilities of different paths being taken. We therefore define a probability space over the set of infinite paths starting in a given state , adapting the standard construction from [32]. Our probability measure is based on the function assigning probability to a given finite path under strategy , defined as . To define measurable sets, for a path we let be a basic cylinder, which is a set of all infinite paths starting with . We then set to be the smallest -algebra generated by the basic cylinders and to be the unique measure on the set of infinite paths such that . It then follows that is a probability space [32].
Example 1.
We consider a simple (one shot) trust game from [34], in which there are two agents, Alice and Bob. At the beginning, Alice has 10 dollars and Bob has 5 dollars. If Alice does nothing, then everyone keeps what they have. If Alice invests her money with Bob, then Bob can turn the 15 dollars into 40 dollars. After having the investment yield, Bob can decide whether to share the 40 dollars with Alice. If so, each will have 20 dollars. Otherwise, Alice will lose her money and Bob gets 40 dollars.
For the simple trust game, the payoffs of the agents are shown in Table 1. The game has a Nash equilibrium of Alice withholding her money and Bob keeping the investment yield. This equilibrium discourages collaboration between agents and has not been confirmed empirically under the standard economic assumptions of pure self-interest [5].
To illustrate our methods, we construct a stochastic multiplayer game with , with being the initial state, , and the transition function defined in an obvious way (see Figure 1). Note that we do not represent payoffs explicitly in our modelling of the trust game, but rather capture them using atomic propositions. For example, is true is state , while holds in . Note also that and proceed in turns, which is captured through joint actions where the other agent takes the silent action . We represent states as pairs:
[TABLE]
where is Alice’s last action and is Bob’s last action. For example, , and .
We now equip agents with strategies. For Alice, we define and , where the former corresponds to high likelihood of Alice investing her money and the latter allocates greater probability to withholding it. For Bob, we set two pure strategies and , corresponding to him keeping and sharing the money with Alice. The strategies are summarised in Table 2.
4.2 Temporal Reasoning about SMGs
We now recall the syntax of the Probabilistic Computation Tree Logic PCTL∗ [3, 4]111Note that we do not consider here the coalition operator, and therefore the logic rPATL* [12] that is commonly defined over stochastic game models. for reasoning about temporal properties in systems exhibiting nondeterministic and probabilistic choices. PCTL∗ is based on CTL∗ [13] for purely nondeterministic systems and retains its expressive power, additionally extending it with a probabilistic operator .
Definition 2.
The syntax of the logic PCTL∗ is as follows.
[TABLE]
where is an atomic proposition, , and .
In the above, is a PCTL∗ (state) formula and an LTL (path) formula. The operator is the (universal) path quantifier of CTL∗ and is the probabilistic operator of PCTL [23], which expresses that holds with probability in relation with . The remaining operators, (next) and (until) follow their usual meaning from PCTL and CTL∗. The derived operators such as , (eventually), (globally), (release) and (existential path quantifier) can be obtained in the standard way.
Let be an SMG. Given a path which has as its last state, a strategy of , and a formula , we write:
[TABLE]
for the probability of implementing on a path when a strategy applies. The relation is defined below. Based on this, we define:
[TABLE]
as the minimum and maximum probabilities of implementing on a path over all strategies in .
We now give semantics of the logic PCTL∗ for concurrent stochastic games.
Definition 3.
Let be an SMG and . The satisfaction relation of PCTL∗ is defined inductively by:
if ,
if not ,
if or ,
if for all ,
if , where
[TABLE]
and for any infinite continuation of (i.e., ):
if ,
if not ,
if or ,
if ,
if there exists such that and for all .
We note that the semantics of state formulas is defined on finite paths (histories) rather than states, whereas the semantics of path formulas is defined on a finite path together with its infinite continuation (rather than a single infinite path). The reason for defining it in such a way is to be consistent with definitions of trust operators (which we introduce in Section 8), whose semantics is dependent on execution history (understood as a sequence of past states of a system).
Below, we write for , for , for and for (inverting the order), and write for , for , for , and for (strict/non-strict variants).
Proposition 1.
Let be an SMG and . The following equivalences hold for any formula :
* iff * 2. 2.
* iff *
Definition 4.
For a given SMG and a formula of the language PCTL∗, the model checking problem, written as , is to decide whether for all initial states .
Example 2.
Here we give a few examples of PCTL∗ formulas that we may wish to check on the trust game from Example 1. The formula
[TABLE]
expresses that the probability of Alice investing in the next step is no greater than 0.9. On the other hand, the formula
[TABLE]
states (the obvious fact) that the probability of Bob keeping the money in the future is no greater than 1. Finally, the formula
[TABLE]
where is an atomic proposition with obvious meaning, states that eventually a state can be reached where Alice has more money than Bob.
All the above formulas are true when evaluated at the state , given in Fig 1.
5 Stochastic Multiagent Systems with the Cognitive Dimension
In this section, we present a framework for reasoning about autonomous agents in multiagent systems. The key novelty of our model is the consideration of agents’ mental attitudes to enable autonomous decision making, which we achieve by equipping agents with goals and intentions (also called pro-attitudes). We enhance stochastic multiplayer games with a cognitive mechanism to represent reasoning about goals and intentions. The system then evolves along two interleaving dimensions: temporal, representing actions of agents in the physical space, and cognitive, which corresponds to mental reasoning processes, i.e., goal and intention changes, that determine the actions that agents take.
5.1 Cognitive Reasoning
We now motivate and explain the concepts of the cognitive state of an agent and the cognitive mechanism, and how they give rise to partial observability.
Cognitive State
We assume that each agent has a set of goals and a set of intentions, referred to as pro-attitudes and viewed as high-level concepts. We follow existing literature, see e.g., Bratman [6] and Gollwitzer [21], etc., and identify commitment as the distinguishing factor between goals and intentions, i.e., an intention is a committed plan of achieving some immediate goal. We therefore think of goals as abstract attitudes, for example selflessness or risk-taking, whereas intentions are more concrete and directly influence agents’ behaviour. Goals are usually static and independent of external factors, whereas intentions are dynamic, influenced by agent’s own goals and by its beliefs about other agents’ pro-attitudes. For the purposes of our framework, we assume that agents use action strategies to implement their intentions and therefore there exists a one-to-one association between intentions and action strategies. This way, agents’ behaviour in the physical space is determined by their mental state.
For an agent , we use to denote its set of goals and to denote its set of intentions. At any particular time, an agent may have several goals, but can only have a single intention. Goals are not required to satisfy constraints such as consistency.
Definition 5.
Let be an agent and let and be its set of goals and intentions, respectively. A cognitive state of consists of a set of goals and an intention, which can be retrieved from global states of the system using the following functions:
, i.e., is a set of agent ’s goals in state ,
, i.e., is the agent ’s intention in state .
To illustrate the concepts, we now extend the trust game given in the previous examples to include agents’ goals and intentions.
Example 3.
It is argued in [34] that the single numerical value as the payoff of the trust game introduced in Example 1 is an over-simplification. A more realistic utility should include both the payoff and other hypotheses, including trust. An example payoff table is given in Table 3, in which Bob’s payoff will increase by 5 to denote that he will gain Alice’s trust if sharing the investment yield and decrease by 20 to denote that he will lose Alice’s trust if keeping the investment yield without sharing. With the updated payoffs, the new Nash equilibrium is for Alice to invest her money and Bob to share the investment yield.
The main point for the new payoffs is for the agents to make decisions not only based on the original payoffs, but also based on the trust that the other agent has. This reflects some actual situations in which one agent may want to improve, or at least maintain, the trust of the other agent. In our modelling of such a game, we show that this can be captured by adding the cognitive dimension and assuming that Bob makes decisions by considering additionally whether Alice’s trust in him reaches a certain level.
For Alice, we let be two goals which represent her attitude towards investment. Intuitively, passive represents the goal of keeping the cash and active represents the goal of investing. For simplicity, we assume that Alice’s intention is determined by her goals and set . We also assume that Alice uses strategy to implement her passive intention, and to implement her active intention, where the strategies are defined in Example 1.
Bob has a set of goals , which represent the goals of being an investor pursuing long-term profits and being an opportunist after short-term profits, respectively. As for Alice, Bob’s intentions are associated with action strategies, and we have already defined two such strategies: , in which Bob shares the investment yield with Alice, and , in which Bob keeps all the money for himself. Hence , with the obvious association. We assume that Bob’s intention will be share when he is an investor and his belief in Alice being active is above a certain threshold, and keep otherwise. Intuitively, when he is an investor, Bob intends to build a good relationship with Alice (in other words, gain Alice’s trust), hoping that it will pay off in his future interactions with her.
We extend the trust game defined in Example 1 by expanding the states to additionally include cognitive states. In particular, each state can now be represented as a tuple:
[TABLE]
such that and are as before and , , , and denote the cognitive part of the state, namely Alice’s and Bob’s goals and intentions.
Partial Observation
It is common that, in real-world systems, agents are not able to fully observe the system state at any given time. In a typical scenario, every agent runs a local protocol, maintains a local state, observes part of the system state by, e.g., sensing devices, and communicates with other agents. It is impractical, and in fact undesirable, from the system designer’s point of view, to assume that agents can learn the local states of other agents or learn what the other agents observe. In the context of our work partial observability arises naturally through the cognitive state, which represents an internal state of every agent that is, in general, not observable by other agents. We formalise this notion with the following definition.
Definition 6.
A partially observable stochastic multiplayer game (POSMG) is a tuple , where
is an SMG,
is a finite set of observations for agent , and
is a labelling of states with observations for agent .
Remark 1.
We note that, unlike partially observable Markov processes (POMDPs), in which observations are probability distributions, we follow the setting in [18] and work with deterministic observations. In [20], it is stated without proof that probabilistic observations do not increase the complexity of the problem.
We lift the observations from states to paths in the obvious way. Formally, for a finite path , we define .
Remark 2.
In our model, an agent remembers both its past observations and the number of states, known as synchronous perfect recall [16]. This assumption is necessary for the definition of belief in Section 7.
Example 4.
For the trust game from Example 3, the agents’ observation functions for are as follows:
[TABLE]
denoting that they cannot observe the opponent’s cognitive state but can observe their last action. The set of observations can be easily inferred from this definition.
We say is fully observable if iff for all . In fully observable systems, agents make decisions based on the current state, whereas in partially observable systems decisions must be based on all past observations.
Cognitive Mechanism
While agents interact with each other and with the environment by taking actions in the physical space, they make decisions through cognitive processes that determine their behaviour. Thus, in addition to the temporal dimension of transitions , we also distinguish a cognitive dimension of transitions , which corresponds to mental reasoning processes. The idea is that each temporal transition is preceded by a cognitive transition, which represents an agent’s reasoning that led to its decision about which action to take. While transitions in the temporal dimension conform to the transition function , cognitive changes adhere to the cognitive mechanism, which determines for an agent its legal goals and intentions. Formally, we have the following definition of a stochastic game extended with a cognitive mechanism.
Definition 7.
A stochastic multiplayer game with the cognitive dimension (SMGΩ) is a tuple , where
is a POSMG,
is the cognitive mechanism of agent , consisting of a legal goal function and a legal intention function , and
is the cognitive strategy of agent , consisting of a goal strategy and an intention strategy .
We refer to the SMG from the above definition as the induced SMG from .
Thus, the SMGΩ model generalises the usual notion of multiplayer games by extending states with agents’ cognitive states, and adding for each agent the cognitive mechanism and ’s cognitive strategies to enable autonomous decision making. We sometimes refer to the set of cognitive mechanisms of all agents as the cognitive mechanism of the system .
The legal goal (resp. intention) function (resp. ) specifies legal goal (resp. intention) changes in a given state. Intuitively, those are goal (resp. intention) changes that an agent is allowed (but might not be willing) to make. One possible use of those functions is to enforce application-specific constraints that goals or intentions must satisfy (see Example 5).
The cognitive strategy determines how an agent’s cognitive state evolves over time. Specifically, the goal (resp. intention) strategy (resp. ) specifies the incurred goal (resp. intention) changes (along with their probabilities), which are under agent ’s consideration for a given execution history. We sometimes call (resp. ) a possible goal (resp. intention) function and require that possible goal (resp. intention) changes are also legal. Formally, for all , we must have and .
Remark 3.
We remark that cognitive strategies and are, in general, not computable. In Section 9 we propose how to realise cognitive strategies so that they can be effectively computed.
We note the following correspondence between the cognitive and temporal dimension: and (regarded as sets) specify all the goals and intentions of a given agent similarly to the way that specifies all the actions of , while the cognitive mechanism identifies possible cognitive transitions in a similar fashion to the transition function playing the same role for the temporal dimension. Finally, a cognitive strategy gives the probability for agents’ goal and intention changes, analogously to an action strategy quantifying the likelihood of actions taken by agents in the temporal dimension.
The following standard assumption ensures that agents’ temporal and cognitive transitions, as well as their cognitive strategies, are consistent with their partial observability.
Assumption 1**.**
(Uniformity Assumption) An SMGΩ satisfies the Uniformity Assumption if the following conditions hold.
Agents can distinguish states with different sets of joint actions or legal cognitive changes: for any two states and and an agent , implies , , and , for all .
Agents can distinguish execution histories which give rise to different cognitive strategies: for any two finite paths , , implies and for all .
Given a state and a set of agent A’s goals , we write for the state obtained from by substituting agent ’s goals with . Similar notation is used for the intention change when . Alternatively, we may write if contains the goal set for and if contains the intention for .
Example 5.
Having extended states of the trust game with goals and intentions in Example 3, we now make into an SMGΩ by introducing cognitive transitions, defining the cognitive mechanism and specifying cognitive strategies of agents.
We give a graphical representation of in Figure 2. Note that w and i stand for Alice’s actions withhold and invest respectively, whereas s and k denote Bob’s actions share and keep. Cognitive transitions are represented with dashed lines. Temporal actions are annotated with probabilities which reflect the intention (i.e., an action strategy) that an agent has in a given state.
Below we explain how we arrived at such a system. The execution of the game starts by agents choosing their goals. While it may seem unnatural (a more realistic approach would probably involve multiple initial states corresponding to agents having different goals), such a way of modelling plays well with our formalism and does not restrict the generality of our approach. Formally, we specify those cognitive transitions using legal goal function for Alice and Bob as follows:
[TABLE]
where .
Once their goals are set, agents begin interacting with one another in the physical space by taking actions. However, each action is preceded by an agent determining its intention, which represents the mental reasoning that results in action selection. Note that we do not depict Alice’s intention change in Figure 2, the reason being our assumption that Alice’s intention is fully determined by her goals.
As mentioned above, Alice’s actions are annotated with probabilities, according to our assumption that cognitive state determines agents’ behaviour. For example, in states and , Alice’s intention is passive, and so the probabilities of withholding and investing the money are given by Table 2. If Alice withholds her money, the game ends. Otherwise, Bob determines his intention (his choice depends on his goals and his belief about Alice’s goals) and performs his action of keeping or sharing his profit. Bob’s legal intentions are given by his legal intention function, defined as:
[TABLE]
where .
Finally, we define Bob’s intention strategy. As mentioned above, Bob takes on intention share only if he is an investor and he believes that Alice is active. The latter depends on Alice’s actions in the physical space (since Bob can’t observe Alice’s cognitive state). In this case, Alice investing her money with Bob increases his belief that she is active. We therefore set:
[TABLE]
Note that the above strategy is pure. While the framework does not enforce it, we believe defining it in such a way more accurately resembles human cognitive processes. Also, as we will see later, pure intention strategies are more compatible with our trust formulations.
Finally, note that we don’t consider goal strategies here. The reason for that is our representation of goals in this example as static mental attitudes which agents possess or not, rather than choose dynamically. We therefore treat the first two cognitive transitions as nondeterministic for now. In Section 6, we introduce a mechanism which motivates choosing such representation.
Remark 4.
We remark that, while defining the intention strategy as in the above example is easy for simple systems, for more complex games this approach does not scale. In particular, we could consider repeated version of the trust game, for which constructing Bob’s intention strategy manually is impractical. However, in Section 7, we formalise the notion of agent’s belief and, in Section 9, we propose an intuitive method of constructing the intention strategy efficiently.
Induced SMG
For a concrete system, it is conceptually simpler to assume a certain, predefined interleaving of cognitive and temporal transitions, as we did in Example 5. However, in general, such interleaving might be arbitrary since agents may change their mental state at any time. It is therefore often useful to think of a SMGΩ as a collection of induced SMGs, each corresponding to one configuration of mental states of agents. Those induced SMGs do not differ as far as their components are concerned (i.e., states, actions and transitions are the same), but different mental states give rise to different behaviour. Execution of such an SMGΩ can then be viewed as starting in one of the induced SMGs, remaining there as long as agents perform temporal actions and moving to a different induced SMG as soon as one agent changes its mental state. In the long run, execution alternates between different standard SMGs, where, at any point, current SMG reflects current mental states of agents, and each temporal transition preserves the current SMG, while each cognitive transition switches to a different SMG. The benefit of such an approach is that each induced SMG can then be reasoned about using standard techniques. We note also that, for the purposes of the logic operators introduced later in the paper, we assume that both temporal and cognitive transitions are available to agents in any state.
Paths
In contrast to the conventional multiplayer games, where each path includes a sequence of temporal transitions, which are consistent with the transition function , in an SMGΩ, in view of the active participation of agents’ pro-attitudes in determining their behaviour, a path can be constructed by interleaving of temporal and cognitive transitions. Each cognitive transition represents a change of an agent’s goals or intention. We now extend the definition of a path to allow cognitive transitions.
Definition 8.
Given a stochastic multiplayer game with the cognitive dimension (SMGΩ) , we define a finite, respectively infinite, path as a sequence of states such that, for all , one of the following conditions is satisfied:
for some joint action such that , 2. 2.
for some and , 3. 3.
for some and .
We reuse the notation introduced in Section 4.1 for regular paths and denote the set of finite (resp. infinite) paths by (resp. ), and the set of finite (resp. infinite) paths starting in state by (resp. ).
The first condition represents the standard temporal transition, while the other two stand for cognitive transitions – the former is a goal change, whereas the latter is an intention change.
We often require that both the legal goal function and the legal intention function are serial, i.e., for any state and any subset of , there exists a state such that , and for any state and any intention , there exists a state such that . This is a non-trivial requirement, since such states can be unreachable via temporal transitions.
Remark 5.
We remark that the seriality requirement for the probabilistic transition function is usually imposed for model checking, and by no means reduces the generality of the problem, as we can introduce absorbing states to accommodate undefined temporal or cognitive transitions in an obvious way.
Deterministic Behaviour Assumption
Recall that intentions of agents are associated with action strategies, thereby determining agents’ behaviour in a physical space. Below, we formalise that idea, in addition requiring that the associated strategies are pure, which simplifies results.
Assumption 2**.**
(Deterministic Behaviour Assumption) An SMGΩ satisfies the Deterministic Behaviour Assumption if each agent’s cognitive state deterministically decides its behaviour in terms of selecting its next local action. In other words, agent’s cognitive state induces a pure action strategy that it follows.
Hence, since global states encode agents’ cognitive states, under Assumption 2 the transition function becomes deterministic, i.e., for every state , there exists a unique joint action such that next state is chosen with probability . Therefore, each SMG induced from , with fixed pro-attitudes, can be regarded as a Markov chain.
Remark 6.
We note that a more general version of Assumption 2 is possible, where the action strategy is not assumed to be pure, and our results can be easily adapted to that variant. In fact, action strategies introduced in Example 1 are not pure and so the trust game does not satisfy the strict version of the Deterministic Behaviour Assumption as stated above. Example 7 illustrates how the calculations can be adapted to handle that.
5.2 Cognitive Reasoning
We can now extend the logic PCTL∗ with operators for reasoning about agent’s cognitive states, resulting in the logic called Probabilistic Computation Tree Logic with Cognitive Operators, PCTL.
Definition 9.
The syntax of the logic PCTL is:
[TABLE]
where , , , and .
Intuitively, the newly introduced cognitive operators (goal), (intention) and (capability) consider the task expressed as and respectively quantify, in the cognitive dimension, over possible changes of goals, possible intentions and legal intentions.
The semantics for PCTL is as follows.
Definition 10.
Let be a SMGΩ, a finite path in and such that . The semantics of previously introduced operators of PCTL∗ remains the same in PCTL. For the newly introduced cognitive operators, the satisfaction relation is defined as follows:
if : and ,
if : and ,
if : and .
Thus, expresses that holds in future regardless of agent changing its goals. Similarly, states that holds regardless of changing its intention, whereas quantifies over the legal intentions, and thus expresses that agent could change its intention to achieve (however, such a change might not be among agent’s possible intention changes).
Remark 7.
We note that, when evaluating PCTL∗ operators, we assume that agents keep their current mental attitudes, i.e., that the future path is purely temporal. Formally, for a SMGΩ , PCTL∗ operators should be interpreted over the SMG induced from . Furthermore, when evaluating PCTL formulas, we assume agents can change their goals and intentions at any time, in line with the ‘induced SMGs’ interpretation presented in Section 5.1. That ensures that the cognitive operators can be applied at any point of execution, as well as meaningfully chained, nested or manipulated in any other way.
Remark 8.
We comment here about our definition of the semantics of , and , whereby the changes of goals and intentions do not incur the changes of other components of the state. This can be counter-intuitive for some cases, e.g., it is reasonable to expect that the intention of the agent may change when its goals are changed. We believe that such dependencies are better handled at the modelling stage. For example, a simultaneous change of goals and intention can be modelled as two consecutive cognitive transitions – a goal change followed by an intention change.
Below, we write with for . For instance, formula expresses that it is possible to achieve by changing agent ’s intention. Note that it is not equivalent to , which quantifies over legal, rather than possible, intentions.
Example 6.
Here we give examples of formulas that we may wish to check on the trust game from Example 5. The formula:
[TABLE]
expresses that, regardless of Alice changing her goals, the probability of her investing in the future is no greater than 90%. On the other hand, the formula:
[TABLE]
states that Bob has a legal intention which ensures that he will not keep the money as his next action. Also, the formula:
[TABLE]
where is an atomic proposition with obvious meaning, states that Alice can find an intention such that eventually a state can be reached where Alice has more money than Bob. Finally, the formula:
[TABLE]
expresses that Alice can find an intention such that it is possible to reach a state such that, for all possible Bob’s goals, the game will always reach a state in which Bob is no poorer than Alice.
In this paper we study the model checking problem defined as follows.
Definition 11.
For a given SMGΩ and a formula of the language PCTL the model checking problem, written as , is to decide whether for all initial states .
The model checking problem amounts to checking whether a given finite model satisfies a formula. For logics PCTL and PCTL∗ the model checking problem over Markov chains is known to be decidable, with the complexity results summarised in Table 4. These logics thus often feature in probabilistic model checkers, e.g., PRISM [36] and Storm [15]. In contrast, the satisfiability problem, i.e., the whether there exists a model that satisfies a given formula, for these logics is an open problem [8]. Therefore. the satisfiability problem for the logic introduced here is likely to be challenging.
Consider a SMGΩ in which agents never change their mental attitudes. Then, thanks to Assumption 2, all transitions in the system are effectively deterministic and can be viewed as a Markov chain. Using complexity results summarised in Table 4 we formalise the above observation with the following theorem.
Theorem 5.1.
If the cognitive strategies of all agents in a system are constant, then the complexity of model checking PCTL over SMGΩ is PSPACE-complete, and model checking PCTLΩ over SMGΩ is PTIME-complete.
However, it is often unrealistic to assume that agents’ cognitive strategies are constant. In Section 9, we suggest a variation of our model based on agents reasoning about their beliefs and trust, all of whose components are finite, which makes it amenable for model checking.
6 Preference Functions and Probability Spaces
In this section, we develop the foundations for reasoning with probabilistic beliefs, which we define in Section 7. In order to support subjective beliefs, we utilise the concept of preference functions, which resolve the nondeterminism arising from agents’ cognitive transitions in a similar way to how action strategies resolve nondeterminism in the temporal dimension. This enables the definition of probability spaces to support reasoning about beliefs, which will in turn provide the basis for reasoning about trust. The central model of this paper, autonomous stochastic multiagent systems, is then introduced.
Preference Functions
To define a belief function, the usual approach is to employ for every agent a preference ordering, which is a measurement over the worlds. This measurement is commonly argued to naturally exist with the problem, see [18] for an example. However, the actual definition of such a measurement can be non-trivial, because the number of worlds can be very large or even infinite, e.g. in [18] and in this paper, and thus enumerating all worlds can be infeasible.
In this paper, instead of an (infinite definition of) preference ordering, we resolve the nondeterminism in the system by introducing preference functions. The key idea for a preference function is to estimate, for an agent , the possible changes of goals or intentions of another agent in a given state using a probability distribution. In other words, preference functions model probabilistic prior knowledge of agent about pro-attitudes of another agent . That knowledge may be derived from prior experience (through observations), personal preferences, social norms, etc., and will in general vary between agents. A uniformly distributed preference function can be assumed if no prior information is available, as is typical in Bayesian settings.
Resolving the nondeterminism (for temporal dimension – by Assumption 2, for cognitive dimension – by preference functions) allows us to define a family of probability spaces for each agent. Since preference functions vary among agents, probability spaces are also different for every agent. Moreover, each agent has multiple probability spaces, corresponding to its own various cognitive states. Intuitively, every probability space represents agent’s subjective view on the relative likelihood of different infinite paths being taken in the system.
We are now ready to define the central model of this paper.
Definition 12.
An autonomous stochastic multi-agent system (ASMAS) is a tuple , where
is an SMGΩ and
is a family of preference functions of agent , defined as
[TABLE]
where:
- –
is a goal preference function of over such that, for any state and , we have only if , and
- –
is an intention preference function of over such that, for any state and , we have only if .
Remark 9.
During system execution, preference functions may be updated as agents learn new information through interactions; we will discuss in Section 9 how this can be implemented in our framework.
Intuitively, a preference function provides agent with a probability distribution over another agent ’s changes of pro-attitudes. Naturally, we expect preference functions to be consistent with partial observability. We therefore extend the Uniformity Assumption in the following way.
Assumption 3**.**
(Uniformity Assumption II) Let be an ASMAS. For an agent and any two states , we assume that implies and for any such that and . That is, agents’ preferences over a given agent are the same on all paths which a given agent cannot distinguish.
We also mention that Assumption 2 (Deterministic Behaviour Assumption) extends to ASMAS in a straightforward manner.
Transition Type
In general, in any state of the system, an agent may choose a temporal or a cognitive transition. However, it is often desirable, e.g., when constructing a probability space, to restrict the type of transition available to an agent.
Definition 13.
Given a path in an ASMAS satisfying Assumption 2 and an agent , we use to denote the type, as seen by agent , of the transition that is taken to move from state to . More specifically, we distinguish five different transition types:
if for some ,
if for some ,
if for some ,
if for another agent and ,
if for another agent and .
Remark 10.
Assumption 2 guarantees that, if the transition form to is temporal, then the action is uniquely determined.
We write for the type of a path . When is a finite path and is a type of an infinite path, we say that is consistent with if there exists an infinite extension of such that .
We note that the type of agent’s own cognitive transitions is defined differently than the type of another agent’s cognitive transitions. This stems from our implicit assumption that agents can observe their own cognitive changes, but they cannot, in general, observe another agent’s cognitive transitions. Formally, we make the following assumption.
Assumption 4**.**
(Transition Type Distinguishability Assumption) Let be an ASMAS. For an agent and any two finite paths , , we assume that implies . That is, agents can distinguish paths of different types.
This assumption is essential to ensure that the belief function is defined over finite paths in the same probability space.
Initial Distribution
We replace the set of initial states with a more accurate notion of initial distribution , as a common prior assumption of the agents about the system, which is needed to define a belief function.
Probability Spaces
We now define a family of probability spaces for an arbitrary ASMAS. Recall that our ultimate goal is to define the belief function. To motivate the following construction, we mention that the belief function provides a probability distribution over paths which are indistinguishable (i.e., have the same observation) to a given agent. There are two important consequences of this: (i) probability spaces will vary among agents, reflecting the difference in their partial observation, and (ii) rather than defining a single probability space, spanning all the possible paths, for a given agent, we may define many of them, as long as every pair of indistinguishable paths lies in the same probability space. Hence, using the fact that agents can observe the type of transitions (by Assumption 4), we parameterise probability spaces by type, so that each contains paths of unique type.
We begin by introducing an auxiliary transition function, specific to each agent, which will be used to define the probability measure.
Definition 14.
Let be an ASMAS. Based on temporal transition function and preference functions , we define an auxiliary transition function for agent as follows for :
[TABLE]
The application of the function resolves the nondeterminism in both the temporal and cognitive dimensions and the resulting system is a family of probability spaces, each containing a set of paths of the same type. While the probabilities of temporal transitions are given by the transition function and computed by all agents in the same way, each agent resolves the nondeterminism in the cognitive dimension differently. For an agent , all possible cognitive transitions of another agent have the same type and hence lie in the same probability space; uses its preference functions to associate probabilities to them. On the other hand, each of ’s own possible pro-attitude changes has a different type and lies in a different probability space; therefore treats it as a deterministic transition and assigns probability 1 to it.
We now construct a probability space for an arbitrary ASMAS , agent and a type in a similar way as in Section 4. The sample space consists of infinite paths of type starting in one of the initial states, i.e., . We associate a probability to each finite path consistent with via function . We then set to be the smallest -algebra generated by cylinders and to be the unique measure such that . It then follows that is a probability space.
Note that, for agents and such that in a system , agents’ probability spaces will in general differ in probability measures and , because their preference functions may be different.
Example 7.
We now define preference functions for Bob and Alice of Example 1. For example, setting:
[TABLE]
indicates that Bob believes Alice is more likely to be active than passive. Similarly, we give Alice’s preference functions. We first note that . Therefore, by Assumption 3, . Setting:
[TABLE]
for , represents that Alice has no prior knowledge regarding Bob’s mental attitudes. Finally, we define Alice’s intention preference over Bob. Since and , Assumption 3 implies that and . We may set:
[TABLE]
to indicate that Alice knows that Bob will keep the money when he is an opportunist, but she thinks it is quite likely that he will share his profit when he is an investor.
We now compute the probability that Alice and Bob will have the same amount of money at the end of the game. In other words, we want to find the probability that Alice invests her money with Bob and Bob shares his profit with her. As noted above, probability spaces differ between agents. We first perform the computation from Alice’s point of view and consider two cases: (i) Alice being passive and (ii) Alice being active. For (i), letting and , we compute:
[TABLE]
Similarly, in case (ii), letting and , we compute:
[TABLE]
Hence, from Alice’s point of view, the probability that both will have 20 dollars at the end of the game is three times higher when she is active, and roughly equal to 1/3. This is consistent with our expectations, since the only difference between the two scenarios is the likelihood of her investing, which is three times greater when she is active.
We now perform a similar computation for Bob. Again, we consider (i) Bob being an investor and (ii) Bob being an opportunist. We start with case (i), but we have to be a little more careful now. In order for the result to be meaningful, all paths in which Bob is an investor must be in the same probability space. However, currently, this is not the case for paths corresponding to different intention changes for Bob. To fix that, we use Bob’s intention strategy to quantify the likelihoods of paths in different probability spaces. We may then compute:
[TABLE]
In case (ii), Bob chooses intention with probability 1 and so the probability of him sharing the profit is 0.
7 Reasoning with Probabilistic Beliefs
In presence of partial observation and, resulting from it, imperfect information that agents have about system state, one resorts to using beliefs to represents agents’ knowledge. In this section, we define a probabilistic belief function of an agent in an autonomous stochastic multiagent system (ASMAS), which models agents’ uncertainty about the system state and its execution history.
In [18], a qualitative belief notion is defined based on a plausibility measure. We consider probability measure instead, and define a quantitative belief function expressing that agent believes with probability in relation to if it knows with probability in relation to . This can be seen as a quantitative variant of the qualitative definition in [44], according to which agent believes if the probability of is close to 1. It is generally accepted that trust describes agents’ subjective probability [19] and therefore needs to be measured quantitatively.
7.1 Belief Function
Before defining the belief function, we establish an equivalence relation on the set of finite paths of an autonomous system for an agent . We say that paths are equivalent (from the point of view of ), denoted , if and only if . Intuitively, each equivalence class contains paths which a given agent cannot differentiate from each other. Note that, by Assumption 4, each equivalence class comprises paths of the same type.
Example 8.
Recall the trust game from Example 5 and the observation function defined on in Example 4. Using that definition, we obtain , which is intuitively correct, since Bob cannot observe Alice’s goals. These two paths form an equivalence class. Similarly, and , and both pairs of paths form an equivalence class.
The belief function quantifies agent’s belief about the execution history of the system at any given time. Intuitively, at any point during system execution, agent’s observation history uniquely identifies an equivalence class (with respect to ), consisting of all paths with that observation. The belief function gives a probability distribution on that equivalence class. We define to be a set of all finite observation histories (path observations), and for a given path observation , denotes the equivalence class associated with . Recall that, for any finite path , denotes a basic cylinder with prefix .
Definition 15.
Let be an ASMAS and an agent in . The belief function of an agent is given by:
[TABLE]
Hence, given that agent ’s path observation is at some point, their belief that the execution history at that time is is expressed as the conditional probability of the execution history being , given that the execution history belongs to the equivalence class . We note that sometimes, e.g., when the observation is clear from the context, we might omit it, and simply write for agent ’s belief that the execution history at some point is .
Example 9.
We return again to Example 5 and let and . Recall from Example 8 that , and let denote that common observation. Hence, is a path observation associated with the equivalence class . We compute and below.
[TABLE]
Similar computation shows that:
[TABLE]
We also let , and recall from Example 8 that . We let denote that common observation and, performing similar computation as above, we obtain:
[TABLE]
Analogously, letting , and , we compute:
[TABLE]
The following theorem gives a recursive definition of the belief function. Intuitively, the beliefs of agent are represented as a distribution over a set of possible states which are reachable by paths consistent with the current observation history. This belief distribution will be updated in the Bayesian way whenever a new observation is taken.
Theorem 7.1.
The beliefs can be computed recursively over the length of path :
For an initial state ,
For a path such that and ,
[TABLE]
7.2 Belief ASMAS
A conceptually simpler construction, defined below, can be effectively used to reason about a single agent’s understanding about the system, when there is no need for nested reasoning on agents’ beliefs. We employ a well-known construction [10] which, for a system and a fixed agent , induces an equivalent belief ASMAS whose states are distributions over states of called belief states. Intuitively, belief states quantify agent’s uncertainty about the current state of a system by specifying their belief, expressed as a probability distribution: although we may not know which of several observationally-equivalent states we are currently in, we can determine the likelihood of being in each one. The belief ASMAS is fully observable but its state space is possibly infinite.
Formally, a belief ASMAS for an ASMAS and an agent is a tuple , where is a set of initial belief states such that:
[TABLE]
We now give the transition function . Intuitively, from a belief state , different belief states are possible, each corresponding to a unique combination of ’s next observation and the type of transition taken. Transition probabilities are then computed based on the temporal transition function or ’s preferences. The definition is split into three parts, reflecting the different types of transitions present in an ASMAS.
First, for and , we have
[TABLE]
where is a belief state reached from by performing and observing , i.e.,
[TABLE]
Intuitively, the belief state reached by agent from by performing and observing is a probability distribution over states such that , where the probability of each state is weighted according to the probabilities of transitions from states in the support of to that state.
Second, for ,
[TABLE]
where is belief reached from by performing ’s goal change into and observing , i.e.,
[TABLE]
Note the we interpret as having value 0 or 1, depending on whether a transition of a specified type exists or not. The case corresponding to an intention change of agent is defined analogously.
Third, for such that ,
[TABLE]
where is belief reached from by performing ’s goal change into and observing , i.e.,
[TABLE]
The case of intention change can be defined in a similar manner.
Example 10.
We illustrate the above construction on the trust game from Example 5 by considering the initial few states of the belief ASMAS corresponding to . Since the game has a single initial state, the belief ASMAS also has a single initial belief state, namely .
We now compute possible belief states after the first transition, i.e. Alice’s goal change. Recall that Bob cannot distinguish states and ; we let . Then the new belief state is , with:
[TABLE]
where we used Bob’s preference function defined in Example 7. Similar computation shows that:
[TABLE]
Since Bob has only one possible observation at this point of the game, we expect that is his only possible belief state after first transition, i.e. . Indeed,
[TABLE]
Next, Bob sets his goal. We let and . If Bob observes , then his belief state is , such that:
[TABLE]
If he observes then his belief state is , with:
[TABLE]
The transition function is as follows.
[TABLE]
Finally, we consider how belief state changes after Alice’s temporal transition. There are four possible observations for Bob at this stage, namely , , , . Hence there are four possible belief states, , , , , such that:
[TABLE]
Figure 3 depicts belief states of which we have computed.
As in our construction of the probability measure for SMGs in Section 4, a strategy profile induces a probability measure on any belief state over infinite paths of ASMAS . We note that, in general, has a (continuous) infinite state space.
8 Reasoning about Beliefs and Trust
In this section, we formalise the notions of trust, which are inspired by the social trust theory of [17]. We define trust in terms of the belief function and further extend PCTLto capture reasoning about beliefs and trust.
In Section 7, a Bayesian-style definition of the belief function is presented. It uses agents’ partial observation function and probability measure, which is in turn defined in terms of preference functions introduced in Section 6. In this section, we assume the existence of such a belief setting, i.e., one belief function for every agent, and define operators to reason about agents’ beliefs and trusts.
Expressing Trust
Our trust operators follow the intuition of social trust concepts from [17], but the technical definitions are different and more rigorous. We distinguish between two types of trust, competence, meaning that agent believes that is capable of producing the expected result, and disposition, which means that agent believes that agent is willing to do what needs. Moreover, we express trust with the usual probabilistic quantification of certainty that we sometimes use in our daily life, e.g., “I am 99% certain that the autonomous taxi service is trustworthy”, or “I trust the autonomous taxi service 99%”. Our formalisation then captures how the value of 99% can be computed based on the agent’s past experience and (social, economic) preferences. Indeed, [17] also provides a justification for quantifying trust with probabilities, e.g. in Section 5, where it is stated that the degree of trust is a function of the subjective certainty of the pertinent beliefs. We do not consider fulfilment belief also discussed in [17].
Beliefs and trust are intimately connected. As agents continuously interact with the environment and with each other, their understanding about the system and the other agents may increase, leading to an update of their beliefs. This change in an agent’s beliefs may also lead to an update of trust, which is reflected in the definition of the semantics of our trust operators.
Changes of beliefs and trust will affect goals and intentions, which will be captured via so called pro-attitude synthesis, which is introduced in Section 9. Based on its updated beliefs, an agent may modify its strategy to implement its intention.
8.1 Probabilistic Rational Temporal Logic
We now introduce Probabilistic Rational Temporal Logic (PRTL∗) that can express mental attitudes of agents in an ASMAS, as well as beliefs and trust. PRTL∗ extends the logic PCTL with operators for reasoning about agent’s beliefs and cognitive trust.
Definition 16.
The syntax of the logic PRTL∗ is as follows:
[TABLE]
where , , , and .
Intuitively, is the belief operator, expressing that agent believes with probability in relation with . is the competence trust operator, expressing that agent trusts agent with probability in relation with on its capability of completing the task , where capability is understood to be the possibility of taking one of its legal intentions defined with function . is the disposition trust operator, expressing that agent trusts agent with probability in relation with on its willingness to do the task , where the state of willingness is interpreted as unavoidably taking an intention defined with function . Recall that we use function for the legal intentions and function for the possible intentions, i.e., intentions available assuming agent’s willingness. We use to range over the two trust operators and .
Before we define the semantics, we require additional notation. We write:
[TABLE]
to denote the strategic ability of agent in implementing on a finite path . Intuitively, gives a lower bound on agent ’s ability to maximise the probability of , while gives an upper bound on agent ’s ability to minimise the probability of .
Moreover, we extend the expression to work with finite paths: for the path and . Intuitively, it is the concatenation of path with a cognitive transition .
For a measurable function , we denote by the belief-weighted expectation of , i.e.,
[TABLE]
With this in mind, we aim to define the new operators so that normalises the probability measure of the formula with agent’s probabilistic belief, whereas operators consider moreover the possible or legal intention changes of another agent . The intention changes are conditioned over agent’s strategic ability of implementing formula , expressed by and .
Definition 17.
Let be an ASMAS and a finite path in . The semantics of previously introduced operators of PCTL∗ and PCTL remains the same in PRTL∗(see Definitions 3 and 10). For the newly introduced belief and trust operators, the satisfaction relation is defined as follows:
if
[TABLE]
where the function is such that
[TABLE]
if
[TABLE]
where the function is such that
[TABLE]
if
[TABLE]
where the function is such that
[TABLE]
We interpret formulas in ASMAS in a state reached after executing a path , in history-dependent fashion. Recall that this path may have interleaved cognitive and temporal transitions. However, when evaluating a given belief or trust formula, we assume that agents do not change their mental attitudes (i.e., the future path is purely temporal, contained within a single induced SMG), which motivates using the probability measure defined in Section 4 in the above definition. The belief formula corresponds to the probability of satisfying in future in the original ASMAS weighted by the belief distribution; in other words, it is a belief-weighted expectation of future satisfaction of , which is subjective, as it is influenced by ’s partial observation and its prior knowledge about encoded in the preference function. The competence trust operator reduces to the computation of optimal probability of satisfying in over legal changes of agent’s intention, which is again weighted by the belief distribution and compared to the probability bound . Dispositional trust, on the other hand, computes the optimal probability of satisfying in over possible changes of agent’s intention, which is weighted by the belief distribution and compared to the probability bound .
For a relational symbol , the expression computes the maximum probability of completing the task on path , among all legal changes of agent ’s intention. Therefore, when interpreting formula , we assume the optimal capability of agent . Note that this capability is not necessarily within ’s possible intention changes. On the other hand, for , the expression computes the minimum probability of completing the task on path that all agent ’s possible intentional changes can achieve. Therefore, when interpreting formula , we consider all possible states of agent ’s willingness. It should be noted that the operators cannot be derived from the other operators.
Remark 11.
We remark that, while defining competence trust in terms of legal intentions should be rather uncontroversial, the disposition trust operator may be expressed in an alternative way. Given that computes ’s trust towards and that intentional attitudes of are in general not observable to , one could argue that it is not realistic to assume that uses ’s intention strategy to compute its trust towards . It would perhaps be more natural to use ’s intention preference function instead, since it precisely represents ’s expectations about ’s mental attitudes. Indeed, it is possible to make such a modification, which we discuss below.
First of all, note that, in the definition of above, we restrict ’s knowledge to the support of , i.e., to ’s possible intentions, rather than allowing to know ’s full intention strategy. As a side note, the consequence of this is that ’s disposition trust towards differs from competence trust only when the set of possible intentions of is a strict subset of ’s legal intentions. In particular, it is the case when ’s intention strategy is pure, such as in Example 5. Hence, an important practical consideration to bear in mind when constructing instances of ASMAS is to keep cognitive strategies pure, or close to pure (with few intentions in the support). In fact, Section 9 provides an easy way to achieve this.
Going back to the alternative way of defining , if we replace ’s intention strategy by ’s intention preferences over , , it makes sense to include in our calculations of trust the full probability distribution that provides, rather than just its support, as we do for . That’s because represents knowledge that realistically possesses, so there’s no reason to introduce any restrictions on it. We then end up with defined as a belief-preference-weighted expectation of agent’s strategic ability of implementing a given formula . Note that, with such formulation of , the last equivalence of Theorem 8.1 does not hold.
Finally, note that disposition trust operator of one agent may be nested inside a belief operator of another agent, which calls for nested preferences (i.e., preferences over preferences) in an idealised version of . We aim to avoid such complexities at this early stages of the development of the framework, and therefore settle for a simplified notion of disposition trust involving intention strategy.
Example 11.
Here we give examples of formulas that we may wish to verify on the trust game defined in Example 5. The formula
[TABLE]
states that Bob believes that, with probability at least 0.6, Alice will invest the money with him in the next step. On the other hand, the formula
[TABLE]
states that Alice can trust Bob with probability no less than that he will keep the money for himself. The formula
[TABLE]
states that, at any point of the game, if Bob is richer than Alice, then with probability at least , in future, he can almost surely, i.e., with probability 1, trust Alice on her ability to become richer.
It is also possible, and often desired, to have a trust operator within the scope of a belief operator. For instance,
[TABLE]
expresses that Bob believes that, with probability at least 0.7, Alice’s trust that he will share the profits with her in the future is at least 0.5. Such construct might represent Bob’s reasoning leading to his decision of whether to share his profit or not, where he considers Alice’s trust towards him as a determining factor. A similar statement might be expressed by the following formula:
[TABLE]
The above states that Bob believes that, with probability at least 0.7, Alice believes that, with probability at least 0.5, Bob has a possible intention which ensures that it is possible that he shares the profit. The first formula may be seen as a quantitative version of the second, as it additionally (implicitly, via operator) considers the probability of Bob sharing the profit. However, both formulas are equivalent for the trust game, assuming the action strategies defined in Example 3 and intention strategy from Example 5. To see that, first note that Bob’s intention strategy is pure, hence he has only one possible intention. Second, since the action strategy implementing that intention (whatever it is) is pure, the probability of him sharing the profit is either 1 or 0. Therefore, takes only two values, 1 and 0, and is equal to 1 whenever for any path for . Hence,
[TABLE]
In general, however, those two formulas differ in their semantics.
Definition 18.
For a given autonomous stochastic multi-agent system and a formula of the language PRTL∗, the model checking problem, written as , is to decide whether for all initial states .
8.2 Restricting to Deterministic Behaviour Assumption
The above semantics is complex because of the quantification over agents’ strategies. However, under Assumption 2, this quantification is not necessary, since the system conforms to a single action strategy, induced from agents’ cognitive states, which we call the induced strategy . As a result, some operators have simpler semantics. We begin with an easy consequence of restricting ourselves to a single action strategy.
Proposition 2.
With Assumption 2 on ASMAS , we have the following equivalence for being a finite path, and being a PRTL∗ formula.
[TABLE]
Moreover, for systems satisfying Assumption 2, we will often omit the component in the last expression above and write instead. Intuitively, it represents the probability of being satisfied on a future path in a system given that the current path is .
Definition 19.
Let be an ASMAS satisfying Assumption 2 and a finite path in . The following are several operators whose semantics can be simplified according to Proposition 2.
if
[TABLE]
if
[TABLE]
where the function is such that
[TABLE]
if
[TABLE]
where the function is such that
[TABLE]
if
[TABLE]
where the function is such that
[TABLE]
Intuitively, given that the action strategy in the system is fixed as , there is no need to consider agents’ strategic abilities, and hence the probability of a given formula being satisfied can be uniquely determined, which simplifies the definitions above.
8.3 A Single-Agent Special Case
The semantics can be further simplified if we work with the single-agent case, in which case we can employ the belief ASMAS construct as given in Section 7.2. Recall that this approach explores belief states (distributions over states of ) and that is a mapping from paths in to paths in belief ASMAS . Therefore, to evaluate belief and trust we can directly employ current belief , instead of working with belief distribution defined on finite paths .
Here we only present the semantics of the belief and trust operators.
Definition 20.
Let be an ASMAS satisfying Assumption 2 and a finite path in . The semantics of the belief and trust operators can be defined on as follows.
if
[TABLE]
where the function is such that
for if
[TABLE]
where the function is such that
[TABLE]
and if is or we replace with in the above.
if for if
[TABLE]
where the function is such that
[TABLE]
for such that and ; if is or we replace with in the above.
Note that ’s belief in is evaluated as an expectation of satisfaction of computed in the current belief state. ’s competence trust in ’s ability to perform reduces to the expectation of the optimal probability of completing , over all legal changes of ’s intention. Similarly, to evaluate ’s disposition trust in ’s willingness to perform we compute the expectation of the optimal probability of completing , over all possible changes of ’s intention .
Remark 12.
The sets of possible intentions of agent can be determined for a given belief state with pro-attitude synthesis defined in Section 9.
8.4 Other Trust Notions
In [17], another concept related to trust called dependence is introduced, whose interpretation is that agent needs agent (strong dependence), or is better off relying on (weak dependence). We now propose how those two concepts can be formalised in an ASMAS under Assumption 2.
Definition 21.
Let be an ASMAS satisfying Assumption 2 and a finite path in . We introduce operators and to express strong and weak dependence, with the semantics given by:
if
if
[TABLE]
where the function is such that
[TABLE]
Intuitively, states that, according to agent ’s beliefs, either (i) the probability of will not be as required unless agent takes on an appropriate intention, or (ii) the probability of will be as required unless takes on a certain intention. In other words, strong dependence of on over means that can control the probability of future satisfaction of . On the other hand, states that, according to ’s beliefs and preferences, intentional changes of agent can bring about better results than any of the available intentional changes of agent .
We note that alternative definitions of the above notions are possible. For example, we could introduce a non-probabilistic version of strong dependence, based solely on the operator. We could define
[TABLE]
Intuitively, here means that can take on an intention such that, regardless of what intention takes on, will not be satisfied, and can take on another intention, such that can take on an intention which ensures that holds. In other words, can either make it impossible for to achieve , or it can allow to make true. We can view the above definition as a more objective, absolute interpretation of strong dependence, whereas the probabilistic version represents a subjective notion, influenced by agent’s understanding of the system execution. Depending on the use case, either variant of the strong dependence operator might be employed.
Weak dependence can also be interpreted in a different way, especially in systems equipped with a reward structure. The intuitive meaning of the expression better off used in the informal definition of weak dependence relates to some implicit notion of agent’s well being. Definition 21 takes the probability of satisfying a given formula as agent’s reward. However, in presence of a reward structure, we could allow to include a reward operator and adapt the definitions of the -functions to compute expected reward.
Example 12.
In the trust game, Bob’s financial situation is dependent on Alice’s actions. We can formally express that in PRTL∗ with the following formula, where is an atomic proposition, true in states in which Bob has more money than in the initial state:
[TABLE]
It expresses that Bob needs Alice’s cooperation to ensure that, at some point in the future, he will have more money than when he started. In fact, Alice’s hopes of making a profit depend on Bob’s cooperation, which we could express by a formula very similar to the one above.
We remark also that we could equip the trust game with a reward structure that reflects agents’ payoffs. We could then express that Bob is weakly dependent on Alice to maximise his payoff with the following formula:
[TABLE]
where returns the expected reward accumulated before the game ends.
8.5 Trust for Systems with Sure Beliefs
We now consider a special class of systems where agent has sure beliefs, i.e., for all finite paths , we have either or . Intuitively, agent is sure about the current system state and the execution history. The following theorem shows that, in such systems, agent ’s beliefs and trusts can be expressed with other operators.
Theorem 8.1.
For ASMAS in which agent has sure beliefs, the following equivalences hold for any finite path , formula , and agent :
* if and only if ,*
* if and only if ,*
* if and only if .*
Intuitively, the first equivalence shows that agent ’s belief of reduces to computing the probability of satisfying . The other two equivalences concern agent acting as a trustor and agent as a trustee. The former indicates that agent ’s trust in ’s competence in achieving is equivalent to the existence of ’s legal intention which ensures satisfaction of , while the latter means that ’s trust in ’s disposition towards achieving is equivalent to ensuring satisfaction of under all possible intentions.
The following proposition shows that the sure-belief system has an equivalent definition as fully observable system. Therefore, Theorem 8.1 also holds for fully observable systems.
Proposition 3.
Let be an ASMAS and an agent in . The following two statements are equivalent:
Agent has sure beliefs, i.e., for all finite paths , we have either or .
Agent has full observation, i.e., for all .
9 Pro-attitude Synthesis
Recall that the cognitive strategies and are defined on the (possibly infinite) set of paths and may lack a finite representation necessary for model checking. We now formalise an idea, which is informally argued in [27, 7], that the changes of pro-attitudes are determined by the changes of beliefs, but not vice versa.
This will enable us to synthesize the cognitive strategies and by considering agent ’s beliefs and trust expressed as formulas of the logic PRTL∗ and used to constrain pro-attitude changes. In particular, we will associate with each set of goals a condition, expressed as a PRTL∗ formula, which will guard that set of goals. The intuitive interpretation of such an association is that an agent takes a set of goals when the associated condition is satisfied. To guard intentions, we additionally use the agent’s own goals, since agents’ intentions are influenced by their goals. We note that such a construction closely resembles human reasoning – for example, recall that in Example 3 we stated that Bob takes intention share when he is an investor (i.e., his goal is investor) and his belief in Alice being active is sufficient. In Example 13, we show how to express this statement formally using pro-attitude synthesis, which consists of evaluating Bob’s belief in Alice being active as a guarding mechanism for his intention to share and setting a minimum belief threshold.
Let be the set of formulas of the logic PRTL∗ that are Boolean combinations of atomic propositions and formulas of the form , , or , such that does not contain temporal operators. The formulas and denote the quantitative variants of and that yield the actual value of the probability/expectation.
The language allows nested beliefs222Because the semantics of trust is based on the belief function , a trust formula is also called a belief formula in this paper., for example , under the condition that the outermost belief operator is for agent . The nesting is useful since one may want to reason about, e.g., an agent’s belief over the other agent’s trust in himself. Moreover, all modal logic formulas in must be in the scope of a belief operator of agent . This is to ensure that agent is able to invoke the synthesis with the limited information it has.
Below, we work with an arbitrary ASMAS and a set of agents in .
Definition 22.
For every agent , we define:
a goal guard function and
an intention guard function .
The guard functions are partial functions associating pro-attitudes with conditions expressed using belief and trust formulas that can be evaluated based on a finite execution history. Note how differs from in that it guards intentions by agent’s own goals. We call trivial if for all . Similarly for .
We recall that is the cognitive mechanism of . Additionally, we set and call it the guarding mechanism. In the following, we present an approach to obtain the infinite structure , i.e., cognitive strategies of all agents, from finite structures and .
First, for agent , we define the goal evaluation function , such that for , is given by:
[TABLE]
Intuitively, evaluates the (probabilistic) satisfiability of agent ’s beliefs or trust expressed as formulas given by . Note that the expressions and return their corresponding probabilistic values, and and return the value [math] or depending on the verification result.
Similarly, we define the intention evaluation function , such that for any , , is given by:
[TABLE]
We now use pro-attitude evaluation functions to provide a finite definition of a cognitive strategy.
Definition 23.
Let be an ASMAS with a cognitive mechanism and let be a guarding mechanism for . In a finite-memory setting, the goal strategy can be instantiated as follows: for any and , we set
[TABLE]
Likewise, the intention strategy can be instantiated as follows: for any and , we set
[TABLE]
where .
This definition allows us to transform the model into , which, besides the cognitive mechanism , contains the cognitive strategy of each agent. Once has been precomputed, model checking a given specification can be carried out on instead of . We refer to this approach as pro-attitude synthesis before model checking. Besides formalising the intuition that agent’s pro-attitudes are affected by its beliefs, this approach makes the interaction of agents’ beliefs and trust possible, without resorting to nested beliefs.
Example 13.
We show how a cognitive strategy can be constructed from the guarding mechanism for Bob in the trust game . Since we assume that goals of agents are static throughout the execution of the game, we only concern ourselves with the intention guard function. We recall our informal assumption that Bob’s intention will be share when he is an investor and his belief in Alice being active is sufficient, and keep otherwise. We formalise it as follows:
[TABLE]
where holds in states in which Alice’s goal is active and we used a value to represent Bob’s belief threshold.
We now synthesize Bob’s intention strategy. We let and . We recall from Example 8 that and we let denote that common observation. By Example 9:
[TABLE]
Therefore, since and (below and in what follows, ):
[TABLE]
Hence
[TABLE]
and so:
[TABLE]
Likewise, letting , and one can show that:
[TABLE]
As expected, if Bob is an opportunist, he keeps the money for himself. However, when he is an investor and Alice invests the money with him, his belief that Alice is active is high enough for him to share the profits, hoping to gain Alice’s trust.
Finally, we remark that, while it may not be immediately clear how powerful pro-attitude synthesis is after considering a simple example such as this, full appreciation of it can be gained by applying it to more complex systems. One such system is provided by an iterated trust game, in which Alice and Bob interact with each other repeatedly, in which beliefs and trust evolve dynamically. Rather than specifying cognitive strategies by hand for each iteration, pro-attitude synthesis enables one to encode them in a natural way via guard functions and generate them dynamically. Such an approach scales well to larger systems and closely resembles human reasoning.
Preference Functions Update
During the execution of the system, agents learn new information about other agents by observing their actions. As a result, their understanding of others’ behaviour, motivations and cognitive state increases. This new knowledge gained by agents is reflected in their belief function, which could be used to update agents’ preference functions. To do that, we extend guarding mechanism of each agent by introducing guard functions of over for every other agent . In particular, for agents and , we define a goal (resp. intention) guard function (resp. ) of over in a similar way as in Definition 22, and then the goal (resp. intention) evaluation function (resp. ) of over . Intuitively, (resp. ) captures ’s expectation of how updates their mental attitudes. In case does not possess such information, (resp. ) are trivial. We then define and (where stands for history, representing that updated preference functions are history-dependent) by weighting the state-defined preferences with respect to the evaluation functions as follows:
,
,
where .
Intuitively, the preference functions of agent over will be adjusted with respect to its current understanding of the system execution and the knowledge it has acquired throughout, represented by a formula in the guarding functions and . The probability space construction from Section 6 can be adapted to work with the updated preference functions . Therefore, we have probability spaces for both pro-attitude synthesis and model checking.
Example 14.
After investing her money with Bob, Alice might be concerned whether she can trust Bob to share his profit with her. Such trust can be formally expressed by a formula , where and indicates that Alice wants to find a lower bound on such trust value. We assume that Alice is active and let , , and . We use Alice’s preference function defined in Example 7, which we recall to be:
[TABLE]
From that, we easily compute Alice’s belief upon observing to be:
[TABLE]
We now compute . We recall from Example 13 that, in state , Bob’s only possible intention change is , and, in state , his only possible intention change is . Since and , we obtain:
[TABLE]
Therefore:
[TABLE]
Hence, Alice can trust Bob with probability at least 50% in his willingness to share his profit with her.
Note that an alternative way of formulating the trust we wish to compute is to use competence trust instead, in which case . Most of the computations stay the same in that case, the exception being the -functions:
[TABLE]
Therefore:
[TABLE]
Hence, Alice can trust Bob with certainty on his capability to share his profit with her. We remark that the difference in the value of competence trust and disposition trust is as expected – intuitively, Alice knows for sure that Bob is capable of sharing his profit with her, but she cannot be sure that he is willing to do that.
Finally, we consider Alice’s belief that Bob will share money with her. We let and recall Alice’s intention preference function over Bob defined in Example 7:
[TABLE]
Hence, after Bob settles his intention, Alice’s belief is as follows:
[TABLE]
Therefore:
[TABLE]
Intuitively, due to inaccuracy of Alice’s prior knowledge about Bob (encoded in preference functions), her belief that Bob will share his profit with her differs from her trust towards Bob sharing the money.
10 Model Checking Complexity
In the next two sections we consider model checking ASMAS against PRTL∗ formulas. We first present the verification procedure and then analyse its complexity.
We redefine the autonomous stochastic multi-agent system of Definition 12 by replacing an infinite structure with a finite structure , defined in Section 9.
Our automated verification framework accepts as inputs an ASMAS satisfying Assumption 2 and a PRTL∗ specification formula . The verification procedure proceeds as follows:
Perform pro-attitude synthesis on the system to obtain . In the new system, guarding mechanism is replaced by cognitive strategies, , of agents. (In this phase, functions are based on preference functions .) 2. 2.
Update the preference functions into according to the results of pro-attitude synthesis, as defined in Section 9. 3. 3.
Model check formula on the system . (In this phase, the belief functions are based on preference functions .)
The checking of expressions in Steps 1 and 3 relies on the corresponding preference functions and , respectively. However, for simplicity of the notations, we still write them as . Note that cognitive strategies synthesised in Step 1 generally lack a precise finite representation. Remark 13 discusses a possible approximate solution, while Appendix 0.B presents a restriction on the system which ensures that a finite representation for exists. Figure 4 summarises the differences between the models introduced in this paper and outlines the model checking process. Unfortunately, the problem is undecidable in general for both the synthesis step and the model checking step. First of all,
Theorem 10.1.
The synthesis of pro-attitude functions whose formulas are in the language is undecidable.
A guarding mechanism is trivial if, for all agents , we have for all and for all and . If the guarding mechanism is trivial then the first two steps can be skipped, and the computation proceeds directly to model checking. In this case, we have
Theorem 10.2.
Model checking PRTL∗ is undecidable, even if the guarding mechanism is trivial.
We note that both of the above problems are undecidable even for formulas concerning beliefs of a single agent. Proofs can be found in Appendix 0.A.
11 Decidable Fragments
To counter the undecidability results, we explore fragments of the general problem. In this section, we only present proof ideas for the complexity results. The details of the proofs can be found in the Appendix. Table 5 summarises complexity results for the proposed fragments.
11.1 A Bounded Fragment
The bounded fragment, named BPRTL∗, allows formulas which 1) do not contain temporal operators and , 2) all operators are immediately prefixed with a probabilistic operator or a branching operator, i.e., in a combination of , , or , and 3) the nested depth of belief and trust operators is constant. The last constraint is needed to ensure that the complexity is not measured over the nested depth of belief and trust operators. For the upper bound, we have the following result.
Theorem 11.1.
The complexity of the bounded fragment BPRTL∗ is in EXPTIME.
In Appendix 0.B, we present an EXPTIME algorithm which performs the verification procedure from Section 10. It uses boundedness of the logic fragment to limit the length of paths that need to be considered to evaluate a guard or the specification formula. It then constructs an expanded system whose states capture all past observations of all agents, enabling belief and trust formulas to be evaluated locally. Model checking the original system is then reduced to model checking the expanded system, which admits a standard recursive labelling procedure, similar to the one used for PCTL model checking.
For the lower bound, we have the following result.
Theorem 11.2.
The complexity of the bounded fragment BPRTL∗ is PSPACE-hard.
The proof is a reduction from the quantified Boolean formula problem. Given a QBF , the reduction constructs an ASMAS with two agents, and , playing a game of two phases. In the first phase, the agents decide the truth values of the variables (atomic propositions) of by changing their intentions. Then, in the second phase, the agent attempts to show that a randomly chosen clause of evaluates to true by proving that one of its literals is true. If they can do that regardless of which clause gets selected, then they have a winning strategy in the game, which is equivalent to being true. The challenge lies in designing the system so that agents’ decisions from phase one are “remembered” until phase two, and devising an appropriate formula to express the existence of a winning strategy for . The details of the proof are in Appendix 0.B.
11.2 A Fragment with and operators
The fragment of this section, named PRTL, works with the and temporal operators in the specification formula . With and operators, the specification formula can express long-run properties about agent’s mental attitudes in the system, and therefore this fragment complements the bounded fragment. However, the fragment is subject to other restrictions as follows.
The guarding mechanism is trivial. That is, the algorithm works with the model checking step without conducting pro-attitude synthesis first.
The specification formula is restricted so that 1) it works with a single agent’s beliefs and trust, 2) there are no nested beliefs or trust, 3) beliefs and trust cannot be in the scope of a probabilistic operator , and 4) there is a constant number of belief or trust operators.
The expanded system, described below, satisfies the restriction that, along any path of the expanded system, the evaluation of belief or trust subformulas for agent are the same on any two expanded states if the support of the probabilistic distributions over the set of states are the same.
Remark 13.
We remark that the pro-attitude synthesis problem is strictly harder than model checking for long-run properties because it needs a finite representation for the set of paths. For this reason, this fragment and PRTL do not handle synthesis. Future work may involve formulating an approach based on order effects [2, 46, 28] to approximate the set . The focus of this paper is on approaches that can be computed precisely.
The restriction on the expanded system is essential. It results from an investigation into the undecidability, which has established that the undecidable cases arise because of the existence of non-monotonic flows of probability between states in two consecutive visits of the same expanded state. By assuming stability (as we do in this fragment) or monotonicity of the flows, decidability can be achieved. Moreover, we note that this fragment has full expressiveness of LTL. In the following, we assume that it is the agent ’s beliefs that the formula is to describe. We have the following result for the upper bound.
Theorem 11.3.
The complexity of the fragment PRTL is in PSPACE.
Given a system and a formula , the algorithm proceeds by first computing those subformulas which do not have belief or trust formulas in their scope. These computations can be done by an adaptation of the usual probabilistic temporal logic model checking. Then, to compute a formula with belief and trust subformulas, we construct an expanded system with the state space , where is the domain of real numbers with fixed precision333We assume that each number can be encoded with complexity .. Although is infinite, we need only a finite number of real numbers. The restriction imposed on the system ensures that the system is of size exponential with respect to the size of the system . However, we do not explicitly construct the system, but instead take an automata-theoretic approach and perform on-the-fly computation by, e.g., two-phase search. The belief and trust formulas can be directly evaluated on the states of the expanded system. The details of the construction are in Appendix 0.C.
We have the following results for the lower bound. Recall that a strongly connected component (SCC) of a graph is a subgraph of in which every vertex is reachable from every other vertex.
Theorem 11.4.
The complexity of the fragment PRTL is PSPACE-hard.
The proof is a reduction from the language universality problem of nondeterministic finite automata. Given an NFA , we construct a single agent system which, starting from an initial state , moves into one of two subsystems and , with a uniform distribution. The system simulates the universal language , while simulates the language of . In other words, every word in has a corresponding execution in and every word in that produces a valid run of has a corresponding execution (one for each unique run) in which ends in a designated state (one labelled ) if the corresponding run on ends in a final state. We define the observation function so that the agent cannot distinguish between paths in and corresponding to the same word. This then allows us to prove that the non-universality of the language of A is equivalent to the satisfaction of a carefully designed formula revolving around agent’s qualitative belief that the system reaches a designated state. Finally, the reduction is completed by showing that the system satisfies the restriction outlined above, which follows by observing that agent’s belief stays constant in all SCCs of the expanded system. The details of the proof are in Appendix 0.C.
11.3 A Polynomial Time Fragment
One of the restrictions in the previous fragment is that beliefs and trust cannot be in the scope of a probabilistic operator. In that fragment, this restriction ensures that the complexity is in PSPACE, because it can be harder to perform quantitative verification of the probabilistic and belief operators. In this section, we partly complement this with a fragment in which the belief or trust operators can be in the scope of a probabilistic operator but need to be qualitative, i.e., almost sureness. We show that this fragment, named PQRTL, is, very surprisingly, polynomial time. Note that, as before, ranges over two trust operators and .
We consider the model checking step and restrict formulas to be of the form or such that, in , there are no belief or trust operators and every temporal operator is immediately prefixed with a branching operator, i.e., in the style of CTL. The system needs to satisfy the formula , which means that, once holds, it will hold henceforth. The following is the result.
Theorem 11.5.
The complexity of the fragment PQRTL is in PTIME.
We give a polynomial time algorithm in Appendix 0.D. The algorithm first constructs a system in which two copies of system run by synchronising their observations and the second copy avoids the states where is satisfiable. The computation is then to find strongly connected components (SCCs) of such that a) the formula is satisfiable on some state of the first copy, b) both copies are closed SCCs, and c) the two copies are equivalent in terms of the acceptance probability of words. We show that the checking of formulas or on states satisfying is equivalent to comparing the reachability probability of these SCCs with the value . The PTIME complexity is due to the fact that the computation of SCCs and checking the three conditions on SCCs can be done in polynomial time; in particular, checking of equivalence of acceptance probability of all words can be done in polynomial time by [50].
12 Conclusions
The paper proposes an automated verification framework for autonomous stochastic multi-agent systems and specifications given in probabilistic rational temporal logic PRTL∗, which includes novel modalities for quantifying and reasoning about agents’ cognitive trust. Our model is an extension of stochastic multiplayer games with cognitive reasoning, which specifies how agents’ goals and intentions change during system execution, and admits probabilistic beliefs on which the trust concepts are founded. We study computational complexity of the decision problems and show that, although the general problem is undecidable, there are decidable, even tractable, fragments. Their existence is made possible by numerous assumptions and restrictions that we place on our system, which are summarised in Table 7.
As can be seen from the illustrative running example in this paper, the framework is applicable to a wide range of scenarios of human-robot interactions. This includes competitive settings such as the trust game, as well as cooperative scenarios, which are more commonly considered in robotics community, such as a table clearing task [11]. Furthermore, the development of trust sensors (see [1]) complements our framework very well; they could serve as a source of agent preferences and for validation purposes.
A natural next step following the development of the framework is implementing its techniques in the form of a model checker. To overcome undecidability, a subset of the problem will be considered, in particular, the bounded fragment BPRTL∗. Since a finite set of finite paths is sufficient to model check a bounded specification formula, pro-attitude synthesis only needs to consider those finite paths and the resulting cognitive strategies have a finite representation. Preference function update also only needs to be performed on the relevant finite paths. Finally, computing the satisfaction of a specification formula is a recursive procedure that keeps track of the execution history to evaluate belief and trust formulas. Other decidable fragments also provide a basis for implementation, but their strong restrictions make them less practical.
Another interesting direction for future works involves investigating how memory decay can be introduced into the framework. Intuitively, humans tend to remember more recent experiences better and this should be reflected in the semantics of trust. As a side effect, decidability will be achieved if appropriately old memory is discarded. With that, a Bellman operator may be defined which will allow more efficient evaluation of trust.
Finally, it would be interesting to study an axiomatisation for our logic, as well as the satisfiability problem, which we believe to be challenging.
Acknowledgments**.**
The authors are supported by ERC Advanced Grant VERIWARE and EPSRC Mobile Autonomy Programme Grant EP/M019918/1.**
Appendix 0.A Undecidability of the General Problem
The undecidability proof is by a reduction from the emptiness problem and strict emptiness problem of probabilistic automata, both known as undecidable problems [43]. A probabilistic automaton is a tuple , where
is a finite set of states,
is the initial state,
is a set of accepting states,
is the finite input alphabet, and
is the set of transition matrix.
For each , defines transition probabilities, such that given , is the probability that makes a transition to when is the input. For every and , we have . Plainly, given a state , an input makes a transition to a distribution on , and we further extend to be a transformer from distributions to distributions. Let be the set of all probabilistic distributions on the set . Given , we write for the distribution transformed from by , such that for all , . Given , we write for the function (we assume function application is right associative).
The emptiness problem of a probabilistic automata is defined as follows: Given a probabilistic automaton and , decide whether there exists a word such that , where and for . Replacing ‘’ by a strict inequality ‘’ yields the strict emptiness problem. Both problems are known to be undecidable.
Pro-attitude Synthesis is Undecidable
First of all, we show that the synthesis of pro-attitude functions in which the formulas are in the language is undecidable. Formally, let be a probabilistic automaton and be a set of atomic propositions. We can then construct an ASMAS such that
, i.e., this is a single-agent system,
,
for some ,
,
the transition relation is as follows for :
[TABLE]
for and , and for , , and .
Intuitively, the system consists of two subsystems, indexed with the third component of the states (i.e., or ), running in parallel without any interaction. The observation is defined as follows:
, and
for all .
The moving from the first subsystem to the second subsystem is done by agent ’s intentional changes, which are guarded with a testing on agent ’s beliefs. We only define relevant intentional attitudes in as follows.
,
As defined in Section 9, the cognitive strategy can be obtained from and , with the latter defined as follows for the intentional strategy.
for some and
The preference functions , the goal attitude in , and the goal guards are not defined, because they are not used in this reduction. The initial distribution is a Dirac distribution over the initial states . Therefore, given a and a number , the (strict) emptiness of the problem is equivalent to checking whether .
Model Checking PRTL∗ without Pro-Attitudes is Undecidable
In the following, we show that model checking PRTL∗ is also undecidable, for systems where the guarding mechanism is trivial. Formally, let be as before and be a set of atomic propositions. We then construct an ASMAS such that
, i.e., this is a single-agent system,
,
for some , with the initial distribution being a Dirac distribution over ,
,
the transition relation is as follows:
[TABLE]
for and .
Agent ’s observation is defined as
, and
for all .
We do not need the functions in this reduction. Given a and a number , the (strict) emptiness of the problem is equivalent to checking whether .
Appendix 0.B A Decidable Fragment of Bounded Length
As shown in Section 0.A, the automated verification problem defined in Section 10 is undecidable in general. In this section, we present a fragment
of the problem whose computational complexity falls between PSPACE and EXPTIME. Note that in the following discussions on decidable fragments (i.e., Appendix 0.B, 0.C, and 0.D), we only consider dispositional trust formula . The competence trust formula can be handled in a similar way.
Bounded Fragment
The bounded fragment works with specification formulas which do not contain temporal operators and , all operators are immediately prefixed with a probabilistic operator or a branching operator, i.e., in a combination of , , or , and the nested depth of belief and trust operators is constant. We remark that the specification formula can be extended to include subformulas of the form , , or . Moreover, the restriction on nested temporal operators can be relaxed by taking the bounded semantics for LTL. We focus on the simpler syntax to ease the notation.
Let be the maximal length of the paths that are needed for the specification formula . Specifically:
,
,
, and
.
0.B.1 Upper Bound
The algorithm proceeds in three steps according to the verification procedure in Section 10.
0.B.1.1 Pro-attitude Synthesis
The purpose of the synthesis is to realise the guarding mechanism, i.e., for every and , compute an equivalent representation for the formulas and for all agents . Here we only consider formulas of the forms and , and claim that formulas of the other forms and can be handled by adapting the technique slightly. Without loss of generality, we let . By the constraint of the language that no temporal operator can be in the scope of a belief operator, the satisfiability of depends only on those paths of length . Moreover, by the semantics of the language PRTL∗, model checking the bounded specification formula requires only those paths of length not greater than . Therefore, for this fragment, the synthesis is equivalent to finding a set of paths , where
[TABLE]
for .
Given a state , we write for the tuple of agents’ observations at state . For , we let be the set of possible observations at time , where denotes that agents have not made any observations at time . The state space of the following expanded system is . For a state of , we write for original state and with for the observations at time , i.e., . Moreover, for a tuple of observations , we write for agent ’s observation. These notations can be extended to work with a sequence of states whenever reasonable, e.g., , etc.
Given , we construct a system such that
,
for , whenever , where if and for , and otherwise,
if
- –
for all ,
- –
, and
- –
.
and otherwise,
,
and are to be defined later,
for with , we have and for all , and
for , we have and for all .
Intuitively, in the new system , agents’ observation history are remembered in the state, and for every time , a separate transition relation is constructed. The transition relation maintains the previous observation history up to time and adds a new observation to the next state .
Before evaluating formulas, we define a new belief function on the constructed system . With this function, we can evaluate belief formulas locally instead of resorting to the observation history as we did for the original system . A sequence of states in the expanded system is a path if, for all , one of the following conditions holds:
for some joint action .
there exist and such that
- –
- –
for all ,
- –
, and
- –
.
Similar for a transition on which some agent changes its intention.
The following proposition states that there is a 1-1 correspondence relation between paths in and paths in .
Proposition 4.
For every path in such that , we have that is an initialised path of . On the other hand, for every initialised path in whose length is no more than , there exists exactly one path in such that .
Note that the transition relation of the constructed system is acyclic, that is, for every state , there does not exist a cyclic path such that for some . Therefore, we can define as the time in which the state appears, or formally, for the greatest number such that .
We can now define a probabilistic function for the system and agent as follows, by considering the preference functions of agent , where and we write for . We note that needs to be on some path of .
[TABLE]
With the non-acyclic property, we can define for every state a reachability probability as follows with respect to a type of paths.
if
, if .
The observation function for agent is defined as follows:
if , , and for all , .
Based on this, contains all possible observations of . Moreover, we let to be the set of states that are indistinguishable to agent at state . We define a belief function as follows for agent :
[TABLE]
For every path in the original system , we construct the following state in the expanded system :
[TABLE]
We have the following proposition to reduce the probability of in into in .
Proposition 5.
For any path of such that , we have that , where is the basic cylinder with prefix .
With this proposition, it is not hard to see that . In the following, we inductively define a satisfiability relation as follows for a boolean combination of atomic propositions and belief formulas of the form or such that is an atemporal formula.
for if
if not
if or
if
[TABLE]
if
[TABLE]
where if , if , and the set contains states such that is on some path of and .
The case of can be done similarly as .
Now we have the following theorem to reduce the problem of model checking on the original system to the model checking on the expanded system .
Theorem 0.B.1.
* if and only if , for a formula in the language .*
Now we can interpret those belief formulas properly with the above theorem, i.e., for each and , we compute the set
[TABLE]
of states in the expanded system . It is noted that . But we do not need to compute because the following procedure will base on instead of .
0.B.1.2 Preference Function Update
This can be done by following the expressions in Section 9. By the system and the functions , we can have the updated preference functions for all . Then we can update the transition functions into by substituting with the new one. Based on these, we can update the reachability function into and the belief function into .
0.B.1.3 Model Checking Specification Formula
The model checking algorithm proceeds by labelling subformulas of on the states in . We use the notation to represent that a formula is labeled on the state . The labelling can be done recursively as follows.
for , if ,
if or ,
if not ,
if for all such that ,
if , where the function is obtained as follows.
- –
.
Intuitively, is the one-step reachability probability of those states satisfying from a given state . Recall that in the expression , the action is determined by state .
if
if where if , if , and the set contains states such that
- –
for some such that ,
- –
for all ,
- –
, and
- –
.
the case of can be done similarly as that of .
with if for all such that
- –
for some such that ,
- –
for all ,
- –
, and
- –
.
with follows the similar pattern as that of .
with if for all such that
- –
such that ,
- –
for all ,
- –
, and
- –
.
It is noted that the above labelling procedure is done locally for all the belief and trust formulas. We have the following theorem to reduce model checking problem to the above labelling algorithm.
Theorem 0.B.2.
* if and only if for all such that .*
0.B.1.4 Analysis of Complexity
For the measurement of the complexity, we use the number of states as the size of the system , and the depth as the size of the specification formula . Moreover, we assume that the sets and , for all , are polynomial with respect to the size of , and the size of the formulas in the guarding mechanism, measured with the number of operators, are also polynomial with respect to the size of . As usual, the set of agents is fixed. Also, because the observation function is defined on states, the size of is no more than the size of .
For the complexity of the fragment, we notice that the size of the expanded system is polynomial with respect to the size of but exponential with respect to the size of the specification formula .
For the pro-attitude synthesis, for every , the determination of whether can be done in EXPTIME.
The update of preference functions and the model can be done in EXPTIME.
For the model checking of the specification formula, the labelling procedure can be done in EXPTIME.
Putting them together, we have that the computational complexity of the bounded fragment of the problem is in EXPTIME. It is noted that, the exponential is with respect to the size of the specification formula. If the formula is fixed, it is in PTIME.
0.B.2 Hardness Problem
The lower bound can be obtained by a reduction from the satisfiability problem of the quantified Boolean formula (QBF), which is to determine if a QBF formula is satisfiable. A canonical form of a QBF is
[TABLE]
where if is an odd number and otherwise, and for all and . Without loss of generality, we assume that is an even number. Every QBF formula can be transformed into this format by inserting dummy variables. For a literal , we write for its variable and for its sign. For example, if then and , and if then and .
The problem can be simulated by a game between two agents and . The game consists of two phases: in the first phase, agents decide the values of variables , and in the second phase, agents evaluate the boolean formula . We write () to denote that the number is odd (even). Figure 5 gives a diagram for the construction. The system has a state space .
Before proceeding to the reduction, we recall notations and which return the intention at state for agents and , respectively. Assuming that agents’ intentions are encoded in the states make it easier to understand the reduction. Similar for the notations and .
In the first phase, the agents and make their decisions by changing their intentions. The states involved in the first phase are . Intuitively, the state represents that the value of variable was set to , and the superscript in the state represents that the state “remembers” the value of variable . We let , where only [math] and will be used in the first phase, and let . On a state or , we define for the case of , and for the case of . We do not define and for the cases of and and for the case of , since they will not be used in this proof. Intuitively, the intentional attitude reflects agent’s choice. Because the value of variable for will be decided by agent , we define , so that agent can choose the value by changing its intention. Similar for when .
Since we will test the beliefs of agent in the specification formula, only agent ’s observations are relevant. We let for any , i.e., it can see both agents’ intentions. However, it is not able to distinguish observations between and .
The idea of the first phase is that the states of the form contribute to the main computation in which agents use their intentions to decide the values of the variables under their controls. Every time a decision is made, the execution moves to both the next variable and a helper computation in which all states are labelled with the fact about the last decision. E.g., in Figure 5, for the first variable , the agent can choose between two states and , at which the variable will take different values and [math], respectively. Without loss of generality, if agent chooses , then the execution will move into both and , where the state remembers that the value of variable is . Therefore, from now on, the execution will be possible on both the main computation from and the helper computation from . But the agent can not distinguish these two executions by its observations. Generalising the above, from variable to , we will need to explore the main computation and the other helper computations, such that one helper computation is added for each variable.
The execution of the first phase can move into those states , where the main computation moves into or . By the existence of executions on these states, the system remembers the choices made by the two agents. Then in the second phase, the agent needs to justify that its choices make the formula true whenever the QBF formula is satisfiable. To do this, we let the executions of the first phase move into those states and with a uniform distribution. Each of these states represents intuitively a clause of the QBF formula. Then the agent will need to pick a literal to see if it can make the clause satisfiable.
Similar to the first phase, the choice of literals is done by agent changing its intention. For the cognitive mechanism, we have that and . That is, agent chooses the literal if its intention is changed into . Note that, we assume that agent can distinguish the clauses, i.e., . And it is able to know which clause the current literal belongs to, i.e., .
After a literal is chosen, the execution will need to move to obtain its value. This is done by a transition into one of the states in the first phase. Let be the sign of the literal and be the value of the literal. Without loss of generality, we let and , then the transition from state will move into , at which the atomic propositions are labelled. For the state , it can only move into the state , at which the atomic propositions are labelled.
Formally, let be a set of atomic propositions, we have such that
,
,
with ,
for ,
the transition function is as follows.
- –
for , ,
- –
, for ,
- –
,
- –
for and ,
- –
for and ,
- –
the labelling function is as follows.
- –
, ,
- –
, ,
- –
the set of possible observations is as follows.
- –
for player , and
- –
we ignore the definition for player as it is not used in the reduction.
the partial observation functions are defined as follows for the player .
- –
for and ,
- –
for ,
- –
for and , and
- –
.
the set of intentions is as follows.
- –
and , and
- –
we ignore the definition for and as they are not used in the reduction.
the guarding mechanism is trivial.
the preference functions are defined as follows.
- –
for ,
- –
for ,
- –
for .
In such a system, we have that is satisfiable if and only if
[TABLE]
Note that in above formula and below, we use instead of to avoid confusion with the agents and . Intuitively, the prefixes and represent the choosing of variables’ values by the agents and , respectively. After the last , the execution moves to the states and . Then, the last is for the agent to choose a specific literal, and then justify that it is satisfiable. The former is represented by the presence of a literal in the formula. The latter is guaranteed by . Without loss of generality, we let be the chosen literal and assume . If then the main computation will reach the state which is labelled with and . By construction, we know that if the variable is assigned the value by one of the agents then the helper computation with superscript is explored, and the helper computation will lead to the state at which the propositions and are labelled. On the other hand, the helper computation with superscript will not be explored, which means that the state labelled with and is not considered possible by the agent . Therefore, we have that . Similar argument can be taken to show that when .
Appendix 0.C A Decidable Fragment with and temporal operators
We present a fragment of the problem that is PSPACE-complete. Unlike the bounded fragment in Section 0.B, this fragment works with the and temporal operators in specification formula . With and operators, the specification formula can express long-term properties about agent’s mental attitudes in the system, and therefore this fragment complements the bounded fragment. However, the fragment is subject to other restrictions, including the following:
The guarding mechanism is trivial. That is, the algorithm works with model checking without conducting pro-attitude synthesis first.
The specification formula has the restrictions that
- –
it works with a single agent’s beliefs and trusts,
- –
there is no nested beliefs or trusts,
- –
beliefs and trusts cannot be in the scope of a probabilistic operator , and
- –
there is a constant number of belief or trust operators.
We make a remark on these constraints. For the first constraint, that we choose to work with a single agent’s beliefs and trusts is because in Section 0.A we have shown that the single-agent fragment is undecidable. The second constraint is imposed to keep the algorithm simple. We conjecture that it can be relaxed. The third and fourth constraints are to keep the complexity in PSPACE. For the probabilistic operator, it requires to compute a set of paths concurrently. We conjecture that the complexity can be in EXPTIME instead of in PSPACE if relaxing this constraint. To complement this, in Section 0.D, we study a fragment in which the probabilistic operator works with qualitative beliefs and trusts. The constraint on the number of belief or trust operators is to keep the expanded system, to be given below, in the size of a polynomial with respect to the formula.
There is a restriction on the system about agent ’s beliefs along the transitions. The restriction, whose details will be given later, is that along any path of an expanded system, the evaluations of belief or trust subformulas are the same on any two expanded states if the support of a probabilistic distribution over the set of states is the same.
Without loss of generality, we assume that it is the agent ’s beliefs that the specification formula is to describe. Note that the fragment has the full expressiveness of LTL.
0.C.1 Upper Bound
Because the guarding mechanism is trivial, we need only handle the third step of the verification procedure.
Preprocessing Sub-Formulas in the Scope of Belief Operators
The first step of the algorithm is to pre-process subformulas in the scope of belief or trust operators. Because there is no nested beliefs, these subformulas do not contain any belief or trust operator. Therefore, they can be handled by the usual probabilistic temporal model checking techniques, with some slight adaptations for the formulas , and . For every such subformula , we introduce a new atomic proposition , which intuitively represents the probability of being satisfied. Let such that is the set of new atomic propositions. We upgrade the labelling function into , which allows us to extract the probability value ”stored“ in .
If then , if , and , otherwise.
If then , where is the probability of satisfying formula among all the temporal paths starting from . We note that, because of Assumption 2, there exists a unique value for .
We assume that is computed from as part of the algorithm and therefore no change to our previous definitions (such as Definition 1) is necessary. Note that, after this pre-processing, all belief or trust formulas are of the form or such that is an atomic proposition. This pre-processing can also be applied to subformulas containing no belief or trust formulas. Therefore, in the following, we assume that in , all subformulas contain at least one belief or trust formulas.
We consider the negated specification formula , and verify the existence of a counterexample. We assume that the formula is in negation normal form, i.e., negation operators only appear in front of atomic propositions.
Construction of Expanded System
Let be the specification formula and be the set of belief or trust subformulas of the form or such that are their atomic propositions. We need some notations. Given a set of states, a probability space on is a triple such that if and only if . Given a probability space , we can evaluate belief and trust formulas as follows.
.
, where if , if .
the case of is analogous to .
as the probability of those states satisfying formula . In the following, we use the probability measure to represent the probability space . Given a probability distribution and a set of states , we define (for a set of states ):
[TABLE]
as the probability measure over , by a temporal transition from in one step. Moreover, on the pro-attitude dimensions, we define:
[TABLE]
and
[TABLE]
for . Intuitively, they are the probability measures over by a goal or intentional transition of agent from the states in . Moreover, the transition is parameterised over the agent ’s preference functions. Now we define the initial belief for agent . Given a state such that , we define to be the set of possible initial states whose observation is the same as . Then, we have
[TABLE]
as the initial belief.
Based on the above notations, we can construct an expanded system which maintains a probability value for each subformula in . The system is such that
, where is the domain of real numbers. Note that, although is infinite, we need only a finite number of real numbers. We assume that all numbers are of fixed precision and can be encoded with complexity .
,
the transition relation is defined as follows.
- –
if
and .
- –
if and only if and .
- –
if and only if and .
.
Constraints on the Expanded System
The constraints include,
there do not exist two states and in the expanded system such that they are reachable from one to the other, , and for some , and
for any two reachable states and such that , only one of them needs to be explored with .
With the above constraints, we can see that the size of the expanded system is . However, we do not need to explicitly construct it. The algorithm explores it on-the-fly.
Model Checking Algorithm
For the algorithm, we use function to denote the satisfiability of the formula on the state . For the base cases of non-temporal operators, we have the following inductive rules:
Algorithm 1**.**
Given a state and a formula , we define the satisfiability relation as follows:
* for if ;*
* if not ;*
* if or ;*
* if for all states such that and .*
* if for all states such that and .*
* if for all states such that for some , and is any distribution such that . Note that, as we stated earlier, no belief formula will appear in the scope of a legal intention operator. So the probability values are not useful.*
For the computation of and , we note that, because the constraint that no belief formula can be in the scope of a probability operator, the components and in the state are irrelevant. Therefore, we can compute and as the usual PCTL model checking.
* if , for being the *th formula in the set .
* if , for being the *th formula in the set .
Note that the above cases have the same results for those distributions whose supports are the same. Now we discuss the case of . With the above Algorithm 1, we note that other formulas can be interpreted directly on the states. Therefore, we can introduce atomic propositions for those , and update the labelling function into if and only if . With this processing, the formula is turned into an LTL formula . Then as the usual LTL model checking, we turn the formula into a Buchi automaton . Let be the automaton such that is a set of states, is a transition relation, is a set of initial states, and is a set of sets of acceptance states. Then we construct their product system as follows.
if and such that .
if we have that
, , and
.
.
Algorithm 2**.**
For the case where the formula is , we have that
* if is empty;*
where is the system of by substituting the initial distribution into .
Then for a formula with nested branching time operators, we can use the approach of CTL∗ model checking. Finally, we have the following theorem to state the correctness of the above algorithm.
Theorem 0.C.1.
* iff, in , holds for all .*
Analysis of Complexity
For the complexity, we need to remember the tuple for Algorithm 1 or the tuple for Algorithm 2. For Algorithm 1, we may need a polynomial number of alternations to handle the negation operators or the pro-attitudes. Therefore, by Theorem 4.2 of [9], it is in NPSPACE=PSPACE, the same complexity as that of LTL model checking. On the other hand, unlike the LTL model checking, the program complexity, i.e., the complexity measured with respect to the size of the system by assuming that the formula is fixed, is also in PSPACE.
0.C.2 Hardness Problem
The PSPACE-hardness of the problem can be obtained by a reduction from the problem of deciding if, for a given nondeterministic finite state automaton over an alphabet , the language is equivalent to the universal language . Let be an NFA such that is a set of states, is an initial state, is a transition function, and is a set of final states.
We construct a system whose states, except for the initial state , can be classified into two subsystems and . Intuitively, the subsystem simulates the execution of and upon reading each input symbol, probabilistically checks whether the current state of the automaton is a final state, while the subsystem simulates the universal language , at the same time synchronising with on words which produce a valid run of .
In particular, each state of is a pair of a symbol of the alphabet and an annotated automaton state, where the latter can be of the form , , , , or for . The state is a regular state corresponding to those of automaton , representing that the state is reached from another state by reading a symbol . However, from a state to another state such that , we need to go through two levels of intermediate states. In the first level, the state represents a decision point from which the execution may or may not conduct a test on the current state. The purpose of the test is to see if the state is a final state. With a chance of 0.5, the path will proceed to which denotes that no test will be conducted. With another chance of 0.5, the path will conduct the test. If is not a final state (e.g., the state of Figure 6), then the execution proceeds to the state , at which the atomic proposition is labelled. If is a final state (e.g., the state of Figure 6), then the execution proceeds with 0.25 chance to the state and another 0.25 chance to the state , at which both the propositions and are labelled. From both the states and , the execution can only move to a self-loop.
The subsystem consists of states which are pairs of a symbol of the alphabet and one of the elements in , and its structure mirrors that of , with the exception of final states (since does not know anything about states of automaton ). The purpose of is to make sure that words which do not produce a valid run of have a corresponding path in . The intuition of the construction can be seen from the diagram in Figure 6 The agent is given distinct observations on those states and , that is, agent can distinguish whether a test occurs at a moment. Formally, let be a set of atomic propositions, the system is such that
, i.e., there is only a single agent ,
, where , , and ,
with ,
, i.e., agent only has a trivial action
the transition function is defined as follows.
- –
for some ,
- –
if , where ,
- –
,
- –
, if ,
- –
, if ,
- –
,
- –
,
- –
, and
- –
.
, , , .
The observation of the agent is defined as follows.
- –
, and
- –
.
other components are omitted as they are not used in this reduction.
In such a system, we have that if and only if
[TABLE]
where is the release operator of LTL. To see this, we show that the language is not universal if and only if there exists an initialised infinite path such that .
() If the language is not universal, then there exists a word such that no execution of on finishes in a final state. From , we can construct a finite path in , but not able to find a path . To see this, we note that each block for represents a piece of execution that moves from a state to another state , such that , without conducting a test. At the state , a decision is made to conduct a test. However, because the word is not a word of , the test will not move into the state . Otherwise, it contradicts with the construction of that only a final state can move into a state of the form .
Because there does not exist such a path , we have that . Moreover, for all the states before on the paths , we have that , and for the state , we have that . Further, because agent can observe the test action, the check of its beliefs will only concern those paths on which the test action is only taken in the last state. Therefore, the probability, under the condition of agent ’s observations, will not leak into those states of the form , and we have . Because the until operator assumes the finiteness of the path, the latter means that for any infinite paths that is consistent with the path .
() If for some infinite path , then there must exist a finite path such that and there is a first test occurs on the state . Now we define function as that and . Intuitively, it abstracts the alphabets from the paths. Therefore, we have that is a word of that cannot reach a final state.
Finally, we also need to show that the system satisfies the constraints. Note that, the expanded system has two kinds of SCCs. The first kind of SCCs include transitions on which no test action is conducted, and the second kind of SCCs include a self loop on those states with a test action. For both the kinds of SCCs, agent ’s belief about the atomic proposition is kept the same: for the first kind of SCCs, it is always the case that while for the second kind of SCCs, it can be or , depending on whether the current path can be abstracted into a word of , and the belief values will not change.
Not that, because the formula is constant with respect to different instances of automata , the PSPACE lower bound is also a lower bound of program complexity. Moreover, the formula complexity, which measures the complexity of problem by the size of the formula by assuming that the system is constant, is also PSPACE-complete: the lower bound comes from the LTL model checking and its upper bound can be derived directly from the combined complexity. Putting the above together, the problem is PSPACE-complete for combined complexity, program complexity, and formula complexity.
Appendix 0.D A Polynomial Time Fragment
A stochastic automaton is a tuple where is a set of states, is a set of symbols, is a transition function such that for every we have , and is an initial distribution over such that . Note that, the stochastic automata defined here are different with the probabilistic automata in Section 0.A: a probabilistic automaton requires that for every and we have . Given a sequence of symbols, the acceptance probability of in a stochastic automaton is
[TABLE]
where is defined as follows: and for an empty sequence of symbols. Two stochastic automata are equivalent if for each string , they accept with equal probability [50].
Given a stochastic automaton , a pair is a component of if and for all and , we have . We say that is a strongly connected component (SCC) if for all , there exists a sequence of symbols such that , where the computation of can be done recursively as follows: and for an empty sequence of symbols. An SCC is closed if for all we have .
Constraints
Assume that we are given a system and a formula or such that
does not contain any belief or trust formulas,
is of CTL-style, i.e., there is no direct nesting of temporal operators, and
the system satisfies that , i.e., once formula holds, it will hold since then.
We consider their negated specification formulas or , and the algorithm, to be given below, is to determine the existence of a witness for them. We make a remark here that, the polynomial time complexity of this fragment relies on the Assumption 2 that the transition function of the system is deterministic, i.e., for every state there is a unique such that . If this restriction is relaxed by allowing the possibility of more than one actions with , it is expected that the complexity could be higher.
Algorithm
Fist of all, we need to compute or for every state and formula , depending on which operator, or , the formula is in the scope of. Recall that is the probability of satisfying among all the temporal paths starting from state . Because of the restrictions on , these can be computed in polynomial time, using a standard PCTL model checking procedure on DTMCs. We can define for a path as , and have the following proposition.
Proposition 6.
For a formula without any belief or trust operator, we have that and whenever .
Because belief formulas and trust formulas can be handled in a similar way, in the following we only work with belief formulas. The technique can be adapted to work with trust formulas. From the system , we can construct a system such that
,
if , , , and , and
.
Intuitively, is the production of two copies of the system such that the two copies preserve the same observations along the transitions (by letting in and in ) and the second copy always selects those states which do not satisfy the formula (by letting ). On such a system , we define operator for such that where
if and .
is the th component of , and
is the th component of .
Intuitively, in , we only consider those initial and transition probabilities of the th copy of the system .
Let be a set of states. A component of is a pair . We define as the th component of for .
Definition 24.
We say that the component is an SCC if either or is an SCC, and is a double-closed SCC if both and are closed SCCs.
By the construction of , we have
Proposition 7.
* is an SCC if and only if is an SCC.*
Moreover, given , we can compute a stationary distribution for each of and . Such a stationary distribution always exists and uniquely exists for a finite , which is a DTMC. Let be the stationary distribution of . Then, from a component , we can construct two stochastic automata and where and are their initial distributions.
Definition 25.
We say that is internal equivalent when two automata and are equivalent. A component is formula-specific with respect to the formula if for some and .
Recall that, two stochastic automata are equivalent if they have the same acceptance probability for all strings. Note that, in the construction of , we require that the second copy always selects those states which do not satisfy the formula . Therefore, a formula-specific component suggests that the component contains inconsistency between two copies of the system with respect to the formula .
Let be the set of paths in , and and be the set of infinite and finite paths in , respectively. We also extend the transition relations and to work with paths in , similar as that of and in stochastic automata. We do not define because the two copies of the system have the same observations.
Let be a finite path such that is in an SCC . Given a path in the SCC , we let be the set of paths that agent cannot distinguish. Then we write
[TABLE]
for the probability of infinite continuations of whose probability ratio between the two copies of the system is maintained (i.e., greater than ). Moreover, we let , if for all number , there exists such that , and , otherwise. We have the following propositions.
Proposition 8.
If is not internal equivalent then for all finite paths whose last state is on .
Proof.
Let be the shortest path on which the two copies of the system have different acceptance probabilities. By the construction of , some transitions are removed due to the restriction of . Therefore, the probability of the second copy is less than the one of the first copy, and we have . Then we can construct a path which contains a large number of pieces of observations that are equivalent to . With this path, we have that, for all , . Therefore, we have that . ∎
Proposition 9.
* if and only if is double-closed and internal equivalent.*
Proof.
() Assume that is double-closed and internal equivalent. By the definition of internal equivalence, for all finite paths , we have that , which means that . Because is double-closed, we have that .
() Assume that . We show that both conditions are indispensable. If is not double-closed and it is the first copy that is not closed, then the probability of will flow out of the SCC. Therefore, for a sufficiently large number . If is not double-closed and it is the second copy that is not closed, then for a sufficiently large , which means that . Moreover, the case in which is double-closed but not internal equivalent is guaranteed by Proposition 8. ∎
Proposition 10.
Let be a finite path such that is on an SCC , and is double-closed, internal equivalent, and formula-specific with respect to . Then if and only if for all , .
Proof.
This is equivalent to proving that
[TABLE]
for .
Now, by the construction of (in which the second copy satisfies ) and the three conditions of , we have that
[TABLE]
The equivalence of
[TABLE]
and
[TABLE]
can be seen by their structures. ∎
With these propositions, we have the following algorithm.
Algorithm 3**.**
After the computation of or for every state and formula , the algorithm proceeds by the following sequential steps:
compute the set of SCCs of such that is formula-specific with respect to , double-closed, and internal equivalent, 2. 2.
for every state satisfying , we do the following:
- (a)
compute the reachability probability to those SCCs from the first step; let the probability value be , and 2. (b)
check whether .
If there exists a state that can satisfy the above computation, then the specification formula does not hold, otherwise holds.
Analysis of Complexity
The complexity of the algorithm is in polynomial time. First of all, the computation of or can be done in polynomial time because is of CTL-style and contains no belief or trust formula. Second, for the first step of the algorithm, the computation of all SCCs of , whose size is quadratic with respect to , can be done in polynomial time by Tarjan’s algorithm, and the checking of the three conditions (i.e., formula-specific with respect to , double-closed, and internal equivalent) can be done in polynomial time. In particular, the checking of internal-equivalent of an SCC can be done in polynomial time is a result of the existence of a polynomial time algorithm for the equivalence of stochastic automata [50]. Third, for the second step of the algorithm, the computation of reachability probability on can be done in polynomial time, and the comparison of values can be done in constant time.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Akash, K., Hu, W., Jain, N., Reid, T.: A classification model for sensing human trust in machines using EEG and GSR. Co RR abs/1803.09861 (2018), http://arxiv.org/abs/1803.09861
- 2[2] Asch, S.: Forming impression of personality. The Journal of Abnormal and Social Psychology 40 (3), 258–290 (1946)
- 3[3] Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Computer Aided Verification. pp. 155–165. Springer Berlin/Heidelberg (1995)
- 4[4] Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. The MIT Press (2008)
- 5[5] Berg, J., Dickhaut, J., Mc Cabe, K.: Trust, reciprocity, and social history. Games and Economic Behavior 10 (1) (1995)
- 6[6] Bratman, M.: Intentions, Plans, and Practical Reason. Harvard University Press, Massachusetts (1987)
- 7[7] Castelfranchi, C., Paglieri, F.: The role of beliefs in goal dynamics: prolegomena to a constructive theory of intentions. Synthese 155 , 237–263 (2007)
- 8[8] Chakraborty, S., Katoen, J.P.: On the satisfiability of some simple probabilistic logics. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 56–65. LICS ’16, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2933575.2934526, http://doi.acm.org/10.1145/2933575.2934526