Emiliano Lorini
email: emiliano.lorini@irit.fr

A Logic of Evaluation

We present a logic of evaluation which clarifies the relationship between knowledge, values and preferences of multiple agents in an interactive setting. Evaluation is a fundamental concept for understanding how an ethical agent's decision is affected by her values. We provide a complete axiomatics for the logic and present a dynamic extension by the concept of value expansion. We show that value expansion indirectly affects the agents' preferences by inducing a preference upgrade operation.

INTRODUCTION

An autonomous agent is, by definition, endowed with endogenous motivations, commonly called goals, which determine her preferences, thereby indirectly influencing her decision-making process. Evaluation is a core aspect of agent autonomy. It is the bridge between the agent's goals and preferences through the lens of the agent's knowledge (or beliefs). This aspect is emphasized in [START_REF] Miceli | The role of evaluation in cognition and social interaction[END_REF] in which an agent's evaluation of a situation (outcome, state, etc.) is defined to be a belief of an evaluating agent about the goodness (or usefulness) of the situation with regard to the agent's goals.

The concept of evaluation is paramount for psychological theories of action [START_REF] Gollwitzer | The volitional benefits of planning[END_REF] and emotion [START_REF] Moors | Appraisal Theories of Emotion: State of the Art and Future Development[END_REF] as well as for cognitive theories of knowledge and beliefs [START_REF] Abelson | Difference between belief and knowledge systems[END_REF]. It is also highly relevant for ethical multiagent systems and, more generally, for machine ethics, one of the central areas of AI nowadays [START_REF] Allen | Prolegomena to any future artificial moral agent[END_REF][START_REF] Etzioni | Incorporating Ethics into Artificial Intelligence[END_REF][START_REF] Wallach | Moral Machines: Teaching Robots Right from Wrong[END_REF]. Indeed, as pointed out by [START_REF] Dignum | Responsible Autonomy[END_REF], for an autonomous agent to be ethical and to behave responsibly, some of her goals must reflect values and norms with which she is expected to comply and which take other agents and their welfare into consideration. This includes both abstract values such as justice, fairness, reciprocity and equity and more concrete ones such as "greenhouse gas emissions are reduced" and "social distancing measures are adopted for fighting against covid-19". 1 A typical example of ethical autonomous agent is a robot whose set of values includes the respect for human integrity [START_REF] Winfield | Towards an Ethical Robot: Internal Models, Consequences and Ethical Action Selection[END_REF].

In order to supply her expected functionality, an ethical agent should be capable of computing her preference ordering over the alternatives directly from her values and then use it, together with her knowledge and belief, as input of her decision-making process. This is what Figure 1 good a situation is, the ethical agent makes an epistemic judgment about whether and how much the situation promotes the achievement of her values. Some evaluations are comparative in the sense that the agent's assessment of the goodness of a certain situation is made in relation to the goodness of another situation, depending on which and how many values are satisfied in each of them. 2This view of evaluation is in line with the philosophical doctrine of pluralistic consequentialism [START_REF] Sen | Well-Being, Agency and Freedom: The Dewey Lectures 1984[END_REF][START_REF] Sen | On Ethics and Economics[END_REF] and with recent theories of reason-based choice [START_REF] Dietrich | A reason-based theory of rational choice[END_REF][START_REF] Dietrich | What matters and how it matters: A choice-theoretic representation of moral theories[END_REF] according to which an ethical agent has to weigh different, and sometimes conflicting, values and properties to assess the relative goodness of a given option or alternative in her choice set. It is also in accord with existing computational models of ethical deliberation and planning in robotics [START_REF] Arkin | Moral Decision Making in Autonomous Systems: Enforcement, Moral Emotions, Dignity, Trust, and Deception[END_REF][START_REF] Vanderelst | An architecture for ethical robots inspired by the simulation theory of cognition[END_REF] and in AI [START_REF] Ajmeri | Elessar: Ethics in Norm-Aware Agents[END_REF][START_REF] Cranefield | No Pizza for You: Value-based Plan Selection in BDI Agents[END_REF][START_REF] Rodriguez-Soto | A Structural Solution to Sequential Moral Dilemmas[END_REF][START_REF] Serramia | Moral Values in Norm Decision Making[END_REF] in which the influence of values on decision and the evaluative component are made explicit.

The aim of this paper is to introduce a logic of evaluation which helps to clarify the relationship between knowledge, values and preferences of multiple ethical agents in a multi-agent setting. The interest of having a multi-agent account of values and evaluation lies in the possibility of modeling interactive situations in which: (i) an agent's value may concern other agents' well-being, safety and integrity, and (ii) agents' decisions are interdependent so that the possibility for an agent to achieve her values may depend on what other agents decide to do. The development of a language with a suitable syntax and semantics for specifying value preferences of ethical agents in the context of sociotechnical systems (STSs) was recently put forward by Murukannaiah et al. [START_REF] Murukannaiah | New Foundations of Ethical Multiagent Systems[END_REF] as a research challenge. In this paper, we make a first step to meet this challenge. We are not the first to propose a logical analysis of ethical reasoning. There are approaches based on preference logic [START_REF] Hansson | The Structure of Values and Norms[END_REF], event calculus (ASP) [START_REF] Berreby | A Declarative Modular Framework for Representing and Applying Ethical Principles[END_REF], temporal-epistemic logic [START_REF] Lorini | A logic for reasoning about moral agents[END_REF], BDI (belief, desire, intention) agent language [START_REF] Dennis | Formal verification of ethical choices in autonomous systems[END_REF] and classical higher-order logic (HOL) [START_REF] Benzmüller | Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support[END_REF]. Nonetheless, none of them has taken the concept of evaluation into account. The latter, we believe, is crucial for elucidating the connection between values and preferences.

The paper is organized as follows. In Section 2, we discuss the conceptual background with special emphasis on the notion of value. In Section 3, we present the language and the semantics of our logic of evaluation, while in Section 4 we concentrate on the notion of choice, in connection with knowledge and value, and show how it can be expressed in the language. Section 5 is devoted to present complete axiomatics for our logic. In Section 6, we move from a static to a dynamic perspective by extending our logic with value expansion operators. We show that value expansion indirectly affects an agent's preferences by inducing a preference upgrade operation in the sense of [START_REF] Van Benthem | Dynamic logic of preference upgrade[END_REF]. A selection of abbreviated proofs is given in the technical annex at the end of the paper.

CONCEPTUAL BACKGROUND

We conceive evaluation as the computation of a preference ordering over a set of epistemic alternatives from a set of actual values. The evaluating agent determines whether a situation that she considers possible is at least as good as another situation that she considers possible in the light of which -and eventually how many -of her values are satisfied in each situation. The evaluation criterion we study in the paper is purely qualitative. We assume that an agent will consider her epistemic alternative v at least as good as her epistemic alternative w if and only if the set of her values satisfied at w is included in the set of her values satisfied at v.

Evaluation is also leveraged by the agent to identify ideal situations in her set of epistemic alternatives, namely, those alternatives at which all her values are satisfied. Clearly, if the agent has conflicting values, i.e., values that cannot be concomitantly satisfied, then the set of ideal situations is empty since there is no epistemic alternative at which two conflicting values are satisfied. In this case, the agent can only identify subideal situations, i.e., situations at which only some of her values but not all of them are satisfied. 3Our logic of evaluation is grounded on the three primitive concepts of knowledge, value and preference, in accordance with the conceptual framework depicted in Figure 1. They will be reflected in the language of the logic by corresponding modal operators of the form K i (knowledge), V i (value) and [⪯ i ] (preference), where i is an agent identifier. The operator K i captures the usual S5 notion of knowledge for logically omniscient and fully introspective agents [START_REF] Fagin | Reasoning about Knowledge[END_REF]. The operator [⪯ i ] is a standard S4 betterness modality [START_REF] Van Benthem | Dynamic logic of preference upgrade[END_REF] reflecting a partial order over agent i's set of epistemic alternatives. The operator V i captures a logically weak notion of value whose only positive property is closure under logical equivalence. We see the latter as the minimal property for values. This assumption is justified by the fact that the notion of value we study is normative (in opposition to descriptive), in the sense that it pertains to a rational resource-unbounded agent who is capable of immediately detaching a new value that ψ from her value that φ and her knowledge that φ and ψ have the same extension.

The reason why the value operator is parameterized by an agent identifier i is that values are assumed to be agent-relative. This does not conflict with the objectivist view of morality, namely the view that all agents start from the same set of ultimate ethical principles which determine the goodness or rightness of any state of affairs or action. 4 The variability of values between two agents may stem from the difference between their epistemic states, despite the fact that the two agents share the same set of ultimate ethical principles. For example, suppose Ann and Bob share the ultimate ethical principle that "unfair acts are deplorable". Nonetheless, they have different interpretations of what 'fairness' means, given their different epistemic states. For instance, Ann is a fervent utilitarian, while Bob is Rawlsian: according to Ann an act is fair if and only if it is aimed at maximizing collective utility while, according to Bob, an act is fair if and only if it is aimed at maximizing utility of the most disadvantaged person. Consequently, Ann and Bob have divergent values about implementation of fairness.

The first negative property of values we want to discuss is that they are not necessarily closed under conjunction. Suppose Mary is organizing a party. Her two dear friends Ann and Bob have recently split up and are actually in a bad relationship. According to Mary, inviting Ann and inviting Bob are both valuable options, since it would be unfair to exclude one of her dearest friends from the party. Nonetheless, if Ann and Bob meet at the party, they will find themselves in an embarrassing situation which may negatively affect the other guests. For this reason, according to Mary, inviting both Ann and Bob to the party is not a valuable option. This example shows that an agent can have conflicting values, without having the value of complying with both of them. In formal terms, it is reasonable to assume that the following formula should be satisfiable:

V i φ ∧ V i ψ ∧ ¬V i (φ ∧ ψ ).
A further negative property of values is that they are not necessarily closed under disjunction. Suppose Ann is a doctor working at the hospital intensive care unit (ICU). A first patient in a critical situation arrives at the unit. Saving her/his life is a value for Ann, since her commitment is to save people's lives. Few minutes later a second patient is taken to the unit. Saving the second patient's life is also a value for Ann. In this situation, Ann does not have the disjunctive value to save the first's patient life or to save the second's patient life. Indeed, she is motivated to save the lives of both patients. This illustrates that an agent can have the value that φ and the value that ψ , -eventually coupled with the conjunctive value that φ ∧ψ -, without having the disjunctive value that φ ∨ψ . In other words, the following formula should be satisfiable:

V i φ ∧ V i ψ ∧ ¬V i (φ ∨ ψ ).
Note that the satisfiability of the previous formula should be independent from the fact that agent i knows that φ and ψ cannot occur together. For example, Ann can still want to save the lives of both patients, notwithstanding her knowledge that she is unable to do so (e.g., because the ICU is not equipped with two automatic ventilators for covid-19 treatment).

Values do not satisfy weakening either. Specifically, the fact that an agent has the conjunctive value that φ and ψ does not necessarily imply that she has the value that φ. In other words, it is reasonable to assume that the following formula should be satisfiable:

V i (φ ∧ ψ ) ∧ ¬V i φ.
For example, suppose Mary and Bob are discussing about the actions for schools during the covid-19 outbreak. According to Mary, children should return to school (φ) with application of social distancing and the use of masks (ψ ). This does not imply that, according to Mary, children should return to school regardless of the fact that social distancing is applied and masks are used.

More generally, since values do not satisfy closure under disjunction or weakening, they are not closed under logical consequence. This means that the fact that ψ is a logical consequence of φ and an agent considers φ a valuable state of affairs does not necessarily imply that the agent considers ψ a valuable state of affairs.

We conclude this section with a remark on the concept of realism for values. The question is whether a rational agent can have values which are incompatible with her knowledge and beliefs. For example, may a rational agent be a fervent pacifist, notwithstanding her knowledge that aggressivity is a natural disposition of human nature and human conflict is unavoidable? In this paper, we study two different logics: the logic of (possibly non-realistic) values and the logic of realistic values. The latter logic assumes that rational agents instantaneously discard non-realistic values. The former is less demanding, as it is prone to accept that an agent may have utopian values in her mind and simply filter them out at a subsequent stage. This is in line with [START_REF] Castelfranchi | The role of beliefs in goal dynamics: prolegomena to a constructive theory of intentions[END_REF], according to whom non-realistic goals and values are not actively pursued and are not taken into consideration during the evaluation process, thereby having no influence on preference formation and decision-making.

LOGICAL FRAMEWORK

In this section, we first present a multi-agent language for describing the relationship between values, knowledge and preferences of multiple agents. Then, we introduce the notion of evaluative model and show how to interpret our language relative to it.

Let Atm be a countable infinite set of atomic propositions and let Agt be a finite set of agents. We define the language L by the following grammar:

φ ::= p | id i | ¬φ | φ 1 ∧ φ 2 | K i φ | V i φ | [⪯ i ]φ,
where p ranges over Atm and i ranges over Agt.

The formula K i φ has to be read "agent i knows that φ", while V i φ has to be read "agent i considers φ a valuable state of affairs" or, simply, "agent i has the value that φ". The formula [⪯ i ]φ has to be read "φ is true at all states that according to agent i are at least as good as the current one". Finally, the special atomic formula id i is meant to stand for "the actual world is an ideal world for agent i". The dual of the epistemic operator K i and of the preference operator [⪯ i ] are defined as usual:

K i φ = def ¬K i ¬φ and ⟨⪯ i ⟩φ = def ¬[⪯ i ]¬φ.
The extended set of atomic formulas Atm + is defined as follows:

Atm + = Atm ∪ i ∈Agt {id i }.
For notational convenience, elements of Atm + are noted x, y, . . . The following definition introduces evaluative models.

Definition 3.1 (Evaluative model

). An evaluative model (EM) is a tuple M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) where:

• W is a non-empty set of worlds or states,

• ≡ i is an equivalence relation on W , • N : Agt × W -→ 2 2 W is a neighbourhood function, • ⪯ i is a partial preorder on W , • V : W -→ 2 Atm + is a valuation function,
and that satisfies the following constraints, for every w, v ∈ W , X ⊆ W and i ∈ Agt:

(C1) ⪯ i ⊆ ≡ i , (C2) if X ∈ N (i, w) then X ⊆ ≡ i (w), (C3) if w ≡ i v then N (i, w) = N (i, v), (C4) w ⪯ i v if and only if Sat M (i, w) ⊆ Sat M (i, v), (C5) id i ∈ V (w) if and only if Sat M (i, w) = N (i, w), with ≡ i (w) = {v ∈ W : w ≡ i v} and Sat M (i, w) = {X ∈ N (i, w) : w ∈ X }.
The class of EMs is denoted by M.

The equivalence relation ≡ i is an epistemic indistinguishability relation. In particular, for each w ∈ W , ≡ i (w) is agent i's information set at world w. The neighbourhood function specifies the agents' values at each world. Specifically, if X ∈ N (i, w) then X is a value of agent i at world w, i.e., at w agent i considers X a valuable (or ideal) state of affairs. The relation ⪯ i specifies a preference ordering for agent i over the possible worlds. Sat M (i, w) is the set of agent i's values that are satisfied at w. According to Constraint C1, an agent's preference ordering is relative to worlds in her information set. Similarly, according to Constraint C2, an agent's value is relative to worlds in her information set. Constraint C3 captures introspection for values, i.e., an agent's set of values should be the same in all worlds in the agent's information set. Constraints C4 and C5 are the central properties of evaluation. They are used to compute an agent's preference ordering and set of ideal worlds from her set of values. According to C4, world v is for agent i at least as good as world w if and only if the set of i's values satisfied at w is included in the set of i's values satisfied at v. 5 According to C5, a world is ideal for an agent if and only if it satisfies all her values. The set of worlds that agent i considers ideal at world w of model M (aka i's set of subjectively ideal worlds at w of M) is:

I M (i, w) = v ∈ ≡ i (w) : id i ∈ V (v) . Since ≡ i is an equivalence relation, if w ≡ i v then I M (i, w) = I M (i, v).
Moreover, thanks to Constraints C3 and C5, if v ∈ I (i, w) then v ∈ X ∈N (i,w ) X . This means that an agent's subjectively ideal world is a world that satisfies all actual values of the agent.

We introduce the usual notation for strict preference, indifference and incomparability:

≺ i = {(w, v) ∈ W × W : w ⪯ i v and v ⪯̸ i w }, ⪰ i = {(w, v) ∈ W × W : v ⪯ i w }, ≻ i = {(w, v) ∈ W × W : w ⪰ i v and v ⪰̸ i w }, ∼ i = {(w, v) ∈ W × W : w ⪯ i v and v ⪯ i w }, || i = {(w, v) ∈ W × W : w ⪯̸ i v and v ⪯̸ i w }.
The following definition precisely defines the realism condition for values we briefly discussed in Section 2. Definition 3.2 (Value realism). Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) be an EM. We say that M satisfies value realism (VR) if and only if, for every w ∈ W , X ⊆ W and i ∈ Agt,

if X ∈ N (i, w) then ≡ i (w) ∩ X ∅.
As we pointed out in Section 2, an agent can have conflicting values. The following definition restricts to the limit case in which an agent's values are globally consistent, i.e., there exists at least one subjectively ideal world for the agent. Definition 3.3 (Value consistency). Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) be an EM. We say that M satisfies value consistency (VC) if and only if, for every w ∈ W and i ∈ Agt, we have I M (i, w) ∅.

Formulas of the language L are interpreted with respect a pointed evaluative model, i.e., an evaluative model and a world in it.

Definition 3.4 (Satisfaction relation). Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V
) be an EM and let w ∈ W . Then:

M, w |= x ⇐⇒ x ∈ V (w), M, w |= ¬φ ⇐⇒ M, w ̸ |= φ, M, w |= φ ∧ ψ ⇐⇒ M, w |= φ and M, w |= ψ , M, w |= K i φ ⇐⇒ ∀v ∈ W : if w ≡ i v then M, v |= φ, M, w |= V i φ ⇐⇒ ||φ|| M i,w ∈ N (i, w), M, w |= [⪯ i ]φ ⇐⇒ ∀v ∈ W : if w ⪯ i v then M, v |= φ, with ||φ|| M i,w = {v ∈ W : M, v |= φ}∩ ≡ i (w).
Note that the interpretation of agent i's value operator V i is relative to i's subjective truth set for φ (i.e., ||φ|| M i,w ), namely, the worlds in i's information set in which φ is true. 6 For every X ⊆ {VR, VC}, we denote by M X the class of EMs satisfying every property in X , where VR and VC are, respectively, the value realism and value consistency condition of Definitions 3.2 and 3.3. Since value consistency implies value realism, we have M VC ⊆ M VR . Clearly, M ∅ = M. For each model class M X , notions of validity and satisfiability for formulas in L relative to M X are defined in the usual way. We write |= M X φ to denote the fact that φ is valid relative to the class M X .

CHOICE OPERATOR

In this section we define a rational choice operator and study its relationship with the notions of value and knowledge. As a preliminary step towards this definition, we introduce the following notion of best alternative as a world in the agent's information set which is either at least as good or incomparable with any other world in the agent's information set. Definition 4.1 (Best alternatives). Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) be an EM, let i ∈ Agt and let w ∈ W . Agent i's set of best alternatives at w is defined as follows:

Best(i, w) = v ∈≡ i (w) : ∀u ∈≡ i (w), u ⪯ i v or u || i v .
A candidate choice for agent i is a ∼ i -equivalence class relative to agent i's set of best alternatives. Definition 4.2 (Candidate choices). Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) be an EM, let i ∈ Agt and let w ∈ W . Agent i's set of candidate choices at w, denoted by Choice(i, w), is the partition of the set Best(i, w) induced by the indifference relation ∼ i . 6 A similar interpretation for the notion of explicit belief is used in [START_REF] Balbiani | A Logical Theory of Belief Dynamics for Resource-Bounded Agents[END_REF].

Intuitively, a candidate choice is a state of affairs that it would be rational for an agent to try to attain.

The previous notion of candidate choice is syntactically expressed through the following abbrevation:

C i φ = def K i (φ ∧ [⪯ i ]φ),
where C i φ has to be read "agent i can rationally choose that φ".

As the following proposition highlights, the operator C i correctly represents the idea that an agent can rationally choose that φ if, from her point of view, φ is a consequence of one her candidate choices.

Proposition 4.3. Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) be an EM, let i ∈ Agt and let w ∈ W . Then, M, w |= C i φ if and only if ∃X ∈ Choice(i, w) such that X ⊆ ||φ|| M i,w .
It is worth noting that, under the assumption of value consistency, the choice operator C i becomes normal. Indeed, we have the following validity for the class M VC :

|= M VC C i φ ∧ C i (φ → ψ ) → C i ψ (1)
Moreover, the rule of necessitation is admissible for the class M:

If |= M φ then |= M C i φ (2)
The reason for the normality of the operator C i in M VC is that the set of candidate choices Choice(i, w) is a singleton in every model of this class. Specifically, Choice(i, w) only includes the set of ideal worlds which satisfy all agent i's values at w. Therefore, under the value consistency assumption, an agent has exactly one candidate choice, hence the formula C i φ can simply be read "agent i rationally chooses that φ". The following example illustrates the interrelation between the concepts of knowledge, value and choice.

Example 4.4. There are two mobile robots 1 and 2 who have to collect objects in a room and an obstacle obstructing the access to the battery charger station. Each robot can decide either to remove the obstacle or to exploit the other robot by letting it remove the obstacle. In order to formalize the example, we assume that the set Atm includes the following atomic propositions with their associated meanings: r 1 ("robot 1 removes the obstacle"), r 2 ("robot 2 removes the obstacle"), c 1 ("robot 1 charges its battery"), c 2 ("robot 2 charges its battery"), f ("the access to the battery charger station is free of obstacles"), e 1 ("robot e 1 is exploited") and e 2 ("robot 2 is exploited"). Each robot is motivated by two values, namely, the value of preserving its own well-functioning by keeping its battery charged and the value of refraining from exploiting the other robot. This is captured by the following abbreviation:

φ 1 = def V 1 c 1 ∧ V 2 c 2 ∧ V 1 ¬e 2 ∧ V 1 ¬e 1 .
Since each robot has no additional values, it knows that a situation in which it keeps its battery charged without exploiting the other robot is an ideal situation:

φ 2 = def K 1 (c 1 ∧ ¬e 2 ) → id 1 ∧ K 2 (c 2 ∧ ¬e 1 ) → id 2 .
Furthermore, each robot knows that the only way to charge a battery is by freeing the access to the battery charger station, and that the only way to free the access to the battery charger station is by one of them removing the obstacle:

φ 3 = def i ∈ {1,2} K i (c 1 ∨ c 2 ) → f ∧ K i f → (r 1 ∨ r 2 ) .
Finally, each robot knows that if one removes the obstactle while the other does not do it, then this counts as an act of exploitation:

φ 4 = def i ∈ {1,2} K i (r 1 ∧ ¬r 2 ) → e 1 ∧ (r 2 ∧ ¬r 1 ) → e 2 .
It is routine exercise to check that, under the previous four hypotheses and the assumption that the robots' values are consistent, each robot can rationally choose to remove the obstacle, but it cannot rationally choose to refrain from doing it:

|= M VC (φ 1 ∧ φ 2 ∧ φ 3 ∧ φ 4 ) → i ∈ {1,2} (C i r i ∧ ¬C i ¬r i ).
If, moreover, both robots have knowledge about the four hypotheses, then they also have knowledge about each other's choices:

|= M VC i ∈ {1,2} K i (φ 1 ∧ φ 2 ∧ φ 3 ∧ φ 4 ) → K i i ∈ {1,2} (C i r i ∧ ¬C i ¬r i ) .

AXIOMATIZATION

In this section, we present an axiomatics for the set of validities of the language L. In order to prove its completeness relative to the semantics defined in Section 3, it is useful to define a weaker semantics based on quasi-models.

Definition 5.1 (Quasi-model).

A quasi-evaluative model (quasi-EM) is like an EM, as defined in Definition 3.1, except that Constraints C4 and C5 are replaced by the following four constraints, for every w, v ∈ W , X ⊆ W and i ∈ Agt:

(C6) if w ⪯ i v then Sat M (i, w) ⊆ Sat M (i, v), (C7) if id i ∈ V (w) then Sat M (i, w) = N (i, w), (C8) if w ≡ i v and id i ∈ V (v) then w ⪯ i v, (C9) if w ⪯ i v and id i ∈ V (w) then id i ∈ V (v).
For every X ⊆ {VR, VC}, the class of quasi-EMs satisfying each semantic property in X is denoted by QM X .

It is routine exercise to verify that every EM is also a quasi-EM. Truth conditions of formulas in L relative to quasi-EMs are just like truth conditions relative to EMs (Definition 3.4). For every X ⊆ {VR, VC}, notions of validity and satisfiability relative to the classes QM X are also defined in the usual way.

As the following theorem highlights, the language L is not expressive enough to distinguish the semantics based on quasi-models from the semantics based on models. Theorem 5.2. Let φ ∈ L and X ⊆ {VR, VC}. Then, φ is satisfiable for the class M X if and only if it is satisfiable for the class QM X .

In the following definition, we precisely define a family of logics of evaluation. We will show that they are sound and complete relative to both the quasi-model and the model semantics.

Definition 5.3 (Logic). We define LEV (Logic of Evaluation) to be the extension of classical propositional logic given by the following axioms and rule of inference:

K i φ ∧ K i (φ → ψ ) → K i ψ (K K i ) K i φ → φ (T K i ) K i φ → K i K i φ (4 K i ) φ → K i K i φ (B K i ) [⪯ i ]φ ∧ [⪯ i ](φ → ψ ) → [⪯ i ]ψ (K [⪯ i ] ) [⪯ i ]φ → φ (T [⪯ i ] ) [⪯ i ]φ → [⪯ i ][⪯ i ]φ (4 [⪯ i ] ) K i φ → [⪯ i ]φ (Mix K i ,[⪯ i ] ) K i (φ ↔ ψ ) → (V i φ → V i ψ ) (Mix1 K i ,V i ) V i φ → K i V i φ (Mix2 K i ,V i ) (V i φ ∧ φ) → [⪯ i ]φ (Mix V i ,[⪯ i ] ) (V i φ ∧ id i ) → φ (Mix V i ,id i ) [⪯ i ]φ → K i (id i → φ) (Mix1 [⪯ i ],id i ) id i → [⪯ i ]id i (Mix2 [⪯ i ],id i ) φ K i φ (Nec K i )
For every X ⊆ {Real V i , Cons V i }, we define LEV X to be the extension of the logic LEV by each axiom in X , where Real V i and Cons V i are the following axioms:

K i φ → ¬V i ¬φ (Real V i ) K i id i (Cons V i )
Note that the base logic LEV is the same as LEV ∅ . For each logic LEV X , notions of theorem and consistency are defined in the usual way. We denote by ⊢ LEV X φ the fact that φ is a theorem of LEV X .

We have all S5-principles for the epistemic operator K i (Axioms K K i , T K i , 4 K i and B K i , and Rule Nec K i ) and the S4-principles for the betterness operator

[⪯ i ] (Axioms K [⪯ i ] , T [⪯ i ] and 4 [⪯ i ] ). Ac- cording to Axiom Mix K i ,[⪯ i ]
, if an agent knows that φ, then φ has to be true at all worlds which are for the agent at least as good as the current one. Indeed, an agent's preference is relative to her epistemic state. Axiom Mix1 K i ,V i is a sort of 'co-extensionality' principle for values: if φ and ψ are equivalent (co-extensional) according to agent i, then i has the value that φ if and only if she has value that ψ . According to Axiom Mix2 K i ,V i , an agent has introspection over her values. Axioms Mix V i ,[⪯ i ] and Mix V i ,id i are the principles relating values with preferences. According to Mix V i ,[⪯ i ] , if the actual world satisfies a certain value, then all better worlds should also satisfy it. According to Mix V i ,id i , if the actual world is an ideal world, then it should satisfy all values. According to Axiom Mix1 [⪯ i ],id i , if φ is true at all better worlds for the agent then, according to the agent, is true at all ideal worlds. Finally, according to Axiom Mix2 [⪯ i ],id i , all better worlds of an ideal world are also ideal worlds. Axioms Real V i and Cons V i are, respectively, the value realism and the value consistency axiom.

The following rule of necessitation for the preference operator and rule of equivalence for the value operator are derivable in LEV by means of Axiom

Mix K i ,[⪯ i ] , Axiom Mix1 K i ,V i and Rule Nec K i : φ [⪯ i ]φ (3) φ ↔ ψ V i φ ↔ V i ψ (4)
Let f c be the correspondence function associating each axiom in {Real V i , Cons V i } to its corresponding semantic property in {VR, VC}:

f c (Real V i ) = VR, f c (Cons V i ) = VC.
Our first result is about soundness and completeness relative to quasi-models. Theorem 5.4. Let X ⊆ {Real V i , Cons V i }. Then, the logic LEV X is sound and complete for the class QM {f c (x ):x ∈X } .

Soundness and completeness relative to models is a direct corollary of Theorem 5.2 and Theorem 5.4. Corollary 5.5. Let X ⊆ {Real V i , Cons V i }. Then, the logic LEV X is sound and complete for the class M {f c (x ):x ∈X } .

VALUE EXPANSION

So far, we have only considered the static aspects of evaluation. In this section, we look at the dynamic aspects by exploring the connection between value change and preference change. We extend the language L introduced in Section 3 by operators of the form [+ J φ], which are used to describe the consequences of a value expansion operation by all agents in the coalition J . We call L + (Atm, Agt) the resulting language and define it by the following grammar:

φ ::= p | ¬φ | φ 1 ∧ φ 2 | K i φ | V i φ | [⪯ i ]φ | [+ J ψ ]φ,
where p ranges over Atm, i ranges over Agt and J ranges over the set of coalitions 2 Agt * = 2 Agt \ {∅}. The new formula [+ J ψ ]φ is meant to stand for "φ holds, after every agent in J has expanded her set of values with ψ ". We assume that value expansion operations are public, i.e., if an agent expands her set of values with ψ , then this is common knowledge among all agents. This assumption could be relaxed by using a variant of event models [START_REF] Baltag | The Logic of Public Announcements, Common Knowledge and Private Suspicions[END_REF] for our semantics, which would allow us to model private and semi-private value change operations. The following definition provides truth conditions for this new type of formulas. Definition 6.1 (Satisfaction relation (cont.)). Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) be an EM and let w ∈ W . Then:

M, w |= [+ J ψ ]φ ⇐⇒ M + J ψ , w |= φ,
where M + J ψ = (W + J ψ , (≡

+ J ψ i ) i ∈Agt , N + J ψ , (⪯ + J ψ i ) i ∈Agt , V + J ψ )
such that W + J ψ = W , and for every i ∈ Agt and w ∈ W :

≡ + J ψ i =≡ i , N + J ψ (i, w) = N (i, w) ∪ {||ψ || M i,w } if i ∈ J , N (i, w) if i J , ⪯ + J ψ i = ⪯ i \ (w, v) : M, w |= ψ and M, v |= ¬ψ if i ∈ J , ⪯ + J ψ i =⪯ i if i J , V + J ψ (w) = V (w) \ id i ∈ Atm + : w ||ψ || M i,w and i ∈ J .
The value expansion operation + J ψ only affects the mental attitudes of the agents in J , while keeping unchanged the mental attitudes of the agents outside J . Specifically, for every agent i in J , (i) it extends i's value set with ψ , (ii) it upgrades i's preference relation by removing from i's information set all preferences of a ψ -world over a ¬ψ -world and, finally, (iii) it shrinks i's set of ideal worlds to ψ -worlds. This update operation is well-defined since it preserves the properties of the model the class M. Proposition 6.2. Let ψ ∈ L + and J ∈ 2 Agt * . Then, if M ∈ M then M + J ψ ∈ M.

