Grzegorz Lisowski

Sylvie Doutre

Umberto Grandi

Aggregation in Value-Based Argumentation Frameworks

Value-based argumentation enhances a classical abstract argumentation graph -in which arguments are modelled as nodes connected by directed arrows called attacks -with labels on arguments, called values, and an ordering on values, called audience, to provide a more fine-grained justification of the attack relation. With more than one agent facing such an argumentation problem, agents may differ in their ranking of values. When needing to reach a collective view, such agents face a dilemma between two equally justifiable approaches: aggregating their views at the level of values, or aggregating their attack relations, remaining therefore at the level of the graphs. We explore the strenghts and limitations of both approaches, employing techniques from preference aggregation and graph aggregation, and propose a third possibility aggregating rankings extracted from given attack relations.

Introduction

The strength of arguments plays an important role in establishing the outcome of a discussion. Strong arguments have a stronger impact on the interlocutors than arguments perceived as weak. In particular, a strong argument can be accepted even if it is undermined by insignificant issues. The methods of formal modelling of the impact of the arguments' strength have been intensively studied in the abstract argumentation literature (see e.g. [START_REF] Matt | A Game-Theoretic Measure of Argument Strength for Abstract Argumentation[END_REF][START_REF] Paul E Dunne | Weighted Argument Systems: Basic Definitions, Algorithms, and Complexity Results[END_REF]). In particular, the problem of the perceived strength of arguments is crucial in a multi-agent environment.

It is far from being clear how a consensus can be reached among multiple agents disagreeing about which arguments are stronger than others. This observation connects to an extensive discussion on methods of finding a consensus among agents who disagree about the aspects of argumentation they participate in (e.g. [START_REF] Paul E Dunne | Argument Aggregation: Basic Axioms and Complexity Results[END_REF][START_REF] Awad | Judgement Aggregation in Multi-Agent Argumentation[END_REF][START_REF] Delobelle | Merging of Abstract Argumentation Frameworks[END_REF]).

One of the approaches to this problem emphasizes the role of values to which arguments appeal in determining their strength. In value-based argumentation, pioneered by Bench-Capon [START_REF] Bench-Capon | Persuasion in Practical Argument Using Value-Based Argumentation Frameworks[END_REF] and whose motivation traces back to Perelman [START_REF] Perelman | The New Rhetoric[END_REF], the concept of abstract argumentation due to Dung [START_REF] Minh | On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games[END_REF] is extended to incorporate the information on the values associated with the particular arguments. More precisely, following Dung's model, arguments are conceived as points in the graph, linked by an attack relation, which allows for designing rationality constraints (semantics) on acceptable sets of arguments. Additionally, each argument is assigned a unique value 1 . Further, in this approach, the strength of arguments is induced by an agent's preference over values that arguments appeal to: an attack from an argument appealing to a weak value on an highly valued argument is blocked. In this way, a defeat graph based on an individual view on the hierarchy of values is induced. The value-based argumentation approach has been further studied and extended in various ways (e.g. [START_REF] Bench-Capon | Audiences in Argumentatio Frameworks[END_REF]).

In this paper we consider a value-based argumentation framework, and several agents, each of them with its own preference over values. In this multi-agent context, a consensus is sought. Observe that the considered consensus is not directly about the choice of acceptable arguments, what is known in the literature as the semantics [START_REF] Minh | On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games[END_REF], but rather about the attack graph itself and its justification in terms of preference over values.

Note that there are two intuitive manners of aggregating the possibly conflicting views of the agents. The first method focuses on the individual ordering over values, and aggregates them into a collective ordering over values that in turns induces an attack relation over labelled arguments. Off-the-shelf techniques from preference aggregation and social choice theory in general can be used to find suitable aggregators (see, e.g., [START_REF] Kenneth | Social Choice and Individual Values[END_REF][START_REF] Allen | Strategy-Proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions[END_REF][START_REF] Gibbard | Manipulation of Voting Schemes: a General Result[END_REF][START_REF] Brandt | Handbook of Computational Social Choice[END_REF]). The second approach to this problem is to aggregate directly the agents' attack graphs, searching for a collective justification in the form of an ordering over the values a posteriori. Techniques in graph aggregation [START_REF] Endriss | Graph Aggregation[END_REF] and belief merging [START_REF] Everaere | An Introduction to Belief Merging and its Links with Judgment Aggregation[END_REF] have already proven useful in various settings related to argumentation [START_REF] Delobelle | Merging of Abstract Argumentation Frameworks[END_REF][START_REF] Delobelle | On The Aggregation of Argumentation Frameworks: Operators and Postulates[END_REF][START_REF] Chen | Preservation of Semantic Properties in Collective Argumentation: The Case of Aggregating Abstract Argumentation Frameworks[END_REF].

The aim of the current paper is to investigate the properties of the two approaches in the context of value-based argumentation, their benefits and limitations. The two possibly conflicting approaches are reminescent of the discursive dilemma in the literature on judgment aggregation [START_REF] Endriss | Judgment aggregation[END_REF][START_REF] Grossi | Judgment Aggregation: a Primer[END_REF], where aggregating the views of a group of agents on the premises supporting a given statement might conflict with the aggregated view on the statement itself, posing a serious challenge to the search for justifications in collective reasoning. This point relates also to the recent line of research on explainability of automated decision-making, which deals with designing methods to explain to a human user automated decisions (see, e.g. [START_REF] Miller | Explanation in Artificial Intelligence: Insights From the Social Sciences[END_REF]). Argumentation theory is already being employed in this context (e.g [START_REF] Fan | On Computing Explanations in Argumentation[END_REF]).

Our contribution After setting the stage for aggregating the views of agents on values and attacks over arguments, we analyze the arguably simpler method of aggregating directly the individual attack relations. As a first impossibility result we show that, if a number of natural properties are expected for the graph aggregation rule, then it is not always possible to extract a collective justification for the aggregated attack relation. We then move to the study of the aggregation of orderings over values. As there are several orderings over values that can justify a given attack relation, we investigate whether the result of the aggregation is stable with respect to this choice. We show a second impossibility result, again under standard axiomatic requirements on the aggregation procedure. As a side result, we characterize frameworks in which the ordering over values justifying a given attack relation is unique. We conclude then by providing an alternative aggregation procedure lying between the two studied approaches. To do so, we make use of the value-based framework, the context of our problem, to define an aggregation procedure over preferences on values that are suitably extracted from the individual attack relations, showing that it can ensure the same axiomatic properties of the preference aggregation rule chosen.

Related Work

It is worth noting that the methods of obtaining a consensus structure of argumentation based on values has been studied before. For instance, Modgil [START_REF] Modgil | Reasoning About Preferences in Argumentation Frameworks[END_REF] explored a modes for metaargumentation about the conflicts between arguments which captures also argumentation about preferences over values. Furthermore, Airiau et al. [START_REF] Airiau | Rationalisation of profiles of abstract argumentation frameworks: Characterisation and complexity[END_REF] studied methods of checking if a set of argumentation frameworks can be seen as a set of defeat graphs reflecting disagreement on the importance of values. This is the closest related work to this paper, and we will refer to it further in the following sections. Finally, preference aggregation in the context of value-based argumentation has been previously proposed in the context of value-based argumentation by Pu et al. [START_REF] Pu | Social Welfare Semantics for Value-Based Argumentation Framework[END_REF].

Outside the realm of value-based argumentation, a number of approaches have recently considered the problem of aggregation in multiagent argumentation. Coste-Marquis et al. [START_REF] Coste-Marquis | On The Merging of Dung's Argumentation Systems[END_REF] were the first to tackle this problem, proposing distance-based methods for the aggregation of argumentation structures. Dunne et al. [START_REF] Dunne | Argument Aggregation: Basic Axioms and Complexity Results[END_REF] later proposed an axiomatic study of the aggregation of argumentation frameworks, later expanded by the work of Delobelle et al. [START_REF] Delobelle | On The Aggregation of Argumentation Frameworks: Operators and Postulates[END_REF]. Closest to our analysis are the works of Awad et al. [START_REF] Awad | Judgement Aggregation in Multi-Agent Argumentation[END_REF] and Chen and Endriss [START_REF] Chen | Preservation of Semantic Properties in Collective Argumentation: The Case of Aggregating Abstract Argumentation Frameworks[END_REF], which focuses on several problems related to the collective rationality of the aggregation process, i.e., whether properties satisfied by the input attack relations are preserved in the collective outcome.

This paper expands previous work by the authors [START_REF] Lisowski | Preventing Manipulation in Aggregating Audiences in Value-Based Argumentation Frameworks[END_REF], building on the Master thesis of Lisowski [START_REF] Lisowski | Preventing Manipulation in Aggregating Value-Based Argumentation Frameworks[END_REF].

Paper structure The paper is organized as follows. In Section 2 we give the basic definitions of valuebased argumentation, preference and graph aggregation, and list a number of desirable properties for the aggregation process. Further, Section 3 describes the properties of the approaches based on aggregating submitted graphs and on preference orderings. In Section 4, we analyze the combined approach. Finally, in Section 5 we provide conclusions and suggestions for further development.

The setting

The model we study in this paper is the value-based argumentation setting, due to Bench-Capon [START_REF] Bench-Capon | Persuasion in Practical Argument Using Value-Based Argumentation Frameworks[END_REF]. This formal framework extends Dung's abstract argumentation model [START_REF] Minh | On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games[END_REF]. Hence, the basic notion employed in the studied setting is of an argumentation framework. It is a directed graph, in which vertices correspond to arguments, and edges to the attack relation, capturing conflicts between arguments. In order to capture how arguments appeal to values, argumentation frameworks are extended to valuebased argumentation frameworks. These are labeled directed graphs, in which labels correspond to values that arguments relate to, an argument relating to one value only. For the sake of simplicity we assume that every argument is associated with a single value. Definition 2. A value-based argumentation framework (VAF) is a tuple VAF = A, →,V, val , where A is a set of arguments, →⊆ A2 is an attack relation, V is a set of values and val : A → V is a function assigning values to arguments.

