H Ounis

B Sareni

X Roboam

A De Andrade

MULTI-LEVEL INTEGRATED OPTIMAL DESIGN FOR POWER SYSTEMS OF MORE ELECTRIC AIRCRAFT

Keywords: Optimal design, multi-level optimization, ATC (Analytical Taget Cascading), power integration

± This paper proposes a particular multi-level optimal design method for complex actuation system for more electric aircraft. This method is applied to a relatively complex power conversion system including a High Speed Permanent Magnet Synchronous Machine (HSPMSM) supplied by a PWM Voltage Source Inverter (VSI) associated with a DC-link filter. Its interest is shown through a comparison with classical design approaches employed in previous works.

INTRODUCTION

Among the main trends and future challenges of electrical networks embedded in MEA (more electric aircraft), mass and loss reduction is of prime LPSRUWDQFH LQ WHUPV RI FRPSHWLWLYHQHVV ³SRZHU LQWHJUDWLRQ´ LV WKHQ D NH\ IDFWRU RI WKLV FKDOOHQJH Results presented in [START_REF] De Andrade | QWHJUDWHG RSWLPDl design for power systems of more electrical aircraft´[END_REF] show that optimizing the components of any system does not deals to an optimization of the system despite its several advantages (short computational time...). Oppositely, a global optimization of multidisciplinary and highly complex systems cannot be faced for many reasons such as: convergence problems, expensive computational time and especially for problems related to project management. In this context, a multi-level formulation for a highly complex optimization problem with the supervision of a system level to control the optimization process seems very interesting to solve the convergence problems of the global approach with a good approximation of the system solution.

This paper addresses the issue of optimal design by PHDQV RI ³VHTXHQWLDO´ ³JOREDO´ DQG ³multi-leveló ptimization approaches for highly complex multidisciplinary systems:

x In the first part, we detail the analytical models of the different components of an electrical drive system for aircraft application (input filter, inverter and machine); x In the second part, a ³sequential´ approach is applied to the aircraft system and compared to the global optimization approach;

x The last part deals with a multi-level optimization method applied to the aircraft system.

SYSTEM MODEL

This example refers to the integrated design of an electrical power system including a HSPMSM supplied by a VSI associated with an input filter (Fig. 1). The actuation mission is ensured by the HSPMSM motor which must operate at specific points in the torque-speed plane depending on the flight mission. On the other hand, the system has to comply with HVDC network standards [START_REF]Airbus Directives (ABD) and Procedures, ABD0100-Equipment-Design, General Requirements For Suppliers[END_REF] during its operation. Considering the main constraints at the device input and output, two design objectives are focused: the whole weight and power losses during the flight mission have to be minimized. In this context, an integrated design process based on the actuation system modeling and optimization has been investigated. Our approach particularly takes into account the mission profile in the integrated optimal design process.

FLIGHT MISSION PROFILE

HSPMSM operating points have to be fulfilled in the Torque-Speed plane depend on flight phases (climb, cruise and descent) and on climatic conditions (i.e., international standard atmosphere, warm or cold weather conditions). These points are illustrated in (Fig. 2) with their associated statistic occurrence. It should be noted that the maximum HSPMSM power which approximately corresponds to the maximum speed and maximum torque values is of small occurrence. Setting the HSPMSM base point close to this point would certainly lead to a system oversizing. This underlines the interest of exploiting ILHOG ZHDNHQLQJ DQG ³RYHU-WRUTXH´ FDSDELOLWLHV LQ WKH integrated design process.

HSPMSM MODEL

A multi-physical model of the HSPMSM has been derived from a previous PMSM model devoted to ground applications [START_REF] Sareni | ³0RGHO VLPSOLILFDWLRQ DQG RSWLPL[END_REF]. This model has been extended in order to take all features related to the PMSM behavior at high speed operation. It includes:

x All characteristics related to the HSPMSM architecture: material types in each region (iron, magnet, sleeve, copper) and associated geometry parameters (i.e. radius length ratio, slot depth, slot width, number of pole pairs, number of slots per pole per phase, equivalent gap, magnet filling coefficient, etc.). Through this geometric model we estimate the HSPMSM mass ;

x An electric model based on the HSPMSM electrical variables (resistance, leakage and main inductances, magnetic flux, voltage) calculated from the HSPMSM geometrical features;

x A magnetic model specifying HSPMSM electromagnetic behaviour in each region (yoke, teethes, air gap, magnet) and magnet demagnetization characteristics.

x The total HSPMSM power losses includes: Joule, iron, aerodynamic and magnet losses;

x A thermal model giving the temperature in each HSPMSM part (copper, insulator, yoke, sleeve, magnet) from the corresponding power losses and from the external temperature imposed by the water jacket. This model also provides:

-the mass estimation of the HSPMSM cooling system; -a HSPMSM control strategy allowing maximum torque per Ampere with field weakening mode.

VSI MODEL

The VSI (Voltage Source Inverter) is a classical two-level structure (Fig. 1) associated with a Space

Vector Pulse Width Modulation (SVPWM) strategy.

The multi-physics VSI model includes:

x A time-frequency approach which allows the determination of the electrical variables (currents and voltages) in time and frequency domains at the VSI input and output. In particular, this approach quickly computes the time evolution of electric variables over a period of the modulation signal at steady state operation. From the SVPWM strategy and the knowledge of VSI switching states, HSPMSM stator voltages are constructed. Then, HSPMSM line currents are easily computed in frequency domain from the HSPMSM impedance using the fast Fourier transform. The corresponding time evolution of HSPMSM currents can also be obtained over the modulation signal period with the inverse fast Fourier transform. Finally, the DC current at the VSI input is deduced from HSPMSM currents and VSI switching states;

x A model of inverter losses including switching losses and conduction losses in diodes and IGBTs; x A geometrical model depending on the IGBT current rating, the dual pack component features and the cooling plate characteristics. This model gives an estimation of VSI and cooling plate masses;

x A thermal model providing the temperature in each component (diode, IGBT, casing) from the associated power losses and from the reference temperature imposed by the cooling plate.

INPUTFILTER MODEL

The input filter includes two cells as showed in Fig. 1. Its model contains:

x The geometrical and physical features of all filter components;

x A two-port network representation which allows the determination of electric variables at the filter input. The HVDC input voltage is given by the HVDC standard and the output filter DC current results from the VSI model.

Considering those given variables, the other complementary variables (i.e., the input filter HVDC current and the output filter voltage) are found through the two-port network impedance matrix.

x The computation of power losses in the filter elements (inductances, capacitors and resistors).

GLOBAL AND SEQUENTIAL SYSTEM OPTIMIZATION

The actuation system optimization has been carried out using three different approaches. The first two approaches have previously been applied in [START_REF] De Andrade | &RXGHUF 5 5XHOODQG ³0XOWL-level optimization of electrical environemental conditioning V\VWHPV IRU PRUH HOHFWULFDO DLUFUDIWV´ th Workshop on Optimization and Inverse 3UREOHPV LQ[END_REF].

x A local and sequential sizing of each part (i.e. the HSPMSM optimization followed by the VSI and input filter optimization);

x A global integrated design approach investigating the simultaneous sizing of all coupled components.

A third optimization approach based on an original multi-level formulation of the problem is also presented in section 4.

SEQUENTIAL OPTIMIZATION

x HSPMSM optimization

The optimal sizing of the HSPMSM has been formulated into a local optimization problem with:

-11 design variables related to the HSPMSM geometric features, electromagnetic variables and mechanical characteristics;

-11 constraints associated with geometrical variables, technological limits and temperature limits in the different motor parts (rotor: magnet, sleeve; stator: insulator, yoke); -2 objectives to be minimized: the HSPMSM mass and the total losses estimated over the flight mission.

Total HSPMSM losses are computed by weighting all losses on each mission point according to its occurrence during the flight.

x VSI and Input Filter optimization

The optimal sizing of the ³input filter + VSI´ set has been formulated into an optimization problem with:

-10 design variables related to the VSI (switching frequency, IGBT current rating) and the R, L, C components of the input filter;

-11 constraints associated with the input filter features, with VSI semiconductors and quality standards on the electrical network (HVDC network quality of low and high frequency currents, maximum ripple of input VSI voltage, maximum harmonic distortion of the HSPMSM);

-2 objectives to be minimized: the mass of the ³input-filter + VSI´ set and the total losses in this subsystem during the flight mission. The whole losses for this supply part include losses in the filter (R, L, and C losses) and VSI (switching and conduction losses).

x

Results

