Justification Based Reasoning in Dynamic Conflict Resolution

TL;DR

This paper introduces a logical framework for modeling and resolving dynamic conflicts in traffic scenarios involving multiple agents with local perceptions and incomplete information.

Contribution

It presents a novel logical approach combining epistemic, modal, justification, and temporal logics to identify conflicts and derive justifications in dynamic traffic situations.

Findings

Framework effectively models conflict identification

Enables reasoning with incomplete and local information

Supports conflict resolution strategies in traffic scenarios

Abstract

We study conflict situations that dynamically arise in traffic scenarios, where different agents try to achieve their set of goals and have to decide on what to do based on their local perception. We distinguish several types of conflicts for this setting. In order to enable modelling of conflict situations and the reasons for conflicts, we present a logical framework that adopts concepts from epistemic and modal logic, justification and temporal logic. Using this framework, we illustrate how conflicts can be identified and how we derive a chain of justifications leading to this conflict. We discuss how conflict resolution can be done when a vehicle has local, incomplete information, vehicle to vehicle communication (V2V) and partially ordered goals.

Equations

$$⊢\square (\varphi \to \psi )\to (\square \varphi \to \square \psi )\text{,}$$

$$\text{from }⊢\varphi \text{ conclude }⊢\square \varphi \text{.}$$

$$⊢\square \varphi \to \varphi \text{,}$$

$$⊢\square \varphi \to ◊\varphi \text{.}$$

$$⊢E:\varphi \to F:\varphi \text{, where E is a subgroup of F.}$$

$$⊢s:(\varphi \to \psi )\to (t:\varphi \to [s\cdot t]:\psi )\text{,}$$

$$⊢s:\varphi \to [s+t]:\varphi \text{,}⊢s:\varphi \to [t+s]:\varphi \text{,}$$

$$\varphi ::=\perp \mid A\mid (\varphi \to \varphi )\mid E:(\varphi )\mid \mathrm{missing}X(\varphi )\mid \mathrm{missing}P(\varphi )\mid (\varphi )\mathrm{missing}U(\varphi )\mid (\varphi )\mathrm{missing}S(\varphi ).$$

$$\displaystyle\begin{array}[]{lcl}(M,r(t))\not\models_{\_}G\bot\text{.}\\ (M,r(t))\models_{\_}GQ&:\Longleftrightarrow&Q\in\pi(r(t))\text{.}\\ (M,r(t))\models_{\_}G\phi\to\psi&:\Longleftrightarrow&(M,r(t))\models_{\_}G\phi\text{ implies }(M,r(t))\models_{\_}G\psi\text{.}\\ (M,r(t))\models_{\_}GE{:}\phi&:\Longleftrightarrow&(M,r^{\prime}(t))\models_{\_}G\phi\text{ for all $r^{\prime}$ with $r(t^{\prime})\mapsto_{\_}Er^{\prime}(t^{\prime})$ for all $t^{\prime}\leq t$.}\\ (M,r(t))\models_{\_}G{\mathord{\mathrm{missing}}{X}}\phi&:\Longleftrightarrow&(M,r(t+1))\models_{\_}G\phi\text{.}\\ (M,r(t))\models_{\_}G{\mathord{\mathrm{missing}}{P}}\phi&:\Longleftrightarrow&(M,r(t^{\prime}))\models_{\_}G\phi\text{ for some $t^{\prime}$ with $t^{\prime}+1=t$.}\\ (M,r(t))\models_{\_}G\phi{\mathord{\mathrm{missing}}{U}}\psi&:\Longleftrightarrow&(M,r(t^{\prime}))\models_{\_}G\psi\text{ for some $t^{\prime}\geq t$ and }\\ &&\text{$(M,r(t^{\prime\prime}))\models_{\_}G\phi$ for all $t^{\prime\prime}$ with $t\leq t^{\prime\prime}<t^{\prime}$.}\\ (M,r(t))\models_{\_}G\phi{\mathord{\mathrm{missing}}{S}}\psi&:\Longleftrightarrow&(M,r(t^{\prime}))\models_{\_}G\psi\text{ for some }0\leq t^{\prime}\leq t\text{ and }\\ &&\text{$(M,r(t^{\prime\prime}))\models_{\_}G\phi$ for all $t^{\prime\prime}$ with $t^{\prime}<t^{\prime\prime}\leq t$.}\end{array}$$

Full text

Justification Based Reasoning in Dynamic Conflict Resolution

1 Introduction

As humans are replaced by autonomous systems, such systems must be able to interact with each other and resolve dynamically arising conflicts. Examples of such conflicts arise when a car wants to enter the highway in dense traffic or simply when a car wants to drive faster than the preceding. Such “conflicts” are pervasive in road traffic and although traffic rules define a jurisdictional frame, the decision, e.g., to give way, is not uniquely determined but influenced by a list of prioritised goals of each system and the personal preferences of its user. If it is impossible to achieve all goals simultaneously, autonomous driving systems (ADSs) have to decide “who” will “sacrifice” what goal in order to decide on their manoeuvres. Matters get even more complicated when we take into account that the ADS has only partial information. It perceives the world via sensors of limited reach and precision. Moreover, measurements can be contradicting. An ADS might use V2V to retrieve more information about the world, but it inevitably has a confined insight to other traffic participants and its environment. Nevertheless, for the acceptance of ADSs, it is imperative to implement conflict resolution mechanisms that take into account the high dimensionality of decision making. These decisions have to be explained and in case of an incident, the system’s decisions have to be accountable.

In this paper we study conflict situations as dynamically occurring in road traffic and develop a formal notion of conflict between two agents. We distinguish several types of conflicts and propose a conflict resolution process where the different kinds of conflicts are resolved in an incremental fashion. This process successively increases the required cooperation and decreases the privacy of the agents, finally negotiating which goals of the two agents have to be sacrificed. We present a logical framework enabling the analysis of conflicts. This framework borrows from epistemic and modal logic in order to accommodate the bookkeeping of evidences used during a decision process. The framework in particular provides a mean to summarise consistent evidences and keep them apart from inconsistent evidences. We hence can, e.g., fuse compatible perceptions into a belief $b$ about the world and fuse another set of compatible perceptions to a belief $b^{\prime}$ and model decisions that take into account that $b$ might contradict $b^{\prime}$. Using the framework we illustrate how conflicts can be explained and algorithmically analysed as required for our conflict resolution process. Finally we report on a small case study using a prototype implementation (employing the Yices SMT solver [1]) of the conflict resolution algorithm.

Outline.

In Sect.  2 we introduce the types of conflict on a running example and develop a formal notion of conflict between two agents. We elaborate on the logical foundations for modelling and analysing conflicts and the logical framework itself in Sect.  3. We sketch our case study on conflict analysis in Sect.  4 and outline in Sect.  4.2 an algorithm for analysing conflict situations as requested by our resolution protocol and for deriving explanation of the conflict for the resolution. Before drawing the conclusions in Sect.  6, we discuss related work in Sect.  5.

2 Conflict

Already in 1969 in the paper “Violence, Peace and Peace Research” [2] J. Galtung presents his theory of the Conflict Triangle, a framework used in the study of peace and conflict. Following this theory a conflict comprises three aspects: opposing actions, incompatible goals, inconsistent beliefs (regarding the reasons of the conflict, knowledge of the conflict parties,…).

We focus on conflicts that arise dynamically between two agents in road traffic. We develop a characterisation of conflict as a situation where one agent can accomplish its goals with the help of the other, but both agents cannot accomplish all their goals simultaneously and the agents have to decide what to do based on their local beliefs. In Sect.  2.1 we formalise our notion of conflict. For two agents with complete information, we may characterise a conflict as: Agents A and B are in conflict, if

nosep Awould accomplish its set of goals $\Phi_{\_}\textit{A}$, if B will do what A requests, while

nosep Bwould accomplish its set of goals $\Phi_{\_}\textit{B}$, if A will do what B requests, and

nosep it is impossible to accomplish the set of goals $\Phi_{\_}\textit{A}\cup\Phi_{\_}\textit{B}$.

A situation where A and B both compete to consume the same resource is thus an example of a conflict situation. Since we study conflicts from the view-point of an agent’s beliefs, we also consider believed conflicts, which can be resolved by sharing information regarding the others observations, strategies or goals. To resolve a conflict we propose a sequence of steps that require an increasing level of cooperation and decreasing level of privacy – the steps require to reveal information or to constrain acting options. Our resolution process defines the following steps:

• $(C_{1})$

Shared situational awareness

• $(C_{2})$

Sharing strategies

• $(C_{3})$

Sharing goals

• $(C_{4})$

Agreeing on which goals to sacrifice and which strategy to follow

Corresponding to $(C_{1})$ to $(C_{4})$, we introduce different kinds of conflicts on a running example – a two lane highway, where one car, A, is heading towards an obstacle at its lane and at the lane to its left a fast car, B, is approaching from behind (cf. Fig.  1). An agent has a prioritised list of goals (like 1. “collision-freedom”, 2.“changing lane” and 3. “driving fast”). We assume that an agent’s goals are achievable.

An agent A has a set of actions $\textit{act}_{\_}\textit{A}$ and exists within a world. At a time the world has a certain state. The world “evolves” (changes state) as determined by the chosen actions of the agents within the world and events determined by the environment within the world. The agent perceives the world only via a set of observation predicates, that are predicates whose valuation is determined by an observation of the agent. Without an observation the agent has no (direct) evidence for the valuation of the respective observation predicate.

Example 1**.**

Let car A want to change lane. It perceives that it is on a two lane highway, the way ahead is free for the next 500 m and B is approaching. Let A perceive B’s speed via radar. That is A makes the observation car B is fast justified by the evidence radar. We annotate this briefly as radar:car B is fast. Further let A derive from lidar data that B is slow – lidar:car B is slow.

In this situation we say agent A has contradicting evidences. Certain evidences can be combined without contradiction and others not. We assume that an agent organises its evidences in maximal consistent sets (i.e., justification graphs of Sect.  3), where each represents a set of possible worlds:

Example 2**.**

There are possible worlds of A where it is on a two lane highway, the way ahead is free for the next 500 m and B is slowly approaching. Analogously A considers possible worlds where B is fast. The state of the world outside of its sensors’ reach is unconstrained.

Observing the world (for some time), an agent A assesses what it can do to achieve its goals in all possible worlds. That is, A tries to find a strategy that guarantees to achieve its goals in all its possible worlds. A strategy determines at each state the action of the agent – the agent decides for an action based on its beliefs formed in the past regarding its possible worlds. If there is one such strategy for A to accomplish its goals $\Phi_{\_}\textit{A}$, then A has a (believed) winning strategy for $\Phi_{\_}\textit{A}$. This strategy might not be winning in the ”real” world though, e.g., due to misperceptions.