We leave for future work the definition of variants of the value expansion operation for the model classes M VR and M VC . Just notice that, in order to preserve value realism, it would be necessary to make the execution of the update operation dependent on the satisfaction of the condition K i ψ . In other words, an agent in J will expand her values withψ , only ifψ is consistent with her knowledge. In order to preserve value consistency, the update operation should be made subject to the satisfaction of the condition K i (ψ ∧ id i ). In other words, for an agent in J to expand her set of values with ψ , ψ has to be consistent with i's set of (envisaged) ideal situations.

It is time to define the the logic DLEV (Dynamic LEV) which extends the logic LEV by the dynamic operators [+ J ψ ]. Definition 6.3. We define DLEV to be the extension of the logic LEV of Definition 5.3 generated by the following reduction axioms for the dynamic operators [+ J ψ ]:

[+ J ψ ]p ↔p (Red + J ψ ,p ) [+ J ψ ]¬φ ↔¬[+ J ψ ]φ (Red + J ψ ,¬ ) [+ J ψ ](φ 1 ∧ φ 2 ) ↔([+ J ψ ]φ 1 ∧ [+ J ψ ]φ 2 ) (Red + J ψ ,∧ ) [+ J ψ ]K i φ ↔K i [+ J ψ ]φ (Red + J ψ ,K i ) [+ J ψ ]V i φ ↔ V i [+ J ψ ]φ∨ K i (ψ ↔ [+ J ψ ]φ) if i ∈ J (Red1 + J ψ ,V i ) [+ J ψ ]V i φ ↔V i [+ J ψ ]φ if i J (Red2 + J ψ ,V i ) [+ J ψ ][⪯ i ]φ ↔ ψ → [⪯ i ](ψ → [+ J ψ ]φ) ∧ ¬ψ → [⪯ i ][+ J ψ ]φ if i ∈ J (Red1 + J ψ ,[⪯ i ] ) [+ J ψ ][⪯ i ]φ ↔[⪯ i ][+ J ψ ]φ if i J (Red2 + J ψ ,[⪯ i ] ) [+ J ψ ]id i ↔(id i ∧ ψ ) if i ∈ J (Red1 + J ψ ,id i ) [+ J ψ ]id i ↔id i if i J (Red2 + J ψ ,id i )
and the following rule of inference:

ψ 1 ↔ ψ 2 φ ↔ φ[ψ 1 /ψ 2 ] (RRE)
It is routine exercise to verify that the equivalences in Definition 6.3 are valid for class M and that Rule RRE preserves validity. The completeness of DLEV for this class of models follows from Theorem 5.5, in view of the fact that the reduction axioms and the rule of replacement of proved equivalents can be used to find, for any L + -formula, a provably equivalent L-formula. Theorem 6.4. The logic DLEV is sound and complete for the class M.

We have presented a logical analysis of both the static and the dynamic aspects of evaluation with the support of a multimodal language for knowledge, values and preferences. Moreover, we have provided sound and complete axiomatics for a family of logics of evaluation.

The evaluation criterion we have studied is purely qualitative. It is based on the idea that, for a world v to be at least as good another world w, the set of values satisfied at w should be included in the set of values satisfied at v. Future work will be devoted to study a variant of the logic LEV based on the following quantitative criterion:

w ⪯ i v if and only if |Sat M (i, w)| ≤ |Sat M (i, v)|.
This alternative criterion makes the preference ordering ⪯ i complete and only works under the assumptions that an agent's value set is countable and that the agent's values have all the same weight. Future work will also be devoted to study further types of value change operation having an indirect influence on preferences including value forgetting -which removes a value from an agent's value set -, and value revision -which expands the agent's value set first and then restores global consistency of the agent's value set -. This latter operation is particularly relevant for the model class M VC .

A more long-term objective is to introduce a variant of the logic of evaluation in which values are graded (i.e., an agent can have values with different weight or priority) and the preference ordering over the worlds in built by taking the values' priorities into account.

We also plan to compare the notion of choice in the seeing to it that (STIT) logic [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF][START_REF] Horty | Agency and Deontic Logic[END_REF][START_REF] Lorini | Temporal STIT logic and its application to normative reasoning[END_REF] with the notion we defined in Section 4. While in STIT choices are given as primitives, in our approach they are computed from values.

Last but not least, we plan to study decidability and complexity of satisfiability checking for the three logics LEV, LEV {Real Vi } and LEV {Cons Vi } . Concerning decidability, we believe we can use filtration techniques to prove it. The limitation of filtration is that, by using it for satisfiability checking, one has to guess a model exponential in the size of the formula to be checked. Thus, by filtration argument, we could only prove that satisfiability checking is in NEXPTIME. Our conjecture is that satisfiability checking for our logics is EXPTIME-complete. It is certaintly EXPTIME-hard since, given Constraint C1 in Definition 3.1, the S5-modality K i plays the role of the universal modality with respect to the S4modality [⪯ i ]. As shown in [START_REF] Hemaspaandra | The Price of Universality[END_REF], adding the universal modality to a multimodal logic with independent modalities such as [⪯ i ] causes EXPTIME-hardness.

A SELECTED PROOFS A.1 Proof of Theorem 5.2

Proof. The left-to-right direction is trivial since every EM is also a quasi-EM.

In order to prove the right-to-left direction, we start with a quasi-EM satisfying φ and transform it to obtain an EM which satisfies the same formulas as the original model. Let M = (W , (≡ i ) i ∈Agt , N , (⪯ i ) i ∈Agt , V ) be a quasi-EM and w ∈ W such that M, w |= φ.

We define the structure M ′ = (W ′ , (≡ ′ i ) i ∈Agt , N ′ , (⪯ ′ i ) i ∈Agt , V ′ ) as follows:

• W ′ = {w 1 : w ∈ W } ∪ {w 2 : w ∈ W };

• for every x, y ∈ {1, 2} and w x , v y ∈ W ′ , w x ≡ ′ i v y if and only if w ≡ iv; • for every x, y ∈ {1, 2} and w x , v y ∈ W ′ , w x ⪯ ′ i v y if and only if: -x = y and w ⪯ i v, or v ∈ I M (i, w); • for every x ∈ {1, 2} and w x ∈ W ′ , V ′ (w x ) = V (w); • for every x ∈ {1, 2} and w x ∈ W ′ , N ′ (i, w x ) = {w 1 : w ∈ X } ∪ {w 2 : w ∈ X } : X ∈ N (i, w) ∪ v y ∈≡ i (w x ) and v y I M ′ (i,w x ) ⪯ ′ (v y ) ∪ I M ′ (i, w x ) .

The first thing to verify is that M ′ is an EM. It is routine exercise to check that every ≡ ′ i is an equivalence relation and that every ⪯ ′ i is a partial preorder. Clearly, it satisfies Constraints C1, C2 and C3 in Definition 3.1 since M satisfies them too. Let us prove that it satisfies Constraint C4. We distinguish two cases: (Case 1) w x I M ′ (i, w x ), and (Case 2) w x ∈ I M ′ (i, w x ). Case 1. We first prove the left-to-right direction. Suppose w x ⪯ ′ i v y . By definition of ⪯ ′ i , we have (i) (x = y and w ⪯ i v or (ii) v ∈ I M (i, w). Since M is a quasi-EM which satisfies Constraints C3, C6 and C7, if v ∈ I M (i, w) then Sat M (i, v) = N (i, v) = N (i, w), and if w ⪯ i v then Sat M (i, w) ⊆ Sat M (i, v). Thus, Sat M (i, w) ⊆ Sat M (i, v). By construction of M ′ , the fact that w x ⪯ ′ i v y , the transitivity of ⪯ ′ and the fact that Sat M (i, w) ⊆ Sat M (i, v), both (i) and (ii) imply Sat M ′ (i, w x ) ⊆ Sat M ′ (i, v y ).

As for the right-to-left direction, suppose v y ⪯ ′ i (w x ). By definitions of ⪯ i and V ′ , the latter implies that v y I M ′ (i, w x ). Thus, v y ⪯ ′ i (w x ) ∪ I M ′ (i, w x ) . Since w x I M ′ (i, w x ), by definition of N ′ , we have ⪯ ′ i (w x ) ∪ I ′ (i, w x ) ∈ N ′ (w x ). Moreover, w x ∈⪯ ′ i (w x ). Therefore, Sat M ′ (i, w x ) ⊈ Sat M ′ (i, v y ). Consequently, Sat M ′ (i, w x ) ⊆ Sat M ′ (i, v y ) implies w x ⪯ i v y .

Case 2. As for the left-to-right direction, suppose w x ⪯ ′ i v y . The latter means that (i) x = y and w ⪯ i v, or (ii) v ∈ I M (i, w). Suppose (i). Since M is a quasi-EM which satisfies Constraint C9, by definition of V ′ and the fact that w x ∈ I M ′ (i, w x ), we have v ∈ I M (i, w). Thus, both (i) and (ii) imply w ∈ I M (i, w) and v ∈ I M (i, w). Hence, by construction of M ′ and the fact that M is a quasi-EM which satisfies Constraints C3 and C7, we have Sat M ′ (i, w x ) = Sat M ′ (i, v y ).

As for the right-to-left direction, suppose v 1 ⪯ ′ i (w x ). By definition of ⪯ ′ i , v I M (i, w). Therefore, v 1 I M ′ (i, w x ). Let X = ⪯ ′ i (v 1 )∪I M ′ (i, w x ) and X ′ = ⪯ ′ i (v 2 )∪I M ′ (i, w x ) . Because of v 1 ⪯ ′ i (w x ) and v 1 I ′ (i, w x ), by definitions of N ′ and ⪯ ′ i , we have X , X ′ ∈ N ′ (i, w x ), X X ′ , v 1 ∈ X and v 1 X ′ . Since w x ∈ I M ′ (i, w x ), by construction of M ′ , we have Sat M ′ (i, w x ) = N ′ (i, w x ). It follows that Sat M ′ (i, w x ) ⊈ Sat M ′ (i, v 1 ). We can conclude that Sat M ′ (i, w x ) ⊆ Sat M ′ (i, v 1 ) implies w x ⪯ i v 1 . In an analogous way, we can prove that Sat M (i, w x ) ⊆ Sat M (i, v 2 ) implies w x ⪯ i v 2 .

In order to prove that M ′ satisfies Constraint C5, we first observe that, by construction of M ′ , if v y ∈ I M ′ (i, w x ) then Sat M ′ (i, v y ) = N ′ (i, v y ).

Figure 1 :

 1 Figure 1: From values to preferences via evaluation

According to contemporary theories of human motivation in philosophy[START_REF] Searle | Rationality in Action[END_REF] and in economics[START_REF] Harsanyi | Utilitarianism and Beyond[END_REF], goals of a rational agent may originate either (i) from somaticallymarked motivations such as desires or physiological needs, or (ii) from ethical considerations, moral values and norms. In other words, there are desire-based goals and value-based goals. In this paper, we will focus exclusively on the latter category.Proc. of

the 20th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2021), U. Endriss, A. Nowé, F. Dignum, A. Lomuscio (eds.), May 3-7, 2021, Online. © 2021 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

