Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems

1 Introduction

Multiagent systems have found many applications in practice [Seuken and Zilberstein, 2008], ranging from coordinated helicopter flights [Nair et al., 2005], to distributed sensors [Pynadath and Tambe, 2002]. In this paper, we focus on probabilistic multiagent systems which can model uncertainty, such as component failure, of the agents and/or their environment.

In multiagent systems it is typical that agents share incomplete information with each other, otherwise multiagent systems will degenerate to systems with a single agent [Kazmierczak et al., 2014]. The incompleteness of information is normally characterized by defining for each agent i an equivalence relation ∼i over all global states of the systems; two global states are considered indistinguishable for a given agent i if they are related by ∼i. Two states that are indistinguishable for an agent may be distinguishable for another agent. It is a natural, and realistic, setting that every agent makes its own decisions based only on the limited information it has; namely, the information provided by its own indistinguishable relation, and nothing else. Decisions of agents are usually formalized by the notion of schedulers (also known as policies or strategies), which are functions taking history executions as input and deciding the next move for each agent. Schedulers only making use of limited information of each agent are called uniform (or decentralized).

To specify the property of probabilistic multiagent systems, in particular the temporal dynamics of agents' knowledge, we use Probabilistic Epistemic Temporal Logic (PETL) (cf. [Delgado and Benevides, 2009]). PETL can be seen as a combination of epistemic logic [Fagin et al., 2004] and probabilistic computation tree logic (PCTL) [Jonsson and Larsen, 1991]. For its semantics, the knowledge operator Ki is defined over agent i's indistinguishable relation and the probabilistic operator [ψ]▷◁d is defined over uniform schedulers.

We study the model checking problem [Baier and Katoen, 2008] for PETL logic, with the following contributions. The first contribution is a set of complexity results, including the undecidability for the general case and the decidability (in P NP and NP-hard) when schedulers are memoryless.

The second contribution is a symbolic model checking algorithm for memoryless schedulers. The algorithm reduces the model checking problem to a mixed integer non-linear programming problem, which can then be solved with a modern SMT solver such as Z3. The reduction procedure is novel, particularly for the part handling loops in the state space. While both strategic and epistemic reasoning on probabilistic multiagent systems have been studied in theory (mainly semantics), detailed works on the algorithmic design, implementation, and validation based on an existing model checker is not available. This paper presents the first tool to enable PETL model checking.

Finally, we validate our tool on models from the International Probabilistic Planning Competitions (IPPC). The experimental results show the scalability of our symbolic algorithm in handling interesting problems.

1.1 RelatedWork

In the non-probabilistic multiagent systems, schedulers with incomplete information have been studied extensively; see for instance [Jamroga, 2003; Jamroga and van der Hoek, 2004]. In [van der Hoek and Wooldridge, 2002], a model checking algorithm is presented for alternating temporal epistemic logic and it is shown that the problem can be reduced to model checking alternating temporal logic [Alur et al., 2002].

The logic PETL was introduced in [Delgado and Benevides, 2009]. However, their semantics is defined under all schedulers, so the corresponding model checking problem has the same complexity with the standard PCTL one. [Huang and Luo, 2013] proposes a probabilistic epistemic logic pATEL∗ , which can be seen as a combination of probabilistic Alternating Time Logic (pATL) [Huang et al., 2012] and epistemic logic. Different from [Schnoor, 2010], in [Huang and Luo, 2013] the epistemic accessibility relations are also probabilistic, namely, there is a probabilistic distribution over the set of indistinguishable states. Most of the existing works are theoretical, without detailed algorithmic design, implementation, and validation. One exception is [Huang et al., 2011], which presents a symbolic model checking algorithm for fully probabilistic systems, i.e., systems without nondeterministic choices. Other exceptions are [Wan et al., 2013; Sultan et al., 2014], which also consider fully probabilistic systems. Different from [Huang et al., 2011], [Wan et al., 2013; Sultan et al., 2014] convert epistemic probabilistic logic model checking problem to the standard PCTL one, and then make use of the PRISMmodel checker. However, their approach can not be extended to deal with our problem, because our problem is under uniform schedulers in probabilistic systems with nondeterministic choices.

Existing model checkers for multiagent systems include MCMAS [Lomuscio et al., 2017], which does not work with probabilistic systems, and MCK [Huang and van der Meyden, 2014; Huang et al., 2011], which cannot handle PETL model checking problem. Probabilistic model checkers such as PRISM [Kwiatkowska et al., 2011] do not work with epistemic logics and incomplete information systems.

