Guillaume Hutzler
email: guillaume.hutzler@ibisc.univ-evry.fr

Hanna Klaudel
email: hanna.klaudel@ibisc.univ-evry.fr

Abderrahmane Sali

Filtering distributed information to build a plausible scene for autonomous and connected vehicles

Keywords: autonomous vehicles, plausibility, confidence, sensor fusion

To make their decisions, autonomous vehicles need to build a reliable representation of their environment. In the presence of sensors that are redundant, but not necessarily equivalent, that may get unreliable, unavailable or faulty, or that may get attacked, it is of fundamental importance to assess the plausibility of each information at hand. To this end, we propose a model that combines four criteria (relevance, trust, freshness and consistency) in order to assess the confidence in the value of a feature, and to select the values that are most plausible. We show that it enables to handle various difficult situations (attacks, failures, etc.), by maintaining a coherent scene at any time despite possibly major defects.

Introduction

Driving autonomy promises many benefits such as facilitating travel by reducing traffic jams and the number of accidents for which man is mainly responsible, or improving the comfort of the users during their travels. The control of autonomous vehicles is carried out in three stages: perception, decision, action. The perception stage corresponds to the acquisition of data by sensors, coupled to the analysis of these data to build the scene (integrated view of the environment). The decision stage corresponds to the selection of actions to be performed by the vehicle based on the scene, the state of the vehicle and its "intentions" (current maneuver, mission to perform). The action stage corresponds to the realization of the actions chosen based on the various actuators of the vehicle.

In a man-controlled vehicle, none of the sensors and features that they measure (speed, engine rpm, position, etc.) are crucial to the driving activity, they are only an assistance to help the driver in smoothly conducting his vehicle. In that case, the perception is mainly achieved by the senses of the driver. In an autonomous vehicle however, the relevance and reliability of environmental information are crucial to the decision-making process: a noisy perception or a rough reconstruction of the scene can lead to a bad decision and therefore a higher risk of accident. To tackle this issue, manufacturers use various and multiple sensors to obtain some redundancy in order to have more certainty about the environment. A problem arises when one has to choose between various values, measured by different sensors or combinations of sensors, for the same physical measure (position, speed, etc.). Sensors may have different margins of errors, or may be weather sensitive, and they may be subject to malfunctions, faults, or even attacks, that may lead to the production of erroneous values. Filtering the values in order to identify the most plausible one in the present context is thus a major stake in building (iteratively and in real-time) a reliable scene and therefore to increase the robustness of the system. This task is very similar to what happens in avionics where integrating data from different sources is necessary in order to build a view of the environment and create so-called situational awareness [START_REF] Frey | F-35 information fusion[END_REF].

In this paper, we first specify the context and related works in section 2. We then define some terminology, explain the criteria used to evaluate the plausibility, and present our algorithm in section 3. We finally explain in section 4 how it was implemented and comment about a selection of results that we obtained.

Context and related work

An autonomous vehicle is a vehicle that has the capability to perceive the surrounding environment, and to make decisions that are transmitted to actuators, so as to drive without human intervention [START_REF] Jo | Development of autonomous car-part i: Distributed system architecture and development process[END_REF]. To this end, it is equipped, among other things, with a set of sensors allowing to analyze the current situation with sufficient accuracy to make a good decision. Sensors may be divided into categories relative to their ranges [START_REF] Yan | Can you trust autonomous vehicles: Contactless attacks against sensors of self-driving vehicle[END_REF]: proximity sensors (e.g. ultrasounds), short-range sensors (e.g. cameras, short-range radars), medium range sensors (e.g. LiDARs, medium range radars), long Range Sensors (e.g. long-range radars) and location sensors (e.g. GPS). Autonomous vehicle manufacturers offer a wide range of sensors in order to respect a cost/accuracy/range compromise.

Communicating vehicles are vehicles that use communication technologies to exchange data (e.g. position, speed, intent) with each other [START_REF] Arena | An overview of vehicular communications[END_REF]. Transmissions travel either directly between vehicles (Vehicle to Vehicle or V2V communication), or through an infrastructure (Vehicle to Infrastructure or V2I communication). Since vehicles may exchange information about their position, speed, steering wheel angle, etc., we may consider the reception of messages from other vehicles as an additional sensor, whose information can be shared with other sensors.

Data fusion

Since the same information can be inferred from various sensors, we do have redundancy of information, hence the need to merge the data to increase the robustness of the system, which is called data fusion [START_REF] Castanedo | A review of data fusion techniques[END_REF]. There are a lot of different approaches in data fusion, and a lot of different classifications altogether, depending in particular on the type of data that are processed (raw data, features, decisions), and the type of data that are produced.

In our case, we are interested in both redundant and complementary data, that we fuse in a feature in-feature out (FEI-FEO) approach (also known as feature fusion, symbolic fusion, information fusion or intermediate level fusion), according to Dasarathy's classification [START_REF] Dasarathy | Sensor fusion potential exploitation-innovative architectures and illustrative applications[END_REF]. In this approach, a set of features is processed so as to "improve, refine or obtain new features" [START_REF] Castanedo | A review of data fusion techniques[END_REF]. We thus assume that we work with features, i.e., values that have already passed through the data analysis process at the lower level. The vehicle has to make a single decision, and the process is thus centralized.

The main constraints that we have to face are the following: the fusion has to occur in real-time since the vehicle does not have the possibility to stop so as to make its next decision; the result of the fusion has to be as precise and reliable as possible since the safety issues, for the passengers and the other users of the road are high; the fusion process has to be fault-tolerant since sensors may be subject to failures and/or attacks. In addition, we wish the fusion process to be verifiable [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF] and explainable [START_REF] Došilović | Explainable artificial intelligence: A survey[END_REF].

Related work

We briefly mention the most popular approaches to data fusion, and how they relate to our case.

Probabilistic models need a priori knowledge (Bayesian inference [START_REF] Rubin | Bayesian inference for causal effects: The role of randomization[END_REF][START_REF] Taylor | Homogeneous functionals and bayesian data fusion with unknown correlation[END_REF]), and are vulnerable to attacks (Dempster-Shafer [START_REF] Dempster | A generalization of bayesian inference[END_REF][START_REF] Jiang | Sensor data fusion based on a new conflict measure[END_REF]). Artificial intelligence approaches based on neural networks [START_REF] Kolanowski | Multisensor data fusion using elman neural networks[END_REF] need a large amount of learning data and also lack explainability. This is also the case for other approaches based on genetic programming that tackle the issue of fault tolerance [START_REF] Bentley | Fault tolerant fusion of office sensor data using cartesian genetic programming[END_REF]. Similarly, approaches based on fuzzy logic [START_REF] Soleymani | A secure trust model based on fuzzy logic in vehicular ad hoc networks with fog computing[END_REF][START_REF] Majumder | Multi-sensors data fusion through fuzzy clustering and predictive tools[END_REF] are not suitable because the system depends on an inference engine designed by human experts, and thus stability is not guaranteed.

Since part of the information available to the vehicle comes from other vehicles, we may also have to take into account the trust that we have in this data. Trust-based approaches [START_REF] Bhuiyan | Trust and reputation management in web-based social network[END_REF][START_REF] Granatyr | Trust and reputation models for multiagent systems[END_REF][START_REF] Zhang | A survey on trust management for vanets[END_REF] provide tools primarily applied to multi-agent systems, based on reputation.

Proposed approach

In this section, we propose a model allowing to build a coherent scene for the Ego vehicle in realtime, enabling it to make well-informed decisions. This vehicle receives features from a set of sensors, and also from other vehicles surrounding it. The model has to take into account the uncertainty of the information related to the environment and the agents, and to withstand possible attacks.

Terminology and outline of the study

At this point, it is useful to define the terminology that we will use in the remaining of the paper.

-A feature is a measure that describes some aspect of an entity in the environment. In the case of autonomous vehicles, features may be the position or speed of the vehicle. -The scene of a vehicle is a set of features that represents both its state and the environment.

-The Ego vehicle is the reference vehicle, which tries to build its own scene.

-The features are produced by information sources, which may include a variety of elements:

it may be a sensor whose raw data are processed to produce the corresponding feature, a collection of complementary features that are combined to produce the target feature, or a prediction about the probable value of a given feature computed from a past scene.

In order to understand the method and algorithm more easily, we will first specify the outline of the study in terms of sensors, features and sources of information.

The reference vehicle, Ego, has the following sensors (gathered in Table 1 with their characteristics, as provided by the manufacturers): three ultrasonic sensors: two on the sides and one behind; four cameras: one behind, three forward (one in the middle and two on the mirrors); a LiDAR; a GPS; and a V2V communication sensor. The features that are taken into account are the P osition (longitudinal and lateral with respect to the road) and Speed (longitudinal and lateral with respect to the road). The sources of information can be:

an individual sensor: each sensor of the Ego vehicle (GPS, LiDAR, Camera, Ultrasonic sensors) is considered as a source of information that computes one or several features; the V2V communication module: the surrounding vehicles may communicate their features (position, speed) to the Ego vehicle; complementary features: a feature can be computed from the values of two or more complementary features. For example, in order to have the absolute position of a vehicle V i , we can combine the relative position of the vehicle V i , given by a camera of Ego, with the absolute position of Ego given by the GPS. the prediction module: the value of the features may be estimated thanks to the information in the previous scene(s).

Table 2 presents the sources of information to be taken into consideration when calculating the P osition features. The checked boxes indicate that the corresponding source of information is to be considered for the calculation of this feature, while δ represents the margin of error of the source.

Criteria for selecting sources

Since we have, potentially, lots of different ways to compute the same feature, the problem consists in selecting, at any time, the most reliable and plausible source of information. To this end, we define criteria that characterize both the quality of the source in general (relevance and trust), and the quality of a given information in particular (freshness and consistency). These criteria are used to compute a global Confidence for each information:

-Relevance: Is a given source of information well suited to measure a given feature? -Trust: Did the source provide information that was considered as correct in a recent past? -Freshness: Is the information considered as recent or out of date? -Consistency: Is the information consistent with the previous values of the same source?

Relevance of the source Each sensor has been designed for a given purpose. But one sensor, which is very relevant to measure a given feature and used mainly in this way, may also be used, although in a less relevant manner, to measure another feature. This relevance is represented by a static percentage defined beforehand for each information source and each feature.

For example, to define the position of Ego, we can use either the GPS or the combination of values coming from a LiDAR (which provides the relative position of a vehicle A with respect to vehicle Ego) with the absolute position communicated by A, or make a prediction based on the last known position and speed of Ego. We can consider that the GPS is perfectly suited to the measurement of this feature, since it has been designed to this end. It can also be assumed that the combination of the relative and absolute positions of A is less suitable because of the potential errors during communication, and also because information received from A may be considered as less trustworthy. Finally, the prediction is a default choice when other sources of information are considered as faulty and should be rated as the least relevant source of information.

Relevance thus defines a partial order between the sources of information for each feature (100% being the most relevant) to favor specific sources of information with respect to others.

Trust in the source Trust in the source is a percentage that reflects the quality of the measurements provided by the source during a limited time window corresponding to a near past. When a source provides a measure that is considered as correct, the trust increases, and conversely it diminishes if the measure is considered incorrect, according to equation [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF].

Trust in the source at iteration t, expressed as a percentage, depends on its value at iteration t -1 and on the distance between the tolerance interval of the value coming from the source (IT s ) and the tolerance interval of the value that has been selected (IT r ) from all possible sources for this feature (a tolerance is fixed for each feature). It is assumed that a penalty must be greater than a reward, in order to quickly detect a malfunction of a source or misleading information sent by a malicious vehicle. It is thus not necessary to rely on any reputation system: a new vehicle will be given at first a medium trust; if the information sent by the vehicle is coherent, the trust will quickly increase, but if it is not, the source will be strongly penalised and quickly discarded.

Trust 0 = 100 Trust t =    min(100, Trust t-1 + σ ++ ) if R ∈ IT s min(100, Trust t-1 + σ + ) if R ∈ IT s and IT r ∩ IT s = ∅ max(0, Trust t-1 + σ -) otherwise (1) with σ -< 0 < σ + < σ ++ and |σ -| > |σ ++ |.
Freshness of information The sources of information are not synchronous. Each source produces features at its own pace, and each value is given a measure of freshness: a value that has just been received at the time of calculation has a freshness of 100%, a value that has an age that exceeds a threshold is considered out of date (see equation 2). We consider a fixed freshness for a time d, before a linear decay, according to a gradient a that may be variable depending on the feature.

Freshness(age) = 100 if age ≤ d 100 -a(age -d) otherwise (2)
To prevent the system from relying solely on its predictions, especially in the case where no reliable source is available, the prediction value is given a freshness, which is the age of the scene from which the prediction has been computed.

Consistency of information

To ensure consistency between the various scenes selected at each moment t, we add a percentage that takes into account the predicted value val p , the measured value val m , and the margin of error toleranceError m associated with val m . The predicted value is calculated from a bounded time window, using a linear regression over the values measured by a sensor. The distance between val p and val m is then calculated. If this distance is less than a certain threshold, a percentage associated with this distance is assigned, otherwise it is considered that this new measured value val m is not consistent with the predicted value val p :

Consistency = 200 - |valp-valm| toleranceErrorm +1 • 100 with 0 ≤ Consistency ≤ 100 (3)
Confidence Based on the four aforementioned criteria, we calculate a global measure of Confidence for each source of information according to the following formula:

Confidence = Relevance • Trust • Freshness • Consistency 100 4
• 100 (4)

The algorithm

At each iteration and for each feature, given the set of values provided for this feature by all the sources of information, the algorithm selects the unique value R in the following steps:

1. calculate, for each source, the value of the feature and a measure of Confidence in the value. 2. select, among all the sources, the one for which the Confidence in the value is the best and store the (plausible) value R of the selected source. In case of equality, we choose the source whose value is higher in the following order: Relevance > Trust > Freshness. In case no source of information has a Confidence above a predefined threshold ζ, the emergency stop is launched. 3. update the trust in all the sources, by attributing rewards or penalties, according to equation [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF]. This enables to quickly disregard faulty or malicious sources, but also to allow a source to have temporary failures (e.g. the GPS in a tunnel), without definitely blacklisting it. Trust in Prediction is a special case: it is given the trust value of the source selected at this iteration.

One may argue that some sources of information rely, for the calculation of a given feature, on the values of other features, which may create mutual dependencies between the different sources of information. To overcome this problem, if some required feature is not available yet, we can use instead the predicted value for this feature.

Implementation and experimentation

We did a large number of simulations using GAMA [START_REF] Taillandier | Building, composing and experimenting complex spatial models with the gama platform[END_REF], a free and open-source agent-based simulation environment, with its "vehicleBehaviorExtension" [START_REF] Sobieraj | Méthodes et outils pour la conception de Systèmes de Transport Intelligents Coopératifs[END_REF], which we have enriched with a set of sensors. Using this framework, we implemented the plausibility algorithm described in this paper, as well as the decision algorithm proposed in [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF]. We have also implemented a simplified version of the action module, which makes it possible to obtain flexible longitudinal and lateral trajectories.

The aim of the experimentation was to validate that the Ego vehicle could always maintain a coherent scene at any time, whatever the perturbations or attacks arising on the sensors. As a first step, we assumed that internal sensors could not be hacked, and that the only attacks could come from communications. We consider in our scenario the following anomalies:

-Noise: a random value in the range of the error margin [-δ,+δ] of the information source is added to the actual value; -Breakdown: a source of information does not provide information at time t; -Fault: the actual value is replaced by a random one.

Our test scene contains two vehicles (Ego and A). Ego has an initial speed of 35 m/s and is controlled by our decision algorithm. Vehicle A has only a V2V sensor, has an initial speed of 28 m/s, and is controlled by IDM (intelligent driving model) [START_REF] Treiber | Congested traffic states in empirical observations and microscopic simulations[END_REF]. The road consists of two lanes with a length of 1 km. Both vehicles are on the same road lane, Ego behind A at some distance, so that Ego has to overtake A before the end of the lane.

Our algorithm uses a set of parameters, which have a direct impact on the performance of the system. For now, we did not achieved any parametric study but selected these values empirically, in order to obtain desired properties (e.g. the time after which a source is disregarded, or considered again after recovering). In the following, we quote the most important ones, with the corresponding values:

the rewards and penalties σ ++ , σ + , σ -, are set respectively to 25, 10 and -30. They have an impact on the time the system takes to eliminate a faulty source of information and to reconsider a previously eliminated source; the source filter threshold ζ =30%; the delay d and the gradient a a in the calculation of freshness: d is equal to the period of the sensor; we assume that this delay remains at 100% as long as the information is available in the period, while beyond this period, it decreases rapidly with gradient a = 8.

Results of experiments and discussion

We first studied the nominal case, i.e., the case with no faults except the noise associated with the sensors. Figure 1 represents the evolution of the selected values of the relative position of vehicle A with respect to Ego. It is very similar to that of actual values, confirming the choices that were made by the algorithm. The change of sources of information around 12k cycles corresponds to the loss of perception of the vehicle A during an overtaking. At first, A is seen by the front camera, then by the right camera, and finally by the rear camera.

We then inject targeted and random faults. Targeted injection aims at analyzing the ability of the solution to withstand potentially critical cases, while random injection tests the solution empirically.

Targeted fault injection Figure 2 shows the impact of fault injection to camera (1) (primary source) and camera (2) (secondary sensor). We injected two faults in each sensor, which consist in random values being provided by the sensors, in the intervals [500ms, 900ms] and [2100ms, 2800ms] for camera [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF] and [750ms, 1050ms] and [1900ms, 2400ms] for camera [START_REF] Arena | An overview of vehicular communications[END_REF]. One may observe that the system rejects the faulty source as soon as the error is injected (camera ( 1) is rejected at time 500ms and camera ( 2) is rejected at time 750ms). The system selects a third source while waiting for the faulty sources to resume, which is the case for camera (1) at time 1900ms, 1s after the end of the first fault. At time 2100ms, camera (1) is rejected again as a second fault occurs, and since camera (2) is also faulty at that time, camera (3) resumes. Camera (2) resumes at time 3400ms and camera (1) resumes at time 3800ms, 1s after the end of their respective fault interval. Random fault injection In this configuration, we inject faults and failures at random times.

-For failures, which may occur at any time, we observe that if occurrence probability is under 50%, the system always manages to find a reliable source of information and that the number of switches increases proportionally to the probability of failure. -For faults, which consist in random values appearing at random moments, if probability of occurrence is under 5% for each information source, we observe that the system always finds a reliable source and a value to select. Indeed, the frequency of injection is very low (on average two injections per second), which allows the system to penalize and then reward the source on average in two cycles. Similarly, since injections do not last long, trust is restored very quickly, and the system thus remains operating.

Limitations Although our proposal gives promising results in most situations, its operation is quite sensitive to the choice of parameters. It may happen for example that the system becomes unstable: when an incorrect value has once been selected, the system penalizes all sources of information that are giving correct values; therefore, once the fault injection phase is over, it cannot find a reliable source to select, either because of a low trust, or because of a low consistency.

This issue may be overcome by implementing several improvements to the method: the first one would be to compute the consistency of a feature with more elaborated methods than a simple linear regression. Kalman filters are good candidates since they would allow to take noise and errors into account; a second possible improvement is to also assess the consistency of the value of a feature with respect to the values provided by the other sources of information for the same feature; A third improvement would be, instead of selecting a single value as the most plausible one, to average the values of all the sources of information that appear to be consistent in the measure of the feature, which is common in the field and would limit the impact of incorrect values.