This aspect is emphasized by Dewey in his theory of valuing, where he defines evaluation as "...an activity of rating, an act that involves comparison... "[14, p. 5].

This situation is typical of moral struggles, as defined by Levi, which "...are provoked by inconsistencies between value commitments and information concerning the kinds of decision problems which arise... "[25, p. 8].

See[START_REF] Nagel | The Limits of Objectivity[END_REF][START_REF] Sen | Well-Being, Agency and Freedom: The Dewey Lectures 1984[END_REF] for further discussion about the compability between moral objectivism and agent-relativity of ethical values.

A similar idea of computing a preorder from a neighbourhood structure or a priority graph can be found in evidence logic[START_REF] Van Benthem | Tracking Information[END_REF][START_REF] Van Benthem | Evidence and plausibility in neighborhood structures[END_REF] and in the logic of preference[START_REF] Liu | Reasoning about Preference Dynamics[END_REF].

ACKNOWLEDGMENTS

Support from the ANR-3IA Artificial and Natural Intelligence Toulouse Institute (ANITI) is gratefully acknowledged.

Now, suppose v 1 I M ′ (i, w x ) and v 1 ∈≡ i (w x ). Thus, by definition of V ′ , v I (i, w) and v 2 I ′ (i, w x ). Therefore, by definition of ⪯ ′ i and N ′ , v 1 ⪯ ′ i (v 2 ) ∪ I ′ (i, w x ) and ⪯ ′ i (v 2 ) ∪ I ′ (i, w x ) ∈ N ′ (i, w x ). Thus, Sat M ′ (i, v 1 )

N ′ (i, v 1 ). We can conclude that Sat M ′ (i, v 1 ) = N ′ (i, v 1 ) and v 1 ∈ ≡ i (w x ) imply v 1 ∈ I ′ (i, w x ). The proof that Sat M ′ (i, v 2 ) = N ′ (i, w x ) and v 2 ∈ ≡ i (w x ) imply v 2 ∈ I ′ (i, w x ) is analogous.

It is easy to show that, for every X ⊆ {VR, VC}, if M satisfies every property in X , then M ′ satisfies them too.

By induction on the structure of the formula φ, we can prove that M, w |= φ if and only if M ′ , w x |= φ, for every x ∈ {1, 2} and w ∈ W . □

A.2 Proof of Theorem 5.4

Proof. It is routine to check that the axioms of LEV are all valid relative to the class of quasi-EMs and that the rule of inference Nec K i preserves validity with respect to this class.

To prove completeness, we use a canonical model argument.

We consider maximally consistent sets of formulas in L (MCSs). The following proposition specifies some usual properties of MCSs.

Proposition A.1. Let Γ be a MCS and let φ,ψ ∈ L. Then:

The following is the Lindenbaum's lemma for our logic. As the proof is standard (cf. [START_REF] Blackburn | Modal Logic[END_REF]Lemma 4.17]) we omit it here. Lemma A.2. Let ∆ be a LEV-consistent set of formulas. Then, there exists a MCS Γ such that ∆ ⊆ Γ.

Let the canonical quasi-EM model be the tuple

i is an equivalence relation and ⪯ i is partial preorder, and that Conditions C1, C2, C3, C6, C7, C8 and C9 in Definitions 3.1 and 5.1 are satisfied. The proof uses Proposition A.1: Axiom T K i guarantees that ≡ c i is reflexive, Axiom 4 K i guarantees that it is transitive, and Axiom

guarantees that it is transitive. We are going to show that M c satisfies Constraints C1, C2, C3 and C6 as an example. We leave to the reader the task of proving that it satisfies Constraints C7, C8 and C9 as well.

As for C1, suppose w ⪯ v i v and w c i v. By definition of ≡ c i , K i φ ∈ w and φ v for some φ. By Axiom Mix K i ,[⪯ i ] and Proposition A.1, [⪯ i ]φ ∈ w. Hence, by definition of ⪯ c i , we have φ ∈ v which leads to a contradiction.

As for C2, suppose X ∈ N c (i, w). The latter means that X = {u ∈≡ c i (w) : φ ∈ u} and V i φ ∈ w for some φ. Thus, clearly, X ⊆≡ c i (w). As for C3, suppose w ≡ c i v, X ∈ N c (i, w) and X N c (i, v). By definition of N c , X = A φ (i, w) for some φ such that V i φ ∈ w and V i φ v. Hence, by Axiom Mix2 K i ,V i and Proposition A.1, K i V i φ ∈ w. Because of w ≡ c i v, the latter implies V i φ ∈ v which leads to a contradiction. Since the relation w ≡ c i v is symmetric, in an analogous way we can prove that w ≡ c i v, X N c (i, w) and X ∈ N c (i, v) also leads to a contradiction.

As for C6, suppose w ⪯ c i v and w ∈ X for some X ∈ N c i (i, w). We are going to prove that v ∈ X and X ∈ N c i (i, v). Suppose not. Thus, either v X or X N c i (i, v). X ∈ N c i (i, w) means that X = A φ (i, w) for some V i φ ∈ w. By Axiom Mix2 K i ,V i and Proposition A.1, the latter implies that X = A φ (i, w) and

). We only need to show that v X also leads to a contradiction. From w ∈ X and X ∈ N c i (i, w), we have w ∈ X and X = A φ (i, w) for some V i φ ∈ w. Thus, by definition of A φ (i, w), φ ∈ w and V i φ ∈ w. By Axiom Mix V i ,[⪯ i ] and Proposition A.1, the latter implies that

Hence, since w ≡ c i v, we have v ∈ X which is in contradiction with the initial assumption.

The next step in the proof is the following existence lemma. The proof is again standard (cf. [START_REF] Blackburn | Modal Logic[END_REF]Lemma 4.20]) and we omit it.

Finally, we can prove the following truth lemma.

Lemma A.4. Let φ ∈ L and w ∈ W c . Then, M c , w |= φ iff φ ∈ w.

Proof. The proof is by induction on the structure of the formula. The cases with φ atomic, Boolean, and the form K i ψ are provable in the standard way (cf. [START_REF] Blackburn | Modal Logic[END_REF]Lemma 4.21]).

The proof for the case φ = V i ψ goes as follows.

(⇒) Suppose M c , w |= V i ψ . Thus, {u ∈≡ c i (w) : M c , u |= ψ } ∈ N c (i, w). Hence, by definition of N c , there exists χ such that V i χ ∈ w and {u ∈≡ c i (w) : χ ∈ u} = {u ∈≡ c i (w) : M c , u |= ψ }. Thus, by induction hypothesis, {u ∈≡ c i (w) : χ ∈ u} = {u ∈≡ c i (w) : ψ ∈ u}. Now, suppose that K i (χ ↔ ψ ) w. By Proposition A.1, it follows that ¬K i (χ ↔ ψ ) ∈ w. This means that K i ((χ ∧¬ψ )∨(¬χ ∧ψ )) ∈ w. By Lemma A.3, the latter implies that there exists v ∈ W c such that w ≡ c i v and ((χ ∧ ¬ψ ) ∨ (¬χ ∧ ψ )) ∈ v which is in contradiction with {u ∈≡ c i (w) : χ ∈ u} = {u ∈≡ c i (w) : ψ ∈ u}. Thus, we have K i (χ ↔ ψ ) ∈ w. From V i χ ∈ w and K i (χ ↔ ψ ) ∈ w, by Proposition A.1 and Axiom Mix1 K i ,V i , it follows that V i ψ ∈ w.

(⇐) Suppose V i ψ ∈ w. Thus, by definition of N c , A ψ (i, w) = {v ∈≡ c i (w) : ψ ∈ v} ∈ N c (i, w). Hence, by induction hypothesis, {v ∈≡ c i (w) : M c , v |= ψ } ∈ N c (i, w). Therefore, M c , w |= V i ψ . □

To conclude the proof, suppose φ is a LEV-consistent formula in L. By Lemma A.2, there exists w ∈ W c such that φ ∈ w. Hence, by Lemma A.4, there exists w ∈ W c such that M c , w |= φ. □


Abdallah Said

Reine Talj

Clovis Francis

Hassan Shraim

Local trajectory planning for autonomous vehicle with static and dynamic obstacles avoidance

Local trajectory planning for autonomous vehicle with static and dynamic obstacles avoidance

Abdallah Said 1,2 , Reine Talj 1 , Clovis Francis 2 and Hassan Shraim 2

Abstract-Trajectory planning is one of the most complex tasks that should be accomplished in order to ensure vehicle autonomous driving. Trajectory planning can be classified into local and global planning. The purpose of local trajectory planning is to find the optimal trajectory to follow a global reference trajectory while avoiding obstacles in a smooth and comfortable way, within the constraints of road driving. This paper presents a trajectory planning algorithm that calculates a path according to a set of predefined way-points describing a global map. The predefined way-points provide the basic reference frame of a curvilinear coordinate system to generate candidate paths, which start with a transient phase, followed by a curve parallel to the road. Each candidate path, associated to a desired velocity profile, is evaluated via a cost function against several criteria including passenger's comfort, static and dynamic obstacles avoidance and overall trajectory tracking. The chosen trajectory is then applied to a full vehicle model using a coupled longitudinal/lateral controller validated on SCANeR studio (OKtal) simulator. A challenging test scenario of SCANeR studio is used to validate the proposed algorithm under Matlab.

I. INTRODUCTION