We have previously performed the sequential optimization by determining HSPMSM Paretooptimal configurations before optimizing the supply part. Those solutions are obtained from 10 independent runs of the NSGA-II evolutionary algorithm with a population size of 100 and number of generation of 500 and using a self-adaptive recombination [START_REF] Sareni | ³5HFRPELQDWLRQ DQG 6HOI-adaptation in Multiobjective *HQHWLF[END_REF]. Fig. 4-a compares the optimal tradeoffs found in the objective space (i.e. HSPMSM mass and losses) with a reference non-optimized solution. All variables are given in per unit (pu) for confidentiality reason. Even if some important gains on both HSPMSM objectives can be observed, we point out they could not be considered as significant at the system level since the supply part is not designed at this step. Then, the multi-objective optimization of the ³input filter +VSI´ set is also performed with regards to three particular HSPMSM configurations extracted from the previous Paretooptimal front. With respect to the reference HSPMSM solution, those configurations are chosen at the same level of mass (i.

GLOBAL OPTIMIZATION

The global multi-objective optimization of all components is investigated in a single optimization loop. In comparison with both component optimization problems described in the previous VXEVHFWLRQV WKH FRPSOH[LW\ RI WKLV ³global problemí s significantly increased since all design variables and constraints are aggregated. Therefore, this new problem includes 21 design variables, 22 constraints and same 2 objectives. It is then solved using the NSGA-II with a population size of 100 and a number of generations of 1000. Pareto-optimal solutions obtained from this system optimization are illustrated in Fig. 4-c and compared with the three particular solutions resulting from the sequential optimization approach (combination by mass and losses additions of HSPMSM and VSI-input filter solutions of Fig. 4-a and Fig. 4-b). As expected, the global optimization of all components clearly outperforms the sequential optimization approach. However, it should be mentioned that convergence on the global optimization problem can be obtained in a reasonable time only if the optimal components found by the sequential approach are inserted in the NSGA-II initial population.

MULTI-LEVEL OPTIMIZATION

The optimal design of highly complex system that involves many disciplines and many fields of expertise cannot be achieved by a single company. Often, subcontractors are called for the design of certain components constituting the system, each one in its specific field. In this context, a global optimization appears very difficult to apply. However, the sequential approach provides some flexibility by performing a separate optimization of each component, but the results obtained in section 3.2 show a large difference between global and sequential approaches. In this part, a ³multi-level optimization´ method is proposed in order to find compromise solutions that draw near the global solutions and which ensure good convergence of the optimization problem while preserving benefits of the sequential approach in terms of structure.

Several approaches of multi-level optimization are proposed in [START_REF]& %HUEHFHD ³0XOWL-level approaches for optimal system design in railway applicDWLRQV´ Université desSciences et Technologie de Lille[END_REF]. Multi-level formulation adopted in this work is based on ATC formulation (Analytical Target Cascading) where the overall system partitioning can be done in several ways such as object or physics (discipline) based partitioning [START_REF] Tosserams | ³A specification languagefor problem partitioning in decompositionǦbased GHVLJQ RSWLPL[END_REF]. After partitioning the original problem, decision variables are categorized in linking variables common to two or more sub-problems and local variables specific to one of them.

The studied optimization problem is divided into two levels: low level (component level) includes +63060 SUREOHP DQG ³LQSXW ILOWHU 96,´ SUREOHP and an upper level (system level) which contains circuit parameters (p, R s , L sync , Ѱ) and switching The Target Cascading approach as presented in the literature [START_REF]LP ³7DUJHW FDVFDGLQJ LQ RSWLPDO V\VWHP GHVLJQ´[END_REF], assumes the knowledge of a system model to evaluate system objectives, thus a local optimization at this level without resorting to low levels is possible (Fig. 5). In our example, there is no model that allows the estimation of mass and total losses at the system level based on adopted system parameters (p, R s , L sync , Ѱ, f dec ). Therefore, a modification is here proposed with respect to the basic formulation: interactions between upper and low levels are clearly seen in Fig. 6.

FORMULATION OF THE MULTI-LEVEL OPTIMIZATION PROBLEM

The optimization problem is divided into two levels:

-Upper (system) level: circuit parameters of the HSPMSM model are themselves the linking variables between components; this appears a good reason to consider them as design parameters of the system level. The switching frequency is added to calculate electrical variables (current and voltage) between components and control sequences of the inverter; it allows a considerable gain in computational time of the ³LQSXW filter +VSIṕ roblem. At this level, mass and total losses of the whole system are optimized.

-Lower (component) level: the most important in this level is how to process targets cascaded from the Total system mass (pu)

Global optimization solutions

Sequential optimization solutions

system level. There are two distinguished cases:

x If system targets are input variables in the original problem of the component (section 3.1), they are considered as data (i.e. known variables) in the multi-level formulation. The pole pairs (p) in the HSPMSM problem is an example of this case;

x On the contrary, for system targets which are output of the component problem (e.g. R s , L sync and Ѱ in the HSPMSM problem), the differences between system targets and local calculated values are minimized with additional equality constraints.

In this level, two component problems are optimized:

x 7KH ³+63060 Sroblem´ is formulated in the same manner as in the sequential approach, with few differences:10decisionvariablesinstead of 11(the number of pole pairs p is deduced from the upper level), 15 constraints instead of 12 (three additional coordination constraints of targets: R s , L sync and Ѱ); x 7KH ³input filter + VSI problem´ UHTXLUHV 5 decision variables instead of 6 (switching frequency is deduced from the upper level) and 9 constraints instead of 11 (the maximum speed constraint and THDI HSPMSM constraints are verified at the upper level). Several variables are pre-calculated by the system level (input current and input voltage of the HSPMSM, control inverter sequences and its input current).

The optimization process involves the following steps:

x Generate a system design parameter vector (p, R s , L sync , Ѱ, f dec );

x Calculate the input currents and voltages of the HSPMSM, control inverter sequences and inverter input current;

x Send targets (p, R s , L sync , Ѱ, f dec ) to HSPMSM problem, switching frequency and precalculated variables to the ³LQSXW Iilter + VSIṕ roblem; x Run a local optimization of each component;

x Send local objectives (mass and total losses); and constraints to the XSSHU ³system´ level;

x Calculate the global objectives at system level.

This loop is redone several times depending on the setting of the optimization algorithm.

MULTI-LEVEL MULTI-OBJECTIVE OPTIMIZATION:

Multi-objective optimization applied to the ³FRPSRQHQW OHYHO´ SUREOHPV DULVHV DGGLWLRQDO GLIILFXOWLHV WR WKH ³V\VWHP OHYHO´ RSWLPL]DWLRQ algorithm. In the ordinary case, for a single individual there is only one solution returned by the -In the HSPMSM problem, equality constraints added to ensure the coherence with the system level targets influence the solution distribution on the Pareto front which becomes a packed front corresponding to a certain class of circuit (Fig. 7). This characteristic allows considering only one particular solution per front. To select this particular solution, different criteria can be used, such as: the minimal error relative to system targets or the minimal distance from ideal objectives; -In the ³LQSXW Iilter + VSI´ problem, as seen in section 3.1, the Pareto front has a particular shape (weak front).Thus, only the optimal solution with minimum mass is returned to the system level (Fig. 4-b).

I machine , V machine I convDC , S u Min M Fil-VSI P Fil-VSI X Fil-VSI = [L 1 , C 1 , C 2 , R C2 , I op ] Constraints: G Fil-VSI = [g 1 ,g 2 «g 8 ] Min M HSPMSM P HSPMSM X HSPMSM = [J s , N epp , g, B y , R dr , R lr , K p , K r , N bp , T pb ] Constraints: G Act =[g 1 ,g 2 «g 15 ] g 13 (R s -R s )² < ѓ 1 g 14 (L syn -L syn )² < ѓ 2 g 15 (Ѱ s -Ѱ s )² < ѓ 3 R s , L syn p , Ѱ M HSPMSM P HSPMSM G HSPMSM M Fil-VSI P Fil-VSI G Fil-VSI G sys = [g 1 , g 2 , G HSPMSM , G Fil-VSI ]
4. [START_REF] Sareni | ³0RGHO VLPSOLILFDWLRQ DQG RSWLPL[END_REF]

. RESULTS

The multi-level optimization problem is solved using the NSGA-II at each level (system and component). It leads to intermediate results between the ³sequential´ and ³global´ approach (Fig. 8). The difference between multi-level approach and global approach solutions can be explained by the limited number of generations of the system level optimization problem (results obtained with only 50 generations). However, multi-level optimization is highly expensive with regard to the computational time (500 hours of CPU time in a standard computer). These disadvantages compared to the global approach can be compensated by the major interest of the multi-level approach in managing projects especially with confidentiality issues between the different project participants. The challenge of our multi-level approach is to minimize the computational time by reducing the number of generations of the system level.

CONCLUSION

In this paper, three optimization approaches have been proposed: a sequential approach with two optimization loops separating power supply and actuation parts. Then, a global optimization with a unique loop integrating all couplings between HVDC network and actuation application with respect to the flight mission has been presented: the global optimization of all components clearly outperforms the sequential optimization approach.

The last approach based on multi-level formulation of the problem is intermediate between both sequential and global approach.

Fig. 1 .

 1 Fig. 1. Actuation system architecture

Fig. 2 .

 2 Fig. 2. Flight mission in the HSPMSM torque-speed plane

  e. M1), at the same level of losses (i.e. M3 WKH ³02´ PRWRU EHLng an intermediate dominant solution. Pareto-optimal solutions of ³input filter + VSI´ set are obtained as previously from NSGA-II runs considering the three particular HSPMSM configurations. Results are illustrated in Fig.4-b. The particular shape of the Pareto-RSWLPDO IURQW FOHDUO\ LQGLFDWHV ³D ZHDN IURQW´ LH WKH ODFN RI FRPSURPLVH EHWZHHQ ERWK objectives. Therefore, only ³input filter+VSIć onfigurations with minimum mass are considered as optimal solutions.

Fig. 4 .

 4 Fig. 4. Pareto-optimal configurations (a) HSPMSM optimal configurations (b) ³Input filter + VSI´ optimal configurations relative to three particular HSPMSM solutions (M1, M2, M3) (c) Optimal configurations obtained from sequential component or global system optimization frequency (f dec ) as decision variables and which ensures the coordination between component problems.

Fig. 5 .

 5 Fig. 5. ATC formulation.

Fig. 6 .

 6 Fig.[START_REF] Sareni | ³5HFRPELQDWLRQ DQG 6HOI-adaptation in Multiobjective *HQHWLF[END_REF]. Adopted multi-level formulation analysis model to the algorithm, against in adopted multi-level formulation, N 1 ×N 2 system solutions are returned for each vector of design system parameters (where N 1 denotes the Pareto front size of the HSPMSM problem andN 2 the Pareto front size of the ³LQSXW Iilter + VSI´ problem).Nevertheless, by analyzing the Pareto fronts of component problems, specific properties can be observed for each case:

Fig. 7 .Fig. 8 .

 78 Fig. 7. Pareto front of HSPMSM problem with equality constraints.

System Optimal Design Model Analysis Model Component Optimal design model Component Optimal design model Analysis Model Analysis Mo Analysis Mo Analysis Model System O t Optima n Model Componen design model gn m Analysis Mo Analysis Model design mo gn mo Analysis Mo System Level Component Level f dec f dec f ^LJƐƚĞŵ WƌŽďůĞŵ ,^WD^D WƌŽďůĞŵ͗ &ŝůƚĞƌͲs^/ WƌŽďůĞŵ͗ Min M sys = M

  HSPMSM +M FIL-VSI P sys = P HSPMSM +P Fil-VSI X Global = [f dec , R s , L syn , p , Ѱ] Contraintes g 1 : Maximum speed constraint g 2 : THDI HSPMSMmax constraint


Marius Bozga
email: marius.bozga@univ-grenoble-alpes.fr

Joseph Sifakis
email: joseph.sifakis@univ-grenoble-alpes.fr

Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework

Keywords: autonomous driving system, map modeling, configuration logic, traffic rule specification

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The validation of ADS raises challenges far beyond the current state of the art because of their overwhelming complexity and the integration of non-explainable AI components. Providing sufficient evidence that these systems are safe enough is a hot and critical need, given the underlying economic and societal stakes.

Institute of Engineering Univ. Grenoble Alpes

This objective mobilizes considerable investments and efforts by key players including big tech companies and car manufacturers. The efforts focus on the development of efficient simulation technology and common infrastructure for modelling the physical environment of ADS and their desired properties. They led in particular to the definition of common formats such as OpenDRIVE [START_REF]ASAM OpenDRIVE® -open dynamic road information for vehicle environment[END_REF] for the description of road networks, and OpenSCENARIO [START_REF]ASAM OpenScenario® -dynamic content in driving simulation, UML modeling rules[END_REF] for the description of complex, synchronized maneuvers that involve multiple entities like vehicles, pedestrians and other traffic participants. Additionally, several open simulation environments such as CARLA [START_REF] Dosovitskiy | CARLA: an open urban driving simulator[END_REF] and LGSVL [START_REF] Rong | LGSVL simulator: A high fidelity simulator for autonomous driving[END_REF] are available for modelling and validation.

The paper proposes a semantic framework for the specification and validation of ADS. The framework provides a precise semantic model of the environment of ADS based on maps. It also includes logics for the specification and validation of properties of the semantic model and of the system dynamic behavior. Maps have been the object of numerous studies focusing on the formalization of the concept and its use for the analysis of ADS. A key research issue is to avoid monolithic representations and build maps by composition of components and heterogeneous data. This motivated formalizations using ontologies and logics with associated reasoning mechanisms to check consistency of descriptions and their correctness with respect to desired properties [START_REF] Beetz | Benefits and limitations of linked data approaches for road modeling and data exchange[END_REF][START_REF] Bagschik | Ontology based scene creation for the development of automated vehicles[END_REF] or to generate scenarios [START_REF] Bagschik | Ontology based scene creation for the development of automated vehicles[END_REF][START_REF] Chen | An ontology-based approach to generate the advanced driver assistance use cases of highway traffic[END_REF]. Other works propose open source map frameworks for highly automated driving [START_REF]ASAM OpenDRIVE® -open dynamic road information for vehicle environment[END_REF][START_REF] Poggenhans | Lanelet2: A high-definition map framework for the future of automated driving[END_REF].

A different research line focuses on the validation of ADS either to verify satisfaction of safety and efficiency properties or even to check that vehicles respect given traffic rules. Many works deal with safety verification in a simple multilane setting. In [START_REF] Hilscher | An abstract model for proving safety of multi-lane traffic manoeuvres[END_REF] a dedicated Multi-Lane Spatial Logic inspired by interval temporal logic is used to specify safety and provide proofs for lane change controllers. The work in [START_REF] Rizaldi | A formally verified motion planner for autonomous vehicles[END_REF] presents a motion planner formally verified in Isabelle/HOL. The planner is based on manoeuver automata, a variant of hybrid automata, and properties are expressed in linear temporal logic.

Other works deal with scenarios for modeling the behavior of ADS. Open-SCENARIO [START_REF]ASAM OpenScenario® -dynamic content in driving simulation, UML modeling rules[END_REF] defines a data model and a derived file format for the description of scenarios used in driving and traffic simulators, as well as in automotive virtual development, testing and validation. The work in [START_REF] Damm | Using traffic sequence charts for the development of HAVs[END_REF] proposes a visual formal specification language for capturing scenarios inspired from Message Charts and shows possible applications to specification and testing of autonomous vehicles. In [START_REF] Schönemann | Scenario-based functional safety for automated driving on the example of valet parking[END_REF] a scenario-based methodology for functional safety analysis is presented using the example of automated valet parking. The work in [START_REF] Fremont | Formal scenario-based testing of autonomous vehicles: From simulation to the real world[END_REF] presents an approach to automated scenario-based testing of the safety of autonomous vehicles, based on Metric Temporal Logic. Finally, the probabilistic language Scenic for the design and analysis of cyber physical systems allows the description of scenarios used to control and validate simulated systems of self-driving cars. The Scenic programming environment provides a big variety of constructs making possible modeling anywhere in the spectrum from concrete scenes to broad classes of abstract scenarios [START_REF] Fremont | Scenic: A language for scenario specification and data generation[END_REF].

Other works focus on checking compliance of vehicles with traffic rules. A formalization of traffic rules in linear temporal logic is proposed in [START_REF] Esterle | From specifications to behavior: Maneuver verification in a semantic state space[END_REF]. Runtime verification is applied to check that maneuvers of a high-level planner comply with the rules. Works in [START_REF] Rizaldi | Formalising and monitoring traffic rules for autonomous vehicles in isabelle/hol[END_REF][START_REF] Rizaldi | Formalising traffic rules for accountability of autonomous vehicles[END_REF] formalize a set of traffic rules for highway scenarios in Isabelle/HOL; they show that traffic rules can be used as requirements to be met by autonomous vehicles and propose a verification procedure. A formalization of traffic rules for uncontrolled intersections is provided in [START_REF] Karimi | Formalizing traffic rules for uncontrolled intersections[END_REF] using the CLINGO logic programming language. Furthermore, the rules are applied by a simulator to safely control traffic across intersections. The work in [START_REF] Esterle | Formalizing traffic rules for machine interpretability[END_REF] proposes a methodology for the formalization of traffic rules in Linear Temporal Logic; it is shown how evaluation of formalized rules on recorded drives of humans provides insight on what extent drivers respect the rules. This work is an attempt to provide a minimal framework unifying the concepts for the specification of ADS and the associated validation problems. The proposed semantic framework clearly distinguishes between a static part consisting of the road network with its equipment and a dynamic part involving objects. We progressively introduce three logics to express properties of the semantic model at different levels. The Metric Configuration Logic (MCL) allows the compositional and parametric description of metric graphs. This is a first order logic with variables ranging over positions and segments. It uses in addition to logical connectives, a coalescing operator for the compositional construction of maps from segments. A MCL formula represents configurations of maps sharing a common set of locations. We discuss a specification methodology and show how various road patterns such as roundabouts, intersections, mergers of roads can be specified in MCL.

The Mobile Metric Configuration Logic (M2CL) is an extension of MCL with object variables and primitives for the specification of scenes as the distribution of objects over maps. M2CL formulas can be written as the conjunction of formulas describing: i) static map contexts; ii) dynamic relations between objects; iii) addressing relations between objects and maps. Last, we define Temporal M2CL (TM2CL), a linear temporal logic whose atomic propositions are formulas of M2CL. We illustrate the use of these logics for the specification of safety properties including traffic rules as well as the description of dynamic scenarios.