Example 3**.**

Let A want to drive slowly and comfortably. A wants to avoid collisions and it assumes that also B wants to avoid collisions. Although A has contradicting evidences on the speed of B and hence believes that it is possible that “B is fast” and also that “B is slow”, it can follow the strategy to stay at its lane and wait until B has passed. This strategy is winning in all of A’s possible worlds.

Even when A has no believed winning strategy, it can have a winning strategy for a subset of possible worlds. Additional information on the state of world might resolve the conflict by eliminating possible worlds. We call such conflicts observation-resolvable conflicts.

Example 4**.**

Let A want to change lane to circumvent the obstacle. It is happy to change directly after B but only if B is fast. If B is slow, it prefers to change before B passed. Further let A have contradicting evidences on the speed of B. A considers a conflict with B possible in some world and hence has no believed winning strategy. Now it has to resolve its inconsistent beliefs. Let B tell A, it is fast, and A trust B more than its own sensors, then A might update its beliefs by dismissing all worlds where B is slow. Then “changing after B passed” becomes a believed winning strategy.

In case of inconsistent evidences, as above, A has to decide how to update its beliefs. The decision how to update its beliefs will be based on the analysis of justifications (cf. Sect.  3) of (contradicting) evidences. The lidar contradicts the radar and B reports on its speed. Facing the contradiction of evidences justified by lidar and radar A trusts the evidence justified by B.

Let the agents already have exchanged observations and A still have no believed winning strategy. A conflict might be resolved by communicating part of the other agent’s (future) strategy:

Example 5**.**

Let A want to change lane. It prefers to change directly after B, if B passes A fast. Otherwise, A wants to change in front of B. Let B so far away that B might decelerate, in which case it might slow down so heavily that A would like to change in front of B even if B currently is fast.

Let A believe “B is fast”. Now A has no believed winning strategy, as B might decelerate. According to (C2), information about parts of the agent’s strategies are now communicated. A asks B whether it plans to decelerate. Let B be cooperative and tell A that it will not decelerate. Then A can dismiss all worlds where B slows down and “changing after B passed” becomes a believed winning strategy for A.

Let the two agents have performed steps $(C_{1})$ and $(C_{2})$, i.e., they exchanged missing observations and strategy parts, and still A has no winning strategy for all possible worlds.

Example 6**.**

Let now, in contrast to Ex.  5, B not tell A whether it will decelerate. Then step (C3) is performed. So A asks B to respect A’s goals. Since A prefers B to be fast and B agrees to adopt A’s goal as its own, A can again dismiss all worlds where B slows down.

Here the conflict is resolved by communicating goals and the agreement to adopt the other’s goals. So an agent’s strategy might change in order to support the other agent. We call this kind of conflicts goal-disclosure-resolvable conflicts.

The above considered conflicts can be resolved by some kind of information exchange between the two agents, so that the sets of an agent’s possible worlds is adapted and in the end all goals $\Phi_{\_}\textit{A}$ of A and $\Phi_{\_}\textit{B}$ of B are achievable in all remaining possible worlds. The price to pay for conflict resolution is that the agents will have to reveal information. Still there are cases where simply not all goals are (believed to be) achievable. In this case A and B have to negotiate which goals $\Phi_{\_}{AB}\subseteq\Phi_{\_}\textit{A}\cup\Phi_{\_}\textit{B}$ shall be accomplished. While some goals may be compatible, other goals are conflicting. We hence consider goal subsets $\Phi_{\_}{\textit{A}\textit{B}}$ of $\Phi_{\_}\textit{A}\cup\Phi_{\_}\textit{B}$ for which a combined winning strategy for A and B exists to achieve $G_{\_}{\textit{A}\textit{B}}$. We assume that there is a weight assignment function $w$ that assigns a value to a given goal combination $2^{\Phi_{\_}\textit{A}\cup\Phi_{\_}\textit{B}}\rightarrow\mathbb{N}$ based on which decision for a certain goal combination is taken. This weighting of goals reflects the relative value of goals for the individual agents. Such a function will have to reflect, e.g., moral, ethics and jurisdiction.

Example 7**.**

Let A’s and B’s highest priority goal be collision-freedom, reflected in goals $\varphi_{\_}{\textit{A},col}$ and $\varphi_{\_}{\textit{B},col}$. Further let A want to go fast $\varphi_{\_}{\textit{A},fast}$ and change lane immediately $\varphi_{\_}{\textit{A},lc}$. Let also B want to go fast $\varphi_{\_}{\textit{B},fast}$, so that A cannot change immediately. Now in step (C4) A and B negotiate what goals shall be accomplished. In our scenario collision-freedom is valued most, and B’s goals get priority over A’s, since B is on the fast lane. Hence our resolution is to agree on a strategy accomplishing $\{\varphi_{\_}{\textit{A},col},\varphi_{\_}{\textit{B},col},\varphi_{\_}{\textit{B},fast}\}$, which is the set of goals having the highest value among all those for which a combined winning strategy exists.

Note that additional agents are captured as part of the environment here. At each step an agent can also decide to negotiate with some other agent than B in order to resolve its conflict.

2.1 Formal Notions

In the following we introduce basic notions to define a conflict. Conflicts, as introduced above, arise in a wide variety of system models, but we consider in this paper only a propositional setting.

Let $f_{\_}1:X\to Y_{\_}1$,…, $f_{\_}n:X\to Y_{\_}n$, and $f:X\to Y_{\_}1\times\ldots\times Y_{\_}n$ be functions. We will write $f=(f_{\_}1,\ldots,f_{\_}n)$ if and only if $f(x)=(f_{\_}1(x),\ldots,f_{\_}n(x))$ for all $x\in X$. Note that for any given $f$ as above the decomposition into its components $f_{\_}i$ is uniquely determined by the projections of $f$ onto the corresponding codomain.

Each agent A has a set of actions $\mathcal{A}_{\_}\textit{A}$. The sets of actions of two agents are disjoint. To formally define a (possible) world model of an agent A, let $S$ be a set of states and $\mathcal{V}$ be a set of propositional variables. $\mathcal{V}$ represents the set of belief propositions. A state $s\in S$ of a (possible) world is labelled with a subset $V\subset\mathcal{V}$ that is (assumed to be) true. $\mathcal{V}\setminus V$ is (assumed to be) false.

A (possible) world model $M$ for an agent A is a transition system over $S$ with designated initial state and current state, all states are labelled with the belief propositions that hold at that state and transitions labelled with actions $\langle\textit{act}_{\_}\textit{A},\textit{act}_{\_}\textit{B},\textit{act}_{\_}\textit{Env}\rangle$ with $\textit{act}_{\_}\textit{A}\in\mathcal{A}_{\_}\textit{A}$ an action of agent A, $\textit{act}_{\_}\textit{B}\in\mathcal{A}_{\_}\textit{B}$ an action of agent B and $\textit{act}_{\_}\textit{Env}\in\mathcal{A}_{\_}\textit{Env}$ an action of the environment.

The set of actions of an agent includes send and receive actions via which information can be exchanged, the environment guarantees to transmit a send message to the respective receiver. Formally a possible world is $M_{\_}{\textit{A}}=(S,\textit{T},\lambda,\pi,s_{\_}*,s_{\_}c)$ with

• •

$\textit{T}\subseteq S\times S$,

• •

$\lambda:\textit{T}\rightarrow\mathcal{A}_{\_}\textit{A}\times\mathcal{A}_{\_}\textit{B}\times\mathcal{A}_{\_}\textit{Env}$,

• •

$\pi:S\rightarrow 2^{\mathcal{V}}$,

• •

$s_{\_}*\in S$, $s_{\_}c\in S$ s.t.

• –

$\forall s\in S$: $(s,s_{\_}*)\not\in\textit{T}$ ($s_{\_}*$ is the initial state)

• –

$\exists s_{\_}1,\ldots,s_{\_}{n+1}\in S$:$\forall 1\leq i\leq n$ $(s_{\_}i,s_{\_}{i+1})\in\textit{T}$, $\land$ $s_{\_}1=s_{\_}*$ $\land$ $s_{\_}{n+1}=s_{\_}c$

(the current state $s_{\_}c$ is reachable from the initial state)

$\land$ $((s_{\_}i,s^{\prime})\in\textit{T}$ $\Rightarrow$ $s^{\prime}=s_{\_}{i+1})$ ( $M$ is linear between $s_{\_}*$ and $s_{\_}c$)

The part of $M$ between $s_{\_}*$ and $s_{\_}c$ represents the history of the current state. A finite run in $M$ is a sequence of states $r=s_{\_}1s_{\_}2\ldots s_{\_}{n+1}$ with $\forall 1\leq i\leq n:(s_{\_}i,s_{\_}{i+1})\in\textit{T}$.

There is one “special” world model that represents the ground truth, i.e., it reflects how the reality evolves. An agent A considers several worlds possible at a time. This is, at each state $s$ of the real world, A has a set of possible worlds $\mathcal{M}_{\_}\textit{A}(s)$. The real world changes states according to the actions of A, B and Env. The set of possible worlds $\mathcal{M}_{\_}\textit{A}(s)$ changes to $\mathcal{M}_{\_}\textit{A}(s^{\prime})$ due to the passing of time and due to belief updates triggered by e.g. observations. For the scope of this paper though, we do not consider the actual passing of time, but study the conflict analysis at a single state of the real world from the point of view of an agent. Since at each state an agent A may consider several worlds possible, it may also consider several histories possible. A strategy is hence a function $\delta_{\_}{\textit{A}}:2^{(2^{\mathcal{V}})^{*}}\rightarrow\mathcal{A}_{\_}\textit{A}$, that determines an action for A based on the set of possible histories. $\mathbb{H}\in 2^{(2^{\mathcal{V}})^{*}}$ represents a set of histories, where a history $h\in\mathbb{H}$ is given via the sequence of valuations of $\mathcal{V}$ along the path from $s_{\_}{*}$ to $s_{\_}{c}$. The set of possible histories at state $s$ is the union of histories of possible worlds $M_{\_}{\textit{A}}\in\mathcal{M}_{\_}\textit{A}(s)$, denoted as $\mathbb{H}(\mathcal{M}_{\_}\textit{A}(s))$.