2 Preliminaries

Given a finite set X, a discrete probability distribution on X is a function µ : X → [0, 1] such that µ(X) = ∑x∈X µ(x) = 1. Let Disc(X) denote the set of all discrete probability distributions over X. We denote by δx ∈ Disc(X) the Dirac distribution such that δx(y) = 1 if y = x, 0 otherwise.

2.1 Probabilistic Concurrent Game Structure

A PO-PCGS (partially observed probabilistic concurrent game structure) with n agents is a tuple

• S is a finite set of states with initial state ¯ s ∈ S;
• Agt is the set of n agents;
• Acti is the set of actions for agent i. We denote by Act = ∏ni=1 Acti the set of full actions;
• T : S ×Act →Disc(S) is a partial transition function;
• For each i ∈ Agt, ∼i is an accessibility equivalence relation on S. For s ∈ S, denote by [s]i the equivalence class of ∼i which contains s;
• AP is a finite set of atomic propositions; and
• L: S → 2AP is a labeling function.

As notation, we let r, s, t, . . . and their variants with indices range over S, a, b, . . . range over Acti, and α, β, . . . range over Act. Given a state s and a full action α, we say that α is enabled by s if T (s, α) = µ, also written s α-→µ. For an agent i ∈ Agt, we denote by EAi(s) ⊆ Acti the set of enabled actions by s for agent i. Similarly, we denote by EA(s) ⊆ Act the set of enabled full actions at state s. We wirte P (s, α, t) = µ(t) where s α-→µ.

The equivalence relation ∼i for the agent i relates states that are considered to be not distinguishable by the agent i; a first consequence is that two related states must enable the same actions, i.e., whenever s ∼i t, then EAi(s) = EAi(t).

A path π is a finite or infinite sequence of alternating states and actions s0α0s1α1 . . ., starting (and ending, if finite) with a state, such that for each k > 0, sk αk --→µk and µk(sk+1) > 0. For π = s0α0s1α1 . . . and k ≥ 0, we denote by π[k] the state sk. If π is finite, then we denote by |π| the size (or, length) of π, i.e., the number of states in π, and by ̂ π↓ its last state. We denote the sets of finite and infinite paths by Paths ∗ and Paths ω , respectively, and we let ̂ π and π and their variants with indices range over Paths ∗ and Paths ω , respectively.

In the following we assume that all states of an PO-PCGS M are reachable, i.e., for each state s ∈ S, there exists a finite path ̂ π = s0α0s1α1 . . . sn such that s0 = ¯ s and sn = s.

Schedulers of PO-PCGS

Schedulers (also known as policies, strategies, or adversaries) are functions that resolve nondeterminism, i.e., they are used to choose the next action to be performed (based on the past history) whenever we reach a state enabling multiple actions. Once nondeterministic choices are solved, we can define an appropriate probability measure for the events in a PO-PCGS, like reaching specific states.

A scheduler for an agent i is a function σi : Paths ∗ → Acti mapping each finite path ̂ π ∈ Paths ∗ to an action in EAi(̂ π↓). A uniform scheduler σi for an agent i is a scheduler such that for each pair of finite paths ̂ π = s0α0s1α1 . . . sn and ̂ π′ = s′0α′0 s′1α′1 . . . s′n , it holds that if for each 0 ≤ k ≤ n, αk = α′k and sk ∼i s′k , then σi(̂ π) = σi(̂ π′ ). A uniform memoryless scheduler for an agent i is a scheduler such that for all states s, t, we have that s ∼i t implies σi(s) = σi(t).

A scheduler σ for a PO-PCGS M with n agents is a tuple (σ1, . . . , σn) such that each σi is a scheduler for agent i. We say that σ is uniform (memoryless) if each σi is uniform (memoryless) and we denote by SU and SUM the sets of uniform and uniform memoryless schedulers, respectively.

A scheduler σ and a state s induce a unique probability measure Prσ,s on the σ-field generated by cylinder sets of finite paths. Intuitively, the probability of (the cylinder set of) a finite path π = s0α0s1α1 . . . sn is the product of the probability of going from sk to sk+1 given that σ has chosen αk, for each k. See [Baier and Katoen, 2008] for more details.

2.2 Probabilistic Epistemic Temporal Logic

In this section we present the syntax and semantics of Probabilistic Epistemic Temporal Logic (PETL) initially introduced in [Delgado and Benevides, 2009] as K-PCTL. PETL formulas are defined according to the following grammar:

where ▷◁ ∈ {<,>,≥,≤}, d ∈ [0, 1], i ∈ Agt, p ∈ AP, and G ⊆ Agt. From the above grammar, we can see that PETL subsumes both PCTL and epistemic formulas.

Let ∼EG = ⋃i∈G ∼i, ∼DG = ⋂i∈G ∼i, and ∼CG be the transitive closure of ∼EG. Let s be a state of a PO-PCGS, and ϕ a PETL formula. We say that s satisfies ϕ, denoted s |= ϕ, iff

• s |= p if p ∈ L(s), s |= ¬ϕ if s ̸|= ϕ, and s |= ϕ1 ∧ ϕ2 if s |= ϕ1 and s |= ϕ2, as usual;
• s |=Kiϕ iff t |= ϕ for all t ∈ [s]i;
• s |= EGϕ iff t |= ϕ for all t ∼EG s;
• s |=DGϕ iff t |= ϕ for all t ∼DG s;
• s |=CGϕ iff t |= ϕ for all t ∼CG s;
• s |= [ψ]▷◁p iff for all σ ∈ SU,

where

• π |=Xϕ iff π[1] |= ϕ;
• π |= ϕ1 Uϕ2 iff there exists k ≥ 0 such that π[k] |= ϕ2 and π[j] |= ϕ1 for all 0 ≤ j < k.

Different from [Delgado and Benevides, 2009], the semantics of PETL in our paper is defined over all uniform schedulers instead of general schedulers. As we have discussed in the introduction, this restriction is natural for multiagent systems.

We want to remark that, while the probabilistic operator [ψ]▷◁d makes use of the schedulers to evaluate the probability of the paths satisfying the path formula ψ, the agents are not aware of the current scheduler, so they can not make use of such an information in evaluating their knowledge. This means that the agents do not have to consider the potential unreachability problem caused by the choices made by the current scheduler (cf. [Jamroga and van der Hoek, 2004]).

3 Model Checking PETL

In this section, we discuss the problem of model checking PETL on PO-PCGSs. We show that the problem is in general undecidable but it becomes decidable if we restrict the schedulers to be memoryless. We then analyze the complexity of the restricted problem.

3.1 Undecidability of General Cases

Theorem 1. The PETL model checking problem, restricted to uniform schedulers, is undecidable, even for PO-PCGSs with a single agent.

Proof. The proof is by reduction of the undecidable problem about the emptiness of a Probabilistic Finite Automaton (PFA) [Rabin, 1963; Paz, 1971] to model checking PETL.

The reductions works as follows: given a PFAA, it is considered as a PO-PCGS MA with a single agent that is only able to distinguish final from non-final states; each state is labelled by f if and only if it is final. Then it is possible to show that, given A and ρ ∈ (0, 1), there exists a finite word w ∈ Σ∗ such that A(w) > ρ (i.e., w is accepted by A with probability at least ρ) if and only if ¯ s ̸|= [tt U f ]≤ρ .

3.2 Complexity under Memoryless Setting

Theorem 2. If restricted to uniform memoryless schedulers, model checking PETL is in P NP and NP-hard. The NPhardness holds even for PO-PCGSs with a single agent.

P NP Membership

Propositional formulas and epistemic formulas can be solved in PTIME. We can decide whether s |= [ψ]▷◁d by:

1. Guessing a scheduler σ ∈ SUM;
2. Deciding whether Prσ,s({ π ∈ Paths ω | π |= ψ }) ▷◁ d, which is model checking PCTL on Markov chain and can be solved in PTIME [Baier and Katoen, 2008].

So s |= [ψ]▷◁d can be solved in NP. However, the probabilistic operator can be nested, so a polynomial procedure with respect to the size of formula is needed to query a NP oracle, which results the PETL model checking problem in P NP .

NP-hardness

We reduce the 3SAT problem to this problem. Let X = {x0, . . . , xk} be a set of Boolean variables. An assignment is a total function θ : X → {0, 1}. Let a clause C be the disjunction of three Boolean variables or their negations. A formula is a conjunction of clauses.

The following problem is well-known to be NP-complete: given any Boolean formula f = C0∧· · ·∧Cl, decide whether there exists an assignment under which f is true.

Given a Boolean formula f, we encode it as a PO-PCGS M = (S, ¯ s, {i}, Act , {∼i}, T , AP, L) as follows:

• S = {¯ s} ∪ { sbm,n | b ∈ {0, 1} ∧ 0 ≤ m ≤ k + 1 ∧ 0 ≤ n ≤ l };
• Act = {α, α0 , α1 } and there is only one agent i;
• ∼i is defined as:

• T is defined as follows:

• for each 0 ≤ m ≤ k, 0 ≤ n ≤ l, and b ∈ {0, 1}:

• AP = {⊤}; and
• L is defined as follows: for each s ∈ S,

Then we have that f is NOT satisfiable iff ¯ s |= [tt U⊤]<1 . The above reduction is obviously in polynomial time.

4 PETLModel Checking Algorithm

In the previous section we have seen that model checking PETL is in general undecidable but it becomes decidable if we restrict the schedulers to be uniform and memoryless. In this section, we present an algorithm, shown as Algorithm 1, to model check PETL against uniform memoryless schedulers in SUM.

In Algorithm 1, we use the following notation:

and [s](∪G)∗ is the least fixed point of fs,G(X) = {s′ ∈ S | ∃t ∈ X ∪ {s}, i ∈ G : s′ ∈ [t]i }. Note that the computation of the fixed point of fs,G requires at most |S| iterations.

Algorithm 1 Procedure to compute the set of states satisfying a PETL formula ϕ

1: procedure Sat(ϕ)

• 2: if ϕ = p return {s ∈ S | p ∈ L(s) };
• 3: if ϕ = ¬ϕ′ return S \ Sat(ϕ′ );
• 4: if ϕ = ϕ1 ∧ϕ2 return Sat(ϕ1) ∩ Sat(ϕ2);
• 5: if ϕ =Kiϕ′ return {s ∈ S | [s]i ⊆ Sat(ϕ′ ) };
• 6: if ϕ = EGϕ′ return {s ∈ S | [s]∪G ⊆ Sat(ϕ′ ) };
• 7: if ϕ =DGϕ′ return {s ∈ S | [s]∩G ⊆ Sat(ϕ′ ) };

• 9: if ϕ = [Xϕ′ ]▷◁d return {s ∈ S | ∀α ∈ EA(s) : T (s, α)(Sat (ϕ′ )) ▷◁ d };
• 10: if ϕ = [ϕ1 Uϕ2]▷◁d return {s ∈ S | ∀σ ∈ SUM : Prσ,s({ π ∈ Paths ω | π |= ϕ1 U ϕ2 }) ▷◁ d };

Since SUM is finite, Algorithm 1 terminates: similarly to the model checking algorithm for PCTL on MDPs (see, e.g., [Baier and Katoen, 2008]), the algorithm follows a bottom-up approach based on the structure of the formula ϕ. All cases follow directly from the semantics; the interesting ones are about the probabilistic operator [ · ]▷◁d which has a temporal formula as argument. For the next operator X, we can directly consider all actions enabled by the state since the type of schedulers does not affect the outcome. Instead, for the until operator U, we have to consider the scheduler, since ϕ1 Uϕ2 may be satisfied by paths of different length. In the following section, we describe an algorithm to deal with all uniformmemoryless schedulers at the same time.

4.1 Dealing with UniformMemoryless Schedulers

In this section we show how to solve the problem of deciding whether s |= [ϕ1 U ϕ2]▷◁d provided that we have computed C = Sat (ϕ1) and B = Sat (ϕ2), i.e., deciding whether s |= [C U B]▷◁d , with respect of all uniform memoryless schedulers. In order to decide whether s |= [CUB]▷◁d , it suffices to consider only Pr max s ({π ∈ Paths ω | π |= C UB}) and Pr min s ({π ∈ Paths ω | π |= C UB}) over all uniform memoryless schedulers.

Let's consider the minimal probability first. Let Agt = {1, . . . , n} and consider xs = Pr min s ({π ∈ Paths ω | π |= C UB }). We write s |= ∃♦B to denote the fact that the set B is reachable from s in the underlying graph of M. Then the vector (xs)s∈S ∈ R|S| ≥0 yields the unique solution of the following programming problem whose constraints are:

1. xs = 1 if s ∈ B;
2. xs = 0 if s ̸|= ∃♦B or s /∈ C \ B;
3. If s ∈ C \ B and s |= ∃♦B, then

1. p[t]i,ai ∈ {0, 1} for all i ∈ Agt , t ∈ S, and ai ∈ EAi(t);
2. ∑ai∈EAi(t) p[t]i,ai = 1 for all i ∈ Agt and t ∈ S;

where xs is minimal.

Note that the above problem is a Mixed Integer Non-Linear Program (MINLP), while the programs of standard PCTL model checking are Linear Programs (LP).