Additionally, we study the validation of properties expressed in the three logics and provide a classification of problems showing that validation of general dynamic properties boils down to constraint checking on metric graphs. Checking that a finite model satisfies a formula of MCL or M2CL amounts to eliminate quantifiers by adequate instantiation of variables. We argue that satisfiability of M2CL formulas can be reduced to satisfiability of MCL formulas which is an undecidable problem. We identify a reasonably expressive decidable subset of MCL and propose a decision procedure. Furthermore, we discuss the problem of runtime verification of TM2CL formulas and sketch a principle of solution inspired from a recent work with a similar configuration logic [START_REF] El-Hokayem | A temporal configuration logic for dynamic reconfigurable systems[END_REF]. We complete the presentation on ADS validation with an analysis of practical needs for a rigorous validation methodology. We describe a general validation environment and show how the proposed framework provides insight into the different aspects of validation and related methodological issues.

c 2 ego c 1 100km/h 100km/h 110km/h 20m 84m 100m

Fig. 1. A scenario example

To illustrate the specification and validation methodology based on the combined use of these three logics, let us consider a concrete example from [START_REF]ASAM OpenScenario® -dynamic content in driving simulation, UML modeling rules[END_REF] describing a scenario involving three cars moving on a two-lane road with their speeds and distances. We use MCL to describe the static environment in which the cars move. In this example, it is a two-lane road, but in the general case it can be a parametric map obtained by composing road segments. To describe a scene, such as the distribution of vehicles on a map, we use M2CL formulas. In this example, a scene is specified by the relative positions of the cars on the map and their speeds. Finally, to specify system properties, which are sequences of scenes, we use TM2CL. In this example, a scene sequence could be: car c 2 passes the ego car and moves to the right lane in front of it. The formulas in TM2CL can be used to specify traffic rules that must be satisfied by vehicle maneuvers.