For nearly two decades, autonomous vehicles have been an important area of academic and industrial research that aims to improve vehicles safety and passenger's comfort. Various competitions have been organized around the autonomous vehicle: The DARP A challenges in the United States (2004,2005,2007), the Korean competitions for autonomous vehicles, the European GCDC competitions (2013,2016), and many others. Autonomous driving can be divided into different stages: environment perception and localization, trajectory planning, and vehicle control. This paper presents a local trajectory planning algorithm for autonomous navigation. The planning algorithm must generate a smooth and safe trajectory based on several criteria. To treat this problem, the perception module must provide information about the vehicle's environment, then, by applying the planning algorithm, an optimal trajectory is generated. Finally, the vehicle's controller ensures tracking the chosen trajectory by generating the reliable control laws.

Different trajectory planning approaches have been developed for the navigation of autonomous vehicles. State lattices can be considered as a grids generalization [START_REF] Pivtoraiko | Efficient constrained path planning via search in state lattices[END_REF] . They are constructed by regularly repeating primitive paths that connect the possible states for the vehicle, in terms of position, 1 Université de Technologie de Compiègne, CNRS, Heudiasyc (Heuristics and Diagnosis of Complex Systems), CS 60 319, 60 203 Compiègne Cedex, France. Email: (abdallah.said, reine.talj)@hds.utc.fr 2 Université Libanaise, Faculté de Génie, Centre de Recherche Scientifique en Ingénierie (CRSI), Liban. Email: (cfrancis, hassan.shraim) @ul.edu.lb curvature or time. The planning problem is then reduced to a boundary value problem. A cost function determines the best path between the pre-calculated networks. State networks [START_REF] Howard | Optimal rough terrain trajectory generation for wheeled mobile robots[END_REF], [START_REF] Ziegler | Spatiotemporal state lattices for fast trajectory planning in dynamic on-road driving scenarios[END_REF] overcome the efficiency limitations of network-based techniques without increasing computing power. However, It is not clear how to move the robot from one cell to another adjacent cell when its dynamics are non-linear and complex.

Another approach is sampling-based planning that relies on sampling the configuration space. This randomized approach has the advantage of providing quick solutions to difficult problems. The disadvantage is that the solutions are widely regarded as sub-optimal and The execution time is unpredictable. As a result, the resulting paths tend to be jerky, redundant, and non-curved, which is not acceptable for autonomous driving applications, especially at high speeds. The most commonly used algorithms are the roadmap method (PRM) [START_REF] Plaku | Samplingbased roadmap of trees for parallel motion planning[END_REF] and Rapid Exploration Trees (RRT) [START_REF] Karaman | Sampling-based algorithms for optimal motion planning[END_REF] .

Numerical optimization methods, adopted in [START_REF] Werling | Optimal trajectory generation for dynamic street scenarios in a frenet frame[END_REF], [START_REF] Lim | Hierarchical trajectory planning of an autonomous car based on the integration of a sampling and an optimization method[END_REF] and [START_REF] Ziegler | Trajectory planning for Bertha-A local, continuous method[END_REF], aim at minimizing or maximizing a function subject to different constraints by using non-linear optimization techniques to solve the trajectory planning problem where the non-holonomy and differential constraints are represented by a system of equality and inequality such as speed, steering speed, acceleration, jerk, etc. They are widely used in autonomous driving systems for their rapid convergence towards locally optimal solutions; however, they are generally not able to find globally optimal solutions, unless an appropriate initial estimate is provided. In addition, they are very time consuming since the optimization of the function takes place at each planning sampling time.

Starting from a set of points describing a global map, the curve interpolation method seeks to generate trajectories in a certain horizon having a specific geometric shape and responding to one or more conditions such as vehicle dynamics and kinematics, comfort, road shape, continuity of curvature, etc. Each candidate is then evaluated via a cost function taking into account several considerations such as distance and time costs, acceleration and collision verification. Geometric representations of trajectories include polynomials [START_REF] Lee | A unified framework of the automated lane centering/changing control for motion smoothness adaptation[END_REF], polynomial spirals [START_REF] Matthew | Parallel Algorithms for Real-time Motion Planning[END_REF], spline curves [START_REF] Wang | Action annotated trajectory generation for autonomous maneuvers on structured road networks[END_REF], Bézier curves [START_REF] Yang | An analytical continuouscurvature path-smoothing algorithm[END_REF] and tentacles [START_REF] Chebly | Local trajectory planning and tracking of autonomous vehicles, using clothoid tentacles method[END_REF].

In [START_REF] Chu | Local path planning for off-road autonomous driving with avoidance of static obstacles[END_REF], the path planner generates a finite set of paths candidate parallel to the base path with different offset shifts and selects the optimal path based on a discrete optimization approach. It is a fast reactive method that reduces the solution space and is therefore well suited for real-time implementation. In our work, the concept of this method was adopted. Several improvements have been proposed on the Our approach is less conservative due to safety considerations in relation to the longitudinal distance of the obstacle. In addition, a collision checking method has been used to reduce the time required. Our method also handles moving obstacles and multi-lane structured environments.

The proposed algorithm was applied on a representative scenario based on real-world driving situations and using a fully controlled vehicle model developed in [START_REF] Chebly | Coupled longitudinal/lateral controllers for autonomous vehicles navigation, with experimental validation[END_REF]. We present in Section II the developed navigation strategy and explain how each module works. The proposed planning module is detailed in section III. Section IV reports some simulation results, while the final Section V concludes the paper.

II. PRESENTATION OF THE NAVIGATION STRATEGY

The autonomous driving system consists of several complementary modules. Each module receives information, processes it and sends it to another one. In Fig. 1, the functional diagram of the developed system is presented where all the blocks are combined together:

• a reference map block which interpolates the reference trajectory and calculates its characteristics which are used in the generation of candidate paths, • a map matching block that attempts to match the vehicle position on the reference map, • a perception block that generates a local occupancy grid taking into consideration the new position of the vehicle and mobile obstacles in order to check the navigability of candidate paths, • a planning block that generates the candidate paths and corresponding desired velocity profile then selects the best trajectory to be executed, • a four-wheeled vehicle dynamic model implemented with a coupled longitudinal/lateral controller and a sub block to match the vehicle position on the desired trajectory.

Since path planning is the goal of this paper, it is detailed in the section III.

A. Reference Map

Generally, a road is represented by a sequence of points and modeled by a parametric curve to define the trajectory of the movement. There are different approaches, such as bezier curve, poly-line model, lanlet model, cubic spline and many others [START_REF] Éry | Map-based curvilinear coordinates for autonomous vehicles[END_REF]. In our work, we use Piece-wise cubic spline curves for map interpolation based on the given way-points P bf to ensure the continuity of the curvature profile and to avoid discontinuities and differentiation problems when passing over one of the way-points. However, it is essential to efficiently link the values of the spline curve parameters to the curvilinear abscissa s in order to simplify and improve the planning and trajectory tracking performance of the vehicle (see [START_REF] Wang | Arclength parameterized spline curves for real-time simulation[END_REF]). A series of arc length parameterized cubic spline curves P (s) = (x(s), y(s)) are generated. Using these curves equations, the curvature profile ρ P bf is calculated first. Then, the base frame velocity profile V P bf is calculated based on the desired speed and road speed limit that guarantees the stability of the vehicle.

B. Map matching

The correspondence of the vehicle's position on the reference map is an unavoidable step. It allows to identify the curvilinear coordinates of the vehicle (or any interesting point) from the Cartesian coordinates in order to use the reference information. In order to make the mapping neither computationally demanding nor difficult to be implemented in real-time embedded systems, we proposed a composite algorithm that starts with the poly-line mapping method [START_REF] Éry | Map-based curvilinear coordinates for autonomous vehicles[END_REF] to find a rough estimate that serves as an initial guess for the quadratic minimization method in [START_REF] Wang | Robust and efficient computation of the closest point on a spline curve[END_REF] (Fig. 2a). It consists in finding on the reference trajectory C, the closest point P b to the vehicle P v . At the end, in a local curvilinear coordinate system ( -→ s , -→ q ), the coordinates (s v , q v ) of the vehicle P v are obtained (Fig. 2b).

C. Perception

To avoid collisions and maintain safe conditions, a candidate path must be checked to determine whether or not it crosses roadsides or obstacles. The perception block is out of the scope of this paper. The present work considers the output of the perception block as an occupancy grid representation. The occupancy grid is a discrete and metric representation of the surrounding environment, where it is represented by a set of square cells. Black cells correspond to a navigable area, and white one may belong to the roadside or obstacles. However, for validation by simulation, the occupancy grids are generated in M atlab. Starting from a global map (Fig. 3), a global occupancy grid is generated (Fig. 4). The local s-spline border Fig. 3: Reference map global map Fig. 4: Global occupancy grid occupancy grid is obtained from the global occupancy grid according to the position and orientation of the vehicle to obtain the local occupancy grid. This latter is constituted of 400 * 400 cells, each of which measures 25 * 25 cm (Fig. 6). These dimensions are related to the horizon of the perception system. At each planning iteration, the local occupancy grid is updated by the new footprint occupied by the moving obstacles existing in its perception zone. However, to take their velocity into consideration, a longitudinal widening of their occupancy is carried out in the grid (Fig. 5). It's equal to the predicted traveled distance during one iteration. moving obstacle fixed obstacle Fig. 5: Vehicle and obstacles occupancy In order to improve the accuracy, efficiency and time consumption for collision checking, the local occupancy grid (Fig. 6) is transformed into a clearance map as shown in Fig. 7. This map represents the distance to the nearest obstacle using the method explained in [START_REF] Felzenszwalb | Distance transforms of sampled functions[END_REF]. The validation of a circular area of the grid is then transformed into a singlepoint validation: if the distance from the center of a circle to the nearest obstacle is greater than its radius, then there is no collision, and vice-versa.

D. Controlled vehicle dynamic model

A full longitudinal and lateral vehicle model is implemented in our algorithm. It has been developed using the multi-body formalism in [START_REF] Chebly | Coupled longitudinal/lateral controllers for autonomous vehicles navigation, with experimental validation[END_REF]. The model inputs are the wheel driving/braking torque τ w and the steering angle δ. Using Dugoff model to estimate tires forces and model matrix calculations, the model outputs are calculated: the

III. PATH PLANNING

Our path planning algorithm must provide the optimal path from a set of paths that helps the vehicle to track a reference trajectory while avoiding static and mobile obstacles and ensuring the safety and comfort of passengers. The navigation strategy is composed of several stages: generation of a set of candidate paths, obstacle detection and paths classification according to their navigability, costs calculation and selection of the optimal one from this set of candidate paths. This selected trajectory is considered as the desired trajectory to be executed by the vehicle at each planning iteration. The entire procedure of the path planning is shown in Fig. 8 and explained in the following.