Then, we can define how an agent's preferences over values determine the strength of values from the perspective of a particular agent. To achieve that, agents are allowed to express preference orderings over values. Following the literature on value-based argumentation, such a preference ordering is called an audience. Definition 3. Let VAF = A, →,V, val . An audience P is a linear ordering 2 over V . We denote that a value v 1 ∈ V is more preferable than a value v 2 ∈ V for P as v 1 ≻ P v 2 .

Then, the way in which agents perceive the strength of arguments influences the way in which they perceive the structure of argumentation. Intuitively, an agent might disregard the fact that a weak argument undermines a strong argument, as it is not important enough to be considered a legitimate reason to reject a vital point. Formally, we say that an argument a defeats an argument b, if a attacks b and either b's value is weaker than a's, or a and b appeal to the same value. It is worth noting that as we require audiences to be linear, this means that a must be stronger than b. Definition 4. Let VAF = A, →,V, val be a VAF and P be an audience. Then, we say that an argument a defeats an argument b for P (we denote it as a → P b) iff a → b and it is not the case that val(b) ≻ P val(a).

Further, given an initial VAF and an audience, we can consider an argumentation framework based on the set of arguments present in VAF, and the defeat relation. Such an argumentation framework is called a defeat graph. Definition 5. Let VAF = A, →,V, val and P be an audience. The defeat graph of VAF induced by P is an argumentation framework AF = A, → P .

Let us illustrate the defined notion with an example, adapted from [START_REF] Airiau | Rationalisation of profiles of abstract argumentation frameworks: Characterisation and complexity[END_REF]:

Example 2.1. Consider a debate regarding the possible ban of diesel cars, aimed at the reduction of air pollution in big cities. The following arguments are included in the discussion:

• A -Diesel cars should be banned.

• B -Artisans, who should be protected, cannot change their cars as it would be too expensive for them.

• C -We can subsidize electric cars for artisans.

• D -Electric cars, which could be a substitute for diesel, require too many new charging stations.

• E -We can build some charging stations.

• F -We cannot afford any additional costs.

• G -Health is more important than economy, so we should spend whatever is needed for fighting pollution.

Further, it can be noticed that these arguments appeal to certain values. In particular, arguments A, G appeal to environmental responsibility (ER), B,C to social fairness (SF), F to economic viability (EV) and D, E -to infrastructure efficiency (IE). These arguments are represented on the graph with a mapping of values depicted on Figure 1. For each argument, the first element of its description is its name, and the second one is the name of the value it appeals to. Let us now consider the structure of this discussion from the perspectives of two experts of a decisionmaking jury, that should decide on whether Diesel cars should be banned or not.

A, ER B, SF D, IE C, SF E, IE F, EV G, ER
For Expert 1, economic viability is the most important. She ranks infrastructure efficiency lower, but higher than social fairness. Environmental responsibility is the least important for her. Then, from her point of view attacks in which the attacker appeals to a less important value than the attacked argument are disregarded. Taking her preferences into account, the structure presented in Figure 2 (a) is obtained, after the elimination of disregarded attacks. Let us now consider another expert of the jury, who believes that economic viability is the most important value. Expert 2 ranks environmental responsibility second, and social fairness third. Finally, she considers infrastructure efficiency as the least important. From her perspective, the structure of successful attacks is much different, as indicated in Figure 2 (b). It is worth observing that in the current paper we assume for the sake of simplicity that agents have a certain common ground. Namely, they agree on the set of arguments and on the values that they appeal to. This assumption is indeed restrictive: in many cases participants of a dispute disagree on these parameters. We aim at addressing these issue in future work.

A, ER B, SF D, IE C, SF E, IE F, EV G, ER A, ER B, SF D, IE C, SF E, IE F, EV G, ER

Aggregating preferences

A natural way of retrieving a collective view on the structure of argumentation taking into account individual opinions on the importance of values is to employ a preference aggregation approach. This method considers a profile of preference orderings, corresponding to individuals' opinions, and provides a single, collective preference ordering. We will denote the set of individuals as N = {1, . . . , n}. Definition 6. Let Pref = {≻ 1 , . . . , ≻ n } be a set of preference orderings over a set V . A profile of preference orderings is a tuple P = ≻ 1 , . . . , ≻ n consisting of the elements of Pref.

Definition 7 (Preference Aggregation Rule). Let V = {v 1 , . . . , v n } be a set of options and P be the set of all linear orderings over V . Then a preference aggregation rule is a function F : P m → P. We denote the set of agents supporting v i ≻ v j in a profile P as N

v i ≻v j P .
This method provides a straightforward way of dealing with disagreements with respect to views on the hierarchy of values. All agents start first by submitting their preference orderings over values. Further, the orderings are aggregated with employment of a chosen preference aggregation function, resulting in a collective preference ordering (≻ coll ). Finally, by applying this collective preference ordering over values to a considered VAF, a collective defeat graph AF coll is obtained. Figure 3 depicts this process. A simple example of a preference aggregation rule, which we will use to illustrate the proposed mechanism, is the Borda rule. Let us first define the rank of an option from the perspective of the given preference ordering.

(≻ 1 , ≻ 2 , . . . ≻ n ) =⇒ F ≻ coll AF coll VAF
Notation 1. Let P be a linear order over some set V . We denote as rank P (v) the position of the option v in the ordering P. Formally, rank

P (v) = |{v ′ ∈ V |v ≻ P v ′ }|.
Then, given a profile P of preference orderings

P i over set V , Borda(P) =≻ coll , such that v i ≻ coll v j iff ∑ P i ∈P rank P i (v i ) > ∑ P i ∈P rank P i (v j ) for every v i , v j ∈ V ,
combined with a tie-breaking rule to obtain a strict ranking in case of equality of the Borda score. 3 Let us illustrate how a collective defeat graph is computed using the Borda rule on our running example.

Example 2.2. (Continuation of Example 2.1) Let us consider an additional expert, Expert 3. Let us present her audience, and let us recall the audiences of the other two experts.

These three experts form a panel P.

• Expert 1: EV ≻ IE ≻ SF ≻ ER • Expert 2: EV ≻ ER ≻ SF ≻ IE • Expert 3: SF ≻ ER ≻ EV ≻ IE
Let us now calculate the result of the Borda rule for P. The scores are: ER: 4, EV: 7, IE: 2, SF: 5. So, Borda(P)= EV ≻ SF ≻ ER ≻ IE. The defeat graph for this ordering is presented in Figure 4; this is the collective defeat graph for the panel. 3 We refer to ∑

A, ER B, SF D, IE C, SF E, IE F, EV G, ER
P i ∈P rank P i (v i ) as to the score of v i .

Aggregating defeat graphs

In performing preference aggregation over values, the previous section assumed that these individual preferences are known, as an input data of the search for a collective position. However, it may happen that what is known from the agents is the way they see arguments and their relationships, that is, what their defeat graph is, and not what their preferences over values are. For instance, the experts may not want to reveal what their inner preferences are, but just present how they see the resulting situation in terms of arguments and attacks. In such contexts, the search for a collective position can be done by aggregating the defeat graphs.

An intuitive requirement for this process is that the resulting collective defeat graph be justifiable with respect to a value-based argumentation framework the input defeat graphs are based on: that is, there should exist an ordering of values that, when applied to the initial known or unknown value-based framework, produces the collective defeat graph.

If graph aggregation is fully justified when the preferences over values are not known, one may also think of using this technique to obtain a collective view when they are known. The two techniques, graph aggregation and preference aggregation, will be compared in further sections. For now, let us present graph aggregation.

A graph aggregation rule is a function taking a profile of graphs as an input and providing a single graph. It is worth noting that in the considered setting we only take into account profiles of graphs sharing the set of vertices and require that the collective graph is also based on this set.

Definition 8 (Graph Aggregation Rule). Let A be a set of arguments and Graphs be the set of all argumentation frameworks based on A. Then a graph aggregation rule is a function F : Graphs m → Graphs. For any pair of arguments a, b ∈ A, we denote the set of agents supporting a → b in a profile AF as N a→b

AF . The aggregation process is depicted on Figure 5. An example of an intuitive class of graph aggregation rules is the class of quota rules. There, an edge is included in the collective graph if a specified fraction of agents includes it in their submitted graphs. Definition 9 (Quota rule). Let AF be a profile of argumentation frameworks. Then, F is a quota rule if there is q ∈ [0, 1] such that for any attack a → b, a → b ∈ F(AF) iff N a→b AF ≥ ⌊q * n⌋, where n is the total number of voters.

(AF 1 , AF 2 , . . . AF n ) =⇒ F AF coll
The most well-known quota rule is the (weak) majority rule, where q = 1 2 . It is worth noting that in the current setting we are often assuming that agents submitting their graphs have a well defined hierarchy of values in mind. Indeed, we can often safely assume that agents submit graphs which are justifiable. A profile is justifiable if there is a single VAF such that all members of the profile are defeat graphs of VAF. 4Definition 10 (Justifiable Profiles). Let AF be a profile of graphs. AF is justifiable if there is a VAF such that for any AF i ∈ AF, AF i is a single defeat graph of VAF.

In the later part of the paper we will mainly focus on graph aggregation rules restricted to justifiable inputs. In such rules, input profiles are only limited to profiles of graphs such that there is a VAF such that all members of the profile are defeat graphs of VAF.

We will be searching for graph aggregation rules which guarantee that if all the graphs considered in an input are defeat graphs of some VAF, then so is the output. It is worth noting that this problem is a special case of the problem of collective rationality, studied intensively in the social choice literature, also in the context of the abstract argumentation (see, e.g [START_REF] Chen | Preservation of Semantic Properties in Collective Argumentation: The Case of Aggregating Abstract Argumentation Frameworks[END_REF][START_REF] Rahwan | Collective Argument Evaluation as Judgement Aggregation[END_REF]). This problem relates to the issue of whether an aggregation rule makes sure that if all of the agents involved in a decision process are submitting an option which satisfies a certain rationality constraint, so does the outcome of the procedure. In the context of graph aggregation, collective rationality means that if all input graphs satisfy a given property, the output graph satisfies it as well.