The paper is structured as follows. In section 2, we study metric graphs and their relevant properties for the representation of map models as well as the logic MCL, its main properties and application for map specification. Section 3 deals with the study of logics M2CL and TM2CL and their application to the specification of safety properties and the description of scenarios. Then, section 4 discusses a classification of validations problems and approaches for their solution. Section 5 concludes with a summary of main results and a discussion about future developments. A long version of the paper is available in [START_REF] Bozga | Specification and validation of autonomous driving systems: A multilevel semantic framework[END_REF]. Moreover, we define s 1 s 2 iff s 1 = s 2 [0, a] for some non-negative a.

Metric Graphs and Metric Configuration Logic

Segments will be used to model building blocks of roads in maps considering three different interpretations. Interval segments simply define the length of a segment. Curve segments define the precise geometric form of the trajectory of a mobile object along the segment. Region segments are 2D-regions of given width around a center curve segment.

Interval Segments. Consider S interval def = {[0, a] | a ∈ R ≥0 },
that is, the set of closed intervals on reals with lower bound 0, concatenation defined by [0,

a 1 ] • [0, a 2 ] def = [0, a 1 + a 2 ] and length ||[0, a]|| def = a. Curve Segments. Consider S curve def = {c : [0, 1] → R 2 | c(0) = (0, 0), c curve} ∪ { } that
is, the set of curves that are continuous smooth1 and uniformly progressing2 functions c, starting at the origin, plus a designated single point curve . The length is defined by taking respectively the length of the curve ||c||

(c 1 • c 2 )(t) def = c 1 ( t λ ) if t ∈ [0, λ] c 1 (1) + c 2 ( t-λ 1-λ ) if t ∈ [λ, 1] where λ = ||c 1 || ||c 1 || + ||c 2 ||
Note that in this definition, c 1 and c 2 are scaled on sub-intervals of [0, 1] respecting their length ratio. We additionally take c • def = • c def = c, for any c. For practical reasons, one can further restrict the set S curve to curves of some form e.g, finite concatenation of parametric line segments and circle arcs. That is, for any

a, r ∈ R * ≥0 , ϕ ∈ R, θ ∈ R * the curves line[a, ϕ], arc[r, ϕ, θ] are defined as line[a, ϕ](t) def = (at cos ϕ, at sin ϕ) ∀t ∈ [0, 1] arc[r, ϕ, θ](t) def = (r(sin(ϕ + tθ) -sin ϕ), r(-cos(ϕ + tθ) + cos ϕ)) ∀t ∈ [0, 1]
Note that a and r are respectively the length of the line and the radius of the arc, ϕ is the slope of the curve at the initial endpoint and θ is the degree of the arc. Fig. 2 illustrates the composition of three segments of this parametric form. , that is, the set of pairs (c, w) where c is a curve and w a positive number, denoting respectively the region center curve and the region width. Region segments can be concatenated iff their curves can be concatenated and if their widths are equal, that is, (c 1 , w)•