Intuitively, having p[s]i,ai = 1 represents the fact that agent i chooses action ai at each state t ∈ [s]i. Each uniform memoryless scheduler corresponds to one assignment for variables p[s]i,ai . The minimal xs is the minimal probability we want.

However, it is not straightforward to adapt the above program to compute the maximal probability Pr max s ({π ∈ Paths ω | π |= C U B}). We explain why with the help of the following PO-PCGS.

In this PO-PCGS, all states have empty label except for L(3) = {p}; there is only one agent who can distinguish every state. We want to compute xs = Pr max s [tt Up] for each state. Clearly, what we want to get is x0 = x1 = 0.5, x2 = 0, and x3 = 1. However, if we use the above program, when the agent chooses b at state 1, we get x0 = x1 and x1 = x0, so x0, x1 can be assigned to any value between 0 and 1. If we take the minimal value, we get 0; if we take the maximal value, we get 1: they are both different from the right answer.

The key part of this problem is that states 0 and 1 form a loop when the agent chooses b at state 1. In this case, x0 and x1 should be both 0, because they can not reach state 3. To force the value of a variable xs to be 0 whenever the scheduler makes the state s unable to reach B, we extend the above problem by adding more constraints. We introduce a new variable fs for each state s, so that 0 ≤ fs ≤ |S|, with the following meaning: fs = 0 means that s ̸|= ∃♦B or s /∈ C \B; fs ≥ 1 means that there is a path from s to B with length fs. The corresponding constraints are as follows:

1. fs = 1 if s ∈ B;
2. fs = 0 if s ̸|= ∃♦B or s /∈ C \ B;

where

Finally, we require that xs is maximal.

Intuitively, fs = 0 =⇒ xs = 0 means that, if state s can not reach states in B under the current scheduler, then xs must be 0. The constraint fs > 0 =⇒ ∨t∈S fs = ft + 1 ∧ Ps,t > 0 represents the fact that under the current scheduler, s can reach a successor t with positive probability Ps,t > 0 and fs = ft + 1, i.e., reaching B from s requires one step more than from t. The constraint fs = 0 ⇐⇒ ∧t∈S (ft = 0 ∧ Ps,t > 0) ∨ Ps,t = 0 ensures that s and each proper successor t of s have value 0, in case under the current scheduler they are not able to reach B. Finally, fs ̸= 1 ∧ 0 ≤ fs ≤ |S| ensures that fs is finite and it is either 0 or an integer strictly larger than 1 (as byproduct of the equality fs = ft +1 from the second constraint).

Consider again the previous example; we have the following constraints (after replacement and simplification):

If p1,b = 1 (thus, p1,a = 0), then we have f0 = f1 = 0 because there is no other assignment satisfying 0 ≤ f0 ≤ 4 ∧ 0 ≤ f1 ≤ 4 ∧ f0 = f1 + 1 ∧ f1 = f0 + 1; if p1,a = 1 (thus, p1,b = 0), then we have f0 = 3 and f1 = 2.

5 Implementation and Experiments

We have implemented the proposed PETL model checking algorithm in ePMC [Hahn et al., 2014] and we present the experiment results in this section. In our implementation, we use the SMT solver Z3 [de Moura and Bjørner, 2008] (version 4.6.0) to solve the MINLP problem. We have also tried to use CPLEX, a high-performance mathematical programming solver, which also supports convex MINLP problems; however it refuses to solve the MINLP problems we generate by stating that they are not convex. The models we use for our experiments are taken from the IPPC competitions held in 2011 and 2014, and the original IPPC domain decription of these models can be found at https://github.com/ssanner/rddlsim. All experiments were conducted on a 3.40GHz Intel Core i7-2600 CPU with 8GB of memory. The source code of our implementation is available at https://github.com/fuchen1991/epmc-petl.

5.1 Robot NavigationModel

In this model, there are several robots moving in a grid, trying to reach a goal area. Every cell makes the robots disappear with a different probability. Once the robot arrives at the goal, it will not disappear any more. Each robots has several actions available at each cell: moving left, right, up, and down. The robots are totally independent, namely, one robot does not know other robots' locations and actions. The properties we are concerned about are the probabilities of the robots getting to the goal or disappearing.

In this experiment, we have 2 robots; we varied the size of the grid by changing the number of rows and columns; the size of the resulting PO-PCGSs is summarized in Table 1.