We will refer to the collective rationality with respect to the property described before as to the preservation of being a defeat graph.

Definition 11 (Preservation of being a defeat graph). A graph aggregation rule preserves being a defeat graph of VAF if whenever for every AF i ∈ AF, AF i is a defeat graph of VAF, so is F(AF).

We can now illustrate the application of graph aggregation rules on the running example.

Example 2.3. (Continuation of Example 2.2). Consider now the defeat graphs induced by the experts' audiences as the input of the aggregation process. We will apply the majority rule to provide a common graph for the panel. Let us list out the attacks such that the majority of agents agree that they should

hold: F → G, F → C, F → E, C → B, E → D, B → A.
Note that these edges corresponds to the graph obtained while using the Borda rule in the Example 2.2. It is worth observing, however, that it is not necessarily always the case, as will be highlighted by the comparison between graph and preference aggregation conducted in the following sections.

Aggregation Axioms

In following sections we will often refer to desirable properties of the aggregation mechanisms under consideration. Here, we will define such properties (or axioms), both for preference and graph aggregation. The considered axioms are standard in computational social choice, and are explained for instance in [START_REF] Brandt | Handbook of Computational Social Choice[END_REF] for preference aggregation and [START_REF] Endriss | Collective Rationality in Graph Aggregation[END_REF] for graph aggregation. The wording of the definitions has been changed for the ease of presentation.

Preference aggregation rule

Let us start with defining the desired properties for the preference aggregation approach. We will start with an informal description of the axioms, which will be followed by a formal definition.

A preference aggregation function is unanimous if it never changes any ordering between options that all agents agree upon; the function is anonymous if it provides the same output regardless of the ordering of items in its input; independent, if the decision about the ordering of two values only depends on the way in which voters order this particular pair. In addition, we will strive to find rules which are not dictatorial. Formally: Definition 12. A preference aggregation function F is:

• Unanimous: if whenever in a profile of orderings P= P 1 , . . . , P n all voters submit that v i ≻ v j , then v i ≻ v j in F(P).

• Anonymous: if for any profile of orderings P= P 1 , . . . , P n , any pair of items v i , v j and any permutation π : N → N , a → b ∈ F(P) iff a → b ∈ F(P π(1) , . . . , P π(n) ).

• Independent: if it holds that for any pair of profiles of preference orderings P, P ′ and any pair of

values v 1 , v 2 ∈ V , if N v 1 ≻v 2 P = N v 1 ≻v 2 P' , then v 1 ≻ v 2 ∈ F(P) iff v 1 ≻ v 2 ∈ F(P'
). • Dictatorial: if there is i such that for any P= P 1 , . . . , P n , F(P) = P i .

Graph aggregation rule

Let us now define corresponding axioms for graph aggregation. They are adopted from [START_REF] Endriss | Collective Rationality in Graph Aggregation[END_REF].

The unanimity axiom states that if all agents agree that some attack should be included in the collective graph, then it is. The anonymity condition expresses that a choice of attacks does not depend on the name of voters. Independence states that all attacks are treated equally in any profile of defeat graphs. We also additionally demand for a rule not to be dictatorial. Formally: Definition 13. A graph aggregation rule F is:

• Unanimous: if for every profile of argumentation frameworks AF= AF 1 , . . . , AF n , if there is some pair of arguments a, b ∈ A such that for every AF i ∈ AF a → i b, a → b ∈ F(AF).

• Anonymous: if for every profile of argumentation frameworks AF= AF 1 , . . . , AF n , any attacks a → b and any permutation π

: N → N , a → b ∈ F(AF) iff a → b ∈ F(AF π(1) , . . . , AF π(n) ).
• Independent: if for any pair of profiles of argumentation frameworks AF, AF',

if N AF a→b = N AF' a→b , then a → b ∈ F(AF) iff a → b ∈ F(AF').
• Dictatorial: if there is i such that for any AF, F(AF) = AF i .

Impossibility Results

In this section we explore the limitation of the two aggregation approaches defined in Section 2, thus comparing aggregation at the level of values with aggregation at the level of attack graphs in the context of value-based argumentation.

Graph aggregation

We will commence with exploring the properties of the graph aggregation in the context of aggregating views on rankings of values.

Note that graph aggregation requires substantially less information than the preference aggregation based mechanism. Indeed, a graph aggregation rule can be used without specifying a context of a VAF. On the other hand, a preference aggregation can only be obtained when the values to which arguments appeal are specified. So, to use preference aggregation in the context of value-based argumentation we need to have the knowledge of both the profile of graphs and the VAF.

Unfortunately, as graph aggregation rules do not take the context of a VAF into account it might be the case that even though all agents participants of a discussion submit argumentation frameworks which are induced by their preferences over values, the collective graph is not justifiable by any preference ordering in the context of a given debate based on values. This is why the preservability of being a defeat graph is of high interest. In this section we will investigate the conditions which graph aggregation rules need to satisfy to preserve being a defeat graph.

Unfortunately, as we will see later, graph aggregation rules that also preserves being a defeat graph cannot satisfy all of the axioms we defined. We begin by showing that no quota rule can preserve being a defeat graph: Proposition 1. Being a defeat graph is not preserved by any quota rule.

Proof. Consider a quota defeat aggregation rule F with an arbitrary quota q ∈ [0, 1]. Then, take some natural number n such that 1 n < q. Further, construct a VAF = A, →,V, val such that A = {a 1 , . . . , a n }, →= {a i → a i+1 |i < n} ∪ {a n → a 1 }. Note that this attack relation forms a cycle. Also, let val(a i ) = v i for any argument a i (now all arguments are assigned unique values). Then, consider a set of agents N = {1, . . . , n}, submitting defeat graphs such that for any i < n, in agent i's perspective only a i → i a i+1 , while for agent n only a n → n a 1 . It is easy to see that these are defeat graphs of VAF. For any agent i, the set of attacks {a n → a m |a n → i a m } is a chain of length n -1. Then, we can consider a preference ordering over values such that for any a n → a m such that a n → i a m , val(a m ) ≻ i val(a n ). Clearly, this gives us a desired defeat graph.

Note now, that in the result of application of F to this profile, no attacks are preserved, as each of them has a support of fewer agents than q * |N|. But now suppose that we have an ordering P over V under which such a defeat graph would be obtained. Then, we would need to have than v n ≻ P v n-1 ≻ P . . . ≻ P v 1 ≻ P v n . But then P is not transitive, so it is not a preference ordering.

Let us consider the following axiomatic characterisation of the class of quota rules:

Theorem 1 ([18]). A graph aggregation F rule is anonymous, monotonic and independent iff F is a quota rule.

This leads us immediately to an impossibility result:

Corollary 1. Any graph aggregation rule preserving being a defeat graph violates anonymity, monotonicity, or independence.

Proof. If a rule F is anonymous, monotonic and independent, by Theorem 1 F is a quota rule. But then, by Proposition 1, F does not preserve being a defeat graph.

By Corollary 1 it follows that all graph aggregation rule preserving being a defeat graph must violate intuitive axioms in the general case. However, we are especially interested in aggregating justifiable graphs. So, we would like to establish which rules restricted to justifiable inputs preserve being a defeat graph. As we will see, this is impossible for an important class of rules.

To establish this result we will employ Arrow's impossibility theorem, one of the cornerstones of social choice theory, stated here in its version for strict linear orders:

Theorem 2 ([2]). Any unanimous and independent preference aggregation rule is dictatorial, when the set of alternatives has at least 3 elements.

We can now show the following: Theorem 3. Any graph aggregation rule restricted to justifiable profiles and preserving being a defeat graph is not independent, not unanimous, or is dictatorial.

Proof. Take a graph aggregation rule which preserves being a defeat graph. Also, suppose towards contradiction that it is unanimous, independent and is not dictatorial. Now, consider a VAF= A, →,V, val