c 2 = arc[1, 10 • , 160 • ] c 1 = line[5, 10 • ] c 3 = line[6, 170 • ] c 1 • c 2 • c 3
(c 2 , w) def = (c 1 • c 2 , w) if c 1 • c 2 = ⊥.
The length of a region segment is defined as the length of its center curve, ||(c, w)|| def = ||c||. Region segments can be equally understood as sets of points in R 2 defined by algebraic constraints. More precisely, for any curve c and width w the region segment (c, w) corresponds to the subset of R 2 defined as {c(t)

+ λ • ortho( ċ(t)) | ċ(t)| | t ∈ [0, 1], λ ∈ [-w 2 , w 2 ]
} where ortho is the orthogonal operator on R 2 defined as ortho((a, b)) def = (-b, a). In particular, the region generated by the curve line[a, ϕ] is a rectangle containing the set of points {(at cos ϕ -λ sin ϕ, at

sin ϕ + λ cos ϕ) | t ∈ [0, 1], λ ∈ [-w 2 , w 2 ]}.
The region generated by the curve arc[r, ϕ, θ] is a ring sector containing the set of points {((r

+ λ)(sin(ϕ + tθ) -r sin ϕ, -(r + λ) cos(ϕ + tθ) + r cos ϕ) | t ∈ [0, 1], λ ∈ [-w 2 , w 2 ]}.
Metric Graphs. We use metric graphs G def = (V, S, E) to represent maps, where V is a finite set of vertices, S is a set of segments and E ⊆ V × S × V is a finite set of edges labeled by non-zero length segments in S . We also denote an edge

e = (v, s, v ) ∈ E by v s -→ G v and we define • e def = v, e • def = v , e.s def = s. For a vertex v, we define • v def = {e|e • = v} and v • def = {e| • e = v}.
We denote by E + ac the finite set of non-empty acyclic 3 directed paths with edges from E. We call a metric graph strongly (resp. weakly) connected if a directed (resp. undirected ) path exists between any pair of vertices. A metric graph is called acyclic if at most one path, directed or undirected, exist between any pairs of vertices. We consider the set 3 illustrates the five cases of the above definition for a simple graph with segments s 1 , s 2 and s 3 . Cases (i) and (ii) correspond to rides on the same segment. Case (iii) corresponds to rides originating and terminating in fragments of the same segment and also involving other segments between them. Finally cases (iv) and (v) are rides originating and terminating at different segments. We define the distance d G between positions p, p as 0 whenever p = p or the minimum length among all segments labeling rides from p to p and otherwise +∞ if no such ride exists. It can be checked that d G is an extended quasi-metric on the set Pos G and therefore, (Pos G , d G ) is an extended quasi-metric space.

Pos G def = V ∪ {(e, a) | e ∈ E, 0 < a < ||e.
(i) e = e , 0 ≤ a ≤ a ≤ ||e.s||, s = e.s[a, a ] (ii) e = e , 0 ≤ a ≤ a ≤ ||e.s||, e • = • e, s = e.s[a, -] • e.s[0, a ] = ⊥ (iii) e = e , 0 ≤ a ≤ a ≤ ||e.s||, w ∈ E + ac , e ∈ w, e • = • w, w • = • e, s = e.s[a, -] • w.s • e.s[0, a ] = ⊥ (iv) e = e , e • = • e , s = e.s[a, -] • e .s[0, a ] = ⊥ (v) e = e , w ∈ E + ac , e, e ∈ w, e • = • w, w • = • e , s = e.s[a, -] • w.s • e .s[0, a ] = ⊥ Fig.

Properties of Metric Graphs

Contraction/Refinement. A metric graph G = (V , S, E ) is a contraction of a metric graph G = (V, S, E) (or dually, G is a refinement of G ), denoted by G G , iff G is obtained from G by
transformations replacing some of its edges e by acyclic sequences of interconnected edges e 1 e 2 ...e n while preserving the segment labeling i.e., e.s = e 1 .s • e 2 .s • ... • e n .s. In Fig. 4, the graph on the right is a contraction of the one on the left iff Note that metric graphs where all vertices have input or output degree greater than one cannot be contracted. Such vertices correspond to junctions (confluence of divergence of roads) when metric graphs represent maps. The following proposition states some key properties on contraction/refinement of metric graphs.

s 12 = s 14 • s 45 • s 52 , s 12 = s 16 • s 62 and s 31 = s 37 • s 78 • s 81 . v 1 v 2 s 81 s 14 s 23 s 78 v 3 v 5 v 6 s 31 s 37 s 16 s 62 s 52 v 4 v 7 v 8 s 45 v 1 v 2 v 3 s 12
Proposition 1. Let Con(G) def = {G | G G }, Ref (G) def = {G | G
G} be respectively the set of contractions, refinements of a metric graph G.

α(s 1 • s 2 ) = α(s 1 ) • α(s 2 ) for all s 1 , s 2 ∈ S such that s 1 • s 2 = ⊥.
For example, the function α CI : S curve → S interval defined by α CI (s) def = [0, ||s||] for all s ∈ S curve is a an abstraction of curve segments as interval segments. Similarly, the function α RC : S region → S curve defined by α RC ((s, w)) def = s for all (s, w) ∈ S region is an abstraction of region segments as curve segments.

Dually, we can define concretization functions γ that go from intervals to curves, and from curves to regions. For example, for any angles ϕ, θ consider γ IC ϕ,θ : S interval → S curve where respectively, γ IC ϕ,θ ([0, a]) abstraction concretization

def = arc[ a θ , ϕ, θ] if θ = 0 or γ IC ϕ,θ ([0, a]) def = line[a, ϕ] if θ = 0.
region metric graph v 1 v 2 v 3 v 4 directed graph curve metric graph interval metric graph v 2 v 3 v 4 v 4 v 3 v 2 v 1 v 2 v 3 v 4 v 1 v 1 [0, a 1 ] [0, a 2 ] [0, a 3 ] c 1 c 2 c 3 (c 1 , w) (c 2 , w) (c 3 , w)

Fig. 5. Illustration of abstraction/concretization on metric graphs

Given a segment abstraction α : S → S , a metric graph G = (V, S , E ) is an α-abstraction of a metric graph G = (V, S, E), denoted by G = α(G), iff G is obtained from G by replacing segments s by their abstractions α(s).

That is, any edge

u s -→ G v is transformed into an edge u α(s) ---→ G v.
In a similar way, γ-concretization on metric graphs is defined for a segment concretization γ : S → S. Fig. 5 illustrates the use of the three segment abstraction levels (respectively as intervals, curves, regions) and their associated metric graphs. Interval metric graphs are α CI -abstractions of curve metric graphs, which in turn are α RC -abstractions of region metric graphs. Propositions 2 and 3 state some key properties on abstraction on metric graphs.

Proposition 2. For a segment abstraction α : S → S and metric graphs G, G such that G = α(G), the labelled transition system (Pos G , S , G ) simulates the labelled transition system (Pos G , S, G ) renamed by α. Proposition 3. Contraction and abstraction commute, that is, for any metric graphs G, G , for any segment abstraction α, if G G then α(G) α(G ).

The Metric Configuration Logic

Syntax. Let consider a fixed set of segments S and assume there exists a finite set S T of segment constructors s T (or segment types), that is, partial functions s T : R m → S ⊥ for some natural m. For example, we can take S T curve = {line : R 2 → S ⊥ , arc : R 3 → S ⊥ } as the set of constructor curve segments S curve .

Let K, Z, X be distinct finite sets of variables denoting respectively reals, segments and vertices of a metric graph. The syntax of the metric configuration logic (MCL) is defined in Table 1.

Table 1. MCL Syntax t ::= a ∈ R | k ∈ K | t + t | t • t arithmetic terms ψK ::= t ≤ t arithmetic constraints s ::= s T (t1, ..., tm) | z ∈ Z | s • s segment terms ψS ::= s = s | s s | ||s|| = t segment constraints p ::= x ∈ X | (x, s, t) | (t, s, x) position terms ψG ::= x s -→ x | p = p | p s p | d(p, p ) = t position constraints φ ::= ψK | ψS | ψG atomic formula | φ ⊕ φ | φ ∨ φ | ¬φ non-atomic formula | ∃k. φ(k) | ∃z. φ(z) | ∃x. φ(x) quantifiers
Semantics. Let G = (V, S, E) be a metric graph fixed in the context, and let σ be an assignment of variables K, Z, X to respectively reals R, segments S, vertices V . As usual, we extend σ for evaluation of arithmetic terms (with variables from K) into reals. Moreover, we extend σ for the partial evaluation of segment terms (with variables from Z) and position terms (with variables from Z and X) into respectively segments S and positions Pos G as defined by the rules in Table 2.

: V × S × R → Pos ⊥ G are defined as pos f wd G (v, s, a) def = (e, a) only if ∃! e = (v, s, v ) ∈ E, 0 < a < ||s|| pos bwd G (v, s, a) def = (e, ||s|| -a) only if ∃! e = (v , s, v) ∈ E, 0 < a < ||s||
We tacitly restrict to terms which evaluate successfully in their respective domains. The semantics of MCL is defined by the rules in Table 3. Note that a formula represents a configuration of metric graphs sharing common characteristics. Besides the logic connectives with the usual set-theoretic meaning, the coalescing operator ⊕ allows building graphs by grouping elementary constituents characterized by atomic formulas relating positions via segments. Hence, the formula φ 1 ⊕ φ 2 represents the graph configurations obtained as the union of configurations satisfying φ 1 and φ 2 respectively. It differs from φ 1 ∨ φ 2 in that this formula satisfies configurations that satisfy either φ 1 or φ 2 .

Table 3. MCL Semantics σ, G |= t ≤ t iff σt ≤ σt σ, G |= s = s iff σs = σs σ, G |= s s iff σs σs σ, G |= ||s|| = t iff ||σs|| = σt σ, G |= x s -→ x iff E = {(σx, σs, σx )} σ, G |= p = p iff σp = σp σ, G |= p s p iff σp σs G σp σ, G |= d(p, p ) = t iff dG(σp, σp ) = σt σ, G |= φ1 ⊕ φ2 iff σ, (V, E1) |= φ1 and σ, (V, E2) |= φ2 for some E1, E2 such that E1 ∪ E2 = E σ, G |= φ1 ∨ φ2 iff σ, G |= φ1 or σ, G |= φ2 σ, G |= ¬φ iff σ, G |= φ σ, G |= ∃k. φ iff σ[k → a], G |= φ for some a ∈ R σ, G |= ∃z. φ iff σ[z → s], G |= φ for some s ∈ S σ, G |= ∃x. φ iff σ[x → v], G |= φ for some v ∈ V
Properties. Table 4 provides a set of theorems giving insight into the characteristic properties of the logic. Theorems (A.i)-(A.v) illustrate important properties of the ⊕ operator that is associative and commutative but not idempotent. As explained below, of particular interest for writing specifications are formulas of the form ∼ φ def = φ ⊕ true. These are satisfied by configurations with graphs that contain a subgraph satisfying φ. Hence, while the formula

x s -→ x charac- Table 4. MCL Theorems (A.i) (φ1 ⊕ φ2) ⊕ φ3 ≡ φ1 ⊕ (φ2 ⊕ φ3) (A.ii) φ1 ⊕ φ2 ≡ φ2 ⊕ φ1 (A.iii) φ ⊕ false ≡ false (A.iv) φ ⊕ φ ≡ φ (in general ) (A.v) φ1 ⊕ (φ2 ∨ φ3) ≡ (φ1 ⊕ φ2) ∨ (φ1 ⊕ φ3) (B.i) ∼∼φ ≡ ∼φ (B.ii) φ =⇒ ∼φ (B.iii) ∼(φ1 ∨ φ2) ≡ ∼φ1∨ ∼φ2 (B.iv) ∼(φ1 ⊕ φ2) ≡ ∼φ1⊕ ∼φ2 ≡ ∼φ1∧ ∼φ2 (C.i) x s -→ x ∧ (φ1 ⊕ φ2) ≡ (x s -→ x ∧ φ1) ⊕ (x s -→ x ∧ φ2) (C.ii) true ≡ (x s -→ x ⊕ ¬(∼x s -→ x )) ∨ ¬(∼x s -→ x ) (D.i) d(p, p ) = t ∧ p s p =⇒ t ≤ ||s|| (D.ii) d(p, p ) = t ∧ d(p , p ) = t =⇒ ∃k. d(p, p ) = k ∧ k ≤ t + t
terizes the graphs with two vertices and a single edge labeled by s, the formula ∼x Note that stronger preservation results for (even simple fragments of) MCL are hard to obtain because the domain of vertex variables is a fixed set of vertices. This makes MCL sensitive to both contraction and refinement. For example, the formula ∃x. ∃y. x s y may not hold before and hold after refinement i.e., if a pair of vertices u, v satisfying the constraint is added by refinement. We provide below abstraction preservation results for MCL formulas. Any segment abstraction α : S → S can be lifted to segment terms by taking respectively α(s

T (t 1 , ..., t m )) def = (αs T )(t 1 , ..., t n ), α(s 1 •s 2 ) def = α(s 1 )• α(s 2 ), α(z) def = z.
Moreover, α can be further lifted to MCL formulas on S. We denote by α(φ) the MCL formula on S obtained by rewriting all the segment terms s occuring in φ by α(s). The following proposition relates abstractions on formulas to abstractions on metric graphs. (i) φ does not contain distance constraints or (ii) for any connected edges e 1 , e 2 such that e 1 • = • e 2 their segments compose, that is, e 1 .s • e 2 .s = ⊥.

ADS Specification

The results of the previous section provide a basis for the definition of both a dynamic model for ADS and of logics for the expression of their properties. The model is a timed transition system with states defined as the distribution of objects over of a metric graph representing a map. Objects may be mobile such as vehicles and pedestrians or static such as signaling equipment. The logics are two extensions of MCL, one for the specification of predicates representing sets of states and the other for the specification of its behavior.

We introduce first the concept of map and its properties. Then we define the dynamic model and the associated logics. Finally, we discuss the validation problem and its possible solutions.

Map Specification

A weakly connected metric graph G = (V, S, E) can be interpreted as a map with a set of roads R and a set of junctions J, defined in the following manner:

-a road r of G is a maximal directed path r = v 0 s1 -→ G v 1 , v 1 s2 -→ G v 2 , ..., v n-1 sn -→ G v n
where all the vertices v 1 , ..., v n-1 have indegree and outdegree equal to one. We say that v 0 is the entrance and v n is the exit of r. Let R = {r i } i∈I be the set of roads of G.

a junction j of G is any maximal weakly connected sub-graph G of G, obtained from G by removing from its roads all the vertices (and connecting edges) except their entrances and exits. Note that for a junction, its set of vertices of indegree (resp. outdegree) one are exits (resp. entrances) of some roads. Let J = {j } ∈L be the set of junctions of G.

Note that G is the union of the subgraphs representing its roads and junctions. For every junction, the strong connectivity of G implies that from any entrance there exists at least one path leading to an exit. Additionally, we assume that maps include information about features of roads, junctions that are relevant to traffic regulations:

roads and junctions are typed : road types can be highway, built-up area roads, carriage roads, etc. Junctions types can be roundabouts, crossroads, highway exit, highway entrance, etc. We use standard notation associating a road or junction to its type e.g., r : highway, j : roundabout. roads, junctions and their segments have attributes. We use the dot notation a.x and a.X to denote respectively the attribute x or the set of attributes X of a. In particular, we denote by r.en and r.ex respectively the entrance and the exit of a road r and by j.En and j.Ex the sets of entrances and exits of a junction j. Similarly, r.lanes is the number of lanes of the road r.

Note that contraction and refinement transform maps into maps. A road may be refined into a road while a junction may be decomposed into a set of roads and junctions. Furthermore, abstraction and concretization transform maps into maps as they preserve their connectivity.

Given a map with sets of roads and junctions R and J respectively, it is possible to derive compositionally its bottom-up and top-down specifications. We show first how we can get formulas ζ j , ζ r and ξ j , ξ r for the bottom-up and top-down specifications of j and r, respectively. Let us consider the junctions illustrated in Fig. 6:

-if ra is a roundabout with n entrances ra.En = {en k } k∈[1,n] alternating with n exits ra.Ex = {ex k } k∈[1,n] then its bottom-up specification is ζ ra def = n k=1 ζ k ⊕ n k=1 ζ k,k+1 , where ζ k def = ex k s k -→ en k and ζ k,k+1 def = en k s k,k+1 ----→ ex k+1 . The top-down specification is ξ ra def = n k=1 ξ k ∧ n k=1 ξ k,k+1 where ξ k def = ∼ζ k and ξ k,k+1 def = ∼ζ k,k+1 .
if in is an intersection with n entrances in.En = {en k } k=1,n and n exits

in.Ex = {ex k } k∈[1,n] then its bottom-up specification is ζ in def = n k=1 ζ k with ζ k def = j∈J k en k s k,j
--→ ex j and J k is the set of indices of the exits of j.Ex connected to the entrance en k . Hence, the top-down specification is

ξ in def = n k=1 ξ k where ξ k def = ∼ζ k .
the formulas for a merger mg and a fork f k with respectively n entrances and n exits and unique exit and entrance respectively, can be obtained as a particular case of an intersection. For a vehicle c, its state s c def = it, pos, sp, wt, ln, ... includes respectively its itinerary (from the set of segments S), its position on the map (from Pos G ), its speed (from R ≥0 ), the waiting time (from R ≥0 ) which is the time elapsed since the speed of c became zero, the lane it is traveling (from R ≥0 ), etc. For a traffic light lt, its state s lt def = pos, cl , ... includes respectively its position on the map (from Pos G ), and its color (with values red and green), etc. For a map G and an initial state s (t0) we define a run as a sequence of consecutive states [s (ti) ] i≥0 parameterized by an increasing sequence of time points t i ∈ R ≥0 , equal to the sum of the time intervals elapsed for reaching the i-th state.

M2CL is equipped with object variables Y with attributes allowing to express constraints on object states. Object variables in Y are typed and denote objects from a finite set O. Constraints are obtained by extending the syntax of MCL to include object attribute terms. For example, if y is a "vehicle" variable then y.it is a segment term, y.pos is a position term, and y.ln, y.sp, y.wt are arithmetic terms of M2CL. Moreover, M2CL allows for equality y = y and existential quantification ∃y of object variables.

The semantics of M2CL formulas is defined on distributions σ, G, s where σ provides an interpretation of variables (including object variables) to their respective domains, G is a metric graph representing the map, and s is the system state vector for objects in O. The evaluation of terms is extended to include object attributes, that is, for any object variable y with attribute attr we define σ y.attr def = s σy (attr ). Equality and existential elimination on objects variables are interpreted with the usual meaning, that is, y = y holds on σ, G, s iff σy = σy and respectively ∃y. ψ holds on σ, G, s iff ψ holds on σ[y → o], G, s for some object o ∈ O.

From a methodological point of view, we restrict to M2CL formulas that can be written as boolean combinations of three categories of sub-formulas:

(i) ψ map describing map specifications characterizing the static environment in which a dynamic system evolves, (ii) ψ dyn describing relations between distributions of the objects of a dynamic system, (iii) ψ add linking itinerary attributes of objects involved in ψ dyn to position addresses of maps described by ψ map .

The following set of primitives used respectively in sub-formulas of the above categories is needed to express ADS scenarios and specifications:

(i) for x, x vertex variables, X set of vertex variables, [x right-of x in X], [x opposite x in X] express constraints on the positioning of x, x with respect to the map restricted to vertices in X (typically a junction): [c turn-right X], [c turn-left X] express constraints on the itinerary of c within the map restricted to vertices in X (typically, a junction):

[x right-of x in X] def = ∃a.∃r.∃ϕ.∃ (0,π) θ. x ∈X x line[a,ϕ] -----→ x ∧x arc[r,ϕ+θ,-θ] ---------→ x [x opposite x in X] def = ∃a.∃ϕ. x ,x ∈X x line[a,ϕ] -----→ x ∧ x line[a,ϕ+π] -------→ x (
[c go-straight X] def = ∃a.∃ϕ. line[a, ϕ] c.it ∧ x,x ∈X c.pos = x ∧ x line[a,ϕ] -----→ x [c turn-right X] def = ∃r.∃ϕ.∃ (-π,0) θ. arc[r, ϕ, θ] c.it ∧ x,x ∈X c.pos = x ∧ x arc[r,ϕ,θ] ------→ x [c turn-left X] def = ∃r.∃ϕ.∃ (0,π) θ. arc[r, ϕ, θ] c.it ∧ x,x ∈X c.pos = x ∧ x arc[r,ϕ,θ] ------→ x b)
for o an object variable, X a set of vertex variables, l an optional arithmetic term, [o@X, l] means that the position of o belongs to the map subgraph restricted to vertices in X and the lane of o is l:

[o@X, l] def = ∃d.∃s. x,x ∈X x s -→ x ∧ o.pos = (x, s, d) ∨ o.pos = x ∧o.ln = l
Scenario Description for ADS. We define a scene as a triplet ψ map , ψ add , ψ dyn of M2CL formulas without universal quantifiers where ψ add defines the addresses of the objects involved in ψ dyn in the map specified by ψ map . As for maps, a scene can have a top-down and a bottom-up specification defined respectively by the formulas, ∼ψ map ⇒ ψ add ∧ ψ dyn and ψ map ∧ ψ add ∧ ψ dyn .

A scenario is a sequence of scenes sharing a common map context and intended to describe relevant partial states of an ADS run. There are several proposals for scenario description languages [START_REF]ASAM OpenScenario® -dynamic content in driving simulation, UML modeling rules[END_REF][START_REF] Damm | Using traffic sequence charts for the development of HAVs[END_REF][START_REF] Fremont | Scenic: A language for scenario specification and data generation[END_REF]. Figure 1 presents a scenario of two scenes taken from [START_REF]ASAM OpenScenario® -dynamic content in driving simulation, UML modeling rules[END_REF]. The initial scene is defined by:

ψmap = [r : road(x, s, y)] ∧ [s.lanes = 2] ψ add = [ego@r, 1] ∧ [c1@r, 1] ∧ [c2@r, 2] ψ dyn = [ego meets(84) c1] ∧ [c2 meets(100) ego] ∧ [ego.sp = c1.sp = 100 ∧ c2.sp = 110]
The second scene after the vehicle c 2 passes the ego vehicle is:

ψ map = [r : road(x, s, y)] ∧ [s.lanes = 2] ψ add = [ego@r, 1] ∧ [c1@r, 1] ∧ [c2@r, 1] ψ dyn = [ego meets(20) c2] ∧ [c2 meets(64) c1] ∧ [ego.sp = c1.sp = 100 ∧ c2.sp = 110]
Note that from a semantic point of view, a scene is characterized by minimal models of M2CL σ, G, s that satisfy the formula and where all irrelevant components of s are omitted. For instance, in the minimal models of the two scenes only the components of s corresponding to c 1 , c 2 and ego are taken.

Temporal M2CL and Specification of ADS

Temporal M2CL (shorthand TM2CL) is defined as the linear time temporal extension of M2CL. The syntax is as follows:

Φ ::= φ | N Φ | Φ U Φ | Φ ∧ Φ | ∃c. Φ | ¬Φ
where φ is M2CL formula. We consider moreover the eventually operator ♦Φ def = true U Φ, and always operator

Φ def = ¬♦¬Φ. The semantics of TM2CL is defined on triples (σ, G, [s (ti) ] i≥0 ) containing respectively an assignment σ of Table 5. Semantics of TM2CL σ, G, [s (t i ) ] i≥0 |= φ iff σ, G, s (t 0 ) ) |= φ σ, G, [s (t i ) ] i≥0 |= N Φ iff σ, G, [s (t i ) ] i≥1 |= Φ σ, G, [s (t i ) ] i≥0 |= Φ1 U Φ2 iff ∃k ≥ 0. ∀j ∈ [0, k -1]. σ, G, [s (t i ) ] i≥j |= Φ1 and σ, G, [s (t i ) ] i≥k |= Φ2 σ, G, [s (t i ) ] i≥0 |= Φ1 ∧ Φ2 iff σ, G, [s (t i ) ] i≥0 |= Φ1 and σ, G, [s (t i ) ] i≥0 |= Φ2 σ, G, [s (t i ) ] i≥0 |= ∃o. Φ iff σ[o → u], G, [s (t i ) ] i≥0 |= Φ, for some u ∈ O σ, G, [s (t i ) ] i≥0 |= ¬Φ iff σ, G, [s (t i ) ] i≥0 |= Φ
vehicle variables defined in the TM2CL context, a map G and a run [s (ti) ] i≥0 on G for a finite set of objects O. The semantic rules are defined in Table 5.

We use TM2CL for both the specification of system properties and traffic rules. The difference between the two concepts is not clear-cut although it is implicit in many works. System properties characterize the desired ADS behavior in terms of relations between speeds and distances taking into account relevant dynamic characteristics. These include properties such as keeping safe distance or keeping acceleration and deceleration rates between some bounds.

Traffic rules are higher-level specifications for enhanced safety and efficiency that usually depend on the driving context. They deal not only with obligations such as yielding right of way and traffic control at junctions but also advice on how to drive sensibly and safely in situations disrupting traffic flow such as congestion, accidents and works in progress. We provide below a formalization of system properties and traffic rules showing the expressiveness of our modeling framework. We formalize a set of traffic rules for an intersection j with all-way stop provided in [26]. The rules are implications of the form ∼ ζ(j) ⇒ Φ(j) where ζ(j) is the MCL formula characterizing j and Φ(j) is a TM2CL formula describing contraints on the driver behavior. We provide below the constraints in English and the corresponding TM2CL formulas: (i) "If a driver arrives at the intersection and no other vehicles are present, then the driver can proceed":

∀c.∀st. [st@j.en] ∧ [c@j.en] ∧ [¬∃c . c = c ∧ [c @j]] ⇒ ♦[c@j]
(ii) "If, on approach of the intersection, there are one or more cars already there, let them proceed, then proceed yourself": 4 ADS Validation

∀c.∀st. [st@j.en] ∧ [c meets(d) st] ∧ [d ≤ dmin] ⇒ [¬[c@j]] U [¬∃c .c = c ∧ [c @j]] (

Classification of Validation Problems

The following categories of validation problems can arise in our framework:

MCL and M2CL Model-Checking: (i) Given a map specification φ as a closed MCL formula and a metric graph G decide if G is a model of φ. The problem boils down to checking satisfiability of a segment logic (SL) formula obtained by quantifier elimination of vertex variables and partial evaluation of graph constraints in φ according to G. We present later in this section a decision procedure for SL. (ii) Similarly, given a distribution specification φ as a closed M2CL formula, a map G and a state s for a finite set of objects O, decide if G, s is a model of φ. Again, the problem boils down to checking satisfiability of a SL formula obtained by quantifier elimination of vertex and object variables an and partial evaluation of attribute terms.

TM2CL Runtime Verification: Given a temporal specification Φ as a TM2CL formula, a map G and a run [s (ti) ] i≥0 of an ADS, check if G, [s (ti) ] i≥0 is a model of Φ. This problem boils down to evaluating the semantics of Φ on the run. In [START_REF] El-Hokayem | A temporal configuration logic for dynamic reconfigurable systems[END_REF] we consider a similar runtime verification problem for temporal configuration logic and runs of dynamic reconfigurable systems. We have shown that the evaluation of linear-time temporal operators and the model-checking of state/configuration specifications can be dealt separately. The same idea can be applied here: on one hand, the temporal formulas can be handled by LamaConv [START_REF]LamaConv -Logics and Automata Converter Library[END_REF] to generate FSM monitors and on the other hand, the model-checking of distribution specifications can be handled by a SMT solver (such as Z3) by using an encoding into a decidable theory.

MCL and M2CL Satisfiability Checking: (i) Given a map specification φ as a closed MCL formula decide if φ is satisfiable, that is, it has at least one model.

We then show in this section that the problem can be effectively solved for a significant fragment of MCL including a restricted form of bottom-up map specifications. Notice that entailment checking, that is, deciding validity of ∀x. φ 1 ⇒ φ 2 for map specifications φ 1 , φ 2 where f v(φ 1 ) = f v(φ 2 ) = x, boils down to checking satisfiability of ∃x. φ 1 ∧ ¬φ 2 , and can be solved under the same restrictions. (ii) Similarly, given a distribution specification φ as a closed M2CL formula decide if φ is satisfiable, that is, it has at least one model. The problem can be reduced to the satisfiability checking of MCL specifications whenever φ is of the restricted form ∃y 1 ...∃y k . φ where y 1 , ... y k are the only object variables occurring in φ .

In this case, every object variable y can be substituted by a finite number of MCL variables y attr encoding its identity and attributes. As example, for a vehicle variable y consider an identity (real) variable y id , a segment variable y it , a position variable y pos , real variables y ln , y sp , y wt , etc. After replacement, we obtain an equisatisfiable MCL formula by enforcing the additional constraints that state attributes are consistently assigned (e.g., (y id = y id ) ⇒ y it = y it ) for all pairs y, y of vehicle variables among y 1 , ..., y k . Finally, notice also that entailment checking between distributed specifications can be solved as well, by reduction to satisfiability checking as explained above.

Satisfiability Checking

Satisfiability Checking of MCL. The satisfiability checking for MCL formula is undecidable in general. Actually, the combined use of edge constraints x s -→ x , equalities on vertex positions x = x , boolean operators and quantifiers leads to undecidability, as it allows the embedding of first order logic on directed graphs.

Nevertheless, for a significant class of MCL formulas, their satisfiability checking can be reduced to satisfiability checking of segment logic (SL), that is, the fragment of MCL without vertex variables, which is a first order logic combining only arithmetic and segment constraints.

A complete metric graph specification ψ * is a MCL formula of the form:

(∧ 1≤i<j≤n x i = x j ) ∧ (∀y. ∨ n i=1 y = x i ) ∧ ( n i=1 n j=1 mij h=1 x i s ijh --→ x j ) ∧ (∧ n i=1 ∧ n j=1 ∧ 1≤h<h ≤mij s ijh = s ijh ) that is
, where the set of free vertex variables is x = {x 1 , ...., x n }. Note that a complete metric specification characterizes a metric graph with precisely n vertices (in correspondence with vertex variables x 1 , . . . , x n ) and, with precisely m ij distinct edges (that is, defined by the constraints x i s ijh --→ x j for h = 1, m ij ), for every pair of vertices x i , x j . Theorem 1. Let ψ * be a complete metric graph specification with free variables x z k. For any MCL formula φ with f v(φ) ⊆ x z k holds 1. the closed MCL formula ∃x. ∃z. ∃k. ψ * ∧ φ is satisfiable iff 2. the closed SL formula ∃z. ∃k.

(∧ n i=1 ∧ n j=1 ∧ 1≤h<h ≤mij s ijh = s ijh )∧(∧ n i=1 ∧ n j=1 ∧ mij h=1 ||s ijh || > 0) ∧ tr(n, E * , µ * , φ) is satisfiable, where n = card x, E * = ∪ n i=1 ∪ n j=1 {(i, s ijh , j)} h=1,mij , µ * = {x i → i} i=1
,n and the translation tr(n, E, µ, φ) is defined in Table 6. If the conjunction of the translated formula tr(n, E * , µ * , φ) and the additional constraints has a model, ones can use it to build a metric graph, isomorphic to G ψ * , satisfying both ψ * and φ. In particular the additional constraints ensure that the metric graph is well formed, that is, all edges are labeled by non-zero length segments, and there are no replicated edges between any pairs of vertices.

Satisfiability Checking of SL. If segments S are restricted to particular interpretations, the satisfiability checking of formula of SL can be further reduced to satisfiability checking of formulas of extended arithmetic on reals.

Theorem 2. If segments S are defined as intervals 1. the closed SL formula φ is satisfiable iff 2. the closed real arithmetic formula tr 1 (φ) is satisfiable, where the translation tr 1 (φ) is defined in Table 7.

Proof. With interval interpretation, segments are precisely determined by their length and all segment operations and constraints boil down to operations and constraints on reals. Moreover, we remark that the transformation does not require multiplication4 on real terms, henceforth, the translated formula tr 1 (φ) belongs to linear arithmetic iff all arithmetic constraints ψ K within φ were linear.

Discussion

The proposed framework relies on a minimal set of semantically integrated concepts. It is expressive and modular as it introduces progressively the basic concepts and carefully separates concerns. It supports a well-defined specification and validation methodology without semantic gaps as discussed in [START_REF] Bozga | Specification and validation of autonomous driving systems: A multilevel semantic framework[END_REF]. Using configuration logic allows the specification of behavioral properties taking into account map contexts. This is a main difference from approaches relying on temporal logics that cannot account for map configurations and where formulas characterize sets of runs in some implicit map environment, usually a simple multi-lane setting. Configuration logic specifies scenes as conjunctions of formulas describing map configurations and vehicle distributions linked by an addressing relation. It enables enhanced expressiveness by combining static and dynamic aspects while retaining the possibility to consider them separately. It considers maps as the central concept of the semantic model and emphasizes the needs for multilevel representation depending on the type of goals to be met including long-term mission goals, mid-term maneuver goals and short-term safety and trajectory tracking goals. Among the three abstraction levels, curve segment models play a central role. Interval segment models can account for simple properties depending only on relative distances between the involved mobiles.

For properties depending on topological and geometric relations, curve segment models are needed. The expression of such properties involves primitives such as go-straight, turn-right, turn-left, right-of and opposite. Region segment models are needed for low level properties taking into account the dimensions of the objects and their movement in the 2D space. The paper is the culmination of work developed over the past three years both on foundations of autonomous systems [START_REF] Harel | Autonomics: In search of a foundation for nextgeneration autonomous systems[END_REF][START_REF] Sifakis | Autonomous systems -an architectural characterization[END_REF] and on modelling and validation of reconfigurable dynamic systems using the DR-BIP component framework [START_REF] Ballouli | Four exercises in programming dynamic reconfigurable systems: Methodology and solution in DR-BIP[END_REF][START_REF] El-Hokayem | A temporal configuration logic for dynamic reconfigurable systems[END_REF]. We plan to extend this work in two directions. The first is to leverage on the DR-BIP execution semantics and formalize ADS dynamics as the composition of object behavior acting on maps. The second is to extend our work on runtime verification of dynamic reconfigurable systems [START_REF] El-Hokayem | A temporal configuration logic for dynamic reconfigurable systems[END_REF] by developing adaptive validation techniques driven by adequate model coverage criteria. These techniques should provide model-based evidence that a good deal of the many and diverse driving situations are covered (e.g. different types of roads, of junctions, of traffic conditions, etc). Finally, we will investigate diagnostics generation techniques linking failures to their causes emerging from risk factors such as violations of traffic regulations and unpredictable events.

def = 1 0

 1 | ċ(t)|dt and || || = 0. The concatenation c 1 • c 2 of two curves c 1 and c 2 is a partial operation that consists in joining the final endpoint of c 1 with the initial endpoint of c 2 provided the slopes at these points are equal. This condition preserves smoothness of the curve c 1 • c 2 defined by c 1 • c 2 : [0, 1] → R 2 where:

Fig. 2 .

 2 Fig. 2. Curve segments and their composition

  s||} of positions defined by a metric graph. Note that (e, 0) and (e, ||e.s||) are respectively the positions • e and e • . Moreover, a s-labelled ride between positions (e, a) and (e , a ) is an acyclic path denoted by (e, a) s G (e , a ) and defined as follows:

3 Fig. 3 .

 33 Fig. 3. Rides in metric graphs -cases (i)-(v) illustrated

Fig. 4 .

 4 Fig. 4. Illustration of contraction/refinement on metric graphs

  (i) the refinement relation is a partial order on the set of metric graphs; (ii) for any metric graph G, both (Con(G), ) and (Ref (G), ) are complete lattices, moreover, (Con(G), ) is finite; (iii) for any metric graphs G, G if G G then (1) the labelled transition systems (Pos G , S, G ) and (Pos G , S, G ) are strongly bisimilar and (2) the quasi-metric spaces (Pos G , d G ) and (Pos G , d G ) are isometric; Abstraction/Concretization. Consider S, S as sets of segments associated with respectively concatenation •, • , and length norm ||.||, ||.|| . A function α : S → S is a segment abstraction if it satisfies the following properties: (i) length preservation: ||s|| = ||α(s)|| , forall s ∈ S (ii) homomorphism wrt concatenation:

  Or, for any positive real w consider γ CR w : S curve → S regions where γ CR w (s) def = (s, w).

s-→

  x characterizes the set of graphs containing such an edge. Thus ∼ is a closure operator which moreover satisfies theorems (B.i)-(B.iv). Finally, theorems (C.i)-(C.ii) relate the atomic formula x s -→ x to coalescing and the complement of their closure. The two last theorems (D.i)-(D.ii) differ from the others in that they express specific properties of segment and position constraints.

Proposition 4 .

 4 Position constraints not involving edge constraints of the form x s -→ x are insensitive to metric graph contraction and refinement.

Proposition 5 .

 5 Let φ be an existential positive MCL formula. Then G |= φ implies α(G) |= α(φ) whenever:

  finally, for a road r the specifications are ξ r def = ∼ζ r with ζ r def = r.en sr -→ r.ex .

Fig. 6 .

 6 Fig. 6. Junctions and roads

  ii) for c, o respectively vehicle, object variables, d arithmetic term, [c meets(d) o] means that c reaches the position of o at distance d: [c meets(d) o] def = ∃z. z c.it ∧ c.pos z o.pos ∧ ||z|| = d (iii) a) for c a vehicle variable, X a set of vertex variables, [c go-straight X],

  iii) "If a driver arrives at the same time as another vehicle, the vehicle on the right has the right-of-way":∀c.∀c . [c@j.en] ∧ [c @j.en ] ∧ [c.wt = c .wt] ∧ [j.en right-of j.en in j] ⇒ [c @j.en ] U [c@j](iv) "(a) If two vehicles arrive opposite each other at the same time, and no vehicles are on the right, then they may proceed at the same time if they are going straight ahead. (b) If one vehicle is turning and one is going straight, the right-of-way goes to the car going straight:" ∀c.∀c . [c@j.en] ∧ [c @j.en ] ∧ [c.wt = c .wt = 0] ∧ [j.en opposite j.en in j]∧ ¬[∃c . [c @j.en ] ∧ [j.en right-of j.en in j] ∨ [j.en right-of j.en in j]]∧ [c go-straight j] ∧ [c go-straight j] ⇒ ♦[c@j] ∧ [c @j] ∀c.∀c . [c@j.en] ∧ [c @j.en ] ∧ [c.wt = c .wt = 0] ∧ [j.en opposite j.en in j]∧ ¬[∃c . [c @j.en ] ∧ [j.en right-of j.en] ∨ [j.en right-of j.en ]]∧ [c go-straight j] ∧ ¬[c go-straight j] ⇒ ♦[c@j] (v) "If two vehicles arrive opposite each other at the same time and one is turning right and one is turning left, the right-of-way goes to the vehicle turning right. Since they are both trying to turn into the same road, priority should be given to the vehicle turning right as they are closest to the lane": ∀c.∀c . [c@j.en] ∧ [c @j.en ] ∧ [c.wt = c .wt = 0] ∧ [j.en opposite j.en in j]∧ [c turn-right j] ∧ [c turn-left j] ⇒ ♦[c@j]