Let $r=s_{\_}0s_{\_}1\ldots s_{\_}n$ be a run in $M_{\_}\textit{A}$ and $\gamma=\upsilon_{\_}1\upsilon_{\_}2\ldots\upsilon_{\_}n\in(\mathcal{A}_{\_}\textit{B}\times\mathcal{A}_{\_}\textit{Env})^{n}$ be a sequence of actions of agent B and Env along $r$. $r$ follows strategy $\delta$, i.e., $r=\textit{r}(\delta,\gamma)$, if $\lambda(s_{\_}{i-1},s_{\_}{i})=(\delta(\mathbb{H}(\mathcal{M}_{\_}\textit{A}(s_{\_}{i-1})),\upsilon_{\_}i),\forall 0\leq i\leq n$. We also write $\textit{r}(\delta,M_{\_}\textit{A})$ to denote the set of runs of $M_{\_}\textit{A}$ that follow $\delta$.

We use linear-time temporal logic (LTL) to specify goals (cf. Def. Def.  9). For a run r and a goal (or a conjunction of goals) $\varphi$, we write $\textit{r}\models\varphi$ if r satisfies $\varphi$, i.e., the valuation of propositions along the state sequence satisfies $\varphi$.111We assume that runs are infinite here. In case of finite runs, we make them infinite by repeating the last state infinitely often. We say $\delta$ is a (believed) winning strategy for $\varphi$ in $M_{\_}{\textit{A}}$, if all runs $r$ of $M_{\_}\textit{A}$ that follow $\delta$ also satisfy $\varphi$, $\forall r\in\textit{r}(M_{\_}\textit{A},\delta):r\models\varphi$. We say that $\delta$ is a (believed) winning strategy of A for $\varphi$ at the real world state $s$ if $\delta$ is a winning strategy for $\varphi$ in all possible worlds $M_{\_}\textit{A}\in\mathcal{M}_{\_}\textit{A}(s)$.

An agent A has a set of goals $\Phi$ and a weight assignment function $w_{\_}\textit{A}:2^{\Phi}\rightarrow\mathbb{N}$ that assigns values to a given goal combination. We write $\textit{r}\models\Phi$ as shorthand for $\textit{r}\models\bigwedge_{\_}{\varphi\in\Phi}\varphi$. We say $\Phi^{\prime}\subset\Phi$ is a believed achievable goal at real world $s$ if there is a strategy $\delta$, that is winning for the conjunction of all goals $\varphi\in\Phi^{\prime}$ in all possible worlds $M_{\_}\textit{A}\in\mathcal{M}_{\_}\textit{A}(s)$. We say $\Phi^{\prime}\subset\Phi$ is a believed maximal goal at real world state $s$ if its is a believed achievable goal and for all believed achievable goals $\Phi^{\prime\prime}\subset\Phi$ it holds that $w(\Phi^{\prime})\geq w(\Phi^{\prime\prime})$. The empty subgoal is defined to be true ($\top$). For each world possible $M_{\_}\textit{A}\in\mathcal{M}_{\_}\textit{A}(s)$ agent A also has

beliefs on the goals of B, $\Phi_{\_}\textit{B}(M_{\_}\textit{A})$, and 2. 2.

beliefs on the importance of subgoals of $\Phi_{\_}\textit{B}(M_{\_}\textit{A})$ to B, $w_{\_}\textit{B}(M_{\_}\textit{A})$, and 3. 3.

a set $\mathbb{J}(M_{\_}\textit{A})$ of justifications for $M_{\_}\textit{A}$, $\Phi_{\_}\textit{B}(M_{\_}\textit{A})$ and $w_{\_}\textit{B}(M_{\_}\textit{A})$.

So at state $s$ of the real world an agent A has belief $\mathcal{B}(\textit{A},s)=\bigcup_{\_}{M_{\_}\textit{A}\in\mathcal{M}_{\_}\textit{A}(s)}(M_{\_}\textit{A},\Phi_{\_}\textit{B}(M_{\_}\textit{A}),w_{\_}\textit{B}(M_{\_}\textit{A}),\mathbb{J}(M_{\_}\textit{A}))$. The justifications support decision making by keeping track of (source or more generally meta) information. They hence can influence decisions on how to update an agent’s knowledge, how to negotiate and what resolutions are acceptable.

Our notion of conflict captures the following concept: Let $\Phi^{\textsf{max}}$ be the set of maximal goals that A beliefs it can achieve with the help of B. But since B might choose a strategy to accomplish some of its maximal goals, A believes that it is in a conflict with B, if it cannot find one winning strategy that fits all possible strategy choices of B.

Definition 1** (Believed Possible Conflict).**

Let $\Phi^{\textsf{max}}_{\_}\textit{A}$ be the set of maximal subgoals of A at state $s$ for which a believed winning strategy $(\delta_{\_}\textit{A},\delta^{\prime}_{\_}\textit{B}):(2^{\mathcal{V}_{\_}\textit{A}})^{*}\to\mathcal{A}_{\_}\textit{A}\times\mathcal{A}_{\_}\textit{B}$ in $\mathcal{M}_{\_}\textit{A}$ exists.

Agent A believes at state $s$ it is in a possible conflict with B, if for each of its winning strategies $(\delta_{\_}\textit{A},\delta^{\prime}_{\_}\textit{B}):(2^{\mathcal{V}_{\_}\textit{A}})^{*}\to\mathcal{A}_{\_}\textit{A}\times\mathcal{A}_{\_}\textit{B}$ for a maximal subgoal $\Phi_{\_}\textit{A}\in\Phi^{\textsf{max}}_{\_}\textit{A}$,

• •

there is a strategy $(\delta^{\prime}_{\_}\textit{A},\delta_{\_}\textit{B}):(2^{\mathcal{V}_{\_}\textit{A}})^{*}\to\mathcal{A}_{\_}\textit{A}\times\mathcal{A}_{\_}\textit{B}$ and a possible world $M\in\mathcal{M}_{\_}\textit{A}$ such that $(\delta^{\prime}_{\_}\textit{A},\delta_{\_}\textit{B})$ is a winning strategy in $M$ for $\Phi_{\_}\textit{B}$, a believed maximal subgoal of the believed goals of B in $M$.

• •

but $(\delta_{\_}\textit{A},\delta_{\_}\textit{B})$ is not a winning strategy for $\Phi_{\_}\textit{A}\cup\Phi_{\_}\textit{B}$ in $M_{\_}\textit{A}$.

The above notion of conflict captures that A analyses the situation within its possible worlds $\mathcal{M}_{\_}\textit{A}(s)$. It assumes that B will follow some winning strategy to accomplish its own goals, while Env is assumed to behave fully adversarial. $A$ believes that $B$ beliefs that one of A’s possible worlds represents the reality. It is an interesting future extension to also allow A having more complicated beliefs about the beliefs of B, as already well supported by the logical framework introduced in Sect.  3. For instance we can capture situations like $A$ considers it possible that there is an obstacle on the road, while it believes that $B$ believes there is no obstacle. This extension does change the base line of our contribution but makes the following presentation more complex. So we refrain from considering beliefs about beliefs for the sake of comprehensibility.

For an example of the conflict notion, consider a situation where A drives on a highway side by side of B and A just wants to stay collision-free, A does not believe to be in a conflict situation when it believes that B also prioritizes collision-freedom, since B will not suddenly choose to crash into A which would violate its own goal. But in case B has no strategy to accomplish collision-freedom (assume a broken car in front of B) within $M_{\_}\textit{A}$, then A assumes that B behaves arbitrarily (achieving its remaining goal $\top$) and A believes to be in conflict with B.

2.2 Applying the Formal Notion

In this subsection we consider the formal notions introduced in the previous subsection and illustrate them – focusing on the examples given at the start of this section.

Propositional Characterisation of the World

For the sake of a small example, let us consider the following propositional characterisation of a world: For each agent $X\in\{\textit{A},\textit{B}\}$ there is a pair of variables $(l_{\_}{X},p_{\_}X)$ storing its position in the road. Further each agent drives a certain speed $s_{\_}X$ abstracted to three different levels, $s_{\_}X\in\{0,1,2\}$ encoding slow, medium and fast speed levels. We consider only time bounded properties. The evolution along the observed time window is captured via copies of $(l_{\_}{X},p_{\_}X,s_{\_}X)$, $(l_{\_}{X,t},p_{\_}{X,t},s_{\_}{X,t})$ where $0\leq t\leq\textit{max\_obs\_time}$ encodes the observed time points. Each agent $X$ can change lane, encoded by increasing or decreasing $l_{\_}X$, and choose between three different speeds, that is, (i) decelerate inducing a change from fast to medium, or, medium to slow, respectively, or (ii) accelerates from slow to medium, or, from medium to fast, respectively.

A Real World Model

In this setting each state of the real world model is labelled with propositions $\{l_{\_}{X},p_{\_}{X},s_{\_}{X}\mid X\in\{\textit{A},\textit{B},o\}\}$ and there are transitions from a state $s$ to a state $s^{\prime}$ labelled $\lambda$(s,s’)=($lc_{\_}1,lc_{\_}2,lc_{\_}3,$ $sc_{\_}1,sc_{\_}2,sc_{\_}3$), where $lc_{\_}i\in\{\texttt{lane\_change},\neg\texttt{lane\_change}\}$ and $sc_{\_}i\in\{a,d,k\}$. $lc_{\_}i$ encodes whether agent X${}_{\_}i$ chooses to perform a lane change and sc${}_{\_}i$ encodes how X${}_{\_}i$ chooses to change its speed, i.e., to accelerate, decelerate or to keep its speed. The target state is labelled according to effect of the chosen action.

The initial state encodes the start situation (of the tour) and the subgraph from the initial state to the current state captures the observed past. A world model has a branching structure from the current state towards the future into the possible different options of lane changing and choices of speed change. Such a world model describes the past, the current state of the world and possible future evolutions. For each point in time $t$ there is hence such a world model. See Fig.  2 for a sketch of an example of a world model at a time $t=4$.

Possible Worlds

Additional to labelling of states and transitions, the real world is also labelled with beliefs of the agents at that time. The gist is

1. R

the real world model captures the past, presence and the possible futures at a time $t$. 2. B

At time $t$ an agent within world model $M$ considers a set of worlds possible. This belief is justified by e.g. evidences from its sensors.

An example is sketched in Fig.  3, where only A’s beliefs are sketched. Note that the state labelling, i.e. the set of true propositions, is not specified in Fig.  3 in order to declutter the figure. Some state labelling is given in Fig.  4.

Let for Fig.  3 be the initial states of the real and the possible worlds be identically labelled, i.e., the agent believes in the ”real” past.

Let us now consider Ex.  1. Agent A has evidence for B being fast and it also has evidence for B being slow. Fig.  4 illustrates that agent A considers the two (sets of) worlds possible that differ in the valuation of the respective state propositions. Agent A believes that a world is possible where B is fast – this is justified by its radar data–, and A considers a world possible where B is slow – justified by its lidar.

We assume that an agent considers any world $M$ possible that can be justified by some non-empty set of consistent evidences. So a possible world $M$ satisfies e.g. a set of constraints that is derived from the agent’s observations, i.e., the sensory evidences, and it also has to be compatible to the agent’s laws/rules about the world, e.g., physical laws.

The evidences provided by radar and lidar in Ex.  1 imply constraints $s_{\_}\textit{A}=fast$ and $s_{\_}\textit{B}=slow$. These constraints are contradictory and hence there is no possible world that satisfies both constraints. So there cannot be an arrow in Fig.  4 from the real world to a possible world that is labelled with a justification set containing both justifications, $\mathbb{J}$ = $\{$radar, lidar$\}$. Nevertheless, the radar and lidar evidences justify that agent A believes in alternative worlds (e.g., B is fast, so it is possible that (a) B was driving at medium speed and accelerated or (b) B was fast and kept its speed.)

Strategy and Possible Worlds

Let us formalise Ex.  3. A considers worlds possible where it has the evidence radar:car B is fast and hence considers worlds possible where B is fast, and also worlds where B is not fast, due to its evidence lidar:car B is slow. We already sketched the possible worlds of A above. In order to specify the goals of A and the goals A believes B has, we use the usual LTL operators222“${\mathord{\mathrm{missing}}{F}}$” denotes the finally modal operator, “${\mathord{\mathrm{missing}}{G}}$” denotes globally, “${\mathord{\mathrm{missing}}{U}}$” denotes until and in addition we use ${\mathord{\mathrm{missing}}{F}}_{\_}{\leq t}\varphi$ to express that within the next $t$ steps $\varphi$ has to be true and likewise ${\mathord{\mathrm{missing}}{G}}_{\_}{\leq t}\varphi$ to specify that at all times up to $t$ $\varphi$ has to hold.

A wants to drive slowly and comfortably, $\varphi_{\_}{cf}={\mathord{\mathrm{missing}}{G}}_{\_}{\leq 3}(s_{\_}\textit{A}=medium\lor s_{\_}\textit{A}=slow)$ and avoid collisions $\varphi_{\_}{cl}={\mathord{\mathrm{missing}}{G}}_{\_}{\leq 10}(p_{\_}{\textit{A}}\not=p_{\_}{\textit{B}}\land p_{\_}{\textit{A}}\not=p_{\_}o)$. A also assumes that B wants to avoid collisions, $\varphi_{\_}{\textit{B},cl}={\mathord{\mathrm{missing}}{G}}_{\_}{\leq 10}(p_{\_}{\textit{B}}\not=p_{\_}{\textit{A}}\land p_{\_}{\textit{B}}\not=p_{\_}o)$. The weight assignment to subsets of goals for A is $w_{\_}\textit{A}(\{\varphi_{\_}{cl},\varphi_{\_}{cf}\})=2$, $w_{\_}\textit{A}(\{\varphi_{\_}{cl}\})=1$ and $w_{\_}\textit{A}(\Phi)=0$ for all all other subsets $\Phi$. This expresses that collision-freedom is indispensable. Further A believes collision-freedom is also indispensable for B. Additionally, A derives from $\Phi_{\_}\textit{B}$ a constraint that expresses that B will not jeopardize collision-freedom and hence it will not drive irrationally into A. This constraint further restricts the set of worlds that A considers possible (cf. Fig.  5).

In this situation, A decides on its next move. It is not aware of the state of real world and decides only based on its current beliefs regarding the possible worlds and associated goals of B and goal weights. A determines that staying on its current lane and not changing its speed now is a good move since it can stop and wait in any case, i.e., this move is the prefix of a winning strategy in M1 and all other possible worlds, in which B is slow, and also in M2 and all other possible worlds that satisfy that B is fast (cf. Fig.  4).

Conflicts

In Ex.  4 A has the goals

• avoid collisions $\varphi_{\_}{cl}={\mathord{\mathrm{missing}}{G}}_{\_}{\leq 10}(p_{\_}{\textit{A}}\not=p_{\_}{\textit{B}}$ $\land$ $p_{\_}{\textit{A}}\not=p_{\_}o)$ and

• change lane $\varphi_{\_}{lc}={\mathord{\mathrm{missing}}{F}}_{\_}{\leq 5}$ change_lane and

• change lane before B has passed, if B is slow, $\varphi_{\_}{flc}=\neg({\mathord{\mathrm{missing}}{G}}_{\_}{\leq 3}s_{\_}\textit{B}=fast)$ $\Rightarrow$ $p_{\_}\textit{A}\geq p_{\_}\textit{B}$ ${\mathord{\mathrm{missing}}{U}}$ change_lane $\land$ ${\mathord{\mathrm{missing}}{F}}_{\_}{\leq 3}\textit{change\_lane}$ and

• do not change before B has passed, if B is fast, $\varphi_{\_}{slc}=({\mathord{\mathrm{missing}}{G}}_{\_}{\leq 3}s_{\_}\textit{B}=fast)$ $\Rightarrow$ ${\mathord{\mathrm{missing}}{G}}_{\_}{\leq 3}\neg\textit{change\_lane}$.

We assume here that A has only short term goals and global goals are determined at a higher level.333Note that also collision-freedom might be sacrificed in so-called dilemma situations. A also assumes that B wants to avoid collisions. The weight assignment to subsets of goals for A is specified as follows $6=w_{\_}\textit{A}(\{\varphi_{\_}{cl},\varphi_{\_}{lc},\varphi_{\_}{flc},\varphi_{\_}{slc}\})$ $>$ $w_{\_}\textit{A}(\{\varphi_{\_}{cl},\varphi_{\_}{lc},\varphi_{\_}{slc}\})$ $=$ $w_{\_}\textit{A}(\{\varphi_{\_}{cl},\varphi_{\_}{lc},\varphi_{\_}{flc}\})$ $>$ $w_{\_}\textit{A}(\{\varphi_{\_}{cl},\varphi_{\_}{lc}\})$ $>$ $w_{\_}\textit{A}(\{\varphi_{\_}{cl},\varphi_{\_}{flc}\})$ $=$ $w_{\_}\textit{A}(\{\varphi_{\_}{cl},\varphi_{\_}{slc}\})$444Note, that $\varphi_{\_}{flc}$ does not imply $\varphi_{\_}{lc}$. $>$ $w_{\_}\textit{A}(\{\varphi_{\_}{cl},\})=1$, $w_{\_}\textit{A}(\Phi)=0$ for all all other subsets.

Obviously A has a winning strategy $\delta_{\_}{\textit{A}(\textit{B})}:2^{(2^{\mathcal{V}})^{*}}\rightarrow\mathcal{A}_{\_}\textit{A}\times\mathcal{A}_{\_}\textit{B}$, i.e., if it could determine also B’s future moves. In this case it can achieve $\{\varphi_{\_}{cl},\varphi_{\_}{lc},\varphi_{\_}{flc},\varphi_{\_}{slc}\}$. If A assumes that B follows a strategy achieving B’s own goals under the assumption that A will cooperate (i.e. B can rule out that A changes lane, forcing B to decelerate), then B can e.g. make up a winning strategy $\delta_{\_}{(\textit{A})\textit{B}}:2^{(2^{\mathcal{V}})^{*}}\rightarrow\mathcal{A}_{\_}\textit{A}\times\mathcal{A}_{\_}\textit{B}$, where A stays at lane 1, B at lane 2 and B chooses its speed arbitrarily without endangering collision-freedom. A does not have a winning strategy for all these strategies of B, since A cannot follow the same strategy if (i) B is fast in its next three steps and if (ii) B is not fast in at least one of the next three steps.

If B tells A how fast it will go in its next three steps, the additional information provided by B, makes A dismiss all possible worlds that do not satisfy the evidence on B’s future behaviour. A can determine an appropriate strategy for all (remaining) possible worlds and the conflict situation is hence resolved.

3 Epistemic Logic, Justifications and Justification Graph

Conflict analysis demands to know who believes to be in conflict with whom and what pieces of information made him belief that he is in conflict. To this end we introduce the logic of justification graphs that allows to keep track of external information and extends purely propositional formulae by so called belief atoms (cf. p. 3.1), which are used to label the sources of information. In Sect.  2 we already used such formulae, e.g., ”radar:car B is fast”. Our logic provides several atomic accessibility relations representing justified beliefs of various sources, as required for our examples of Sect.  2. It provides justification graphs as a mean to identify belief entities which compose different justifications to consistent information even when the information base contains contradicting information of different sources, as required for analysing conflict situations.

First, this section provides a short overview on epistemic modal logics and multi-modal extensions thereof. Such logics use modal operators to expressing knowledge and belief stemming from different sources. Often we will refer to this knowledge and belief as information, especially when focusing on the sources or of the information. Thereupon the basic principles of justifications logics are shortly reviewed. Justification logics are widely seen as interesting variants to epistemic logics as they allow to trace back intra-logical and external justifications of derived information. In the following discussion it turns out that tracing back external justifications follows the same principles as the distribution of information over different sources.

Consequently, the concept of information source and external justification are then unified in our variant of an epistemic modal logic. This logic of justification graphs extends the modal logic by a justification graph. The nodes of a justification graph are called belief entities and represent groups of consistent information. The leaf nodes of a justification graphs are called belief atoms, which are information source and external justifications at the same time, as they are the least constituents of external information. We provide a complete axiomatisation with respect to the semantics of the logic of justification graphs.

3.1 Justification Graphs

Modal Logic and Epistemic Logic.

Modal logic extends the classical logic by modal operators expressing necessity and possibility. The formula ${\mathord{\Box}}\phi$ is read as “$\phi$ is necessary” and ${\mathord{\Diamond}}\phi$ is read as “$\phi$ is possible”. The notions of possibility and necessity are dual to each other, ${\mathord{\Diamond}}\phi$ can be defined as $\lnot{\mathord{\Box}}\lnot\phi$. The weakest modal logic $\mathrm{K}$ extends propositional logic by the axiom $\mathbf{K}_{\_}{\mathord{\Box}}$ and the necessitation rule $\mathbf{Nec}_{\_}{\mathord{\Box}}$ as follows

$\displaystyle\vdash{\mathord{\Box}}(\phi\to\psi)\to({\mathord{\Box}}\phi\to{\mathord{\Box}}\psi)\text{,}$

($\mathbf{K}_{\_}{\mathord{\Box}}$)

$\displaystyle\text{from }\vdash\phi\text{ conclude }\vdash{\mathord{\Box}}\phi\text{.}$

($\mathbf{Nec}_{\_}{\mathord{\Box}}$)

The axiom $\mathbf{K}_{\_}{\mathord{\Box}}$ ensures that whenever $\phi\to\psi$ and $\phi$ necessarily hold, then also $\psi$ necessarily has to hold. The necessitation rule $\mathbf{Nec}_{\_}{\mathord{\Box}}$ allows to infer the necessity of $\phi$ from any proof of $\phi$ and, hence, pushes any derivable logical truth into the range of the modal operator ${\mathord{\Box}}$. This principle is also known as logical awareness. Various modalities like belief or knowledge can be described by adding additional axioms encoding the characteristic properties of the respective modal operator. The following two axioms are useful to model knowledge and belief:

$\displaystyle\vdash{\mathord{\Box}}\phi\to\phi\text{,}$

($\mathbf{T}_{\_}{\mathord{\Box}}$)

$\displaystyle\vdash{\mathord{\Box}}\phi\to{\mathord{\Diamond}}\phi\text{.}$

($\mathbf{D}_{\_}{\mathord{\Box}}$)

The axiom $\mathbf{T}_{\_}{\mathord{\Box}}$ and $\mathbf{D}_{\_}{\mathord{\Box}}$ relate necessity with the factual world. While the truth axiom $\mathbf{T}_{\_}{\mathord{\Box}}$ characterises knowledge as it postulates that everything which is necessary is also factual, $\mathbf{D}_{\_}{\mathord{\Box}}$ characterises belief as it postulates the weaker property that everything which is necessary is also possible. Under both axioms $\vdash{\mathord{\Box}}\bot\to\bot$ holds, i.e. a necessary contradiction yields also a factual contradiction.

Multi-modal logics are easily obtained by adding several modal operators with possibly different properties and can be used to express the information of more than one agent. E.g., the formula $e_{\_}i{:}\phi$ expresses that the piece of information $\phi$ belongs to the modality $e_{\_}i$. Modal operators can also be used to represent modalities referring to time. E.g., in the formula ${\mathord{\mathrm{missing}}{X}}\phi$ the temporal modality ${\mathord{\mathrm{missing}}{X}}$ expresses that $\phi$ will hold in the next time step. An important representative of a temporal extension is linear temporal logic ($\mathrm{LTL}$).

In multi-agent logics the notions of common information and distributed information play an important role. While common knowledge captures the information which is known to every agent $e_{\_}i$, we are mainly interested in information that is distributed within a group of agents $E=\{e_{\_}1,\dots,e_{\_}n\}$. The distributed information within a group $E$ contains any piece of information that at least one of the agent $e_{\_}1$, …, $e_{\_}n$ has. Consequently, we introduce a set-like notion for groups, where an agent $e$ is identified with the singleton group $\{e\}$ and the expression $\{e_{\_}1,\dots,e_{\_}n\}{:}\phi$ is used to denote that $\phi$ is distributed information within the group $E$. The distribution of information is axiomatised by

[TABLE]

Note that groups may not be empty. The modal logic for distributed information contains for every group $E$ at least the axiom $\mathbf{K}_{\_}E$, the necessitation rule $\mathbf{Nec}_{\_}E$, and the axiom $\mathbf{Dist}_{\_}{E,F}$ for any group $F$ with $E\subseteq F$.

Justification Logics.

Justification logics [3] are variants of epistemic modal logics where the modal operators of knowledge and belief are unfolded into justification terms. Hence, justification logics allow a complete realisation of Plato’s characterisation of knowledge as justified true belief. A typical formula of justification logic has the form $s{:}\phi$, where $s$ is a justification term built from justification constants, and it is read as “$\phi$ is justified by $s$”. The basic justification logic $J_{\_}0$ results from extending propositional logic by the application axiom and the sum axioms

$\displaystyle\vdash s{:}(\phi\to\psi)\to(t{:}\phi\to[s\cdot t]{:}\psi)\text{,}$

($\mathbf{Appl}$)

$\displaystyle\vdash s{:}\phi\to[s+t]{:}\phi\text{,}\quad\vdash s{:}\phi\to[t+s]{:}\phi\text{,}$

($\mathbf{Sum}$)

where $s$, $t$, $[s\cdot t]$, $[s+t]$, and $[t+s]$ are justification terms which are assembled from justification constants using the operators $+$ and $\cdot$ according to the axioms. Justification logics tie the epistemic tradition together with proof theory. Justification terms are reasonable abstractions for constructions of proofs. If $s$ is a proof of $\phi\to\psi$ and $t$ is a proof of $\phi$ then the application axiom postulates that there is a common proof, namely $s\cdot t$, for $\psi$. Moreover, if we have a proof $s$ for $\phi$ and some proof $t$ then the concatenations of both proofs, $s+t$ and $t+s$, are still proofs for $\phi$. In our framework we were not able to derive any meaningful example using the sum axiom of justification logic. Therefore this axiom is omitted in the following discussion.

Discussion.

All instances of classical logical tautologies, like $A\lor\lnot A$ and $s{:}A\lor\lnot s{:}A$, are provable in justification logics. But in contrast to modal logics, justification logics do not have a necessitation rule. The lack of the necessitation rule allows justification logics to break the principle of logical awareness, as $s{:}(A\lor\lnot A)$ is not necessarily provable for an arbitrary justification term $s$. Certainly, restricting the principle of logical awareness is attractive to provide a realistic model of restricted logical resources. Since we are mainly interested in revealing and resolving conflicts, the principle of logical awareness is indispensable in our approach.

Nevertheless, justification logic can simulate unrestricted logical awareness by adding proper axiom internalisation rules $\vdash e{:}\phi$ for all axioms $\phi$ and justification constants $e$. In such systems a weak variant of the necessitation rule of modal logic holds: for any derivation $\vdash\phi$ there exists a justification term $t$ such that $\vdash t{:}\phi$ holds. Since $\phi$ was derived using axioms and rules only, also the justification term $t$ is exclusively built from justification constants dedicated to the involved axioms. Beyond that, $t$ is hardly informative as it does not help to reveal external causes of a conflict. Hence, we omit the axiom internalisation rule and add the modal axiom $\mathbf{K}_{\_}t$ and the modal necessitation rule $\mathbf{Nec}_{\_}t$ for any justification term $t$ to obtain a justification logic where each justification term is closed under unrestricted logical awareness.

An important consequence of the proposed system is that $\cdot$ becomes virtually idempotent and commutative.555For any instance $\vdash s{:}(\phi\to\psi)\to(s{:}\phi\to[s\cdot s]{:}\psi)$ of $\mathbf{Appl}$ there is an instance $\vdash s{:}(\phi\to\psi)\to(s{:}\phi\to s{:}\psi)$ of $\mathbf{K}_{\_}s$ in the proposed system. Moreover, it is an easy exercise to show that any instance of $\vdash s{:}(\phi\to\psi)\to(t{:}\phi\to[t\cdot s]{:}\psi)$ is derivable in the proposed system.

These insights allows us to argue merely about justification groups instead of justification terms. It turns out that a proper reformulation of $\mathbf{Appl}$ with regard to justification groups is equivalent to $\mathbf{Dist}_{\_}{E,F}$, finally yielding the same axiomatisation for distributed information and compound justifications.

Belief Atoms, Belief Groups, and Belief Entities.

So far, we argued that assembling distributed information and compound justifications follow the same principle. In the following we even provide a unified concept for the building blocks of both notions. A belief atom $e$ is the least constituent of external information in our logic. To each $e$ we assign the modal operator $e{:}$. Hence, for any formula $\phi$ also $e{:}\phi$ is a formula saying “$e$ has information $\phi$”. Belief atoms play different roles in our setting. A belief atom may represent a sensor collecting information about the state of the world, or it may represent certain operational rules as well as a certain goal of the system. The characteristic property of a belief atom is that the information of a belief atom has to be accepted or rejected as a whole. Due to its external and indivisible nature, $e$ is the only source of evidence for its information. The only justification for information of $e$ is $e$ itself. Consequently, $e{:}\phi$ can also be read as “$e$ is the justification for $\phi$”. This is what belief atoms and justifications have in common: either we trust a justification or not.

The information of a system is distributed among its belief atoms. The modal logic for distributed information allows us to consider the information which is distributed over a belief group. While belief groups can be built arbitrarily from belief atoms, we also introduce the concept of belief entities. A belief entity is either a belief atom, or a distinguished group of belief entities. Belief entities are dynamically distinguished by a justification graph. In contrast to belief groups, belief entities and belief atoms are not allowed to have inconsistent information. Hence a justification graph allows us to restrict the awareness of extra-logical evidences – so we can distinctively integrate logical resources that have to be consistent.

Justification Graphs.

Let $\mathcal{V}$ be a set of propositional variables and let $\mathcal{E}$ be the set of belief entities. The designated subset $\mathcal{E}_{A}$ of $\mathcal{E}$ denotes the set of belief atoms.

Definition 2** (Language of Justification Graphs).**

A formula $\phi$ is in the language of justification graphs if and only if $\phi$ is built according to the following BNF, where $A\in\mathcal{V}$ and $\emptyset\neq E\subseteq\mathcal{E}$:

[TABLE]

Using the descending sequence of operator precedences (${:}$, $\lnot$, $\lor$, $\land$, $\to$, $\leftrightarrow$), we can define the well-known logical connectives $\lnot$, $\lor$, $\land$ and $\leftrightarrow$ from $\to$ and $\bot$. Often, we omit brackets if the formula is still uniquely readable. We define $\to$ to be right associative. For singleton sets $\{e\}\subseteq\mathcal{E}$ we also write $e{:}\phi$ instead of $\{e\}{:}\phi$. The language allows the usage of temporal operators for next time (${\mathord{\mathrm{missing}}{X}}$), previous time (${\mathord{\mathrm{missing}}{P}}$), until (${\mathord{\mathrm{missing}}{U}}$), and since (${\mathord{\mathrm{missing}}{S}}$). Operators like always in the future (${\mathord{\mathrm{missing}}{G}}$) or always in the past (${\mathord{\mathrm{missing}}{H}}$) can be defined from the given ones.

Definition 3** (Justification Graph).**

A justification graph is a directed acyclic graph $G$ whose nodes are belief entities of $\mathcal{E}$. An edge $e\mapsto_{\_}Gf$ denotes that the belief entity $e$ has the component $f$. The set of all direct components of an entity $e$ is defined as $G(e):=\{f\mid e\mapsto_{\_}Gf\}$.

The leaf nodes of a justification graph are populated by belief atoms, i.e. for any belief entity $e$ it holds $e\in\mathcal{E}_{A}$ if and only if $G(e)=\emptyset$.

Definition 4** (Axioms of a Justification Graph).**

Let $G$ be a justification graph. The logic of a justification graph has the following axioms and rules.

1. (i)

As an extension of propositional logic the rule of modus ponens $\mathbf{MP}$ has to hold: from $\vdash\phi$ and $\vdash\phi\to\psi$ conclude $\vdash\psi$. Any substitution instance of a propositional tautology $\phi$ is an axiom. 2. (ii)

Belief groups are closed under logical consequence and follow the principle of logical awareness. Information is freely distributed along the subgroup-relation. For any belief group $E$ the axiom $\mathbf{K}_{\_}E$ and the necessitation rule $\mathbf{Nec}_{\_}E$ hold. For groups $E$ and $F$ with $E\subseteq F$ the axiom $\mathbf{Dist}_{\_}{E,F}$ holds. 3. (iii)

Belief entities are not allowed to have inconsistent information. Non-atomic belief entities inherit all information of their components. For any belief entity $e$ the axiom $\mathbf{D}_{\_}e$ holds. If $E$ is a subgroup of the components of $e$, then the axiom $\mathbf{Dist}_{\_}{E,e}$ holds. 4. (iv)

In order to express temporal relation the logic for the justification graph includes the axioms of Past-LTL (LTL with past operator). A comprehensive list of axioms can be found in **[4]**. 5. (v)

Information of a belief entity $e\in\mathcal{E}$ and time are related. The axiom $(\mathbf{PR}_{\_}E):\quad\vdash e{:}{\mathord{\mathrm{missing}}{P}}\phi\leftrightarrow{\mathord{\mathrm{missing}}{P}}e{:}\phi$ ensures that every belief entity $e$ correctly remembers its prior beliefs and establishes a principle which is also known as perfect recall (e.g., see **[5]**).

Definition 5** (Proof).**

Let $G$ be a justification graph. A proof (derivation) of $\phi$ in $G$ is a sequence of formulae $\phi_{\_}1,\dots,\phi_{\_}n$ with $\phi_{\_}n=\phi$ such that each $\phi_{\_}i$ is either an axiom of the justification graph or $\phi_{\_}i$ is obtained by applying a rule to previous members $\phi_{\_}{j_{\_}1},\dots,\phi_{\_}{j_{\_}k}$ with $j_{\_}1,\dots,j_{\_}k<i$. We will write $\vdash_{\_}G\phi$ if and only if such a sequence exists.

Definition 6** (Proof from a set of formulae).**

Let $G$ be a justification graph and $\Sigma$ be a set of formulae. The relation $\Sigma\vdash_{\_}G\phi$ holds if and only if $\vdash_{\_}G(\sigma_{\_}1\land\dots\land\sigma_{\_}k)\to\phi$ for some finite subset $\{\sigma_{\_}1,\dots,\sigma_{\_}k\}\subseteq\Sigma$ with $k\geq 0$.

Definition 7** (Consistency with respect to a justification graph).**

Let $G$ be a justification graph.

1. (i)

A set $\Sigma$ of formulae is $G$-inconsistent if and only if $\Sigma\vdash_{\_}G\bot$. Otherwise, $\Sigma$ is $G$-consistent. A formula $\phi$ is $G$-inconsistent if and only if $\{\phi\}$ is $G$-inconsistent. Otherwise, $\phi$ is $G$-consistent. 2. (ii)

A set $\Sigma$ of formulae is maximally $G$-consistent if and only if $\Sigma$ is $G$-consistent and for all $\phi\not\in\Sigma$ the set $\Sigma\cup\{\phi\}$ is $G$-inconsistent.

Semantics.

Let $S$ be the state space, that is the set of all possible states of the world. An interpretation $\pi$ over $S$ is a mapping that maps each state $s$ to a truth assignment over $s$, i.e. $\pi(s)\subseteq\mathcal{V}$ is the subset of all propositional variables which are true in the state $s$. A run over $S$ is a function $r$ from the natural numbers (the time domain) to $S$. The set of all runs is denoted by $\mathcal{R}$.

Definition 8**.**

Let $G$ be a justification graph. A Kripke structure $M$ for $G$ is a tuple $M=(S,\mathcal{R},\pi,({\mapsto_{\_}e})_{\_}{e\in\mathcal{E}})$ where

1. (i)

$S$* is a state space,* 2. (ii)

$\mathcal{R}$* is the set of all runs over $S$,* 3. (iii)

$\pi$* is an interpretation over $S$,* 4. (iv)

each $\mapsto_{\_}e$ in $(\mapsto_{\_}e)_{\_}{e\in\mathcal{E}}$ is an individual accessibility relation $\mapsto_{\_}e\subseteq S\times S$ for a belief entity $e$ in $\mathcal{E}$.

Definition 9** (Model for a Justification Graph).**

Let $M=(S,\mathcal{R},\pi,({\mapsto_{\_}e})_{\_}{e\in\mathcal{E}})$ be a Kripke structure for the justification graph $G$, where

1. (i)

$\mapsto_{\_}e$* is a serial relation for any belief entity $e\in\mathcal{E}$,* 2. (ii)

${\mapsto_{\_}{E}}$* is defined as ${\mapsto_{\_}{E}}=\bigcap_{\_}{e\in E}{\mapsto_{\_}e}$ for any belief group $E\subseteq\mathcal{E}$,* 3. (iii)

${\mapsto_{\_}e}\subseteq{\mapsto_{\_}E}$* holds for all non-atomic belief entities $e\in\mathcal{E}\setminus\mathcal{E}_{A}$ and any subgroup $E\subseteq G(e)$.*

We recursively define the model relation $(M,r(t))\models_{\_}G\phi$ as follows:

[TABLE]

When $(M,r(t))\models_{\_}G\phi$ holds, we call $(M,r(t))$ a pointed model of $\phi$ for $G$. If $(M,r(0))$ is a pointed model of $\phi$ for $G$, then we write $(M,r)\models_{\_}G\phi$ and say that the run $r$ satisfies $\phi$. Finally, we say that $\phi$ is satisfiable for $G$, denoted by $\models_{\_}G\phi$ if and only if there exists a model $M$ and a run $r$ such that $(M,r)\models_{\_}G\phi$ holds.

Proposition 1** (Soundness and Completeness).**

The logic of a justification graph $G$ is a sound and complete axiomatisation with respect to the model relation $\models_{\_}G$. That is, a formula $\phi$ is $G$-consistent if and only if $\phi$ is satisfiable for $G$.

While the soundness proof is straightforward, a self-contained completeness proof involve lengthy sequences of various model constructions and is far beyond the page limit. However, it is well-known, (e.g., [6]), that $\mathrm{K}^{D}_{\_}n$, the $n$-agent extension of $\mathrm{K}$ with distributive information is a sound and complete axiomatisation with respect to the class of Kripke structures having $n$ arbitrary accessibility relations, where the additional accessibility relations for groups are given as the intersection of the participating agents, analogously to Def. 9.(ii). Also the additional extension $\mathrm{KD}^{D}_{\_}n$ with $\mathbf{D}_{\_}E$ for any belief group $E$ is sound and complete with respect to Kripke structures having serial accessibility relations, analogously to Def. 9.(i). The axioms of justification graph are between these two systems. Def. 9.(iii) explicitly allows belief entities to have more information than its components. Various completeness proofs for combining LTL and epistemic logics are given e.g., in [5].

Extracting Justifications.

Let $\Sigma=\{\sigma_{\_}1,\dots,\sigma_{\_}n\}$ be a finite set of formulae logically describing the situation which is object of our investigation. Each formula $\sigma_{\_}i\in\Sigma$ encodes information of belief atoms ($\sigma_{\_}i\equiv e_{\_}i{:}\phi_{\_}i$ with $e_{\_}i\in\mathcal{E}_{A}$), facts ($\sigma_{\_}i\equiv\phi_{\_}i$ where $\phi_{\_}i$ does not contain any epistemic modal operator), or is an arbitrary Boolean combinations thereof. Further, let $G$ be a justification graph such that $\Sigma$ is $G$-consistent and $e$ be a non-atomic belief entity of $G$. For any formula $\phi$ we may now ask whether $\phi$ is part of the information of $e$. If there is a proof $\Sigma\vdash_{\_}Ge{:}\phi$, then $\phi$ is included in $e$’s information. To extract a justification for $e{:}\phi$ we use that $\Sigma\cup\{\lnot e{:}\phi\}$ is $G$-inconsistent and accordingly unsatisfiable for $G$. If we succeed in extracting a minimal unsatisfiable core $\Sigma^{\prime}\subseteq\Sigma\cup\{\lnot e{:}\phi\}$ a minimal inconsistency proof can be recovered, from which finally the used justifications are extracted.

The following proposition allows to use SAT/SMT-solvers for a restricted setting and has been used in our case study.

Proposition 2** (SAT Reduction).**

Let $\Sigma=\{\sigma_{\_}1,\dots,\sigma_{\_}n\}$ be a set of formulae such that each element $\sigma_{\_}i$ is of the form $e_{\_}i{:}\phi_{\_}i$ with $e_{\_}i\in\mathcal{E}_{A}$ and $\phi_{\_}i$ does not contain any epistemic modal operators. Further, let $e$ be an arbitrary belief entity that does not occur in $\Sigma$. Then $G=\{e\mapsto_{\_}Ge_{\_}i|e_{\_}i\text{ occurs in }\Sigma\}$ is a justification graph for $\Sigma$ if and only if $\Phi=\{\phi_{\_}1,\dots\phi_{\_}n\}$ is satisfiable over the non-epistemic fragment of the logic of justification graphs.

Proof.

The satisfiability relation for the non-epistemic fragment is independent of the accessibility relations $\mapsto_{\_}e$, $e\in\mathcal{E}$ and, consequently, also independent of $G$. In particular, $\Phi$ is satisfiable if and only if there exists a model $M^{\prime}=(S,\mathcal{R},\pi)$ and a run $r$ such that $(M^{\prime},r)\models\Phi$.

Let $G=\{e\mapsto_{\_}Ge_{\_}i|e_{\_}i\text{ occurs in }\Sigma\}$ be a graph.

Let us first assume that $G$ is a justification graph for $\Sigma$. Then according to Def. 9 there exists a Kripke structure $M=(S,\mathcal{R},\pi,({\mapsto_{\_}e})_{\_}{e\in\mathcal{E}})$ and a run $r$ such that $(M,r)\models_{\_}Ge_{\_}i{:}\phi_{\_}i$ for all $e_{\_}i{:}\phi_{\_}i\in\Sigma$. Hence, we have $(M,r^{\prime})\models_{\_}G\phi_{\_}i$ for all $r^{\prime}$ with $r\mapsto_{\_}{e_{\_}i}r^{\prime}$. Furthermore, from item (i) and (iii) of Def. 9 we observe that ${\mapsto_{\_}e}$ is not empty and ${\mapsto_{\_}e}\subseteq{\mapsto_{\_}{e_{\_}1}}\cap\dots\cap{\mapsto_{\_}{e_{\_}n}}$. Hence, there exists at least one run $r^{\prime}$ that satisfies all formulae in $\Phi$. Since $\Phi$ does not contain epistemic operators, we found a model $M^{\prime}=(S,\mathcal{R},\pi)$ and a run $r^{\prime}$ such that $(M^{\prime},r^{\prime})\models\Phi$.

For the other direction, let us assume that there exists some model $M^{\prime}=(S,\mathcal{R},\pi)$ and a run $r$ such that $(M^{\prime},r)\models\Phi$. We extend $M^{\prime}$ to a Kripke structure $M=(S,\mathcal{R},\pi,({\mapsto_{\_}{e^{\prime}}})_{\_}{e^{\prime}\in\mathcal{E}})$ by setting $r\mapsto_{\_}{e^{\prime}}r^{\prime}$ for all $e^{\prime}\in\mathcal{E}$ if and only if $r=r^{\prime}$ for all $r,r^{\prime}\in\Pi$. Then $(M,r)\models_{\_}Ge_{\_}i{:}\phi_{\_}i$ for all $e_{\_}i{:}\phi_{\_}i\in\Sigma$ since $(M^{\prime},r^{\prime})\models\phi_{\_}i$ holds for all $r\mapsto_{\_}{e_{\_}i}r^{\prime}$ by construction of the accessibility relations. Moreover, since all accessibility relations are equal and reflexive, $\mapsto_{\_}e$ is serial. ∎

4 Identifying and Analysing Conflicts

In this section we first present an abstract algorithm for the conflict resolution of Sect.  2 that starts at level $(C_{1})$ and proceeds resolution stepwise up to level $(C_{4})$. We then sketch our small case study where we applied an implementation of the abstract algorithm.

4.1 Analysing Conflicts

For the analysis of conflicts we employ SMT solvers. Prop.  2 reduces the satisfiability of a justification graph to a SAT problem. To employ SMT solving for conflict analysis, we encode the (real and possible) worlds of Sect.  2 via logic formulae as introduced in Sect.  3. Each state $s_{\_}i$ is represented as a conjunction of literals, $s_{\_}i\equiv\bigwedge v\land\bigwedge\neg v^{\prime}$. Introducing a dedicated propositional variable $v_{\_}t$ for each $v\in\mathcal{V}$ and time step $t$ allows us to obtain a formula describing a finite run on $M$. A predicate of the form $\bigwedge_{\_}{(s,s^{\prime})\in\textit{T}}(s_{\_}{t}\rightarrow s^{\prime}_{\_}{t+1})$ encodes the transition relation T. The effect of performing an action $a_{\_}t$ at state $s$ is captured by a formula of the form $a_{\_}t\to(s_{\_}t\rightarrow s^{\prime}_{\_}{t+1})$. Using this we can encode a strategy $\delta$ in a formula $\psi_{\_}\delta$ such that its valuations represent runs of $M$ according to $\delta$. All runs according to $\delta$ achieve goals $\Phi$ if and only if $\psi_{\_}\delta\land\neg\Phi$ is unsatisfiable. These logical encodings are the main ingredients for using a SAT solver for our conflict analysis. Since there are only finitely many possible strategies, we examine for each strategy which goals can be (maximally) achieved in a world $M$ or in a set of worlds $\mathcal{M}$. Likewise we check whether A has a winning strategy that is compatible with the strategies A believes B might choose.

Since we iterate over all possible worlds for our conflict analysis, we are interested in summarising possible worlds. We are usually not interested in all $v_{\_}t$ – e.g. the speed of B may at times $t$ be irrelevant. We are hence free to ignore differences in $v_{\_}t$ in different possible worlds and are even free to consider all valuations of $v_{\_}t$, even if A does not consider them possible. This insight leads us to a symbolic representation of the possible worlds, collecting the relevant constraints. Now the justification graph groups the constraints that are relevant, with other words, $e{:}\phi$ and $e^{\prime}{:}\neg\phi$ will not be components of the same justification graph if the valuation of $\phi$ is relevant. In the following we hence consider the maximal consistent set of possible worlds, meaning encodings of possible worlds that are uncontradictory wrt. the relevant propositions, which are specified via the justification graph.

4.2 Algorithmic approach

In this section, we sketch an abstract algorithm for the conflict resolution at levels $(C_{1})$ to $(C_{4})$ as in Sect.  2. Note that we do not aim with Alg.  1 for efficiency or optimal solutions but aim to illustrate how satisfiability checks can be employed to analyse our conflicts.

The following algorithms describe how we deal with logic formulae encoding sets of possible worlds, sets of runs on them, etc. to analyse conflicts (cf. Def.  1, \autopagerefdef:conflict) via SMT solving. We use $\Sigma_{M}$ to refer to a formula that encodes a maximal consistent set of possible worlds (cf. Sect.  4.1), i.e., that corresponds to a justification graph. We use $\Sigma_{\mathcal{M}}$ to refer to a set of formulas $\Sigma_{M}\in\Sigma_{\mathcal{M}}$ that encode the set of possible worlds $\mathcal{M}$ structured into sets of possible worlds via justification graphs. We use $\mathcal{M}$ and $\Sigma_{\mathcal{M}}$ synonymously. Also we often do not distinguish between $\Sigma_{M}$ and $M$ – neglecting that $\Sigma_{M}$ represents a set of worlds that are like $M$ wrt to the relevant constraints.

Fig.  6 provides an overview of the relation between the initial information base $\Sigma_{\_}{I}$ of agent $A$, its set $\Sigma_{\mathcal{M}}$ of possible worlds $\Sigma_{M}$, winning strategies, resolution, and stepwise update of the information $\Sigma_{\_}{R}$ during our conflict resolution process. The initial information base defines the set of possible worlds $\mathcal{M}$, which is organised in sets of maximal consistent worlds $\Sigma_{M}$. Based on $\Sigma_{\mathcal{M}}$, $A$’s set of strategies $\Delta_{\_}A$ is checked whether it comprises a winning strategies in presence of an agent $B$ that tries to achieve its own goals. If no such winning strategy exists, $A$ believes to be in conflict with $B$. At each level $(C_{i})$ the resolution procedure tries to determine information $\Sigma_{\_}{R}$ of level $(C_{i})$ to resolve the conflict. If the possible worlds are enriched by this information, the considered conflict vanishes. The new information is added to the existing information base and the over-all process is re-started again until either winning strategies are found or $\Sigma_{\_}{R}$ is empty.

How to find a believed winning strategy.

Alg.  1 finds a winning strategy of agent $A$ for a goal $\Phi{}_{A}$ in $\Sigma_{\mathcal{M}}$ tolerating that $B$ follows an arbitrary winning strategy in $\Sigma_{M}\in\Sigma_{\mathcal{M}}$ for its goals, i.e. it finds a strategy that satisfies $\Phi{}_{A}$ in all possible worlds $\Sigma_{\mathcal{M}}$ where $\Phi{}_{A}$ is maximal for $\Sigma_{\mathcal{M}}$ and in each possible world $\Sigma_{M}\in\Sigma_{\mathcal{M}}$ agent $B$ may also follow a winning strategy for one of its maximal goals $\Phi{}_{B}$. If such a strategy cannot be found, $A$ believes to be in conflict with $B$ (cf. Def.  1).

Input for the algorithm is (i) a set $\Sigma$ of formulae describing the current belief of $A$, e.g. its current observations and its history of beliefs –we call it the information base in the sequel–, (ii) a set of goals $\Phi{}_{A}^{\mathit{max}}$ of $A$ that is maximal in $\mathcal{M}$, (iii) a set of believed goals $\Phi{}_{B}^{\mathit{max}}$ of $B$ that is maximal for a $\Sigma_{M}\in\Sigma_{\mathcal{M}}$, (iv) a set of possible actions $\mathcal{A}{}_{A}$ for $A$ and (v) a set of believed possible actions $\mathcal{A}{}_{B}$ for $B$.

First (L. 2 of Alg.  1) is to construct sets of maximal consistent sets of possible worlds that together represent $\mathcal{M}$. In L. 3 the set $\Delta_{A}$ is determined, which is the set of strategies accomplishing a maximal goal combination for $A$ assuming $B$ agrees to help, i.e., all winning strategies $(\delta{}_{A},\delta{}_{B}^{\prime})$ that satisfy $\Phi{}_{A}\in\Phi{}_{A}^{\mathit{max}}$ in all possible worlds $\Sigma_{M}\in\Sigma_{\mathcal{M}}$, where $\Phi{}_{A}$ is maximal for $\mathcal{M}$.

In lines 5 ff. we examine whether one of $A$’s strategies (where $B$ is willing to help) works even when $B$ follows its strategy to achieve one of its maximal goals $\Phi{}_{B}\in\Phi{}_{B}^{\mathit{max}}$ in $\Sigma_{M}$.

To this end TestIfNotWinning is called for all of $A$’s winning strategies $(\delta{}_{A},\delta{}_{B}^{\prime})\in\Delta_{A}$ (L. 6). The function TestIfNotWinning performs this test iteratively for one maximal consistent set of worlds $\Sigma_{M}$ (Alg.  2 L. 2). Let $\Delta_{B}$ be the set of joint strategies achieving a goal $\Phi{}_{B}\in\Phi{}_{B}^{\mathit{max}}$ that is maximal in $\Sigma_{M}$. We check the compatibility of $A$’s strategy $(\delta{}_{A},\delta{}_{B}^{\prime})$ to every $(\delta{}_{A}^{\prime},\delta{}_{B})\in\Delta_{B}$ (Alg.  2 L. 3). A strategy of $A$ $(\delta{}_{A},\delta{}_{B}^{\prime})$ is compatible to all of $B$’s strategies $(\delta{}_{A}^{\prime},\delta{}_{B})$ if all joint strategies $(\delta{}_{A},\delta{}_{B})$ achieve the maximal goals for $A$ and $B$ (Alg.  2 L. 6).666Note that according to Sect.  2.1, we have $\Phi{}_{B}=\texttt{true}$ if $B$ cannot achieve any goal. This reflects that $A$ cannot make any assumption about $B$’s behaviour in such a situation. If the joint strategy $(\delta{}_{A},\delta{}_{B})$ is not a winning strategy for the joint goal $\Phi{}_{A}\cup\Phi{}_{B}$ (Alg.  2 L. 6), the function GetJustifications extracts the set of justifications for this conflict situation (Alg.  2 L. 7). The set of justifications is added to the set of conflict causes $\mathcal{C}$ (Alg.  1 L. 8.). Since strategy $(\delta{}_{A},\delta{}_{B}^{\prime})$ is not compatible to all of $B$’s strategies, it is hence not further considered as a possible conflict-free strategy for $A$ (Alg.  1 L. 9).

A strategy that remains in $\Delta_{A}$ at Alg.  1 L. 10 is a winning strategy for one of $A$’s goals in all possible worlds $\Sigma_{M}$ regardless of what maximal goals $B$ tries to achieve in $\Sigma_{M}$. However, if $\Delta_{A}$ is empty at Alg.  1 L. 10 , $A$ is in a (believed) conflict with $B$ (Def.  1). In this case, conflict resolution is attempted (cf. lines 10 ff. in Alg.  1). Function FixConflict from Alg.  3 is called with the set of conflict causes, the current conflict resolution level, and the current information base and goals. For each conflict cause, an attempt of resolution is made by function Resolve. The conflict is analysed to identify whether adding/updating information of the current resolution level helps to resolve the conflict. If there are several ways to resolve a conflict, justifications can be used to decide which resolution should be chosen. Note that conflict resolution hence means updating of the information base $\Sigma$ or goal sets $\Phi{}_{A}^{\mathit{max}}$ and $\Phi{}_{B}^{\mathit{max}}$.

Line 13 of Alg.  1 checks if some new information was obtained from the resolution procedure. If not, resolution will be restarted at the next resolution level. If new information was obtained, FindStrategy is called with the updated information. If the result is a non-empty set of strategies, the algorithm terminates by returning them as (believed) winning strategies for $A$. However, if the result is the empty set, resolution is restarted at the next resolution level. If $\Delta_{A}$ is empty at level $(C_{4})$, the conflict cannot be resolved and the algorithm terminates.

Termination.

Alg.  1 eventually terminates under the following assumptions. The first assumption is that the set of variables $\mathcal{V}{}$ and hence the information base $\Sigma$ is finite. In this case, the construction of maximal consistent possible worlds $\Sigma_{\mathcal{M}}$ terminates since there is a finite number of possible consistent combinations of formulae and the time horizon for the unrolling of a possible world $\Sigma_{M}$ is bounded.

Together with finite sets $\Phi{}_{A}^{\mathit{max}}$, $\Phi{}_{B}^{\mathit{max}}$, $\mathcal{A}{}_{A}$, and $\mathcal{A}{}_{B}$, the construction of strategies, i.e. functions StratA and StratA, terminates since there are only finite numbers of combinations of input histories and output action and there is only a finite number of goals to satisfy. All loops in algorithms 1, 2, and 3 hence iterate over finite sets.

The extraction of justifications terminates since runs are finite and consequently the number of actions involved in the run, too. Furthermore, for each state in a run, there are only a finite number of propositions that apply. Together with a finite number of propositions representing the goal, GetJustifications can simply return the (not necessarily minimal) set of justifications from all these finite many formulae as a naive approach.

Alg.  1 terminates if a non-empty set $\Delta_{A}$ is derived by testing and/or resolution, or if a fixed point regarding $\Sigma$, $\Phi{}_{A}^{\mathit{max}}$, and $\Phi{}_{B}^{\mathit{max}}$ is reached. Since all other loops and functions terminate, the only open aspect is the fixed point whose achievement depends on Resolve. We assume that Alg.  1 is executed at a fixed time instance s.t. $A$’s perception of the environment does not change during execution. Thus, $\Sigma$ contains only a finite number of pieces of information to share. If we assume that that sharing information leads only to dismissing possible worlds rather then considering more worlds possible, then this a monotonic process never removing any information.777Otherwise the set of already examined worlds can be used to define a fixed point. Furthermore, we assume that the partial order of goals leads, if necessary, to a monotonic process of goal negotiation which itself can repeated finite many times until no further goals can be sacrificed or adopted from $B$. Thus, if $\Delta_{A}$ remains to be the empty set in line 15, the fixed point will eventually be reached.

Furthermore, we do not consider any kind of race conditions occurring from concurrency, e.g. deadlock situations where $A$ can’t serve $B$’s request because it does not know what its strategy will be since $A$ wait’s for $B$’s respond, and vice versa.

So in summary, the algorithm terminates under certain artificial assumptions but cannot determine a resolution in case without an outside arbiter. In practice such a conflict resolution process has to be equipped with time bounds and monitors. We consider these aspects as future work.

4.3 Case study

We implemented the algorithm sketched above in a Java program employing Yices [1] to determine contradictions and analysed variations of a toy example to evaluate and illustrate our approach.

We modelled a system of two agents on a two lane highway. Each agent is represented by its position and its lane. Each agent has a set of actions: it can change lane and drive forward with different speeds. We captured this via a discrete transition relation where agents hop from position to position. The progress of time is encoded via unrolling, that is we have for each point in time a corresponding copy of a variable to hold the value of the respective attribute at that time. Accordingly the transition relation then refers to these copies.

Since we analyse believed conflicts of an agent, we consider several worlds. In other words, we consider several variations of a Yices model. Each variation represents a justification graph summarising the maximal consistent set of evidences and thereby representing a set of worlds which is justified by this set of evidences.

We modify the Yices file by adding additional constraints according to the algorithm Sect.  4.2. For the steps $(C_{1})$ to $(C_{4})$ we add constraint predicates, e.g., that encode that information about certain observations have been communicated by say $B$ to $A$, constraints that specify that $B$ tells $A$ it will decelerate at step $4$ and constraints that encode goal combinations.

We employed Yices to determine whether there is conflict. The key observation is: If Yices determines that it holds that $\neg\varphi$ is satisfiable in our system model, then there is the possibility that the goal is not achieved – otherwise each evolution satisfies $\varphi$ and there is a winning strategy for the model.

5 Related work

Studying Traffic Conflicts.

According to Tiwari in his 1998 paper [7] studying traffic conflicts in India, one of the earliest studies concerned with traffic conflicts is the 1963 paper [8] of Perkins and Harris. It aims to predict crashes in road traffic and to obtain a better insight to causal factors. The term traffic conflict is commonly used according to [7] as “an observable situation in which two or more road users approach each other in space and time to such an extent that a collision is imminent if their movements remain unchanged” [9]. In this paper we are interested in a more general and formal notion of conflict. We are not only interested in collisions-avoidance but more generally in situations where traffic participants have to cooperate with each other in order to achieve their goals – which might be collision-freedom. Moreover, we aim to provide a formal framework that allows to explain real world observations as provided by, e.g., the studies of [7, 8].

Tiwari also states in [7] that it is necessary to develop a better understanding of conflicts and conjectures that illusion of control [10] and optimism bias theories like in [11] might explain fatal crashes. In this paper we develop a formal framework that allows us to analyse conflicts based on beliefs of the involved agents, –although supported by our framework–we here do not compare the real world evolution with the evolution that an agent considers possible. Instead we analyse believed conflicts, that are conflicts which an agent expects to occur based on its beliefs. Such conflicts will have to be identified and analysed by prediction components of the autonomous vehicles architecture, especially in settings where misperception and, hence, wrong beliefs are possible.

In [12] Sameh et al. present their approach to modelling conflict resolution as done by humans in order to generate realistic traffic simulations. The trade-off between anticipation and reactivity for conflict resolution is analysed in [13] in order to determine trajectories for vehicles at an intersection. Both works [12, 13] focus on conflicts leading to accidents. Regarding the suggested resolution approaches, our resolution process suggests cooperation steps with increasing level cooperation. This resolution process is tailored for autonomous vehicles that remain autonomous during the negation process.

Strategies and Games.

For strategy synthesis Finkbeiner and Damm [14] determined the right perimeter of a world model. The approach aims to determine the right level of granularity of a world model allowing to find a remorse-free dominant strategy. In order to find a winning (or remorse-free dominant) strategy, the information of some aspects of the world is necessary to make a decision. We accommodated this as an early step in our resolution protocol. Moreover in contrast to [14], we determine information that agent $A$ then want requests from agent $B$ in order to resolve a conflict with $B$ – there may still be no winning (or remorse-free dominant) strategy for all goals of $A$. In [15] Finkbeiner et. al.presented an approach to synthesise a cooperative strategy among several processes, where the lower prioritised process sacrifices its goals when a process of higher priority achieves its goals. In contrast to [15] we do not enforce a priority of agents but leave it open how a conflict is resolved in case not all their goals are achievable. Our resolution process aims to identify the different kinds of conflict as introduced in Sect.  2 that arise when local information and beliefs are taken into account and which not necessarily imply that actually goals have to be sacrificed.

We characterize our conflict notion in a game theoretic setting by considering the environment of agents $A$ and $B$ as adversarial and compare two scenarios where (i) the agent $B$ is cooperative (angelic) with the scenario where (ii) $B$ is not cooperative and also not antagonistic but reasonable in following a strategy to achieve its own goals. As Brenguier et al. in [16] remark, a fully adversarial environment (including $B$) is usually a bold abstraction. By assuming in (ii) that $B$ maximises its own goals – we assume that $B$ follows a winning strategy for its maximal accomplishable goals. So we are in a similar mind set than at assume-guarantee [17] and assume-admissible [16] synthesis. Basically we consider the type of strategy (winning/admissible/dominant) as exchangeable, the key aspect of our definition is that goals are not achievable but can be achieved with the help of the other.

Logics.

Justification logic was introduced in [3, 18] as an epistemic logic incorporating knowledge and belief modalities into justification terms and extends classical modal logic by Plato’s characterisation of knowledge as justified true belief. However, even this extension might be epistemologically insufficient as Gettier already pointed out in 1963 [19]. In [20] a combination of justification logics and epistemic logic is considered with respect to common knowledge. The knowledge modality $K_{\_}i$ of any agent $i$ inherits all information that are justified by some justification term $t$, i.e. $t{:}\phi\to K_{\_}i\phi$. In such a setting any justified information is part of common knowledge. Moreover, justified common knowledge is obtained by collapsing all justification terms into one modality $J$ and can be regarded as a special constructive sort of common knowledge. While our approach neglects the notion of common information, we use a similar inheritance principle where a belief entity inherits information of its components, cf. Def. 4.(iii). A comparison of the strength of this approach with different notions of common knowledge can be found in [21]. While justification logic and related approaches [22, 23], aim to restrict the principle of logical awareness and the related notion of logical omniscience, we argue in Sec. 3 that the principle of logical awareness as provided by modal logic is indispensable in our approach. A temporal (LTL-based) extension of justification logic has been sketched in [24]. This preliminary work differs from our approach wrt. the axiom systems used for the temporal logic part and the justification / modal logic part, cf. the logic of justification graphs axiomatised in Section 3. Our logic and its axiomatisation incorporates a partial order on the set of beliefs that underlies their prioritization during conflict resolution, which contrasts with the probabilistic extension of justification logic outlined in [25].

6 Conclusion

Considering local and incomplete information, we presented a new notion of conflict that captures situations where an agent believes it has to cooperate with another agent. We proposed steps for conflict resolution with increasing level of cooperation. Key for conflict resolution is the analysis of a conflict, tracing and identifying contradictory evidences. To this end we presented a formal logical framework unifying justifications with modal logic. Alas, to the authors’ best knowledge there are no efficient satisfiability solvers addressing distributed information so far. However, we exemplified the applicability of our framework in a restricted but non-trivial setting. On the one hand, we plan to extend this framework by efficient implementations of adapted satisfiability solvers, on the other hand by integrating richer logics addressing decidable fragments of first order logic, like linear arithmetic, and probabilistic reasoning.