such that V = {v 1 , v 2 , v 3 }, A = {a v i |v i ∈ V }, val(a v i ) = v i
and →= {a → b|a, b ∈ A and a = b}. Now consider an argumentation framework AF which is a defeat graph of VAF. Note, that it corresponds to a unique preference ordering over V . We can thus encode any profile P of preference orderings over V as a profile of defeat graphs AF P of VAF. Define now a preference aggregation rule F ′ : P m → P, such that v i ≻ v j ∈ F ′ (P) iff a v i → F(AF P ) a v j . Notice that F ′ (P) is a linear ordering: as F(AF) is a defeat graph of VAF, we have that F ′ (P) is connected since for every pair v i , v j ∈ V 2 there is an attack a v i → a v j . It is also anti-symmetric, as for every pair of arguments a v i , a v j we need to have that either a v i → F(AF) a v j or a v j → F(AF) a v i while it is not the case that a v i → F(AF) a v j and a v j → F(AF) a v i . Otherwise it would be impossible to find a symmetric preference ordering P' such that F(AF) is a defeat graph of VAF induced by P'. By a similar argument we can show that we cannot have that a v i → F(AF a v j , a v j → F(AF) a v k and a v k → F(AF) a v i . From this it follows that F ′ (P) is transitive.

We need to demonstrate that if F is unanimous, independent and non-dictatorial, then so is F ′ . If F is unanimous: suppose that F ′ is not and take a profile of preference orderings P such that for some pair of values v i , v j , for every P k ∈ P v i ≻ k v j but v j ≻ F ′ (P) . Then, by construction of F we would have that for every member of the profile AF of graphs induced by P a v i → a v j , but it would not be the case in F(AF), which contradicts the assumptions. If F is independent, suppose that F ′ is not and take profiles of orderings P, P' over V such that for some v i , v j we have that v i ≻ v j ∈ F ′ (P) while v j ≻ v i ∈ F ′ (P') even though v i ≻ v j is supported by the same voters in both profiles. Then, by construction of F we would have that for the pair of profiles of graphs AF, AF' induced by P, P' a v i → F(AF) a v j but a v j → F(AF') a v i , so F wouldn't be independent. Finally, if F ′ would be dictatorial, by construction of F we would have that for some i, in any profile AF, F(AF) = AF i , so by contraposition if F is non-dictorial, so is F ′ . But this means that by Theorem 2 we cannot have independent, unanimous and non-dictatorial rules restricted to justifiable profiles which preserve being a defeat graph.

This result shows that it is not possible to find any rule satisfying all the considered desiderata. However, we can still consider natural rules preserving being a defeat graph. Note that any representativevoter rule satisfies this property. These are the rules which always select some graph represented in the input profile (see e.g., [START_REF] Endriss | Binary Aggregation by Selection of the Most Representative Voter[END_REF]). Another intuitive move would be to select an argumentation framework which is a defeat graph of a VAF justifying the input profile and minimizing a distance from the submitted graphs, in line with techniques from belief merging cited in the related work section. This approach is however not guaranteed to work, and investigating this issue is an interesting direction for future work, as it might be the case that the output of such a rule is not a defeat graph of a second VAF' which also happen to justify the input profile.

Preference aggregation

Let us now proceed to the study of properties of preference aggregation based mechanisms. These mechanisms have a major advantage over graph aggregation: they always produce justifiable outputs. However, the outcome of the preference aggregation based mechanism is dependent on the context of VAF. By the context of a VAF we mean the assignment of values to arguments. Indeed, it is worth noting that a preference aggregation mechanism does not always ensure that if two profiles of preference orderings induce the same profile of defeat graphs, they will produce the same collective defeat graph. They might, in principle, provide different graphs depending on the context of VAF. As we will see further, this is the case for all reasonable preference aggregation based mechanisms.

Formally, we will be looking for preference aggregation rules corresponding to some graph aggregation rule.

Definition 14 (Corresponding graph aggregation). Let F be a preference aggregation rule. A graph aggregation function F ′ corresponds to F if for every profile of justifiable argumentation frameworks, VAF= A, →,V, val and a profile of preference orderings P justifying AF with respect to VAF, the defeat graph A, → F(P) = F ′ (AF).

A necessary condition for the existence of a graph aggregation rule corresponding to a preference aggregation rule F, is that given a VAF and a profile AF of its defeat graphs, application of F will result in the same collective defeat graph, no matter which profile of preference orderings justifying AF is chosen. Formally, we will refer to this property as to interpretation independence.

Definition 15 (Interpretation Independence). A preference aggregation rule F is interpretation independent if for every VAF and profile AF of defeat graphs of VAF, we have that for every pair of profiles P, P' justifying AF with respect to VAF, A, → F(P) = A, → F(P') .

The aforementioned fact follows from the following lemma: Lemma 1. If there is a graph aggregation rule corresponding to a preference aggregation rule F, then F is interpretation independent.

Proof. Proof by transposition. Take a aggregation rule F which is not interpretation independent. Then take a profile AF of defeat graphs of a VAF such that for two profiles of preference orderings P, P', F produces different outcomes (AF, AF'). Then note that any graph aggregation function corresponding to F would need to have both AF and AF' as the output for AF, which is not possible. However, interpretation independence only holds if F is independent.

Proposition 2. A preference aggregation rule F is interpretation independent iff F is independent.

Proof. (⇐) Consider any VAF = A, →,V, val , as well as a profile of its defeat graphs AF. Also, let F be any independent preference aggregation rule. Further, take any pair of profiles P, P' of preference orderings over V inducing AF. Now suppose that A, → F(P) = A, → F(P') . Without loss of generality assume that there is an attack a → b such that a → b ∈ A, → F(P) but a → b / ∈ A, → F(P') . Then, by connectedness we know that val(a) ≻ val(b) ∈ F(P). Otherwise we would have that val(b) ≻ val(a) ∈ F(P), so the attack would be blocked. Then, take the set of voters N (⇒) Proof by transposition. Take a preference aggregation rule F which is not independent. Let us show that there is some VAF and a profile of its defeat graphs such that for two distinct profiles P 1 , P 2 of preference orderings justifying it, the defeat graphs induced by F(P 1 ) and F(P 2 ) are not equal. We know that there is a pair of values v 1 , v 2 and a pair of profiles of preference orderings

P 1 , P 2 such that N v 1 ≻v 2 P 1 = N v 1 ≻v 2 P 2 but v 1 ≻ v 2 ∈ F(P 1 ) while v 1 ≻ v 2 / ∈ F(P 2 )
. Take these profiles and construct a VAF= A, →,V, val such that V is the set of values ordered by P 1 and

P 2 , A = {a v k |v k ∈ V }, →= {a v 1 → a v 2 , a v 2 → a v 1 }
and for any val(a v k ) = v k . Now, consider a profile AF of defeat graphs of VAF induced by P 1 . Note that both P 1 and P 2 justify AF since

N v 1 ≻v 2 P 1 = N v 1 ≻v 2 P 2 . We know, however, that v 1 ≻ v 2 ∈ F(P 1 ) while v 1 ≻ v 2 /
∈ F(P 2 ). Thus, we have that in the defeat graph induced by F(P 2 ), a v 2 → a v 1 , which is not the case in the graph induced by F(P 1 ) .

It turns out that as a consequence of the Arrow's impossibility theorem, we can only guarantee that a preference aggregation rule is Interpretation Independent if it is not unanimous or is dictatorial.

Theorem 4. The only unanimous preference aggregation rule corresponding to a graph aggregation function is a dictatorship.

Proof. From Proposition 2 and Theorem 2 we have immediately that any unanimous, interpretation independent preference aggregation rule is dictatorial. Then, by Lemma 1 we get that the only unanimous preference aggregation rule corresponding to a graph aggregation function is a dictatorship.

On a more positive side, let us highlight two situations where preference aggregation rules are always interpretation independent. The first such situation is when a given VAF only admits defeat graphs justifiable by a unique preference ordering. The following proposition characterizes such VAFs. Proposition 3. For every VAF= A, →,V, val we have that for every defeat graph AF of VAF, AF is justifiable by a unique preference ordering iff for every v 1 , v 2 ∈ V there is a pair of arguments a 1 , a 2 such that val(a

1 ) = v 1 , val(a 2 ) = v 2 and a 1 → a 2 or a 2 → a 1 .
Proof. (⇒) Proof by transposition. Take a VAF= A, →,V, val such that for a pair of values v 1 , v 2 ∈ V , for any a 1 , a 2 ∈ A if val(a 1 ) = v 1 and val(a 2 ) = v 2 , a 1 → a 2 and a 2 → a 1 . We will show that there are ≻, ≻ ′ such that A,

→ ≻ = A, → ≻ ′ . Let for every v 1 , v 2 ∈ V such that v 1 , v 2 / ∈ {v i , v j }, v 1 ≻ v 2 iff v 1 ≻ ′ v 2 . Also, let for every v 1 / ∈ {v i , v j }, v 1 ≻ v i , v 1 ≻ v j , v 1 ≻ ′ v i and v 1 ≻ ′ v j . Now take any attack a → b. Note that by construction of ≻, ≻ ′ , if val(a) / ∈ {v i , v j } or val(b) / ∈ {v i , v j }, a → ≻ b iff a → ≻ ′ b. But if it is not the case, a → b. So, A, → ≻ = A, → ≻ ′ .
(⇐) Take a VAF= A, →,V, val such that for every v 1 , v 2 ∈ V there is a pair of arguments a 1 , a 2 such that val(a 1 ) = v 1 , val(a 2 ) = v 2 and a 1 → a 2 or a 2 → a 1 . Then suppose that there are two preference orderings ≻, ≻ ′ such that A, → ≻ = A, → ≻ ′ . Consider a pair of values v 1 , v 2 such that v 1 ≻ v 2 but v 2 ≻ v 1 . W.l.o.g assume that there is a pair of arguments a 1 , a 2 such that val(a 1 ) = v 1 , val(a 2 ) = v 2 and a 1 → a 2 . But we know that a 1 → ≻ a 2 iff a 1 → ≻ ′ a 2 , and hence v 1 ≻ v 2 iff v 1 ≻ ′ v 2 , which contradicts the assumptions.

Another situation guaranteeing interpretation independence is when a VAF has not more than two values, as shown in the following proposition. Proposition 4. For every VAF = {A, →,V, val} such that |V | ≤ 2, either all defeat graphs are justified by a unique preference ordering, or all defeat graphs of VAF are equal.

Proof. Consider any such VAF = {A, →,V, val} and let V = {v 1 , v 2 } (note that if V is a singleton, all defeat graphs of VAF are equal by definition of a defeat graph). Suppose that for some pair of arguments a 1 , a 2 such that val(a 1 ) = v 1 and val(a 2 ) = v 2 , a 1 → a 2 or a 2 → a 1 . Then, by Proposition 3 we have that all defeat graphs of VAF are justified by a unique preference ordering. Also, if this is not the case, for all attacks a → b in →, val(a) = val(b). So, by definition of a defeat graph, for any preference ordering ≻, →=→ ≻ .

Retrieved orderings

Note that both of the approaches considered so far have some drawbacks. On the one hand, we have shown that any graph aggregation function satisfying desirable properties cannot ensure that a VAF justifying a profile of graphs justifies also the collective graph. On the other hand, obtaining a collective defeat graph using preference aggregation functions requires more information than the employment of graph aggregation and we cannot ensure its correspondence to any graph aggregation rule. In this section we explore an aggregation method which combines the two approaches. Our goal will be to provide a procedure which both makes sure that the collective argumentation framework is always a defeat graph of the same VAF as the input graphs, and that it corresponds to some graph aggregation rule.

To this purpose we consider the following mechanism. First, a profile of defeat graphs on a given VAF is submitted by the agents. Then, a profile of preference orderings justifying the profile is derived (multiple choices are possible). Further, these preferences are aggregated using a suitable preference aggregation function, which in turns induces a collective defeat graph on the initial VAF.

The considered mechanism is illustrated in Figure 6. The lower tier of the picture represents a profile of defeat graphs of a certain VAF. Each ≻ i is a preference ordering inducing AF i , and is aggregated into ≻ coll by means of a preference aggregation function F. This step is depicted as an arrow in the upper tier. The collective defeat graph AF coll is then induced by VAF using ≻ coll . Let us define the proposed method formally. Note that to ensure the functionality of the proposed mechanism, it is required that the selected choice of preference orderings is predetermined: we do not distinguish between exact preferences over values that agents believe in, as long as they induce the appropriate profile of defeat graphs. To cope with this issue, we will always specify a selection of justifications. Intuitively, we infer preference orderings over values that participants of a debate have, based on their perceived strength of arguments.

(≻ 1 , ≻ 2 , . . . ≻ n ) =⇒ F ≻ coll (AF 1 , AF 2 , . . . AF n ) AF coll VAF VAF VAF VAF
Definition 16 (Justification selection). Let (Graphs VAF ) n be the collection of all profiles of defeat graphs of VAF= A, →,V, val of length n, and Prefs n be the set of all profiles of preference orderings over V of length n. Then a justification selection is a function J : (Graphs VAF ) n → Prefs n such that J(AF) induces AF for any profile AF in (Graphs VAF ) n .

Then, we can provide a definition of the proposed mechanism.

Definition 17 (C J F -mechanism). Take VAF= A, →,V, val , a profile AF of defeat graphs of VAF, a preference aggregation function F, and a justification selector J. Then, C J F (VAF, AF) amounts to the defeat graph AF = A, → F(J(AF)) .

Henceforth, for the sake of clarity we will often assume that a justification selection is fixed and omit the superscript J. Let us illustrate the mechanism on the running example. The proposed mechanism C F enjoys a number of interesting properties. First, this method does not require information about the exact preference orderings over values, so it does not require us to demand agents to provide additional information, as it was the case when the preference aggregation method was involved. However, we still have not ensured that there is a graph aggregation rule corresponding to any mechanism C F . To satisfy this, we would need to have that the collective graph is not dependent on the chosen VAF justifying a profile of graphs. Definition 18 (VAF-Independence). C F is VAF-Independent if for any profile of justifiable graphs AF and a pair VAF, VAF' of VAFs justifying AF, C F (AF, VAF) = C F (AF, VAF').