def=

  len-s T (t1, ..., tm) tr1(s = s ) def = tr1(||s||) = tr1(||s ||) tr1(||z||) def = kz tr1(s s ) def = tr1(||s||) ≤ tr1(||s ||) tr1(||s • s ||) def = tr1(||s||) + tr1(||s ||)) tr1(||s|| = t) def = tr1(||s||) = t

  associativity: for any segments s 1 , s 2 , s 3 either both (s 1 •s 2 )•s 3 and s 1•(s 2 •s 3 ) are defined and equal, or both undefined; (ii) length additivity wrt concatenation: for any segments s 1 , s 2 whenever s 1 • s 2 defined it holds ||s 1 • s 2 || = ||s 1 || + ||s 2 ||; (iii) segment split: for any segment s and non-negative a 1 , a 2 such that ||s|| = a 1 + a 2 there exist unique s 1 , s 2 such that s = s 1 • s 2 , ||s 1 || = a 1 , ||s 2 || = a 2 . The last property allows us to define consistently a subsegment operation: s[a 1 , a 2 ] is the unique segment of length a 2 -a 1 satisfying s = s 1 • s[a 1 , a 2 ] • s 2 where s 1 , s 2 are such that ||s 1 || = a 1 , ||s 2 || = ||s|| -a 2 , for any 0 ≤ a 1 ≤ a 2 ≤ ||s||. For brevity, we use the shorthand notation s[a, -] to denote the subsegment s[a, ||s||].

	2.1 Segments and Metric Graphs
	Segments. We build contiguous road segments from a set S equipped with a
	partial concatenation operator • : S × S → S ∪ {⊥} and a length norm ||.|| : S →
	R ≥0 satisfying the following properties:
	(i)