Finally, a parametric study is necessary in order to fine-tune the algorithm. By understanding precisely the role of each parameter, this will enable on the one hand to improve and stabilize the results, and on the other hand to give the user the choice between different driving options, all of which guaranteeing a safe behavior.

Conclusion and perspectives

The objective of this project was to design an algorithm to increase the robustness of the decision of an autonomous vehicle, taking into account the redundancy of the information collected by the sensors. To this end, we proposed a mechanism to select in real time, among the values coming from the various sensors, the most plausible ones to be used in the construction of the scene, in order to have the best possible decision making.

The approach is partially inspired by trust-based approaches, and is adapted to the particular context of our project and its constraints. This resulted in a hybrid model that analyzes the operation of sensors (or more generally sources of information), as well as the variation of the measured or computed values. This model takes into account the relevance of a source for a feature, the trust in the source, the freshness of the information and the consistency of the information in time.

In order to assess the validity of the proposal, we conducted an intensive campaign of experiments. Only a few results are presented in this article, but the model has demonstrated a highly satisfying behaviour and has met the expectations in a large range of conditions, either in the nominal case or in the presence of various forms of failures. Some limitations have clearly been identified, but one of the main strength of the algorithm lies in its modular design, which enables a lot of adaptations and tuning for the computation of each of the four criteria. In the process of developing the algorithm, some parts of the model have deliberately been kept simple (and even naive) in a first step and the parameterization has been done very quickly and empirically. This was to validate the general principle of the computation of a global measure of confidence in the values provided by the various sources of information, and the selection of the most plausible one, without focusing on details of implementation or specific optimizations. Now that the approach has proved to be valid, we will concentrate on these details, notably to improve the computation of the consistency of the values.

Fig. 1 .

 1 Fig. 1. Selected value R of relative position of vehicle A with respect to Ego: nominal case

Fig. 2 .

 2 Fig. 2. Relative position of vehicle A wrt Ego: fault injection into camera (1) and camera (2)

Table 1 .

 1 Ego's sensors with their respective tolerances δ.

	Sensor	Feature	Sampling	Angle	Range	δ
	GPS	P os abs , Speed abs	25 Hz	-	-	1m
	LiDAR	P os rel , Speed rel	20 Hz	360 •	150 m	1%
	Camera	P os rel , Speed rel	20 Hz	120 •	200 m	0.5%
	Ultrasound	P os rel	20 Hz	120 •	4 m	0.05%
	V2V	P os abs , Speed abs	1 Hz	360 •	1 km	1m
	Source of information	P os abs Ego P os abs Vi P os rel Vi	δ
	GPS					1m
	V2V Communications				1m
	LiDAR					1%
	Camera					0.5%
	Ultrasound					0.05%
	(GPS, V2V communications)				1m + 1m
	(GPS, LiDAR)					1m + 1%
	(GPS, Camera)					1m + 0.5%
	(GPS, Ultrasound)			1m + 0.05%
	(V2V Communications, LiDAR)				1m + 1%
	(V2V Communications, Camera)				1m + 0.5%
	(V2V Communications, Ultrasound)			1m + 0.05%
	Prediction					0

Table 2 .

 2 Sources of information to calculate the P osition features of Ego and vehicles Vi.


Johan Arcile
email: johan.arcile@gmail.com

Raymond Devillers

Hanna Klaudel
email: hanna.klaudel@ibisc.univ-evry.fr

Models for the dynamic exploration of the state spaces of autonomous vehicles

We present multi-agent timed models, called MAPTs, where each agent is associated with a regular timed schema upon which all possible actions of the agent rely. MAPTs allow for a layered structure of the state space, so that it is possible to explore the latter dynamically and use heuristics to greatly reduce the computation time needed to address reachability problems. We then use an available tool for the Petri net implementation of MAPTs, to explore the state space of autonomous vehicle systems and compare this exploration with timed automata-based approaches in terms of expressiveness of available queries and computation time.

Introduction

In this paper we propose models and methods tailored for efficient model-checking of multi-agent systems composed of periodic communicating autonomous agents evolving in a constrained environment. Typical examples of such systems are systems of Communicating Autonomous Vehicles (CAVs), where each vehicle (agent) observes its environment (the road, the other vehicles) and periodically evaluates its environment in order to make a decision on the action to perform. The decision policies of CAVs often rely on trajectory planning algorithms studied in 3D simulation, sometimes in conjunction with on-road experiments [START_REF] Katrakazas | Real-time motion planning methods for autonomous on-road driving: State-of-the-art and future research directions[END_REF][START_REF] Kuwata | Real-time motion planning with applications to autonomous urban driving[END_REF][START_REF] Furda | Enabling safe autonomous driving in real-world city traffic using multiple criteria decision making[END_REF][START_REF] Likhachev | Planning long dynamically feasible maneuvers for autonomous vehicles[END_REF][START_REF] Glaser | Maneuverbased trajectory planning for highly autonomous vehicles on real road with traffic and driver interaction[END_REF]. While it is possible to plan a collision-free trajectory for a vehicle with this technique, this does not guarantee the efficiency or robustness of a given decision policy.

Therefore, various properties of such systems are of interest to study safety, efficiency and robustness of the decision choices when some variability is introduced in the reaction times, transmission delays, etc. They can be either Boolean ones (e.g. Does some vehicle overtake another one before some milestone? Is a collision possible for a given safety distance?) or numerical ones (e.g. What is the minimal distance between two vehicles? What is the biggest deceleration for some vehicle?). This motivates the use of formal methods and several approaches exist focusing on the properties of vehicles (functional layer [START_REF] Foughali | Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots[END_REF] or soundness of vehicle platooning [START_REF] Kamali | Formal verification of autonomous vehicle platooning[END_REF]) or a system of vehicles in their environment. Their drawbacks are twofold: some only allow for basic interactions [START_REF] Quottrup | Multi-robot planning : a timed automata approach[END_REF] while others lead to unsatisfactory computation times because of their high-level of realism [START_REF] O'kelly | APEX : Autonomous vehicle plan verification and execution[END_REF].

The framework VerifCar [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF] allows to answer such questions, with a specific focus on the impact of latencies and communication delays on the behaviour of CAVs. Each vehicle is modelled by an agent which performs time restricted actions that impact the valuation of shared variables describing the agents' states and the environment. The system is highly non-deterministic due to overlaps of timed intervals in which the actions of various agents can occur. This model is based on timed automata with an interleaving semantics [START_REF] Alur | Automata for modelling real-time systems[END_REF], and is implemented in Uppaal [27], a state of the art tool for real time systems with an efficient state space reduction for model checking. Furthermore, Uppaal allows to consider complex shared data structures and update functions, which are needed to model CAV systems. However, it is limited in terms of the kind of queries that may be asked on the models and deals only with discrete values for the shared variables, which is not always convenient and may lead to imprecise computations.

A closer look at the state spaces in the applications studied with VerifCar shows that they take the form of a directed acyclic graph (DAG). Each agent also has syntactically the form of a DAG between clock resets, and various forms of agents' communications are modelled through shared variables. Our goal is then to exploit these peculiarities to build a dedicated checking environment for reachability problems, when the models satisfy the kind of restricted forms we observed for CAV systems (as well as some other application domains). The hope is that this will allow to get rid of the uncomfortable restrictions we observed on the kind of queries that may be solved, while allowing to do it efficiently. Our aim is thus to change the balance between the expressiveness of the models and the richness of the queries while keeping a reasonable efficiency.

Concretely, we want to explore the state graph dynamically (checking temporal logic properties and computing numerical indicators directly as we explore states) to avoid constructing the full state space, and therefore not to loose time and memory space storing and comparing all previously reached states. The objective is to be able to tune the verification algorithm with heuristics that will choose which path to explore in priority, which might significantly speed up the computation time if the searched state exists. That implies that our algorithms should explore the graph depth-first, since breadth-first algorithms cannot explore paths freely and are restricted to fully explore all the states at some depth before exploring the next one.

For systems featuring a high level of concurrency between actions, such as the CAV systems, most of the non-determinism results from possibly having several actions of different agents available from a given state, that can occur in different orders and which often lead eventually to the same state. This corresponds in the state space to what is sometimes called diamonds. Breadth-first exploration allows to compare states at a given depth and therefore remove duplicates. On the other hand, depth-first exploring such a state space with diamonds, leads to examine possibly several times the same states or paths, which is not efficient. In this context, our aim is to detect and merge most identical states coming from diamonds while continuing to explore the state space mainly depth-firstly. This diamond detection will consist in a breadth-first exploration in a certain layer of the state space, each layer corresponding to some states at a given depth having common characteristics. It turns out that such layers are typically observed in the state spaces of CAV systems. This allows for a depth-first exploration from layer to layer, while greatly reducing the chances of exploring several times the same states. The class of models on which this kind of algorithm can be applied will be referred to as Multi-Agent with timed Periodic Tasks (MAPTs).

In order to analyse a model, it is useful to translate it into formalisms for which we have existing tools. Like in [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF], we may use networks of Timed Automata [START_REF] Alur | Automata for modelling real-time systems[END_REF] and the tool Uppaal [27] or Time Petri net analyzers, such as Romeo [START_REF] Lime | Romeo: A parametric model-checker for Petri nets with stopwatches[END_REF] or Tina [START_REF] Berthomieu | The tool TINA -construction of abstract state spaces for Petri nets and time Petri nets[END_REF]. However, to keep a better control on the models and queries, we chose to implement our algorithms with Zinc [START_REF] Pommereau | ZINC: a compiler for "any language"-coloured Petri nets[END_REF], a compiler for high-level Petri nets that generates a library of functions (in Python) allowing to easily explore the state space. In particular, this allows to apply heuristics leading to faster computation times. Another gain when comparing to Uppaal is that it is easy to represent complex data structures, possibly using non-integer variables, thus limiting the loss of information.