Unfortunately, as we will see, this can be the case only if F violates unanimity or is dictatorial.

Proposition 5. If C F is VAF-Independent, then F is dictatorial or non-unanimous for |V | ≥ 4.
Proof. Let us firstly show that any VAF-Independent C F requires F to be independent for profiles based on at least 4 values. Suppose that F is not independent. Then, take two profiles P, P' over a set V with |V | ≥ 4 such that for some pair of values v 1 , v 2 we have that

N v 1 ≻v 2 P = N v 1 ≻v 2 P' but v 1 ≻ F(P) v 2 while v 2 ≻ F(P') v 1 .
Then, consider a profile of graphs AF= AF 1 , . . . AF n such that n = |P| and for

AF i ∈ AF, AF i = {A, → i } and A = {a v i |v i ∈ V }, → i = {a v 1 → i a v 2 } if v 1 ≻ i v 2 , otherwise → i = {a v 2 → i a v 1 }
. Now take two VAFs such that AF is a profile of defeat graphs of VAF justified by P, while AF is a profile of defeat graphs of VAF' justified by P', such that for both VAFs, a v 1 and a v 2 attack each other, val(a v 1 ) = val ′ (a v 1 ) = v 1 and val(a v 2 ) = val ′ (a v 2 ) = v 2 , while for some pair of arguments a v i , a v j , val(a v i ) = v i , val(a v j ) = v j and val ′ (a v i ) = v j , val ′ (a v j ) = v i . Now note that the outcome of C F (AF, VAF), C F (AF, VAF') only depends on the collective preference ordering over v 1 , v 2 . So, we will have that

a v 1 → C F (AF,VAF) a v 2 , while a v 2 → C F (AF,VAF') a v 1 . So, C F is not VAF-Independent. It follows now from Theorem 2 that if C F is VAF-Independent, then F is dictatorial or non-unanimous.
This leads us to conclude that when there are at least 4 values, if F is non-dictatorial and unanimous, a two arguably basic properties, then C F does not correspond to any graph aggregation rule. Note, however, that this issue is solved once we fix the VAF justifying particular profiles of defeat graphs.

Let us first define a fixed selection of a VAF for a profile of graphs. Definition 19 (VAF selection). Let (Graphs) n J be the collection of all justifiable profiles of argumentation frameworks of length n, and VAFs be the set of all VAFs. Then a VAF selection is a function S : (Graphs) n J → VAFs such that for any profile AF, S(AF) is such that for every AF i ∈ AF, AF i is a defeat graph of S(AF).

We can now define the modified mechanism. Definition 20 (C VAF F,S mechanisms with fixed VAF). Let F be a preference aggregation rule. Then, the combined mechanism is the function C VAF F,S : Graphs J → Graphs, where Graphs J is the set of all justifiable profiles of graphs, such that C VAF F,S (AF) = A, → F(P) such that P is a profile of preference orderings justifying AF from the perspective of S(AF).

In what follows we will assume that S is fixed and drop the subscript when clear from context. Then, it is not difficult to show that C VAF F corresponds to a graph aggregation rule.

Observation 1. Any C VAF F corresponds to a graph aggregation rule restricted to justifiable inputs.

Proof. Take a profile of graphs AF justifable by a given VAF and a combined mechanism C VAF F . Then notice that the choice of VAF and of the profile of preference orderings justifying AF have been predetermined, and thus we can only obtain one graph. This is the case for all justifiable profiles of graphs. So, C VAF F indeed corresponds to a graph aggregation rule.

Not only this movement ensures the existence of a corresponding graph aggregation rule, but also that the correspondent inherits beneficial properties of the used preference aggregation rule. (2) Take any anonymous preference aggregation rule F. Then, suppose that the graph aggregation rule F ′ corresponding to C VAF F is not anonymous. Then, take a VAF and a profile of preference orderings P and a sequence AF of defeat graphs induced by P such that there is a permutation π of AF such that F ′ (AF) = F ′ (π(AF)). But now note that this would imply that F(P) = F(π(P')) which cannot be the case by anonymity of F.

(3) Take any independent preference aggregation rule F. Then, suppose that the graph aggregation rule F ′ corresponding to C VAF F is not independent. So, take a VAF and two profiles of defeat graphs AF, AF' of VAF such that there is some attack a → b such that N a→b AF = N a→b AF' , but a → b ∈ F ′ (AF) while a → b / ∈ F ′ (AF'). Note that by connectedness of preference orderings, for any justification P, P' of AF, AF', N So, we have provided an alternative method of aggregating agents' views on the importance of values in the context of value-based argumentation. This has allowed us to overcome the issues we pointed out for the preference aggregation and graph aggregation approaches: we ensure that the outcome of the procedure is a defeat graph of the considered VAF, while making sure that the mechanism corresponds to a graph aggregation rule restricted to justifiable inputs.

In this paper we have explored three plausible methods of aggregating agents' views in the context of value-based argumentation, in order to obtain a collective argumentation framework: preference-based, graph-based, and combination-based aggregation methods.

For the preference aggregation approach, we have shown that non-dictatorial rules never correspond to graph aggregation rules and thus, depending on the context, different collective argumentation frameworks can be obtained even though agents perceive the defeat relation in the same manner. On the other hand, no graph aggregation approach satisfying intuitive properties can ensure that the outcome of the procedure is a defeat graph of the same VAF as the input graphs. These issues can be circumvented by an aggregation approach combining preference aggregation with the extraction of an ordering over values from the individual attack relations, which fixes a VAF and devises a suitable aggregation procedure for the specific context. This is one of the main conclusions of this work: obtaining a justifiable collective argumentation graph is not possible without taking into consideration the underlying VAF, which acts as the context of the problem.

This observation leaves a vast room for further research, investigating further aggregators that are specific to a given (class of) VAF. In the current setting we have restricted ourselves to studying preference orderings over values expressed as linear orderings. This is a strong requirement. It would be of high interest to study the aggregation problems stated in this paper when agents are allowed to consider particular values as equally important. Moreover, it would be interesting to study the scenario in which agents do not agree on the assignment of values to arguments. Further, it would be of natural interest to investigate, following e.g. Kaci and van der Torre [START_REF] Kaci | Preference-based argumentation: Arguments supporting multiple values[END_REF], the scenario in which arguments appeal to multiple values. Finally, studying classes of argumentation problems which are not affected by the problems highlighted in the paper would be very beneficial towards showing the applicability of the proposed approaches.

Definition 1 .

 1 An argumentation framework (AF) is a pair AF = A, → , where A is a set of arguments and →⊆ A 2 is the attack relation. We denote the fact that a, b ∈→ as a → b. a, b ∈→ is denoted a → b.

Figure 1 :

 1 Figure 1: Value-based argumentation framework VAF of Example 2.1; each node is labeled with its name and the name of the value it appeals to; the arrows correspond to the attack relation.

Figure 2 :

 2 Figure 2: Defeat graphs based on (a) Expert 1's (EV ≻ IE ≻ SF ≻ ER) and (b) Expert 2's (EV ≻ ER ≻ SF ≻ IE) audiences. In the graphs, nodes are labeled with names of arguments and names of values they appeal to. The arrows correspond to the induced defeat relations based on the experts' audiences.

Figure 3 :

 3 Figure 3: Preferences over values are aggregated into a collective ordering on values, which in turn induces an attack graph once a VAF is fixed.

Figure 4 :

 4 Figure 4: Collective defeat graph for the panel P, under the Borda rule.

Figure 5 :

 5 Figure 5: Individual graphs are aggregated into a collective graph.

  val(a)≻val(b) P . Note that they must correspond to defeat graphs in which a → b is included. Other defeat graphs can only be justified with orderings in which val(b) ≻ val(a) and, by connectedness requirement, preservation of a → b needs to be justified with an ordering in which val(a) ≻ val(b). So, N val(a)≻val(b) P is also the set of supporters of val(a) ≻ val(b) in P'. So, by independence, val(a) ≻ val(b) ∈ F(P'). So, a → b ∈ A, → F(P') . Contradiction.

Figure 6 :

 6 Figure6: The individual attack graphs AF i are provided a justification order over values ≻ i , which are then aggregated using a preference aggregation rule F, and the collective ordering ≻ coll so obtained induces a collective attack graph AF coll justified by it.

Example

Proposition 6 .

 6 Let F be a preference aggregation rule. Then it holds that:[START_REF] Airiau | Rationalisation of profiles of abstract argumentation frameworks: Characterisation and complexity[END_REF] If F is unanimous, then the graph aggregation rule F ′ corresponding to a C VAF F is unanimous. (2) If F is anonymous, then the graph aggregation rule F ′ corresponding to a C VAF F is anonymous. is monotonic. (3) If F is independent, then the graph aggregation rule F ′ corresponding to a C VAF F is independent.Proof.(1) Take any unanimous preference aggregation rule F. Then, suppose that the graph aggregation rule F ′ corresponding to C VAF F is not unanimous. Then, take a VAF and a profile of preference orderings P * inducing a profile of defeat graphs AF such that there is an attack a → b such that for anyAF i ∈ AF, a → b ∈ AF i , but a → b / ∈ F ′ (AF).Note that then val(a) = val(b). Then, we must have that all agents submit that val(a) ≻ val(b). But then, by unanimity of F, val(a) ≻ val(b) ∈ F(P * ), and thus a → b ∈ F ′ (AF). Contradiction.

  by independence, a ≻ b ∈ F(P) iff a ≻ b ∈ F(P). So, if a → b ∈ F ′ (AF), then a → b ∈ F ′ (AF'). Contradiction.

  4.1. (Continuation of Example 2.3) Consider the profile of graphs submitted by the experts as in Example 2.3. Note that they are all defeat graphs of the VAF presented in Example 2.1. Thus, we can retrieve the preference orderings justifying them and apply the Borda preference aggregation rule. Let us assume that the tie-breaking protocol follows a fixed ordering ER > SF > IE > EV . Finally, once the collective preference ordering has been obtained, we can construct the collective defeat graph. Suppose that the selector J associates with Expert 1 and Expert 3 the same orderings as in Example 2.2, while for Expert 2 the selectore chooses EV ≻ ER ≻ IE ≻ SF. If we aggregate the three preferences using the Borda rule we obtain EV ≻ ER ≻ SF ≻ IE, which is a different result than the one in Example 2.2. If we then construct the associated collective defeat graph, we observe that the attack from the argument B on A is blocked, while the remaining ones are as in the collective graph of Example 2.2.

The generalisation of the model by allowing arguments to appeal to multiple values has been studied by, e.g., Kaci and van der Torre[START_REF] Kaci | Preference-based argumentation: Arguments supporting multiple values[END_REF]. For the sake of simplicity, in the current paper we will work with the simple scenario in which an argument is assigned a unique value.

A linear ordering is an irreflexive, transitive and complete binary relation.

Justifiability of profiles of graphs has been studied in depth in[START_REF] Airiau | Rationalisation of profiles of abstract argumentation frameworks: Characterisation and complexity[END_REF].

Acknowledgments

We would like to thank Sonja Smets for useful comments in the early phases of this project. Most of the work was completed when Grzegorz Lisowski was hosted at the University of Toulouse in 2018.


Neeraj Kumar Singh
email: nsingh@enseeiht.fr

Hao Wang

Virtual Environment Model of Glucose Homeostasis for Diabetes Patients

Keywords: Homeostasis, Diabetes, Formal methods, Environment modelling

A medical device is designed to meet the patient specific requirements. The required biological behaviour of the medical device is driven by mostly the operating environment. Most of the time, a medical device fails due to lack of understanding of the system requirements, including the functional and non-functional requirements. For example, the U.S. Food and Drug Administration (FDA) has reported a large number of serious illnesses and deaths related to IIP. Our approach is to trigger hidden requirements at an early stage of the system development. In order to achieve our goal, this paper proposes an abstract development of virtual environment model of the glucose homeostasis for diabetes patients to analyze the patient specific medical devices, such as an Insulin Infusion Pump (IIP). The main objective of this environment model is to assist in the construction, clarification, and validation of the system requirements by developing and designing the closed-loop model of medical devices.

I. INTRODUCTION

Since software plays a vital role for better controllability, operability and safety in medical domains, the device manufacturers are required to validate any software used in their devices, and test rigorously the functional behaviour of the device for detecting critical flaws and security vulnerabilities. To address the critical flaws and security vulnerabilities including device development process, the regulators provide guidelines to develop a safe and dependable critical medical systems. These guidelines play a major role to comply with certification standards. Due to increasing system complexities, regulatory agencies are always looking for new methods and tools for improving the engineering-based review strategy that could provide the system assurance.

The Insulin Infusion Pump (IIP) is a complex medical device that is used by millions of people to regulate normal levels of glucose for controlling diabetes. This device is used to deliver insulin doses in a controled manner in order to maintain an appropriate level of glucose. Over the past few years, IIPs have been used successfully to treat diabetes. However, the failure rate of the IIPs have increased tremendously. These failures cause several deaths and serious illnesses. The U.S. Food and Drug Administration (FDA) reported 17,000 adverseevents from 2006 to 2009 including 47 deaths due to IIP's malfunctions [START_REF] Chen | Insulin pump software certification[END_REF]. The root causes of these device failures are considered as product design and engineering flaws, which are identified by the FDA officials during investigation of the reported deaths and illnesses related to the IIPs.

The medical device manufacturers use an artificial environment model for simulating and testing the functionalities and effectiveness of medical devices. Such type of environment models are very expensive and critical to use for testing and validating the medical devices. These models are based on complex mathematical equations, that require high computation and large memory for simulating the environment. However, these models are not able to simulate and to check the overall functionalities of a device. It is important to know that, these models are also not applicable to use at the early phases of the development life-cycle for testing or verifying the requirements. Our experience and knowledge show that an environment model can be used for validating the system requirements at an early stage of the system development. This approach has some other benefits, such as finding missing requirements, validating assumptions and strengthening the existing requirements. To apply this approach, we need to develop the closed-loop model by using an abstract model of the virtual environment. The designed abstract model should capture all the essential features. The closed-loop model is a combined model of the medical device model and the environment model, where both models interact to each other using sensors and actuators. Medical device model uses actuators and sensors to respond according to the functional activities of the virtual environment. If sensors sense abnormal activities then the device must actuate for delivering medicine or any other activities. If sensors sense normal behaviours then the device should not do anything. By observing the virtual behaviour of the environment, we can ensure that the medical device behaves correctly under the required conditions. This approach has potential benefits of giving a confidence in the product development that the behaviour of medical device is safe within the biological virtual environment.

As far as we know, there is no environment model for IIP, which can be used for simulating and testing the system requirements at an early stage of the system development during design and development. This paper contributes by providing the development of virtual environment model of the glucose homeostasis for diabetes patients to analyze the patient specific medical devices like Insulin Infusion Pump (IIP). The prime use of this environment model is to assist in the construction, clarification, and validation of the given system requirements by designing the closed-loop model using formal methods at an early stage of the development life-cycle. We use a simple logic for modelling the biological environment of an IIP. The environment model is based on continued monitoring of the glucose-insulin regulatory system [START_REF] Li | Modeling the glucose-insulin regulatory system and ultradian insulin secretory oscillations with two explicit time delays[END_REF]. The proposed virtual environment model describes normal and diabetic conditions, by using α-cells and β-cells, and rising or dropping plasma glucose level to model the pancreatic behaviour, and blood test levels for the diagnosis of diabetes/pre-diabetes. The key features of this model is to consider both normal and abnormal (hyperglycemia or hypoglycemia) behaviour that can be used to characterize a patient model. There are several benefits of our approach: 1) Development of simple and complex environment models using simple logic in several refinements; 2) Use of an environment model for identifying missing requirements and emerging behaviour; 3) Assist in meeting the criteria of certification standards; and 4) Validation of the system assumptions and behavioural requirements.

The structure of this paper is as follows. Section II presents the related work. Section III presents basic concepts of the virtual environment modeling. Section IV presents glucose homeostasis (GH) system, and the formal definition of the glucose homeostasis (GH) is presented in Section V. Section VI discusses the usability of the environment model. We conclude the paper and discuss the future work in Section VII.

II. RELATED WORK

The human biological system is one of the complex, dynamic and infinite systems, that is not fully understood yet. The medical practitioners and engineers use physical and mathematical model to characterize the biological behaviour. Over the last decade, several models exist for describing the glucose homeostasis and diabetes. These models are either clinical or non-clinical. The clinical models are used for identifying and predicting the diagnostics, control, progression, complication, etc. of diabetes. The non-clinical models are used for modelling the insulin-glucose, hepatic glucose, glucagon, and insulin receptor dynamics, beta-cell insulin release, and brain glucose homeostasis. The first mathematical model based on differential equations to model the glucose and insulin concentration, illustrating the dynamics of insulinglucose for diagnostic purpose and evaluating several parameters of the diabetic and pre-diabetic conditions proposed in [START_REF] Bolie | Coefficients of normal blood glucose regulation[END_REF]. The proposed model was very useful for describing the dynamics of insulin and glucose and their concentration level. An integrated insulin-glucose model for analyzing the diabetic condition using a bidirectional insulin-glucose feedback mechanism was presented in [START_REF] Silber | An integrated model for glucose and insulin regulation in healthy volunteers and type 2 diabetic patients following intravenous glucose provocations[END_REF]. The theoretical treatment of the effect of external potassium on oscillations in the pancreatic β-cells was presented in [START_REF] Chay | Theory of the effect of extracellular potassium on oscillations in the pancreatic beta-cell[END_REF]. This model was able to demonstrate that insulin infusion may be useful for mimicking pancreatic insulin secretion. There are several models produced by academia and industries that incorporate different physiological processes associated with insulinglucose dynamics and different variations [START_REF] Ajmera | The impact of mathematical modeling on the understanding of diabetes and related complications[END_REF].

The literature suggests that existing models, with their mathematical constraints and higher order differential equations, are not easy to express in first order logic, and thus make it difficult to express the system requirements for verification purpose. Moreover the existing models have been developed for specific purposes that cannot support desired global behaviours. We want to describe the complete system by introducing the abstract notions of possible features that can be later extended for any particular use. The concept of environment modelling for GH system is motivated by our previous work on heart modelling [START_REF] Singh | Using Event-B for Critical Device Software Systems[END_REF] and GH modelling [START_REF] Singh | Formalizing the glucose homeostasis mechanism[END_REF]. We have adopted the same methodology to design an efficient and optimum environment model for the GH system based on abstract notions of pancreatic behaviours. The model is defined through analyzing the glucose regulation mechanism. The virtual environment model is described abstractly using first-order logic considering various safety properties at each incremental step, and normal and abnormal behaviour (hyperglycemia, hypoglycemia or diabetic complications).

III. METHODOLOGY FOR ENVIRONMENT MODELLING

To use an environment model for developing the medical systems, we need to focus on the expressiveness of the selected modelling language to describe the complex and realistic environment using various levels of abstraction. The modelling language should have well-defined syntax and semantics for the tools to analyze desired behaviour. The language should allow refinement based modelling including temporal, functional, reactive and non-deterministic behaviour for specifying the required components of environment. The Event-B modelling language fulfills the basic requirements as an environment modelling language. In fact, there is another benefit that we can also use the same modelling notations for designing the medical systems. The refinement approach allows to model both the medical system and the environment together to specify the required level of abstractions as well as concrete details. Environment modelling requires higher level of abstractions to describe non-deterministic behaviour compared to the system behaviour. Functional behaviour of both the environment and system models are described by the dynamical states, which show system interactions using sensors and actuators.

The environment model provides essential information about environment components, basic characteristics of each component, and structural relationship between components. The structural relationship between two components shows a common interface channel or medium to exchange the information. All these components together form the overall environment that simulates the virtual operating environment for medical systems. Each component can have several instances of the environment, which can be specified nondeterministically for capturing the functional behaviours. The environment model can have numerous sensors and actuators including system components. The environment components are described formally, and a list of properties validates the expected functional behaviours of the components. Following, we discuss further in detail various guidelines for modelling the virtual environment model for medical systems [START_REF] Singh | A Virtual Glucose Homeostasis Model for Verification, Simulation and Clinical Trials[END_REF].

A. Modelling Components

To design an environment model, we need to include all the essential components to describe the required system behaviour. These essential components can be expressed in both abstract and concrete as per the granularity levels of the system component definition. For example, few components can be described abstractly to capture only desired behaviour and to avoid the complex computations. Note that the complex computation should not affect the required system behaviour. The development of the environment model can start from a very abstract model that can be further enriched by introducing new components or details of the components. Each refinement level contains more components or detailed functionalities. All the models from abstract to concrete levels can be used for simulation purpose that can satisfy the required behaviour of the system.

B. Components Composition

The environment components are linked to each other through physical or logical relationships. The relationship preserves architectural definition of the system components. The given relationships allow all the environment components to communicate or to exchange the information. Each component responses according to the current actual input that is sensed by sensors. A large system can consist of several small components, which can be specified by functions. Each system component uses different types of sensors that can be described as functions with different sensors types. These small components can be used further to design the virtual environment model.

C. Properties of Components

To design an environment model, only components definitions and relationships are not enough. These things only provide the skeleton of an environment model, but it cannot provide any guarantee that we have designed the correct environment model. To design a correct environment model, we need to provide a set of properties related to the functional behaviours. Model properties are indispensable to characterize the environment components to satisfy the required behaviours. It is important to include those properties that are necessary to check system requirements. These may include behaviour constraints of a component, required input attributes for components, and state invariants for each component with respect to the medical systems for verifying the desired behaviour.

D. System Modelling

To ensure the effectiveness of environment modelling, it is important to include the system model itself for analyzing the overall system behaviour. In fact, we need to model both the system model and the environment model together to understand the peculiar behaviour of the system. For instance, to analyze an Insulin Infusion Pump (IIP), we need to model both the IIP and GH model. However these two models connect to each other and form a closed-loop model. These models interface with each other as sensors and actuators. It is important to include the details of the system and environment model including sensors and actuators for interaction considering desired levels of detail, and required safety properties.

E. Model Simulation

The environment models developed using any methodology require simulation and dynamic execution for understanding the correctness of biological behaviour. The simulation allows to check the temporal behaviour, interactions between of system components, and new changes evolving over time. However, it must meet all the requirements for a real biological system. Simulation not only guarantees the correctness of system behaviours, but also helps domain experts to understand the designing environment.

IV. THE GLUCOSE HOMEOSTASIS SYSTEM

Glucose is the major metabolic fuel of the human body.

To maintain an appropriate level of glucose in the body and to provide normal functionality, we need a regular supply of glucose to the body. Failure of the glucose level causes several diseases such as diabetes mellitus, galactosemia and glycogen storage diseases [START_REF] Ajmera | The impact of mathematical modeling on the understanding of diabetes and related complications[END_REF].

Fig. 1 depicts the normal GH system 1 , which presents the structural flow of the hormones and a functional behavioural pattern of the different organs. It is vital for the body to maintain an appropriate glucose concentration, so both low and high glucose levels are serious, life-threatening problems. The body regulates its glucose concentration using the pancreas and the liver. The pancreas produces two main hormones insulin and glucagon to control the GH system. The body cells use the available glucose whenever the body receives glucose from the infusion or hepatic function. There are two different types of cells that use the glucose. For instance, the brain and nervous system cells use glucose without insulin, while other types of cells like muscle and fat cells use glucose with the help of insulin. The glucose concentration level fluctuates in the body, and is maintained in the plasma through the pancreatic secretion of glucagon and insulin. In general, the body attempts to maintain an appropriate level of glucose in the body, but there are some natural stable oscillations that occur in the glucose and insulin concentrations [START_REF] Li | Modeling the glucose-insulin regulatory system and ultradian insulin secretory oscillations with two explicit time delays[END_REF].

Low and high glucose levels are the two main biological responses that the body uses to maintain an appropriate plasma glucose concentration. When the glucose level drops, then the α-cells in the pancreas produce glucagon, which is transformed into glucose with the help of the liver. This process helps to increase the glucose concentration in the body. Similarly, when the plasma glucose level goes higher than expected, then the β-cells in the pancreas are stimulated to lower the glucose concentration [START_REF] Ajmera | The impact of mathematical modeling on the understanding of diabetes and related complications[END_REF]. This stimulation process 1 The 'normal GH system' is when the GH system functions as it should, i.e., there are no abnormal behaviours exhibited by the system. Fig. 1. The GH System (adopted from [START_REF] Ajmera | The impact of mathematical modeling on the understanding of diabetes and related complications[END_REF]) can be completed within 5 to 15 minutes, and during this period the insulin is produced by β-cells of the pancreas. The secreted insulin can be used by insulin dependent cells to utilize the available glucose, and to stop the natural hepatic glucose production for reducing the glucose concentration in the blood. The liver is the central organ for regulation of glucose and glycogen and behaves as a distributor of nutrients through blood to other tissues. The presence of insulin inhibits the transformation of glucagon to glucose.

V. FORMAL DEFINITION OF GLUCOSE HOMEOSTASIS

The GH model is mainly based on the glucose regulation system of the body. This method uses advanced capabilities of the combined approach of formal verification and behaviour simulation, in order to achieve considerable advantages for GH system modelling. Fig. 1 shows the main components of the GH system. The system comprises different states of the glucose level in the blood and biological organs, in order to control the glucose level. To formalize the GH system, we consider eight significant landmark nodes (Hi, No, Lo, Ac, Bc, Li, St, Tr) in the homeostasis functional network as shown in Fig. 2, which can control the GH system. We have identified these landmarks through a literature survey [START_REF] Ajmera | The impact of mathematical modeling on the understanding of diabetes and related complications[END_REF], [START_REF] Li | Modeling the glucose-insulin regulatory system and ultradian insulin secretory oscillations with two explicit time delays[END_REF], [START_REF] Bolie | Coefficients of normal blood glucose regulation[END_REF], [START_REF] Silber | An integrated model for glucose and insulin regulation in healthy volunteers and type 2 diabetic patients following intravenous glucose provocations[END_REF], and use them to express an abstract functionality of the system. We introduce the necessary elements to formally define the GH systems as follows:

Definition 1 (The GH System). Given a set of nodes N, a transition T, is a pair (i, j), with i, j ∈ N . A transition is denoted by i j. The GH system is a tuple GHS = (N, T, N 0 ) where:

• N = { Hi, No, Lo, Ac, Bc, Li, St, Tr } is a finite set of landmark nodes in the GH network; • T ⊆ N × N = {No → Hi, Hi → No, No → Lo, Lo → No, Hi → Hi, No → No, Lo → Lo, Hi → Bc, Lo → Ac, Bc → Li, Ac → Li, Li → St, Li → Tr, St → No, Tr → No, St → Hi, Tr → Lo, Tr → Hi,

is a set of transitions to present data flow between two landmark nodes. It should be noted that the last three transitions are possible when we consider the case of failure of the GH system;

Glucose Level Drops

Glucose Level Rises

Hi

No Lo Ac Bc

Li

St Tr

Insulin Release

Glucagon Release

Fig. 2. The GH Automata

• N 0 = No is the initial landmark node (normal glucose level);

The automata shows the flow of the GH system, where by default the GH system is considered to be in its normal state (No). The normal state indicates that there is an appropriate glucose level in the blood. Whenever the glucose level fluctuates in the blood, resulting in a high or low glucose level, the GH system controls the fluctuated glucose level with the help of the pancreas and liver. The high and low states are presented by Hi and Lo nodes (see Fig. 2). The pancreas has two type of cells: α-cells and β-cells, which are indicated by the Ac and Bc nodes, respectively. The liver is denoted by the Li node that is used to convert the glycogen to glucose using glucagon, and to store the glucose as glycogen in the liver with the help of insulin. If the liver is well behaved, then the glucose level either rises or drops according to whether there is a low or high glucose level in the blood, respectively. Eventually, the glucose level returns to an appropriate level.

A. Diabetes or Abnormal Homeostasis System

Fig. 3 presents abnormal behaviour of the GH system. The liver plays a central and crucial role for regulating the glucose level in the blood. The main task of the liver is the continual supply of required glucose energy sources to the body. Failure of the GH system causes several diseases, and in particular, diabetes. There are two type of diabetes: insulin-dependent diabetes (also know as type 1 diabetes) and non insulindependent diabetes (also know as type 2 diabetes). Insulindependent diabetes may be caused by insufficient or no insulin secreted due to β-cells defects. In non insulin-dependent diabetes, insulin is produced, but the insulin receptors in the target cells do not work due to insulin resistance in the cells, so the insulin has no effect. In both cases there can be a very high glucose level in the blood. Low glucose level can be caused by α-cell defects or abnormal glucagon release, which can be further classified as insufficient or no glucagon secretion, excess insulin, and excess glucagon secretion. Excess glucagon secretion and defects in β-cells may also indicate a persistent high glucose level, which can be classified as hyperglycemiainduced diabetes complications [START_REF] Ajmera | The impact of mathematical modeling on the understanding of diabetes and related complications[END_REF]. Fig. 3. Abnormal GH System (adopted from [START_REF] Ajmera | The impact of mathematical modeling on the understanding of diabetes and related complications[END_REF])

B. Blood Sugar Concentration

The blood sugar concentration or blood glucose level is an amount of glucose (sugar) present in the blood of the body. The body naturally regulates blood glucose levels as a part of metabolic homeostasis. The glucose level fluctuates many times in a day. In general, the glucose level is always low in the morning, and it can rise for about an hour after having a meal. There are two types of tests used to detect abnormal behaviours: FPG (Fasting Plasma Glucose) Test and the OGTT (Oral Glucose Tolerance Test) [START_REF] Siperstein | The glucose tolerance test: a pitfall in the diagnosis of diabetes mellitus[END_REF]. The FPG test is used to detect diabetes and pre-diabetes. The FPG test measures blood glucose in a person who has fasted for at least 8 hours and is most reliable when given in the morning. The OGTT can be used to diagnose diabetes, pre-diabetes, and gestational diabetes. This test is applied when a person has fasted for at least 8 hours and 2 hours after the person drinks a liquid containing 75 grams of glucose dissolved in water. The normal glucose level should be within the range of 70 mg/dL to 99 mg/dL for a non-diabetic person using the FPG test, while the glucose level should be within the range of 70 mg/dL to 139 mg/dL for a non-diabetic person using the OGTT [START_REF] Siperstein | The glucose tolerance test: a pitfall in the diagnosis of diabetes mellitus[END_REF]. In the case of low glucose level, for both FPG and OGTT tests the glucose level should be within the range of 0 mg/dL to 70 mg/dL. Similarly, for a high glucose level, readings should be greater than 126 mg/dL in the FPG test, and greater than 140 mg/dL using the OGTT. A blood sugar level outside of the normal range indicates an abnormal glucose concentration. A high level of glucose is referred to as hyperglycemia and a low level of glucose is referred to as hypoglycemia. Property 1 (Glucose level in blood). The blood glucose level defines different stages, such as hyperglycemia, hypoglycemia and normal. We say that the glucose level is low (hypoglycemia) if F P G ∈ 0..69 or OGT T ∈ 0..69, and the glucose level is high (hyperglycemia) if F P G ≥ 126 or OGT T ≥ 200, and the glucose level is normal if F P G ∈ 70 .. 99 or OGT T ∈ 70 .. 139. We classify pre-diabetes to be the range where F P G ∈ 100 .. 125 or OGT T ∈ 140 .. 199.

C. Formalization of the GH System

To develop a virtual biological environment of GH based on formal techniques, we use the Event-B modelling language [START_REF]Modeling in Event-B: System and Software Engineering[END_REF] that supports an incremental refinement to design a complete system in several layers, from an abstract to a concrete specification. Initial model captures the basic behaviour and biological requirements of the GH system in an abstract way. The subsequent refinements are used to introduce αcells and β-cells of the pancreas, functional behaviour of liver to convert and to store the glucose, abnormal conditions of the pancreas, diabetic conditions, and diabetes complications, and blood sugar concentration for assessing diabetes. The developed system results the dynamic behaviours of virtual GH biological environment that covers the both normal and abnormal behaviours (hyperglycemia, hypoglycemia or diabetic complications). A list of safety properties are defined at each incremental level to guarantee the correctness of designed virtual biological environment model for GH. A detail formalization process of the virtual biological environment model is available in [START_REF] Singh | Formalizing the glucose homeostasis mechanism[END_REF].

VI. USABILITY OF ENVIRONMENT MODEL

This section presents usability of environment modelling for developing an IIP as follows:

A. Verifying patient safety in closed-loop

The closed-loop system allows to monitor according to the system requirements as per the physiological needs. Each patient has specific needs according to the diabetic symptoms, which can be diagnosed by using an IIP. In fact, an IIP has configuration parameters that allow to configure the device for each patient by doctors by analyzing the chronicle conditions. To verify at an early stage of the system development, the environment model can be used by developing a close-loop system. Environment models describe normal and abnormal conditions of patients that can be helpful to analyze the IIP requirements and to check consistencies for finding missing requirements. The integration of the environment modelling and IIP allows to evaluate whether the IIP provides an appropriate therapy for diabetes as per the patient needs without delivering excessive insulin.

B. Checking functional requirements

The closed-loop system exposes several conditions for normal and abnormal diabetic conditions, which are represented in (Fig. 3) using a range of situations that occur due to several types of malfunctions. The state of glucose homeostasis is presented as a boolean state to show normal and abnormal states. The insulin delivery mechanism is specified under various conditions. Some behaviour requirements are given as follows: 1) β-cells and α-cells defects cause high plasma glucose level. It is important that insulin must be released in an appropriate amount to stabilize the glucose level. 2) Insulin resistance in cells does not allow to reduce the high plasma glucose level, where an IIP requires to delivery insulin to control the glucose level. 3) Abnormal glucagon release also causes excessive glucagon secretion that maintains the high plasma glucose level. However, the IIP must deliver insulin as per the body requirements. We have discussed various abnormal behaviours of patients. These scenarios must be covered in the environment model and the closed-loop model should provide evidence that the IIP delivers insulin doses whenever they are required by the patient. The insulin delivery process must be coordinated with GH model to ensure required amount of insulin for maintaining the normal glucose level.