A. Generation of candidate paths

The objective is to generate candidate paths while avoiding obstacles shifted by a lateral offset from the reference trajectory (Base Frame). The planning algorithm generates a finite number of candidates, each of them having Desired best path a separate lateral offset q f to cover the entire width of the lane (Fig. 9). The generation of these candidate paths consists of two stages: the generation of candidate path in the coordinate system ( -→ s , -→ q ) in order to facilitate their representation and then their transformation into Cartesian coordinates in the global coordinate system ( -→ X , -→ Y ).

In the curvilinear coordinate system ( -→ s , -→ q ):

The candidate path starts from the last executed point P t-1 des of the desired trajectory at the previous planning iteration to ensure its continuity. It consists of a transient phase to reach the offset already defined q f , followed by a permanent phase where it will be parallel to the road to continue with this offset. The P t-1 des is matched on the global map, so the curvilinear coordinate (s P t-1 des , q P t-1 des ) and other characteristics of the first corresponding point P 0 bf on the base frame of the new candidate path are obtained (Fig. 10). First, from the width of the lane (the vehicle width is subtracted to avoid the generation of candidate paths near borders) and the desired lateral sampling resolution ∆q, the number of last points (s i f , q i f ) on the candidate paths are determined. The arc length s f is that traveled by the candidate path all along the reference trajectory. It consists of two phases, s f 1 for transient phase and s f 2 for permanent phase. It is proportional to the speed of the vehicle v V with the gain K v , bounded by the minimum ∆s f -min and the maximum l max acceptable length and given by:

s f 1 = ∆s f 1-min + K v1 V v , s f 2 = max(∆s f 2-min , 2 d ss -s f 1 ) s f = min(l max , s f 1 + s f 2 ) (1)
where the safe stop distance d ss is the distance required to stop the vehicle traveling at a speed V v with the maximum longitudinal deceleration a dec-max x and defined by:

d ss = d ss0 + V 2 v 2a dec-max x (2)
where d ss0 is a minimum safety gap. Next, for each of candidate path, a fourth order polynomial (eq. 3) describes the lateral shift polynomial q i M (s) to provide a smooth change (Fig. 9) ensuring the C 2 continuity while avoiding the discontinuity of the curvature with respect to the desired one in the last iteration.

q i M (s) =      a i 0 + a i 1 ∆s + a i 2 ∆s 2 s P t-1 des s s f 1 , +a i 3 ∆s 3 + a i 4 ∆s 4 , q i f , s f 1 s s f (3)
where ∆s = s-s P t-1 des . The coefficients of fourth order polynomials a i are determined based on the boundary conditions below: In the global coordinate system ( -→ X , -→ Y ): The candidate paths are generated in the curvilinear coordinate system, but the planning results should be converted to the Cartesian coordinate system approved by the maneuver system (Fig. 10).

q i (s P t-1 des ) = q P t-1 des , ∂q i ∂s (s P t-1 des ) = tan(θ P t-1 des -θ bf ), ρ i (s P t-1 des ) = ρ P t-1 des , q i (s i f 1 ) = q i f , ∂q i ∂s (s i f 1 ) = 0 (4)
First, from P 0 bf , a base frame trajectory is constructed along the reference trajectory starting from s P t-1 des and ending on s f , then its characteristics are calculated (curvature ρ P bf , limit velocity V limit P bf , desired velocity V des P bf and normal vector ---→ N P bf ). Second, for each candidate path, we proceed, point by point, by the transformation between the Cartesian coordinate system and the curvilinear coordinate system. The trajectories are deduced as follows:

-

----→ OM i (s) = ---→ OP bf + q i (s) ---→ N P bf (5)
If the point M belongs to a circle around the vehicle (P v , L P A ) which represents the perception area of the vehicle, we calculate its characteristics. First, we calculate the curvature of each point on the candidate path ρ i M as follows:

ρ i M = S i M Q i M ρ P bf + (1 -q i ρ P bf ) ∂ 2 q i ∂s 2 + ρ P bf ∂q i ∂s 2 Q i M 2 (6)
with:

S i M = sgn(1 -q i ρ P bf ), Q i M = ∂q i ∂s 2 + (1 -q i ρ P bf ) 2 .
(7) Now, we check if the candidate path is executable by the vehicle due to the steering limitation: ρ max is the curvature corresponding to the maximum steering angle that can be executed by the vehicle. So, if at any point M of the candidate path, ρ M > ρ max , the candidate path is considered as not executable and it is rejected from the available set of paths. If all candidate paths are not executable, an emergency braking mode is activated: the planning algorithm selects the longest navigable path providing the maximum distance to the obstacle, (III-B), and brake with high deceleration and zero desired speed.

Determination of the desired velocity profile:

The vehicle must follow a predefined velocity profile or brakes in case of obstacle detection or no executable trajectory. Starting from desired velocity profile of the base frame V des P bf and for each point of candidate path, we calculate the desired initial velocity at a point M for the candidate i, V des0 M i , and its limit V limit M i imposed by the velocity limit of the base frame V P limit bf as follows:

V des0 M i = S i M Q i M V des P bf , V limit M i = S i M Q i M V P limit bf (8)
Another limitation V ρ M i is imposed by the lateral acceleration to improve vehicle stability and passenger comfort:

V ρ M i = a max y ρ i M ( 9
)
where a max y is the maximum acceptable lateral acceleration in the comfort zone.

Finally, the desired velocity profile of each point on the candidate path V des M i is calculated as follows:

V des M i = min(V limit M i , V ρ M i , V des0 M i ) ( 10
)
Due to perception limit, the safe stop distance must be less than the perception horizon of the vehicle. So, the desired velocity is also maximized by the value calculated using equation ( 2) for d ss = L P A .

B. Obstacle detection and paths classification

For the rest of the executable candidate paths, an obstacle detection procedure is carried out. So, on each point of this path and as described in the sub-Section II-C, we validate the footprint of the vehicle represented by several circles as shown in Fig. 11: a large circle and six other small circles.

Fig. 11: Example of collision checking

First, an evaluation of the large circle is carried out: if there are no obstacles, we pass to the next point on the path (Fig. 11). In the case where an obstacle is present, a more precise validation is carried out based on the test of the 6 small circles. Once the first obstacle is detected, the free distance traveled on the path to reach the obstacle is called the collision distance d obs . The obstacle type, fixed or moving, is also determined and is also associated with its speed V obs , if it is a moving obstacle. The next step is to classify the trajectory based on the collision distance into three classes as follows:

     d i obs < L s → no navigable trajectory L s < d i obs < l i max → partially navigable trajectory d i obs ≥ l i max → navigable trajectory (11)
where l i max is the length of corresponding candidate path and L s is the adapted security distance [START_REF] Althoff | Can automated road vehicles harmonize with traffic flow while guaranteeing a safe distance?[END_REF] that the vehicle must keep with the vehicles that precede it and is calculated using the following formula :

L s = d ss ,
for fixed obstacle

d ss0 + V f ∆t + V 2 f -V 2 p 2a dec-max x
, for mobile obstacle (12) where ∆t is the average reaction time of autonomous vehicles, V f is the following vehicle's speed and V p is the preceding vehicle's speed.

If there is no navigable paths on the reference lane, the generation of an additional set of paths candidate is performed on the adjacent lanes (Fig. 12). Note that braking is performed whenever there is no navigable paths on all the lanes. Fig. 12: Generation of path candidate on one and two lanes

C. Selection of the desired trajectory

The desired path is either the optimal one from the executable and navigable set of paths. Or, if there are none, the path who has the greatest distance to the obstacle is chosen to brake the vehicle. Among all remained candidate paths, we seek to choose the optimal trajectory to execute it. These trajectories are evaluated according to different criteria including smoothness, safety, consistency with the initial state of the vehicle and the reference trajectory tracking. Once these criteria have been estimated and the corresponding cost function is evaluated, they are normalized, weighted and combined in a linear manner within a cost function which we seek to minimize.

Smoothness cost C K [i]: Low smoothness induces additional lateral acceleration which degrades passenger comfort. The lateral acceleration of the vehicle is related to the curvature especially at constant speed (eq. 9). So, to reduce the slackness of a path, the integration of the curvature squared along a trajectory i is chosen as a criterion of smoothness for this trajectory as follows:

C K [i] = ρ i M 2 ds i M = ρ i M 2 Q i M ds (13)
where ds i M is the curvilinear abscissa along the i path and ds is that along the base frame.

Consistency cost C c [i]: A sudden change in the trajectory requires excessive energy and an extra effort of control. Therefore, to avoid generating a trajectory that is significantly different from that of the previous step, a measure of similarity between the previous trajectory and the current candidate path is required. We simplify it in our algorithm to the difference between the index of the current path i and that of desired path at previous planning iteration.

C c [i] = |i -i t-1 des | ( 14
)
Cost of tracking the reference trajectory C r [i]: This criterion leads the vehicle to follow the global reference trajectory in order to position itself in the center of the desired lane. As the candidate paths are generated around this center by a defined lateral offset, the cost of following the reference trajectory is proportional to this offset. The further you go, the more the cost increases and is given by: [START_REF] Wang | Arclength parameterized spline curves for real-time simulation[END_REF] where d i-bf is the lateral distance between the path i and the base frame. safety cost C s [i]: we define two safety costs: a longitudinal cost C sl and a lateral cost C sL . The first one measures the navigability of the trajectory itself and how far the obstacle is, while the lateral one takes into account the navigability of the adjacent trajectories. The collision distance d obs [START_REF] Wang | Action annotated trajectory generation for autonomous maneuvers on structured road networks[END_REF], is transformed into a safety cost as follows:

C r [i] = d 2 i-bf
C sl [i] = 0 obstacle-free trajectory 2 - 2 1+e -c 1 d i obs otherwise (16
)

g[k] = 1 √ 2πσ exp - (k ∆q) 2 2σ 2 (17)
C sL [i] = j∈Γ i C sl [j] g[i -j] n Γ i (18) C s [i] = C sl [i] + W SlL C sL [i] (19)
where c 1 is a cost setting parameter, ∆q is the desired lateral sampling resolution, σ is the standard deviation of the discrete Gaussian convolution for the risk of collision and is calculated by considering that g[ Lv ∆q ] = 0.5. Γ i is the set of indexes of executable paths without i, n Γ i is their number and W SlL is a weighting coefficient between the two costs.

Total cost and optimal path selection: As our different costs criteria are measured in different units, we use the normalization technique to make them dimensionless. Hence, we apply the following formula:

C . [i] = C . [i] -min(C . ) max(C . ) -min(C . ) (20)
Then, the total cost function C T [i] of a given trajectory is defined as the weighted sum of the normalized cost functions defined above:

C T [i] = W K C K [i] + W c C c [i] + W r C r [i] + W s C s [i] (21)
with W K , W c , W r and W s are the weighting coefficients of smoothness, consistency, reference tracking and safety respectively.

At this final step, the selected trajectory is represented by a series of points defined by the curvilinear abscissa, x and y coordinates, velocity and curvature. This trajectory is interpolated using the same method explained in II-A to facilitate the vehicle's matching in the control/model block. To show the flexibility and the safety aspects of the presented approach, we present in Fig. 14 a one challenging test scenario, instead of several simple scenarios, which shows:

IV. SIMULATION RESULTS

• passing through a tight passage • overtaking fixed obstacles • lane change maneuver • vehicle speed adaptation • overtaking a moving obstacle The trajectory of the vehicle is represented by its colored footprint relative to its instantaneous longitudinal speed.

As shown in Fig. 14, the vehicle starts traveling along the center road at speed of 30 km/h. It passes through a tight passage (t=4s) to avoid static obstacles in a straight road then accelerate to reach the desired speed. Or, when entering the curvy road, the vehicle encounter a fixed obstacle blocking the lane and a mobile obstacle on the other lane (t=8s), so the planning algorithm slows down the vehicle, leaving the way for the moving obstacle (t=10s). Then, the vehicle is accelerated to pass the fixed obstacle (t=15s). At t=18s, we see an overtaking of a mobile obstacle traveling at v obs = 25km/h (t=18s). The overtaking and returning maneuvers The overtaking is permissible while the speed difference between vehicle and obstacle is greater than 20 km/h. The planner start overtaking (t=22s) after approaching from obstacle to reach the security distance (eq.12) and selects a smooth and comfortable path on the left lane to pass the mobile obstacle while increasing its speed. The vehicle reach the second lane's center at t=22s and travel along to reach a sufficient safety distance (t=25s) to start returning to the host lane. At t=29s, the vehicle succeeds to reach the center of the road and travel at the desired speed while entering a curvy road.

In Fig. 15, the base frame curvature profile is shown in dotted line. Smooth motion can be seen from the generated continuous curvature profile ensured by the order 4 of the lateral offset polynomial. We see also the longitudinal speed profile. The base frame limit speed is around 57 km/h. Based on selected trajectories and driving situations, the desired speed profile is shown in dashed line. Its limit based on comfort acceleration, shown in Dash-dot line, is well respected, especially at t=10, 15 and 18s in the three different maneuvers. The vehicle is traveling at the desired speed with an acceptable longitudinal speed error and track perfectly the maximal acceptable speed between t=22 and 25s when passing mobile obstacle on the second lane. Note that the longitudinal acceleration is suitable for comfortable travel and limited between ±1.5m/s 2 for comfort travel and can reach -3m/s 2 in case of emergency braking (t=8s). From the lateral acceleration profile, we can deduce that the vehicle stability is ensured, which improves passenger comfort. The maximal lateral acceleration (±4m/s 2 ) reached at t=10, 15, 20 and 29s in the different scenarios shows the performance of our proposed method on the limit of stability. Also, the small lateral error shows that the vehicle is able to follow accurately the trajectory generated by the planning algorithm during the entire course. The lateral curvilinear coordinate is presented to show its smooth variation. The vehicle position in the mobile obstacle overtaking maneuver is displayed between t=18 and 29s.

V. CONCLUSION

A reactive trajectory planning algorithm for on-road navigation has been developed. It's able to follow a reference trajectory while passing fixed and mobile obstacles. Within the road driving rules and vehicle's dynamic constraints, the velocity is adapted to ensure passenger's comfort. Many other scenarios are tested and the results show good behavior in rather complicated driving situations. In the future, we look to implement our planning algorithm on a real experimental vehicle in Heudiasyc laboratory and to optimize the cost function coefficients in eq. 21 in order to take into consideration the driving situation in an optimal way (comfort oriented, stability, reference tracking, trajectory smoothness,...).

Fig. 1 :

 1 Fig.1: Functional diagram of the algorithm method of generating the path candidates and on the selection criteria. Our approach is less conservative due to safety considerations in relation to the longitudinal distance of the obstacle. In addition, a collision checking method has been used to reduce the time required. Our method also handles moving obstacles and multi-lane structured environments. The proposed algorithm was applied on a representative scenario based on real-world driving situations and using a fully controlled vehicle model developed in[START_REF] Chebly | Coupled longitudinal/lateral controllers for autonomous vehicles navigation, with experimental validation[END_REF]. We present in Section II the developed navigation strategy and explain how each module works. The proposed planning module is detailed in section III. Section IV reports some simulation results, while the final Section V concludes the paper.

Fig. 2 :

 2 Fig. 2: Map matching

Fig. 7 :

 7 Fig. 6: Local occupancy grid

Fig. 8 :

 8 Fig. 8: Path planning diagram

Fig. 9

 9 Fig. 9: Lateral offset polynomial in ( -→ s , -→ q )

Fig. 13 :

 13 Fig. 13: SCAN eR studio : global map To validate our planning algorithm, it was applied to a fairly realistic scenario taken from SCANeR studio simulator. Several fixed and moving obstacles are introduced so as to cover several commonly encountered driving scenarios. It was simulated in M AT LAB by taking into account the vehicle's dynamics. The vehicle block (model and controller) is running at a frequency of 50 Hz, and the rest of the system is running at 5 Hz. At each simulation step, the local occupancy grid is updated based on the new position of the vehicle and mobile obstacles are also added if there are any.To show the flexibility and the safety aspects of the presented approach, we present in Fig.14a one challenging test scenario, instead of several simple scenarios, which shows:

Fig. 14 :Fig. 15 :

 1415 Fig. 14: Simulation results: trajectories and vehicle's speed


Venkata Suresh Vajrala

Valentin Saunier

Lionel Nowak

Emmanuel Flahaut

Christian Bergaud

Ali Maziz

Carbon Nanofiber/PEDOT Based Macro-Porous Composite for High Performance Multifunctional Neural Microelectrode

come   L'archive ouverte pluridisciplinaire

Here in this work, we present a new macro-porous, conductive, and stable nanocomposite, made up of carbon nanofibers (CNFs) and PEDOT polymer, coated on a flexible neural microelectrode array (Fig. 1A-B). A fully controlled one-shot electrodeposition strategy was developed using chronopotentiometry technique, to coat flexible Au-microelectrode surfaces with macro-porous CNF/PEDOT nanocomposite. The oxidized CNFs were used as a dopant and infused within the conductive PEDOT, electrochemically, in such a way that their excellent electronic, mechanical, chemical properties, and resulting combined performances can be exploited to yield better quality neural recordings, electrical stimulation and neurotransmitter detection. At first, CNFs were oxidized to be dispersible in water (unlike raw CNFs) by vortex and sonication. Later, CNF/PEDOT composite was deposited on Au-electrodes galvanostatically, resulted in a 3D porous and fibrous network (Fig. 1B-D). Then, CNF/PEDOT deposits were characterized through electrochemical impedance spectroscopy (EIS) and pulse current injection. The composite microelectrodes showed low impedance, 16 ± 2 kΩ for a typical electrode area of 1250 µm 2 , at 1kHz (value corresponding to the neuron firing frequency) (Fig. 1E). Voltage transient responses were measured, at continuous 1ms-biphasic current pulses (cathodic first) in biologically relevant aCSF media, resulted in a charge-injection limit value of 7.6 ± 1.3 mC/cm² (Fig. F). Among all reported organic nanostructured composite materials that were deposited on flexible metallic substrates, CNF/PEDOT displayed superior electrical properties and charge injection capabilities [5]. Next, the capability of CNF/PEDOT composite electrode for in-vitro Dopamine (DA) sensing was evaluated by chronoamperometry, at 130mV vs SCE (oxidation potential of DA). The current responses submitted to DA injections resulted in linear regression (Fig. 1G, R²>0.99), with a high sensitivity of 13.4pA/nM.µm², compared to similar electrochemical sensors [6]. Overall, these electrodes displayed excellent electrical properties: low impedance (16 ± 2 MΩ.µm2 at 1 kHz) and high charge injection capabilities (7.5 ± 1.3 mC/cm²) making them promising candidates for bidirectional electrophysiology, while being capable to detect neurotransmitters like dopamine. Finally, integrated upon flexible neural probes, these composite microelectrodes were tested in-vivo on mouse brain slices as recording and stimulating electrodes (Fig. 1H). They displayed excellent performances, being capable to record spontaneous activities of neurons (sharp wave-ripples and single unit action potentials) and allowed to stimulate electrically the brain slice tissues, to obtain safe and stable evoked potentials. The obtained results show a great prospect for CNF/PEDOT composites for developing next-generation microelectrodes for applications in neural therapies.

Figure 1 .

 1 Figure 1. (A) Optical micrograph of flexible neural probe. (B) CNF/PEDOT deposition on 4 Au-microelectrodes of the implant. SEM images, (C) top view and (D) crosssectional view of the composite electrode. (E) EIS measurement on modified

Carbon Nanofiber/PEDOT Based Macro-porous Composite For High Performance Multifunctional Neural Microelectrode Venkata

  Suresh Vajrala a , Valentin Saunier a , Lionel Nowak b , Emmanuel Flahaut c , Christian Bergaud a and Ali Maziz a a Laboratory for Analysis and Architecture of Systems, CNRS, Toulouse, France b Centre de Recherche Cerveau et Cognition (CerCo), CNRS, Toulouse, France c CIRIMAT, Université de Toulouse, route de Narbonne, F-31062 Toulouse, France Brain study methods mainly rely on neurochemical detection and electrophysiology, respectively to study the molecular dynamics [1] and electrical activity [2] in the brain cellular environment. Since the brain functioning relies on careful orchestration of both neurotransmitter and neuroelectric activities, coupled monitoring of them holds great promise in elucidating the brain functioning mechanisms and its related diseases e.g. Parkinson's, epilepsy, etc [3]. Most of the conventional implantable neural interfacing technologies are comprised of noble metals on silicon/ polymer substrates. They suffer from inferior electrical properties, mechanical tissue-electrode mismatch, incompatible surface area, and low signal-to-noise ratio [4]. To address the need, researchers around the world are developing innovative soft materials with multimodal functionalities, especially the organic flexible materials such as conductive polymers and carbon allotropes, to fuel the next-generation multimodal neural electrode devices [5].

Acknowledgments

Agence Nationale de la Recherche (ANR-15-CE19-0006 and ANR-19-CE19-0002-01) and French RENATECH network.