Table 2 shows the time needed to compute the maximal probability of a robot eventually reaching its goal area. We can see that Z3 takes almost the whole execution time, so one can get better performance by using a faster solver.

Table 3 shows instead the time needed to get the minimum probability of a robot eventually reaching its goal area, which is 0. As we can see, computing minimal probability scales much better, since Z3 has fewer constraints to satisfy.

It is interesting to observe how the number of variables and constraints generated for computing Sat ([ϕ]▷◁d ) is loosely related to the number of transitions |T | of the PO-PCGS (cf. Tables 1 and 2). This is due to the fact that a single constraint may correspond to several concrete transitions; for instance, the choice by the scheduler of each transition s α-→µ from a state s in [t]i with full action α involving the (agent) action ai is represented by a single constraint p[t]i,ai ∈ {0, 1}.

As formulas involving epistemic operators, consider Φ1 = Pr max [G(Krobot1 (row1 ̸= row2 ∨ col1 ̸= col2) ∧ ¬disappeared1 ∧ ¬disappeared2)] and Φ2 = Pr max [G(Drobot1,robot2 (row1 ̸= row2 ∨ col1 ̸= col2) ∧ ¬disappeared1 ∧¬disappeared2 )], requiring to compute the maximal probability of robot1 (together with robot2 , resp.) always knowing that the two robots are not in the same cell and that both robots have not disappeared, respectively. Table 4 shows the results for these two formulas on the instance with 2 rows and 5 columns, where in every cell the probability of disappearing lies in the interval (0, 1), and the two robots have different goals and initial cells, with respect to three different accessibility relations: R1 represents the fact that each robot is oblivious of the other robot; R2 encodes the fact that the robots know whether they are in the same cell; and in R3 each robot knows whether the other robot is at Manhattan distance at most 2.

First we note that for R1, Z3 is not needed to solve Φ1 because the robot does not know whether it is in the same initial cell with the other robot. Then, by giving the robots more knowledge, like by means of DG or by the accessibility relations, then each robot knows some detail about where the other robot is so they can avoid to be in the same cell.

5.2 Reconnaissance Model

In this model, there is a N ×N grid with 2 robots, a base for each robot, some hazard areas, and some objects in different locations. The main task of the robots is to reach an object and study its properties; to this aim, one robot has sensors to detect water while the other has a camera to take pictures. The robots' movements are deterministic while taking a picture or sampling for water are probabilistic: with positive probability it is possible to get blurred pictures or not recognizing water. Moreover, if a robot runs into a hazard or it is on an adjacent square, then it has a positive probability of damaging its sensor, which increases sharply the probability of sensor failure. The sensor can be repaired at the robot's base.

Initially, the two robots are in different cells and they know whether they are in the same location.

Table 5 shows the results regarding the minimum probability of taking a good picture and identifying water on different sizes of the grid. The resulting probability is 0, induced by a scheduler never making the robots use their sensors. Similarly to the navigation model cases, Z3 is the bottleneck of our implementation, that is anyway scaling reasonably well.

Regarding the effect of analyzing epistemic operators, consider the formulas Φ3 = Pr max [G(rw x ̸= rc x ∨ rw y ̸= rc y)] and Φ4 = Pr max [GErw,rc(rw x ̸= rc x ∨ rw y ̸= rc y)] which ask for the maximal probability of the two robots always (knowing of) being on different cells, respectively; the results are shown in Table 6, with the same number of variables and constraints as in Table 5. As we can see, since the robots know whether they are in the same cell, the two formulas are essentially equivalent and they require roughly the same time to be computed.

6 Conclusion and FutureWork

In this paper we have considered the problem of model checking probabilistic multiagent systems with respect to a probabilistic epistemic logic. We have shown that the problem is in general undecidable; we have also shown that it becomes decidable when restricted to the class of uniform memoryless schedulers. For the latter class we have proposed a decision algorithm, analyzed its complexity, and evaluated a prototypical implementation on models from the IPPC competitions. The experimental evaluation confirms the theoretical results about the complexity of the model checking problem. As future work, we plan to investigate how to make the algorithm more scalable in practice as well as how to enrich the logic, such as by adding reward predicates or ω-regular properties.

Acknowledgments

This work was supported by the National Natural Science Foundation of China (Grants Nos. 61532019, 61650410658, 61761136011), by the CDZ project CAP (GZ 1023), and by the CAS/SAFEA International Partnership Program for Creative Research Teams. Yuan Feng was also partially supported by the Australian Research Council (Grant Nos. DP160101652 and DP180100691).