C. Analyzing clinical requirements

Clinical requirements depend on the patient needs such as insulin resistance in cell, β-cells defect, α-cells defect, insufficient insulin secretion, insufficient glucagon secretion, excess insulin and excess glucagon secretion. These requirements are common critical conditions, which can vary for each patient because of different physiological needs.

The GH model is presented as abstract as possible to capture all possible scenarios of the natural glucose homeostasis system. Whenever, the functional behaviour of α-cells and β-cells change; or insulin and glucagon releasing behaviour change; or the functional behaviour of natural glucose homeostasis change, the glucose levels, which represents high plasma glucose level or low plasma glucose level will be affected. Moreover, we introduce other abnormal condition details, and blood sugar concentration using stepwise refinement. The present model is still abstract to cop with several major normal and abnormal conditions. For instance, we have not done any special treatment in our model to capture the required time duration to stabilise the normal glucose level after releasing insulin. The timing requirements can vary for each patients and it results in many symptoms, primarily those symptoms result from the delayed, non-physiologic timing of insulin release in relation to high glucose level. The normal and abnormal states of GH model are represented through the abstract behaviour, and α-cells and β-cells release functions requirements. In case of abnormal state of the glucose homeostasis, the IIP delivers the required amount of insulin to maintain the glucose level.

D. Finding essential safety properties