The existing works on state space reduction such as [START_REF] Vernadat | Covering step graph[END_REF][START_REF] Clarke | State space reduction using partial order reduction[END_REF] use partial-order reductions to explore a subset of the graph, and [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] adapts this methods to Time Petri nets. In those approaches, some independent transitions are merged together to build a single transition in the state space. This requires to know beforehand those different paths leading to a common state, which cannot be done in the models we address. Indeed, diamonds may appear or not depending on the values of the shared variables.

Other approaches, using bounded model checking [START_REF] Clarke | Bounded model checking using satisfiability solving[END_REF][START_REF] Biere | Bounded model checking[END_REF][START_REF] Penczek | Verifying epistemic properties of multi-agent systems via model checking[END_REF], where a Boolean formula describes an execution of a given length, have been used for studying temporal logic properties. The size of the Boolean formula being exponential in function of the number of variables, this method is effective in terms of computation time only for a restricted length. This is particularly problematic for the systems we study, where the state of the system is described by a large number of scalar variables. In addition, this kind of approaches does not generally allow to prove safety properties, hence to be able to conclude on the non-reachability of a state.

Concerning the exploration algorithms, since the systems we aim to model with MAPTs produce acyclic state spaces, this allows us to use more efficient on-the-fly algorithms for CTL than those proposed in the literature for general cases, such as [START_REF] Bhat | Efficient on-the-fly model checking for CTL[END_REF][START_REF] Ben-David | Scalable distributed onthe-fly symbolic model checking[END_REF].

In this paper, we start with a formal definition of MAPT, give some examples and provide a translation to high-level Petri nets. Then, we present the exploration algorithms taking advantage of the layered structure, weak and strong variables, and heuristics. Finally, we use MAPT in experiments that highlight the benefits of our approach in terms of expressiveness of available queries and computation time, and compare them with VerifCar when possible. The contributions of the paper are the introduction and analysis of the MAPTs, as well as the efficient exploration method dedicated to this new formalism.

Syntax and semantics of MAPTs

We first define G-MAPTs, composed of several agents that may interact through shared variables. Each agent is associated with a unique local clock and performs actions occurring in some given time intervals. There is no competition between agents in the sense that no agent will ever have to wait for another one's action in order to perform its own actions. However, there may be non-determinism when several actions are available at the same time, as well as choices between actions and time passing.

A G-MAPT is a tuple (V, F, A, Init) where:

-V is a set of values; -F is a (finite) set of calculable functions from V to V; -A is a set of n agents such that ∀i ∈ [1, n], agent A i df = (L i , C i , T i , E i ) with: • L i is a set of localities denoted as a list L i df = (l 1 i , . . . , l mi i ) with m i > 0, such that ∀i = j, L i ∩ L j = ∅; • C i is the unique clock of agent A i , with values in N (we assume C i = C j if i = j
, but they may have the same value); • T i is a finite set of transitions, forming a directed acyclic graph between localities, with a unique initial locality l 1 i and a unique final locality l mi i , each transition being of the form (l, f, I, l ) where l, l ∈ L i are the source and destination localities, f ∈ F is a transformation function and

I df = [a, b] is an interval with a, b ∈ N and a ≤ b; • E i ∈ N \ {0} is the reset period of agent A i . -Init is a triple ( --→ init L , --→ init C , init V ) = ((l 1 , • • • , l n ), (init 1 , • • • , init n ), init V ) where ∀i ∈ [1, n], l i ∈ L i , init i ∈ N and init V ∈ V.
For each agent A i and each locality l ∈ L i , we shall define by l • = {(l, f, I, l ) ∈ T i } the set of transitions originated from l, and by • l = {(l , f, I, l) ∈ T i } the set of transitions leading to l. We assume that • l 1 i = ∅ and (l mi i ) • = ∅. Moreover, when i = j, since L i ∩ L j = ∅, T i ∩ T j = ∅ too, so that each transition belongs to a single agent, avoiding confusions in the model. A simple example of a G-MAPT M with two non-deterministic agents is represented in Ex. 1.

In the semantics, for each agent A i , we emulate a transition r i from l mi i to l 1 i that resets clock C i every E i time units. As such, each agent in the network cycles over a fixed period. There can be several possible cycles though, since a given locality may be the source of several transitions, so that there may be several paths from l 1 i to l mi i . The behaviour of the system is defined as a transition system where Init is the initial state. A state of a G-MAPT composed of n agents is a tuple denoted by s = ( l, c, v) where l

= (l 1 , • • • , l n ) with l i ∈ L i the current locality of agent A i , c = (c 1 , • • • , c n ) where c i ∈ N is the value of clock C i ,
and v ∈ V. We shall sometimes consider that v is the value of some shared variable V used to model the evolution of the system.

There are three possible kinds of state changes: a firing of a transition, a clock reset and a time increase. From the state s = ( l, c, v):

-A transition (l, f, [a, b], l ) ∈ T i can be fired if l i = l and a ≤ c i ≤ b. Then, in the new state, l i ← l and V ← f (v). -For any agent A i , clock C i can be reset if l i = l mi i and c i = E i . Then, C i ← 0 and l i ← l 1 i . -Time can increase if ∀i ∈ [1, n], either there exist at least one transition (l, f, [a, b], l ) ∈ T i with l i = l and c i < b, or l i = l mi i and c i < E i . A time increase means that ∀i ∈ [1, n], C i ← c i + 1.
The transition system associated with a G-MAPT is driven by these state changes, from the initial state. It may be observed that there is a single shared element in such a system: variable V ; all the other ones are local to an agent. It is unique but its values may have the form of a vector, and an agent may modify several components of this vector through the functions of F used in its transitions, thus emulating the presence of several shared variables. The values of V are not restricted to the integer domain, but there is only a countable set of values that may be reached: the ones that may be obtained from init V by a recursive application of functions from F (V is not modified by the resets nor the time increases). However this domain may be dense inside the reals, for instance.

Example 1. Let M = (V, F, A, Init) where:

-V = R × N; -F = {f 1 , f 2 , f 3 , f 4 } with f 1 (x, y) → (2x, y + 1) f 2 (x, y) → (x + 1.3, y + 1) f 3 (x, y) → ( x 2 , y) f 4 (x, y) → (2x, y) -A = {(L 1 , C 1 , T 1 , E 1 ), (L 2 , C 2 , T 2 , E 2 )} with L 1 = {1, 2} T 1 = {(1, f 1 , [1, 2], 2), (l, f 2 , [3, 3], 2)} E 1 = 5 L 2 = {3, 4} T 2 = {(3, f 3 , [1, 2], 4), (3, f 4 , [3, 3], 4)} E 2 = 5 -Init = ((1, 3), (0, 0), (0.5, 0)).
A visual representation of M and the initial fragment of its dynamics is depicted in Fig. 1. ♦ G-MAPT semantics when considered in a naive way is prone to a state space explosion phenomenon. Motivated by our target applications, we restrict G-MAPTs with Assumption 1 to produce state spaces being DAGs.

Assumption 1 (acyclicity of the state space) 1. V may be promoted into a partially ordered set (V, <) and there exist an agent A i such that, in all paths from l 1 i to l mi i in the local graph of A i (see for example Fig. 1), there exists a transition

t df = (l, f, [a, b], l ) such that for all v ∈ V, v < f (v); in general, V = W × X,
where (X, <) is a known ordered set and the order is extended in a natural way to V by stating that

(w, x) < (w , x ) iff x < x ; 1 2 [1, 2] f1 [3, 3] f2 E1 = 5 3 4 [1, 2] f3 [3, 3] f4 E2 = 5
(1, 3; 0, 0)

(1, 3; 1, 1) (1, 3; 2, 2) (1, 3; 3, 3) +1 +1 +1 (2, 3; 1, 1) (2, 3; 2, 2) (2, 3; 3, 3) +1 +1 (1, 4; 1, 1) (1

and there is no

f ∈ F such that for some v ∈ V, we have f (v) < v.
Item 1 ensures that at least one agent increments the variable V at least once between two of its resets.

Item 2 ensures that no function can decrease the variable V . The result is an absence of cycles in the whole state space of the G-MAPT.

Furthermore, in order to shorten the computation time of the queries, we also consider an accelerated semantics that often allows to increase time by several time units in one step. We shall not detail it here (see [START_REF] Arcile | Conception, modélisation et vérification formelle d'un système temps-réel d'agents coopératifs : application aux véhicules autonomes communicants[END_REF][START_REF] Arcile | Dynamic exploration of multi-agent systems with timed periodic tasks[END_REF]) but we shall use it in the experiments shown later in this paper. It needs the following assumptions:

Assumption 2 (strong liveness) 1. If the initial locality of some agent A i is the terminal one (l i = l mi i ), then the initial value of clock C i satisfies init i ≤ E i ; 2. otherwise (when l i = l mi i ), we have init i ≤ max{b | (l i , f, [a, b], l ) ∈ l i • }); 3. moreover, for each agent A i , if l ∈ L i \ {l 1 i , l mi i }, then max{b | (l , f, [a, b], l) ∈ • l} ≤ min{b | (l, f , [a , b ], l ) ∈ l • }; 4. and we have max{b | (l , f, [a, b], l mi i ) ∈ • l mi i } ≤ E i .
Items 1 and 2 ensure that, when the system is started, either in the terminal locality or in a non terminal one of some agent, the time is not blocked and we shall have the possibility to perform an action in some future.

Item 3 ensures that whenever a non terminal locality is entered, any (and not only some) transition originated from that locality will have the possibility to occur in some future (the case when we enter an initial locality is irrelevant since resets reinitialise the corresponding clock to 0). Item 4 captures similar features in the case when we enter a terminal locality. In other words, each transition or reset in l • is enabled when entering l or will be enabled in the future (after possibly some time passings in order to reach the lower bound a). Definition 2. A MAPT is a G-MAPT satisfying Assumptions 1 and 2.

Translation into high-level Petri nets