Table 2 .

 2 Evaluation of MCL terms σs T (t1, ..., tm)

		def = s T (σt1, ..., σtm)	σ(x, s, t)	def = pos f wd G (σx, σs, σt)
	σ s • s	def = σs • σs	σ(t, s, x)	def = pos bwd G (σx, σs, σt)
	where pos f wd G , pos bwd G

Table 6 .

 6 Translation rules for Theorem 1.(complete definition in [6])

	tr(n, E, µ, ψK )	def = ψK
	tr(n, E, µ, ψS)	def = ψS
	tr(n, E, µ, x	s -→ y)	def =	s = s ijh if E = {(i, s ijh , j)}, µx = i, µy = j false otherwise
	tr(n, E, µ, p = p )	def = eq-pos(n, E, µ, p, p )
	tr(n, E, µ, p	s p )	def = acyclic-path(n, E, µ, p, s, p )
	tr(n, E, µ, φ1 ⊕ φ2)	def = E 1 ∪E 2 =E tr(n, E1, µ, φ1) ∧ tr(n, E2, µ, φ2)
	tr(n, E, µ, φ1 ∨ φ2)	def = tr(n, E, µ, φ1) ∨ tr(n, E, µ, φ2)
	tr(n, E, µ, ¬φ)	def = ¬tr(n, E, µ, φ)
	tr(n, E, µ, ∃k. φ)	def = ∃k. tr(n, E, µ, φ)
	tr(n, E, µ, ∃z. φ)

def

= ∃z. tr(n, E, µ, φ) tr(n, E, µ, ∃x. φ)

def = n i=1 tr(n, E, µ[x → i], φ) Proof. (1 ⇒ 2)

If the formula ψ * ∧ φ is satisfiable, then it has a metric graph model isomorphic to the (unique up to edge labeling) metric graph G ψ * specified by ψ * . The translated formula tr(n, E * , µ * , φ) represents the evaluation of the semantics of φ on the metric graph G ψ * according to the rules defined in Table

3

.

It must be therefore satisfiable as well, as initially ψ * ∧ φ is satisfiable. (2 ⇒ 1)

Table 7 .

 7 Translation rules for Theorem 2 tr1(||s T (t1, ..., tm)||)

the derivative ċ exists and is continuous on [0, 1]

the instantaneous speed | ċ|, that is, the Euclidean norm of the derivative is constant

except if needed for encoding the length of segment types