The closed-loop model provides higher assurance for safety and security. The environment based closed-loop modelling approach offers to find ambiguities and inconsistencies in the IIP specification. The abstract representation and set theory allow to software engineers to specify system requirements and desired safety properties. The generated proof obligations and discharging them show the correctness of system requirements according to the defined properties. Any inconsistencies between requirements are identified and fed back to main system requirements. This iterative process allow to find the correct requirements as per defined notions of the environment.

Another benefit of this approach is that the environment model can be reused with other systems, wherever a system requires environment modelling for verification and validation. This environment is always considered as a separate system, which can be further changed as per stakeholder demands for multiple purposes, such as simulation and testing. Each time this environment model can produce a different set of safety properties according to the integration of a new device specification.

VII. CONCLUSION AND FUTURE CHALLENGES

There are several existing clinical models based differential equations and higher order polynomial equations that require significant computation and a large memory for implementation, which cannot be used at the early stage of the system development for developing the closed-loop model for verifying a IIP. In this paper, we have presented a methodology for modelling a biological environment of the GH using simple logical mathematics in an abstract way to simulate the desired behaviour to avoid the mathematical complexity. This is the first computational model based on logical concepts to simulate the GH behaviour in order to analyze the normal and diabetic conditions. The developed model highlights a different aspect of the problem, making different assumptions and establishing different properties concerning the variation in glucose levels, normal and diabetic conditions, and malfunction of biological organs like the liver and pancreas. This is a promising simulated biological environment model that can be used to develop a closed-loop model of the biological environment and IIP. As we know that the FDA has already reported several recalls related to IIP, so our approach may help to identify the possible bugs in early phase of the development life-cycle of IIP. Our most important contribution is that this formal model helps to obtain certification for the medical devices related to the homeostasis system, such as IIP. This environment model can also be used as a diagnostic tool to diagnose or understand patient requirements.