A high-level Petri net [START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use[END_REF] can be viewed as an abbreviation of a low-level one [START_REF] Peterson | Petri Net Theory and the Modelling of Systems[END_REF] where tokens are elements of some set of values that can be checked and updated when transitions are fired 3 . Here, we express a G-MAPT as a high-level Petri net to be implemented with Zinc [START_REF] Pommereau | ZINC: a compiler for "any language"-coloured Petri nets[END_REF].

Formally, a high-level Petri net is a tuple (S, T, λ, M 0 ) where:

-S is a finite set of places; -T is a finite set of transitions; λ is a labelling function on places, transitions and arcs such that • for each place s ∈ S, λ(s) is a set of values defining the type of s,

• for each transition t ∈ T , λ(t) is a Boolean expression with variables and constants defining the guard of t and • for each arc (x, y) ∈ (S × T ) ∪ (T × S), λ(x, y) is the annotation of the arc from x to y, driving the production (on y, when x ∈ T and y ∈ S) or consumption (from x, when x ∈ S and y ∈ T ) of tokens (see an example below). -M 0 is an initial marking associating tokens to places, according to their types: for each s ∈ S, M 0 (s) is a finite multiset of values in λ(s).

The semantics of a high-level Petri net is captured by a transition system containing as states all the markings which are reachable from the initial marking M 0 . A marking M is directly reachable from a marking M if there is a transition t enabled at M , whose firing leads to M ; it is reachable from M if there is a sequence of such firings leading to it. A transition t is enabled at some marking M if the tokens in all the input places of t allow to satisfy the flow expressed by the annotations of input arcs and the guard of t, through a valuation of the variables involved in the latter. The firing of t consumes the concerned tokens in input places of t and produces tokens on output places of t, according to the annotations of the output arcs and the same valuation, as shown below for a transition before and after the firing.

1 s 1 2 s 2 (0, 0) s 3 t x > 0 x y (w, z) (w + x, z + y) s 1 s 2 (1, 2)
s 3 t x > 0 x y (w, z) (w + x, z + y) Definition 3. Given a G-MAPT Q = (V, F, A, Init) with |A| = n, its trans- lation to a high-level Petri net N = translate(Q) = (S, T, λ, M 0 ) is defined as follows: -S = {s A , s C , s V } with λ(s A ) df = L 1 × • • • × L n where L i is the set of localities of agent A i (its jth element is denoted l j i ), λ(s C ) df = N n and λ(s V ) df = V. For any token x of the type λ(s A ) or λ(s C ), x[i] is the i th element of the list. -T df = T trans ∪ T reset ∪ {t time } where • T trans is the smallest set of transitions such that, for each agent A i = (L i , C i , T i , E i ) in A and for each transition (l, f, [a, b], l ) ∈ T i , there is a transition t ∈ T trans such that λ(s A , t) df = x, λ(s C , t) df = y, λ(s V , t) df = z, λ(t, s A ) df = x where x [i] ← l and ∀j = i, x [j] ← x[j], λ(t, s C ) df = y, λ(t, s V ) df = f (z) and λ(t) df = (x[i] = l) ∧ (a ≤ y[i] ≤ b)
. This is equivalent to the set of transitions of the G-MAPT.

• T reset is the smallest set of transitions such that, for each agent

A i = (L i , C i , T i , E i ) in A, there is a transition t ∈ T reset such as λ(s A , t) df = x, λ(s C , t) df = y, λ(t, s A ) df = x where x [i] ← l 1 i and ∀j = i, x [j] ← x[j], λ(t, s C ) df = y where y [i] ← 0 and ∀j = i, y [j] ← y[j], and λ(t) df = (x[i] = l mi i ) ∧ (y[i] = E i ) where m i df = |L i |. This is equivalent to the set of clock resets of the G-MAPT. • λ(s A , t time ) df = x, λ(s C , t time ) df = y, λ(t time , s A ) df = x, λ(t time , s C ) df = y , where ∀i ∈ [1, n], y [i] ← y[i] + 1, and λ(t time ) df = G 1 ∧ • • • ∧ G n
where G i acts as the "upper bound guard" for all the transitions in agent

A i , i.e., G i df = (g 1 ∨ • • • ∨ g mi ) with m i = |L i | and ∀j ∈ [1, m i -1], g j df = (x[i] = l j i ) ∧ (y[i] < B), where B = max{b|(l j i , f, [a, b], l ) ∈ l j i •
} is the highest upper bound of the intervals from all outgoing transitions of l j i and g mi

df = (x[i] = l mi i )∧(y[i] < E i ). This is equivalent to a time increase. -(M 0 (s A ), M 0 (s C ), M 0 (s V )) = Init is the initial marking
The translation associates singletons as arc annotations for all arcs. As a consequence, during the execution, starting from the initial marking which associates one token to each place, there will always be exactly one token in each of the three places. Each reachable marking, where s A contains l, s C contains c and s V contains v, encodes a state ( l, c, v) of the considered G-MAPT.

It is easy to see [START_REF] Arcile | Conception, modélisation et vérification formelle d'un système temps-réel d'agents coopératifs : application aux véhicules autonomes communicants[END_REF] that the transition system of a G-MAPT Q is isomorphic to the one of its translated Petri net translate(Q). It is easily possible to modify this translation to correspond to the accelerated semantics (mentioned, but not detailed, above).

Dynamic exploration of a MAPT

When model checking a system, one usually has the choice between a depth-first and a breadth-first exploration of the state space. For reachability properties (where one searches if some state satisfying a specific property may be reached), depth-first (directed and limited by the query) is usually considered more effective. However, the majority of the non-determinism in systems featuring a high level of concurrency (such as CAV systems) leads to diamonds. Indeed, if transitions on different agents are available at a state then they may occur in several possible orders, all of them converging most of the time to the same state (if the applied functions commute). In order to avoid exploring again and again the same states, a depth-first exploration needs to store all the states already visited up to now, which is usually impossible to do in case of large systems. For example, if states s1 and s2 share a common successor s3, when the algorithm will compute the successors of s1, it will classically remove s1 from the stack and continue with its successors, until reaching s3 and exploring all paths from s3, forgetting each time the nodes already visited. That way, when the algorithm has explored all paths from s1 and starts exploring from s2, there is no memory of s3 having been explored already, and thus all paths starting from it will be explored again.

On the contrary, using breadth-first algorithms would partly allow to avoid that issue, because duplicate states obtained at a given depth can be removed. However, this would also imply exploring all reachable states at a given depth and forbid using heuristics to guide and limit the exploration.

An idea is then to combine both approaches, which is possible for MAPTs, using the layered approach described next. A MAPT may be non-deterministic but it is strongly live and has a DAG state space. For instance, the G-MAPT M from Ex. 1 satisfies both assumptions (acyclicity is satisfied due to y being incremented in all cycles of A 1 ) and so is actually a MAPT.

Layered state space

The state space of a MAPT shows an interesting characteristics: apart from having no cycles, its structure can often be divided in layers such that all states on the border of a layer share the same vectors of localities and clocks (and thus, the same set of enabled transitions) and are situated at the same time distance from the initial state. The only difference concerns the value of the variable, due to the non-determinism and the concurrency inherent to this kind of models. Non-determinism means that an agent has the choice between several transitions at some location; concurrency means that at least two agents may perform transitions at some point. In the first case, several paths may be followed by the agent to reach some point, leading to different values of the variable; in the second case, transitions of the two agents may be commuted, leading again to different values of the variable if the corresponding functions do not commute.

For instance, if agent A i in a MAPT starts at l 1 i with a null clock, after E i time units and before (E i + 1) time units, it shall necessarily pass through its reset (it is possible that it performs other transitions before and/or after this reset without modifying its clock, but it is sure the agent will go through this reset before performing a new time passing). Hence, if each agent starts from its initial locality with a null clock, after lcm{E 1 , . . . , E n } (i.e., the least common multiple of the various reset periods; denoted in the following by lcm(E)) time units, it is sure we shall revisit the initial localities with null clocks, but possibly with other values of the variable V , yielding the border of a layer. From this border the same sequences of transitions/resets/time-passings as initially will occur periodically (with a period of lcm(E)), leading to new borders, with the initial localities and the null clocks.

Exploring layered state space The function N extBorder(state) takes a state ( l, c, v) and computes, through a breadth-first exploration, the set of successors up to the next border. To do so we introduce a function N extState(s), which returns the set of all successors of state s. This is used iteratively in a depth-first exploration to jump from a state to one of its successors belonging to the next border. During this exploration, an additional function may be used to check if a visited state satisfies some condition. Such a use of layers allows to reduce the number of explored paths by detecting diamonds caused by the order of transitions of concurrent agents.

Exploration using strong and weak variables The approach presented above does not deal with diamonds spreading on a time distance longer than the one between two adjacent borders. For example, it may still happen that two different states s 1 and s 2 belonging to the same border have a common successor s in the future. To cope with this issue, it is more interesting to perform the breadthfirst exploration that computes successors at the next border for the set {s 1 , s 2 } instead than taking them separately. In general, it is not obvious to know or guess which states should be kept together in the computation of the next border. Indeed, one should be able to determine when sets of states should be split in sub-sets and when they should be kept together. To perform such a clustering, it may be interesting to exploit the properties of target applications, such as CAVs.

A possible solution is to assume V df = V w × V s , where V w (weak) is a "less important" part of V and V s (strong) a "more important" one, such that states differing in the valuation of V s are unlikely to have a common successor, while this is not the case for V w . Symmetrically, states with the same valuation of V s are more likely to have a common successor. This may give us a criterion to cluster states and jump from a set of states to the set of their successors at the next border. The choice of V s and V w is of course system-dependent and should be defined by an expert, or with the help of a simulation tool. As an example, elements that can be assigned a new value independently of their previous one might be considered as weak, while elements whose value changes depend on their present value (for instance the position of a moving object) might be considered as strong.

The function ClusteredN extBorder(state set) is then an easy variant of N extBorder(state), taking a set of states and producing a set of clusters, i.e., sets of states having identical values of variables in V s . It is used in a similar way as N extBorder() to explore in a depth-first manner the layered state space, the only difference being that it jumps from a cluster belonging to some border to a cluster belonging to the next one, based on the choice of V s .

Exploration algorithms

This section is dedicated to exploration algorithms of finite prefixes of MAPTs: states that do not have successors in the considered prefix will be called final. The algorithms are denoted with the CTL temporal logic syntax. Since this temporal logic is meant to explore infinite paths, we shall consider that each final state has a self loop.

Our algorithms have two main characteristics: they operate "on-the-fly", which means that they do not store the entire visited state space (but only a cut of it), and they can be tuned with heuristics defining a priority on paths to be explored, that might significantly speed up the computation time if the searched states exist. To do so we rely on the procedure ClusteredN extBorder() mentioned above. Since our algorithms do not store all the states that have been explored, we do not return traces of execution, unlike what is usually proposed by standard temporal logic model checking tools.

Although the general case for checking reachability CTL formulas has not yet been implemented (left for a future work), it can be done easily thanks to the absence of cycles in the state space. Here, we shall present the algorithms used in our experiments. The atomic formulas p can be any Boolean formula using variables or current localities of the state where p is checked. It is also possible to use clock values, but only with the original semantics: the accelerated semantics reduces the state space in a way that preserves the sequences of transitions, but not all the clock values.

The algorithm for EF p (meaning a reachable state satisfies p) consists, starting from a stack containing the initial state, in taking the first element s of the stack, returning it if p is true on s, and otherwise adding the result of ClusteredN extBorder() to the stack. The algorithm continues recursively until reaching p or there is no more states to explore in the considered finite prefix. Additionally, we return true if p is satisfied by a state between two borders, i.e., during an application of ClusteredN extBorder().

The algorithm for EGp (meaning there exists a path where p is always true) works in a similar way, but the state s is returned if p is true on s and if s is final, and ClusteredN extBorder(s) is added to the stack only if p is true on s. Additionally, states where p is not true are dropped when explored in ClusteredN extBorder(). That way, only states where p is true are explored.

We shall also describe how to check nested CTL queries, of the kind EF (p ∧ EF q), meaning that a reachable state satisfies p and from that state a reachable state satisfies q, and EF (p∧EGq), meaning that a reachable state satisfies p and from that state there exist a path where q is always true. Those nested queries are implemented using a marking function (i.e., a Boolean indicator). EF (p ∧ EF q) is implemented as follows. Whenever p is true on a state, the state is marked. Whenever a state is marked, all its successors are marked. Starting from a stack containing the initial state, the first element s of the stack is returned if q is true on s and s is marked. Otherwise, the result of ClusteredN extBorder(s) is added to the stack. The same marking process is performed between two borders, i.e., in ClusteredN extBorder(). We continue recursively until a state validates the property or there is no more state to explore. As for EF (p ∧ EGq), states are marked whenever both p and q are true or the state is a successor of a marked state and q is true. If a marked final state is reached, it validates the property and is returned. Again, the same marking process is performed in ClusteredN extBorder().

To have a better idea of how those algorithms are implemented, we provide Algorithm 1 computing EF (p ∧ EGq).

Experiments

In this section we illustrate the performances of our exploration algorithms applied to three models used in [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF], featuring various state space sizes. Those models represent systems of autonomous vehicles circulating on a portion of highway where each vehicle communicates with the other ones to make decisions about its behaviour.

More specifically, we assume that the road section is composed of three unidirectional lanes the vehicles move on, and we store at any time the coordinates (position) of each vehicle on it. Each vehicle is represented by a rectangle with a given length and width, centered on its position. Its state is thus described by a record containing its position, current longitudinal and lateral speeds, longitudinal acceleration (in a given range from negative to positive values), current direction and knowledge about intentions of other vehicles (for example in the form of timed trajectories).

Since we are focusing on the efficiency and robustness of decision choices and not on the control of vehicles (i.e., the module responsible for producing a trajectory according to the decision choices), we abstract from the physical laws involved in a maneuver such as rotation or inertia. In other words, we assume that turning the steering wheel impacts the speed value that will make the rectangle move on the x-axis, while its longitudinal speed still makes it move on the y-axis.

At a constant frequency of 10 Hz, the speed and position of each vehicle is updated by a transition of an agent environment update.

We assume that the vehicles (1) observe the behavior of their neighbors and that the information obtained from the perception sensors is always accurate and immediate and (2) communicate and receive pieces of information, which are not directly observable, such as the planned lane change of the other vehicles; these communications are timed in order to realistically represent the delays between emissions and receptions of data. The behavior of each vehicle consists in repeating endlessly, at its own constant frequency:

a computation allowing to make a decision on the immediate action to be performed (i.e., execution of the decision algorithm) in the form of an acceleration (speed increase, braking, no change) and a direction (left, right, no change), followed by the communication of its own intention (in the form of the trajectory it wishes to follow) to all vehicles (close enough to be) able to receive this information. Received information coming from the other vehicles is stored in the database of the vehicle and used when running the decision algorithm.

A decision algorithm has been implemented for the experiments [START_REF] Arcile | Conception, modélisation et vérification formelle d'un système temps-réel d'agents coopératifs : application aux véhicules autonomes communicants[END_REF] but should not be considered as one of our contributions: our goal here is not to promote a clever decision making algorithm but to illustrate how MAPTs and their exploration algorithms can be used to efficiently check temporal logic queries in complex multi-agent systems. As such, this section focuses on the comparison of execution times rather than on the actual results, which are detailed and discussed in [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF]. Sources for the models and algorithms used in this section are available in [START_REF]Sources of the MAPTs models and exploration algorithms[END_REF].

In the following, we first discuss the advantages and drawbacks of using various types of layer-based explorations. Then, we provide some heuristics, and experiment them in order to (hopefully) observe the gain that can be achieved with them. Finally, we compare this method with the framework VerifCar [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF], which uses Uppaal, and we provide a verification method for the analysis of such systems that is more efficient and less constrained than the one proposed in [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF]. Note that Uppaal uses real clocks but in our context (resets only occur at periodic integer times and functions do not rely on clocks) there is no obstacle in replacing them by integer ones.

Efficiency of the layer-based exploration.

Here, we compare, for several exploration algorithms, the full exploration time and the reachability time of the first occurrence of a final state. They are explored in breadth-first, depth-first without layers and depth-first with layers (with and without the use of strong/weak variables). The sizes of the state spaces for Models 1, 2 and 3 are respectively of 7751, 52732 and 285944 states. As shown in Table 1, one can see that the breadth-first algorithm has the best full exploration time in any case, but the time before reaching any final state is close to the full exploration one, which makes it the worst technique in this case. On the other hand, the standard depth-first algorithm is the fastest for reaching a final state, but it does not fully explore the state space even after 50 hours of computation.

Results for Model 1 show that as long as the layer based approach is used, the full exploration time is very close to that of the breadth-first one. This indicates that there is almost no diamonds covering several layers, meaning that different states belonging to the border of a layer almost never share a common successor. For this reason the use of weak variables has no effect. Although this case is rather simple, it clearly highlights the advantage of layer-based exploration: with almost no increase in full exploration time, it is able to reach a final state much faster.

Model 2 and 3 have much more complex state spaces and, in both cases, the layer-based algorithm that does not rely on weak variables to aggregate states is not able to explore the full state space even after 50 hours of computation. On the contrary, using even a small number but well chosen weak variables (6 out of 39), it is possible to fully explore the state space. In both cases, exploration is about five times longer than the exploration time of breadth-first algorithm. When using a large number of weak variables (30 out of 39), the exploration is much shorter (about 1.5 times the time of breadth-first algorithm). One can note however that the larger V w , the longer it takes to reach a final state. Indeed, as states are aggregated layer by layer, a too large V w would result in an exploration similar to a breadth-first one, where all states are kept together and final states are only reached at the end of the computation. With the weak variables chosen, the time to reach a final state remains however reasonable.

In the next experiments, the depth-first algorithms always use layers and a fixed non-empty V w .

Heuristics

Exploration algorithms based on layers allow the use of heuristics. These heuristics guide the exploration, choosing among all the unexplored states the one that will most likely lead to a state that satisfies the checked property. The heuristics we use associate a weight to each state, such that when a new state is discovered, it is placed in a list ordered by weight of states to explore. The weight is a prediction of the distance between the current state and a state satisfying the property.

Therefore, a reachability property may be associated with a heuristics that takes a state as an input and returns a weight as an output. Below is a list of heuristics that we used for experiment purposes together with the property they are associated with: plus the estimated time to reach the end of the road portion, assuming the current speed is maintained. It is used with property EF travel time vh sup n, where travel time vh ≥ n is true in a state if vh reaches the end of the road portion in n time units or more. The idea is to check in priority states where vh is predicted to reach the end of the road with the longest time. 3. time to overtake vh 1 vh 2 : is the time before both vehicles arrive at the same longitudinal position if they keep their current speed. It is used with property EF ttc vh 1 vh 2 ≤ n, where ttc vh 1 vh 2 is the value of the time to collision indicator between vh 1 and vh 2 (i.e., the delay before there is a collision between the two vehicles if they keep their current speed), and n is a time to collision value. The idea is to check in priority states where one of the vehicles is getting closer to the other one with the higher speed.

These heuristics have been used on Model 3, with results given in Table 2. The scenario in Model 3 considers three vehicles positioned as depicted in Fig. 2 on a two lane road portion that is 500 m long, with one additional junction lane. Initially, vehicle A is on the right lane at position 0 m with a speed of 30 m/s, vehicle B is on the left lane at position 30 m with a speed of 15 m/s and vehicle C is on the junction lane at position 40 m with a speed of 20 m/s. They all aim at being on the right lane at the end of the road portion.

The first two queries (EF arrival B bef ore A and EF travel time A ≥ 15.9) can only be true in a final state (the deepest layer). As such, the reachability time with the breadth-first algorithm is close to the full exploration time with the same algorithm. In general, the breadth-first reachablity time depends on the depth of the first state that satisfies the property. One can observe that for the fourth query (EF ttc A B ≤ 0), the state is actually reached at a lower depth, which is reflected by the reachability time.

As the depth-first algorithm without heuristics randomly chooses which paths to explore first, the reachability time varies. The number of states in the whole state space that satisfies the property thus impacts the mean reachability time with this algorithm, i.e., when there is more possibility to verify the property, the average time needed is shorter. As we do not want to rely on luck, this is not satisfying.

On the other hand, depth-first algorithm with heuristics explores states in a given order (depending on their weights) and therefore the reachablity time is always the same. The heuristics we used could of course be modified and improved, but they are enough to show a significant decrease of the reachability time. Even for the fourth query, where the breadth-first is faster than the depthfirst algorithm, the heuristics allows to quickly identify the state that satisfies the property.

Comparison with VerifCar

We will now compare the reachability time obtained with Uppaal with the ones obtained with the depth-first exploration algorithms with heuristics, on Model 3. We observed that Uppaal first constructs the state space in about 106 s, then is able to answer almost instantly if a searched state exists. It can therefore answer several queries after constructing the state space, unlike our heuristicsbased dynamic exploration algorithms, which have to explore the state space from scratch for each query. Yet, most of the states we aimed for can be reached easily, and the computation took only about 4 seconds. Queries depicted in Table 2 are those where states were harder to reach. Compared to the ones we obtained in [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF], these results indicate that, when a reachability property is satisfied, our algorithms have the same kind of execution time than the ones observed with Uppaal. On the other hand, if the reachability property is not true, they are slower than Uppaal, which depending on the kind of query takes between 34 and 370 seconds, which equals the full exploration time with this tool for Model 3. As mentioned previously, the full state space exploration time with depth-first algorithms on this Model, is in our case, of 667 seconds. This is not a surprise since Uppaal is a mature tool using many efficient optimisations. However, Uppaal is restricted in terms of query language, at least in two ways interesting for us. First, it is not possible to directly check bounds of a given numerical indicator, and such bounds should be obtained by dichotomy, requiring several runs for each indicator, such as proposed in the methodology of [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF]. Second, it is limited to a subset of CTL (accepting mainly non nested queries). Our algorithms do not have such restrictions. Indeed it is possible to do a full exploration of the state space while keeping, for each state, the lower and higher values reached on the paths leading to the state, for a given set of indicators. That way, all the information needed to analyse the behaviour of the system, can be obtained after only one full exploration. This is performed as a standard breadth-first exploration (storing states in a file) with the difference that each state is associated with a set of pairs (min, max), being the (temporary) bounds of the considered indicators. Each time a state is explored, the value for each indicator is computed, and it overwrites min if it is smaller, and max if it is greater. That way, each state s contains, for each indicator, the smallest and highest values that exist on the paths from the initial state to s. As several paths can lead to s, we will consider that s reached from path P 1 and s reached from path P 2 are equivalent only if the set of their indicators are equal. Therefore, some diamonds might be detected (i.e., two identical states coming from different paths) but not merged together in order to keep information about their respective paths. That way it is possible to have several versions of the same state, but with different indicator values. If one is interested in the reachability of states (for instance, if an indicator is equal to some value), this can easily be done in the same way, by adding Boolean variables to the set of indicators. At the end of the exploration, we get this way the set of all final states, together with all the information that has been carried on their respective paths. It therefore contains all the information needed to analyse finely the system. For the case of Model 3, getting the arrival order together with the bounds for travel time and worst time-to-collision takes 708 seconds. In comparison, the time needed by Uppaal to obtain the same information with the dichotomy procedure is 3553 seconds. Also, the DAG shape of the state space allows us to implement nested CTL queries. For the experiments, we used a query of the kind EF (p ∧ EGq), which is the negation of the "leads to" operator p --> ¬q (the only nested operator available in Uppaal, in addition to deadlock tests) and two of the kind EF (p ∧ EF q), which cannot be expressed in Uppaal.

In [START_REF] Arcile | Verifcar: a framework for modeling and model checking communicating autonomous vehicles[END_REF], arrival C bef ore A --> arrival B bef ore A was used and reached a state invaliding the property in 110 seconds. Its negation can be expressed here as EF (arrival C bef ore A ∧ EG¬arrival B bef ore A) and our algorithm finds the state validating the property in about 10 seconds. The properties EF (ttc A B ≤ 1 ∧ EF arrival A bef ore C) and EF (ttc A B ≤ 1 ∧ EF arrival A bef ore B), that cannot be checked in Uppaal, can be expressed here. The first one expresses the possibility for vehicle A to arrive ahead of vehicle C after a dangerous situation has occurred, involving a time to collision of less than 1 second. The second is similar for vehicle A and B in the same conditions. The first query is false and needs to explore the whole state space to give an answer (in 680 seconds), while the second one is true and finds a state satisfying the property in about 10 seconds.

Finally, it is worth mentioning that discretisation is needed for Uppaal, and therefore approximations may be mandatory in some cases, leading to a loss in precision and realism. In addition to a better expressiveness, the model checking process presented in this paper also ensures that no approximation is needed, hence a higher level of realism is achieved.

Conclusion

We introduced G-MAPTs, multi-agent timed models where each agent is associated with a regular timed schema upon which all possibles actions of the agent rely. The formalism allows to easily model systems featuring a high level of concurrency between actions, where actions are not temporally deterministic, such as the CAVs. We have then formalised MAPTs (Multi-Agent with timed Periodic Tasks), by soundly constraining G-MAPT ones. We also presented how to extract a layered structure out of a MAPT, that allows to detect diamonds while exploring the system depth-first. A translation from G-MAPT to highlevel Petri nets allowed us to implement a dedicated checking environment for this formalism with the (free) academic tool Zinc. Algorithms implemented in such environments explore state spaces dynamically and can be used together with heuristics that allow to reduce the computation time needed to reach some states in the model. Finally, experiments highlighted the efficiency of our abstractions, and a comparison of model checking CAVs systems with the framework VerifCar has been performed. Although our checking environment does not return traces of executions and is not better for full exploration times than the state of the art tool Uppaal used in VerifCar, it has a better expressiveness both on the model, since we can compute with non-integer numbers, and on the queries since nested CTL ones can be checked. The heuristics performed well for reachability problems and we also provided an exploration algorithm that allows to gather all information needed to analyse the system in one run, which greatly decreased the time needed to gather the same amount of information when using VerifCar. Although we developed this method with the case study of autonomous vehicles in mind, this formalism and all the abstractions and algorithms presented in this paper can be easily applied to any multi-agent real time systems where agents adopt a cyclic behaviour, such as mobile robots completing cyclically tasks according to their own objectives, flying drone squadrons, etc.

Fig. 2 .

 2 Fig. 2. Initial positions and possible trajectories of autonomous vehicles for the scenario in Model 3.

  Algorithm 1 EF (p ∧ EGq) exploring.add(init) {add initial state to the stack of states to explore} while exploring do successors ← N extBorder(exploring.pop()) {removes the state at the end of the stack and store all its successors} for all s ∈ successors do if (check(p, s) or parent marked(s)) and check(q, s) then mark(s) {s is marked if either p is true on s or q is true on s and its predecessor is marked} end if if is marked(s) and check(f inal, s) then return true {returns true if s is a marked final state} else if not check(f inal, s) then exploring.add(s) {otherwise and if s is not a final state, add it to the stack}

	end if
	end for
	end while
	return false

Table 1 .

 1 Comparison of full exploration time and time to reach the first occurrence of a final state state for exploration algorithms in breadth-first, depth-first with and without layers and with or without the use of weak variables. ∞ means that the exploration was stopped after 50 hours of computation without a result.

	Exploration algorithm	Full exploration time (s)	First occurrence of a final state (s)
		Model 1 Model 2 Model 3	Model 1 Model 2	Model 3
	Breadth first	10.8	52.1	420	10.7	52	419.9
	Depth-first without layers	∞	∞	∞	3.3	4.6	3.9
	Depth-first layered(Vw = ∅)	11	∞	∞	4.5	6.6	4.1
	Depth-first layered (small Vw)	11	250	2015	4.5	7.4	6
	Depth-first layered (large Vw)	11	71	667	4.5	14.4	7.2

  1. distance vh 1 vh 2 : returns the longitudinal position of vehicle vh 1 minus that of vehicle vh 2 . It is used with property EF arrival vh 1 bef ore vh 2 , where arrival vh 1 before vh 2 is true in a state if vehicle vh 1 reaches the end of the road portion before vehicle vh 2 does. The idea behind is to check in priority states where vh 1 is the most ahead of vh 2 . 2. estimated travel time vh: returns the time traveled since the initial state 4

  Exploration algorithmEF arrival B bef ore A EF travel time A ≥ 15.9 EF ttc A C ≤ 1.14 EF ttc A B ≤ 0

	Breadth-first	416	427	292	95
	Depth-first without heuristics	234-357	167-340	247-547	277-483
	Depth-first with heuristics	131	149	103	13

Table 2 .

 2 Comparison of reachability time for exploration algorithms in breadth-first and depth-first with and without heuristics. As depth-first without heuristics is non deterministic, the two values correspond to the fastest and the slowest runs obtained for each query (five runs where performed each time).

We shall allow infinite value sets, but there will never be infinitely many tokens in the system

Elapsed time since initial state can be estimated by counting how many times an agent has returned to its initial locality.


1

The multilayers control of ARGONAUTE 1 contents Jean Molinier Institut de biologie moléculaire des plantes, 12 rue du Général Zimmer, 67000 Strasbourg, France.

Correspondance : jean.molinier@ibmp-cnrs.unistra.fr ARGONAUTE proteins (AGO) are key effectors of the RNA silencing pathways involved in the regulation of gene expression and in antiviral defense (Vaucheret, 2008). Among the 10 AGO proteins present in Arabidopsis, AGO1 is essential for plant development and defense response, participating in both miRNA-and siRNA-mediated gene silencing (Vaucheret, 2008).

Given that AGO1 depletion is lethal, only hypomorphic mutant plants are viable and display a large variety of developmental phenotypes (Vaucheret, 2008). Importantly, the fine tuning of AGO1 content is an important process orchestrated by several different pathways [START_REF] Cho | Post-Translational Regulation of miRNA Pathway Components, AGO1 and HYL1, in Plants[END_REF]. It was recently described that the mode of action of AGO1 is not only restricted to the post-transcriptional gene silencing pathway taking place in the cytoplasm. Indeed, several nuclear AGO1 functions have been identified [START_REF] Bajczyk | Novel Nuclear Functions of Arabidopsis ARGONAUTE1: Beyond RNA Interference[END_REF]. Thus, the characterization of the different AGO1 pools implies that specific subcellular pathways might trigger AGO1 turnover and that complex regulatory processes might interplay to specifically fine tune AGO1 content.

Using a genetic screen designed to uncover factors involved in the miRNA pathway, Ré et al. (2019) showed that an effector of the Polycomb Repressor Complex 2, the histone methyltransferase CURLY LEAF (CLF), regulates an AGO1 negative regulator, the F-BOX WITH WD-40 2 protein (FBW2; [START_REF] Earley | An endogenous F-box protein regulates ARGONAUTE1 in Arabidopsis thaliana[END_REF]. Ré et al. (2019) demonstrated that AGO1 is preferentially degraded when bound to RNA targets (Figure 1). This study depicts a good example of the complexity and of the multilayer (direct/indirect) control of AGO1 homeostasis.

Regulation of AGO1 content

Both post-transcriptional and post-translational processes fine tune AGO1 contents. A selfregulation pathway involving the miR168 negatively regulates AGO1 transcripts by mRNA cleavage (Figure 1) modulating the proper assembly of the RNA-Induced Silencing Complex.

Strikingly, AGO10 also acts as a negative regulator of AGO1 content by loading preferentially a 22-nt miR168 isoform and by translation inhibition (Figure 1; [START_REF] Mallory | Redundant and Specific Roles of the ARGONAUTE Proteins AGO1 and ZLL in Development and Small RNA-Directed Gene Silencing[END_REF][START_REF] Iki | Structural Flexibility Enables Alternative Maturation, ARGONAUTE Sorting and Activities of miR168, a Global Gene Silencing Regulator in Plants[END_REF]. This highlights that AGO1 and AGO10 interconnect to efficiently control AGO1 homeostasis likely in a tissue-specific manner.

The post-translational regulation of AGO1 has also been reported to play an important role during plant-virus interactions. Following virus infection both miR168 and AGO1 mRNA accumulate whereas AGO1 protein content decreases suggesting that post-translational pathway may act as a negative regulator (Figure 1). Indeed, several viral suppressor proteins hijack the plant silencing machinery by either direct interaction with AGO1, inhibiting its cleavage activity or by triggering AGO1 destabilization (Figure 1). The AGO1 proteolytic degradation, in a viral context, was shown to be predominantly mediated by autophagy (Figure 1). In the presence of the viral suppressor P0 of the Turnip yellows virus, considered to be an F-box like protein, AGO1 co-localizes with the autophagosomal membrane protein ATG8 [START_REF] Derrien | Degradation of the antiviral component ARGONAUTE1 by the autophagy pathway[END_REF]. Moreover, in the presence of P0, AGO1 protein content increased in response to autophagy inhibitor whilst it remained unchanged in the presence of proteasome inhibitor. These results support the idea that autophagy-dependent AGO1 destabilization is likely the main pathway involved in the regulation of AGO1 content during viral infection. Nevertheless, the P25 silencing suppressor of the Potato virus X, targets AGO1 destabilization through the Ubiquitin-proteasome system (UPS), suggesting that AGO1 content could be regulated by more than one degradation pathway (Figure 1).

In a non-viral context AGO1 was described to be negatively regulated by FBW2 (Figure 1), which is an F-box protein known to mediate the ubiquitination of interacting targets [START_REF] Earley | An endogenous F-box protein regulates ARGONAUTE1 in Arabidopsis thaliana[END_REF]. FBW2 expression is under the control of the histone methyltransferase CLF (Figure 1) involved in the deposition of the repressive trimethylation mark on the lysine (K) of histone H3 (H3K27me3). Interestingly, CLF-mediated regulation of FBW2, and thus also of AGO1, appeared to be tissue-specific (Ré et al., 2019). Both, high amount of ubiquinated AGO1 and strong reduction of AGO1 levels have been detected in clf mutant plants compared to WT control Arabidopsis plants (Ré et al., 2019). This demonstrates that the facultative heterochromatin mark, H3K27me3, represses FBW2 expression, linking indirectly the epigenomic landscape dynamics to AGO1 ubiquitination/turnover. SUMOylation, another process biochemically related to ubiquitination, was described to negatively regulate human Ago2 stability, the ortholog of the plant AGO1, showing that a panoply of ubiquitin-related mechanisms target AGO proteins to degradation. Moreover, hydroxylation of the human Ago2 proline 700 enhances Ago stability. Impairment of Ago2 hydroxylation in the presence of the proteasome inhibitor MG132, restores Ago2 contents, highlighting that particular posttranslational modifications (PTM) likely antagonize the proteasome-mediated degradation pathway. Thus, an important issue would be to decipher whether hydroxylation, SUMOylation or even other types of PTM (i.e phosphorylation) could affect the stability of the plant AGO proteins in response to particular growth conditions or in a tissue specific manner and how these PTM could interplay with the proteolytic mechanisms (Figure 1).

AGO1 homeostasis in response to abiotic stresses

AGO1 plays an important role in plant response to various abiotic stresses such as salt and cold [START_REF] Dolata | Salt Stress Reveals a New Role for ARGONAUTE1 in miRNA Biogenesis at the Transcriptional and Posttranscriptional Levels[END_REF][START_REF] Liu | Arabidopsis ARGONAUTE 1 Binds Chromatin to Promote Gene Transcription in Response to Hormones and Stresses[END_REF]. miR168 is induced upon Abscisic acid treatment, suggesting that the cytoplasmic post-transcriptional AGO1 regulation is also mediated by environmental stresses.

Interestingly, it was recently described that the mode of action of AGO1 is not only limited to the cytoplasm [START_REF] Bajczyk | Novel Nuclear Functions of Arabidopsis ARGONAUTE1: Beyond RNA Interference[END_REF]. Indeed, nuclear AGO1 functions have been characterized (Figure 1) and involve miRNA loading [START_REF] Bologna | Nucleo-cytosolic Shuttling of ARGONAUTE1 Prompts a Revised Model of the Plant MicroRNA Pathway[END_REF], chromatin control of miRNA or protein coding genes expressions (Dolota et al., 2016;[START_REF] Liu | Arabidopsis ARGONAUTE 1 Binds Chromatin to Promote Gene Transcription in Response to Hormones and Stresses[END_REF], DNA repair of photolesions (Schalk et al., 2017). Collectively, these studies revealed that several different subcellular pathways (cytoplasmic and nuclear) likely exist to control AGO1 homeostasis.

A novel function of AGO1 in the repair of UV-induced DNA lesions has been established (Schalk et al., 2017). AGO1 forms a nuclear complex with the DNA repair factor DNA Damage Binding protein 2 (DDB2), to initiate, within chromatin, an siRNA-mediated repair of UVinduced DNA lesions (Schalk et al., 2017). Interestingly, upon recognition of photodamage the DDB2-AGO1-siRNAs complex is released from the damaged sites (< 30 min) in an Ataxia telangiectasia and Rad3-related (ATR)-dependent manner (Schalk et al., 2017). Given that DDB2 degradation upon UV stress depends not only on the CULLIN4-DNA Damage Binding protein 1A (CUL4-DDB1A) ubiquitin E3 ligase complex, but also on ATR it could be assumed that this particular AGO1 pool may indirectly be targeted to the UPS through its association with DDB2. Therefore, an important issue would also be to consider that AGO1 homeostasis may rely on the post-translational regulation of its interactors.

Interestingly, clf plants display UV hypersensitivity and reduction of both cytoplasmic and nuclear AGO1 pools (Ré et al., 2019). While it is known that some ubiquitin E3 ligase complexes predominantly act in the nucleus (i.e CUL4-DDB1), it remains unknown whether an FBW2 nuclear pool exists or whether nuclear autophagy may also contribute to AGO1 turnover in plants. Therefore, the proper regulation of AGO1 contents upon UV exposure, may rely on coordinated nucleo-cytoplasmic proteolytic mechanisms in which CLF and therefore FBW2 may contribute (Figure 1). It should hence be of great interest to decipher the subcellular dynamics of the discrete AGO1 pools and to identify their regulatory complexes in response to environmental stresses and/or in particular cellular niches. Such line of investigation represents an important challenge in the comprehensive study of AGO1 homeostasis.

In the nucleus, AGO1 is involved in miRNA loading, transcription and DNA repair. It could be assumed that AGO1 homeostasis is regulated through ubiquitin-mediated proteolytic pathways that remain to be identified.

The histone methyltransferase CURLY LEAF (CLF) acts as a negative regulator of FBW2 expression. When FBW2 expression is released (i.e in clf mutant plants) AGO1 is ubiquitinated and destabilized when bound to RNA targets.

Acknowledgements

J.M is supported by the GDR EPIPLANT.

Figure legend

AGO1 is ubiquitinated (Ub) and predominantly targeted to autophagy and/or to a lower extend to the Ubiquitin-proteasome system (UPS).

During plant development, in a tissue specific manner and in response to environmental stresses AGO1 content is modulated through (i) the self-regulation pathway involving the miR168 that negatively regulates AGO1 transcripts (ii) AGO10-mir168a-mediated translational inhibition (iii) putative post-translational modifications (pink circle) (iv) the F-BOX WITH WD-40 2 protein (FBW2) that destabilizes AGO1 in a ubiquitin-dependent manner.