Satyajit Das

Kevin J M Martin

Philippe Coussy

Davide Rossi

Luca Benini

Efficient Mapping of CDFG onto Coarse-Grained Reconfigurable Array Architectures

In the approaching era of IoT, flexible and low power accelerators have become essential to meet aggressive energy efficiency targets. During the last few decades, Coarse Grain Reconfigurable Arrays (CGRA) have demonstrated high energy efficiency as accelerators, especially for high-performance streaming applications. While existing CGRAs mostly rely on partial and full predication techniques to support conditional branches, inefficient architecture and mapping support for handling control flow limits the use of CGRAs in accelerating either only inner loop bodies, or transformed loops specifically adapted to the target CGRA. This paper proposes a novel CGRA architecture with support for jump and conditional jump instructions and a lightweight global synchronization mechanism to enable complete Control Data Flow Graph (CDFG) mapping in an ultra-lowpower environment. The architecture is coupled with a complete design flow that efficiently maps applications with heavy control flow starting from a generic C language description. The proposed mapping approach reduces the impact of wasteful instruction issues in the conventional approaches of predication providing an average energy improvement of 1.44x and 1.6x when compared to the state of the art partial and full predication techniques. Moreover, the proposed method achieves an average speed-up up to 21x and an energy improvement up to 50.42x while executing applications with heavy control flow with respect to sequential execution on a low-power embedded CPU, demonstrating its suitability for next generation IoT applications.

I. INTRODUCTION

During the last few decades, CGRA architectures have been mainly proposed for accelerating high-performance compute intensive and applications providing significant energy efficiency boost with respect to general-purpose processors. CGRAs are indeed an interesting trade-off between Field Programmable Gate Arrays (FPGAs) and many-core architectures thanks to their capability to exploit spatial computation typical of hardwired accelerators while maintaining high-level programmability typical of general-purpose processors [START_REF] Taylor | Is dark silicon useful? harnessing the four horsemen of the coming dark silicon apocalypse[END_REF]. However, in most state of the art models, CGRAs are coupled to a general purpose processor, where the processor executes the control parts and delegates data-flow parts to the CGRA [START_REF] Bouwens | Architectural exploration of the adres coarse-grained reconfigurable array[END_REF][START_REF] Singh | Morphosys: an integrated reconfigurable system for data-parallel and computationintensive applications[END_REF], precisely inner loop part. Hence, the success of such a partitioning is limited to applications where the execution time in the CGRA plus the communication overhead is less than the execution time on the processor only. This approach has demonstrated effectiveness in high performance environments, but it is much more challenging for deeply embedded applications where relatively small datasets do not allow CGRAs to fully exploit their streaming capabilities. Moreover, existing CGRAs mostly rely on partial and full predication techniques to support conditional branches [START_REF] Han | Power-efficient predication techniques for acceleration of control flow execution on cgra[END_REF] [START_REF] Han | Acceleration of control flow on cgra using advanced predicated execution[END_REF]. Although these techniques have be proven to be extremely effective for high-performance applications, as they can efficiently expose parallelism hence leading to faster execution, they also lead to a waste of resources and redundant instruction fetches, not suitable for a low-power environment where the primarily target is energy efficiency. This paper proposes a framework to execute full control flow on CGRAs in an ultra-low-power (ULP) environment, completely releasing the host processor from performing loops control. This solution addresses standalone execution of all the levels of the loops, who is capable of mapping both loops and conditionals, and gives great flexibility to accommodate full application mapping on the CGRA. To enable lightweight support for control flow in CGRAs, we propose a novel CGRA architecture capable of executing jump and conditional jump instructions, and capable of synchronizing processing elements after executing jump or conditional jump. This approach also eases power management of unused tiles of the CGRA, that can be clock gated and power managed when waiting on global synchronization barriers, avoiding unnecessary waste of energy. When compared to state of the art methods to handle conditionals in CGRAs, namely partial and full predication, the proposed approach provides an average energy improvement of 1.44x and 1.6x, respectively, when executing a wide set of signal processing applications. When compared to a low-power OpenRISC CPU [START_REF] Lampret | Openrisc 1000 architecture manual. Description of assembler mnemonics and other for OR1200[END_REF], a 4x4 CGRA architecture implemented in 28nm UTBB FD-SOI [START_REF] Magarshack | Utbb fd-soi: A process/design symbiosis for breakthrough energy-efficiency[END_REF] technology achieves 100 MHz of operating frequency and power density of 1.78 µW/MHz at 0.6V, compared to 45 MHz and 3.54 µW/MHz achieved by the CPU, with an area overhead of 2.5x. When executing a wide range of signal processing applications our results show that the proposed CGRA architecture, along with the mapping approach, achieves an average speed-up of 21x, 4.8x and 4.8x with respect to a low power CPU, with -O0, -O2, -O3 optimization options, respectively, leading to a peak energy improvement of 50.42x.

The paper is organized as follows. The next section discusses the background and related work. Section 3 presents the context and contribution of this paper. Subsequently the mapping method is described in section 4. Section 5 elaborates on the need for hardware support to handle full control flow of an application and also presents the CGRA architecture to support mapping of CDFG. In section 6 experimental set-up is presented and results are discussed. Finally the paper concludes in section 7.

II. BACKGROUND

Several solutions have been proposed to map large applications with control flow onto CGRAs. The most commonly employed solution is to couple the CGRA with a host processor. Loosely coupled CGRAs like MorphoSys [START_REF] Singh | Morphosys: an integrated reconfigurable system for data-parallel and computationintensive applications[END_REF] or FLORA [START_REF] Lee | Flora: Coarse-grained reconfigurable architecture with floating-point operation capability[END_REF] employ shared registers or a special bus to connect the CPU to the CGRA. In Morphosys a tiny RISC processor, a fixed 8×8 16-bit Processing Element (PE) array, a data cache and DMA controller are linked together. The RISC processor handles control flow code, while the PE array accelerates data flow. ADRES [START_REF] Bouwens | Architectural exploration of the adres coarse-grained reconfigurable array[END_REF] defines a template which allows application optimization, using two modes of operation (VLIW mode and CGRA mode) in mutually exclusive manner. VLIW mode handles the outer loops and CGRA mode concentrates on executing inner loop part. ADRES implements predicated operations for inner loop control flow.

Partial predication [START_REF] Han | Power-efficient predication techniques for acceleration of control flow execution on cgra[END_REF] maps instructions of both if-part and else-part on different PEs. If both the if-part and the else-part update the same variable, the final result is computed by selecting the output from the path that must have been executed based on the evaluation of the branch condition. Full predication [START_REF] Han | Acceleration of control flow on cgra using advanced predicated execution[END_REF] addresses the loss of performance due to the execution of both paths and the select operations. It does not require a select operation, instead, the operations that update the same variable are mapped to the same PE but at different times. The correct value of the output will be present in the PE after the maximum time. Since operations from one of the paths are executed at runtime and operations of the other path are squashed, the performance of full predication is degraded. Since the PE fetches the instructions on an unnecessary path, the condition can be checked only after fetching.

An upgrade of full predication was proposed in [START_REF] Han | State-based full predication for low power coarsegrained reconfigurable architecture[END_REF]. This scheme prevents the wasted instruction issues from false conditional path by introducing sleep and awake mechanisms, but it does not improve performance in terms of latency. Dual issue scheme in CGRA [START_REF] Han | Power-efficient predication techniques for acceleration of control flow execution on cgra[END_REF] improves the latency by issuing two instructions to a PE simultaneously, one from the if-path, another from the else-path. But this proposition is too restrictive, as far as imbalanced conditionals are concerned. All the approaches mentioned in this section do not map the outer loops of a nested loop application. Rather they focus on innermost loop only.

This paper implements all the conditionals efficiently inside the CGRA, improving energy consumption, whereas low power CGRA like [START_REF] Ozaki | Cool mega-arrays: Ultralow-power reconfigurable accelerator chips[END_REF] only focuses on DFG mapping. HPC Machines like RHyMe [START_REF] Das | Rhyme: Redefine hyper cell multicore for accelerating hpc kernels[END_REF], ReN É [START_REF] Madhu | Flexible resource allocation and management for application graphs on ren É mpsoc[END_REF] can execute loops independently. These architectures are based on REDEFINE [START_REF] Alle | Redefine: Runtime reconfigurable polymorphic asic[END_REF] CGRA, which consists of a set of reconfigurable data-paths called HyperCells interconnected through a network-on-chip (NoC). While the data flow in these architectures rely on power hungry communication through switched network and NoC, the architecture proposed in this paper uses simple point to point data communication. Also the proposed CGRA architecture supports automated global synchronization of processing elements (PE) to orchestrate kernel execution. This makes it suitable for the ultra low power environment, as shown in the experiments.

III. CONTEXT AND CONTRIBUTION

This paper focuses on mapping complete applications (including control structures) onto a CGRA. The high level abstraction of the application is directly taken as an input in the form of a CDFG. The other input is the CGRA model where the CDFG has to be mapped on. Formally, a CDFG is represented as G = (V, E) where V is the set of basic blocks and E ⊆ V × V is the set of directed edges representing control flow. A Basic Block (BB) is represented as a data flow graph (DFG) or BB = (D, O, A) where D is the set of data nodes, O is the set of operation nodes and A is the set of arcs representing data dependencies. A basic block is a sequence of consecutive statements in which flow of control enters at the beginning and leaves at the end of basic block. The control flow at the end of basic block is supported with jump (jmp) and conditional jump (cjmp) instructions. Considering the execution flow of the above mentioned CDFG:

BB 1 → BB 2 → (either BB 3 or BB 8) if BB 3 → BB 4 → (either BB 5 or BB 6) → BB 7 → BB 2 • • • in CGRA,
it becomes imperative to synchronize all the tiles to the execution of the same basic block. When the execution flow jumps from one basic block to another, all the tiles in CGRA must be synchronized to the current basic block execution. This is necessary as all the tiles can be used concurrently or sequentially to execute a single basic block. Hence, several basic block can use same PE in different time.

Table I presents a theoretical study of the efficiency of this synchronization based approach over partial and full predication. Here we have considered a conditional that has n operations in each path. All the n outputs of n operations from each path will be used in the rest of the program. Hence, partial predication needs to execute 3n instruction (2n from both the paths and n select instructions). Full predication requires to fetch all the 2n instructions, but it can squash execution of n instructions from the false path depending on the predicate value. The proposed approach in one hand reduces the wasteful execution of the partial predication and instruction fetches in the full predication, decreasing overall energy consumption while executing kernels. The results show that the proposed approach achieves an average of 1.44× and 1.6× energy improvement over partial and full predication.

In summary the contributions of this work are: (a) A mapping support for full control flow of an application onto the CGRA. (b) A novel CGRA architecture to support execution of CDFGs, which is implemented using STMicroelectronics UTBB FD-SOI 28nm technology. (c) The efficiency of control flow execution over cpu performance. We show that, we are able to execute CDFGs with much more parallelism than a single cpu, leading to significant speed-up and energy efficiency boost, even with very moderate assumptions on the available bandwidth to memory. In addition, the area overhead of CGRA with different dimensions is given with respect to a cpu. (d) The energy improvement for execution of several kernels using the proposed mapping approach, compared to the state of the art mechanisms to handle control flow.

IV. PROPOSED METHOD

A. Problem formulation

As the basic blocks in a CDFG are represented as DFGs, any of the known DFG mapping onto CGRA [START_REF] Hamzeh | Regimap: Register-aware application mapping on coarse-grained reconfigurable architectures (cgras)[END_REF][START_REF] Peyret | An automated design approach to map applications on cgras[END_REF][START_REF] Chen | Graph minor approach for application mapping on cgras[END_REF][START_REF] Kim | Fast modulo scheduler utilizing patternized routes for coarse-grained reconfigurable architectures[END_REF] can be applied to map the basic blocks. Mapping of the basic blocks is done independently, since execution of basic blocks are mutually exclusive. So each basic block can use the maximum available resources, increasing the flexibility of the mapping. Problem arises for the variables which are used in several basic blocks. As an instance, variable c in the CDFG (Fig. 1) is used as result in BB 3 and as operand, in BB 4, BB 5 and BB 6. So the same register allocation must be used in BB 4, BB 5 and BB 6 where c was written in BB 3. The same goes for X1, X2, X3, X4, X5, i, a and b. These variables will be referred to as symbol variables in this paper. Allocated registers for these variables will be denoted with an overline, as variable name. In our sample program m, n are the input arrays and p is the output array. The inputs and outputs are dealt with normal load and store operations in CGRA.

Another problem arises while ordering the basic blocks for mapping, i.e. traversing the CDFG. To illustrate this problem let's consider a scenario, scenario 1 where BB 6 is mapped first, BB 3 is mapped next and so on. When mapping BB 6, variables c and X5 are placed at c and X5. When mapping BB 3, c and X5 which are already mapped in BB 6, must be considered because c will be used to map c in BB 3. In other words, the placement of the variables in the memory elements must be respected. Also a, b, X1 and X2 must not reuse X5. Otherwise, X5 will have wrong value when executing BB 6. Let's consider scenario 2 with another order, like first BB 3 and then BB 6 and so on, then it is necessary to pass c and X5 from BB 3 to BB 6 mapping. To keep c and X5 alive in BB 6, c and X5 both must be used in mapping of BB 6. The placement or binding information which are passed from the mapping of one basic block to mapping of the other basic block is referred as constraints (e.g. scenario 1: c and X5 passed from BB 6 to BB 3). There are two kinds of constraints. Constraints related to data that are used within a basic block mapping phase (e.g. scenario 1: c in BB 3 mapping) are called as target location constraints. Some of the data related to the constraints may not be used in the basic blocks but the constraints must be respected in the mapping of basic blocks. In order to keep these variables alive it is necessary to reserve the memory elements. Hence, while mapping the basic block, these resources must not override (e.g. scenario 1: X5 in BB 3 mapping). These are called reserved location constraints. If the number of reserved location constraints is high, mapping a basic block becomes more complex. The number of reserved location constraints varies with the traversal of the CDFG. The effect becomes more prominent for larger applications with large number of data, larger number of basic blocks and complex control flow. Hence, an appropriate traversal is necessary to map the full CDFG efficiently.

The basic solution to deal with the symbol variables is to load and store the variables when necessary. The symbol variables will be stored where they are used as results and will be loaded when used as operands. This basic solution reduces the complexity of the mapping as there is no constraints in the basic block mapping. On the other hand it requires a huge memory bandwidth, significantly reducing the energy efficiency of the system. In the rest of the paper this basic solution is referred to as systematic load-store based approach.

B. Proposed approach

The proposed solution is named as register allocation based approach. The idea is to map the symbol variables in the register file of the processing element (PE). The symbol variables will be written in register file, where they are used as results and be retrieved from the registers where used as operands. In this approach, the effects of constraints in mapping are inevitable. Reserved location constraints restrict the use of some resources. Target location constraints force to reuse some resources. If there is only a single target location constraint in a basic block mapping, it becomes easier to start mapping from the known place. But as a matter of fact situations often arise where there appear several target location constraints while mapping a basic block. Forced placements by these constraints induce extra routing effort. To illustrate this, lets consider a scenario where BB 1 and BB 4 in Fig. 1 are already mapped (variables X1, X2, X3, X4, X5, c, i already mapped). The mapping of BB 3 must be done with target location constraints c, X1 and X2 and reserved location constrains X5, X3, X4 and i . a and b will be mapped in the respective PEs where X1 and X2 are allocated. Extra routing effort may be necessary to bring a and b to the PE where c is allocated. The mapping can be done because the addition operation attached to c must produce it in c which is a register in the register file (RF) of the corresponding PE. A graphical view of this issue is presented in Fig. 2, where BB 3 is being mapped onto a 3 × 1 CGRA with 4 registers in the RFs of each PE (R0 is the output register, see Fig. 4). In this CGRA, we consider the register files are local to the PEs. Connection between PEs are from output register (R0) to the inputs of neighbouring PE.

Fig. 2. Extra routing due to constraints in DFG mapping

As we can see in Fig. 2, execution starts with the target location constraints c (P E3 -R2), X1 (P E1 -R1) and X2 (P E2 -R3), and the reserved location constraints X3 (P E2 -R2), X4 (P E1 -R4), X5 (P E3 -R4) and i (P E3 -R1). The target location constraints force to map a, b in P E1 and P E2. Let's say they are mapped in P E1 -R2 and P E2 -R1, as they will be produced in cycle 1. In cycle 2, a and b can not be accessed to produce c. That is why extra routing is necessary to map the operation attached to c. The routing of a, b from the register file to the output registers is done in cycle 2 and in the next cycle c is generated in c which is (P E3 -R2). Hence, mapping of the operation attached to c in this case, will experience longer schedule due to the constraints.

As mentioned earlier CDFG traversal has an impact on the number of reserved location constraints during the basic block mapping. Hence, it is necessary to select the basic blocks wisely for mapping. Four traversal strategies have been studied: 1) Forward breadth first traversal, 2) backward breadth first traversal, 3) depth first traversal and 4) random traversal. It appears that forward breadth first traversal induces the least number of reserved location constraints in the mapping of basic blocks 1 . Due to the data-flow between the basic blocks, generated symbol variables are most likely to be used in the successor basic blocks. In the forward breadth first traversal, the basic blocks with a greater number of symbol nodes are mapped earlier which also helps to reduce the number of target location constraints. More precisely the modified forward breadth first traversal is used to order the basic blocks while mapping. Fig. 3 shows the full compilation flow. The compiler takes application C code and the CGRA model as inputs. The C 1 the comparaison results are not given due to space limitation code is compiled to produce a CDFG. Each basic block in this CDFG is then mapped following the modified forward breadth first manner. At last the compiler produces the binary for each PE. As the mapping depends on control flow, CGRA which is being targeted by this approach must support two additional instructions jmp and cjmp. Every processing element in the CGRA executes the same jmp or cjmp instruction after execution of corresponding basic block, to synchronize to the next basic block execution. Every basic block has a starting address which is referred in jmp or cjmp instruction. Each processing element (PE) has its own instruction memory (IM), so that different instructions can be stored at the same address of each IM. Therefore, each PE can operate differently according to the instructions stored in the local IM. This makes it possible to achieve Multiple Instruction Stream, Multiple Data Stream (MIMD) operation in the processor array. The PEs are organized as an array using a mesh torus topology (Fig. 4), giving the opportunity to connect directly to four neighbouring PEs. A. Architecture of PE Fig. 5 shows the system level architecture of a PE. The internal blocks are explained as follows. Input mux: Two input muxes are there for selecting two operands (OpA and OpB). The sources are the neighbouring PEs and the register file. 32bits ALU+multiplier (16x16 bits) executes arithmetic and logical operations. The shifter performs shift operation on OpA by OpB bits. Load store unit (LSU) is optional for the PEs. Controller is responsible for selecting the address of next instruction to be executed. For the CGRAs coupled with host, this unit has to carry extra burden of managing stalls. Regular Register File (RRF) and Output Register (OR) are used to store temporary variables. Constant register file (CRF) is dedicated to store constants. Cond Register is one bit register, which contains 0 for all the normal operations and true conditions. The value is set to 1 on false condition. The boolean OR of all the control bits from all the PEs gives the indication that one PE has executed false condition. Consequently in the next cycle, offset address of the basic block from false path is fetched. Jump Register contains the address to be jumped. Instruction Memory holds 32, 20-bits instruction.

VI. EXPERIMENTS & RESULTS

A. Experimental setup

The proposed mapping flow has been fully automated through a software tool implemented by using Java and Eclipse Modeling Framework (EMF). GCC 4.8 is used to generate CD-FGs from applications described in C language. A cycle accurate model of the CGRA architecture presented in this paper has been developed in C++. The binary generated by the CGRA compiler is fed into this simulation model. The latency of all operations in CGRA is assumed one cycle, without loss of generality. Load and store operations requires two CGRA operations, one for address bus transaction and the other for data bus transaction. Firstly, the (a) proposed register allocation based approach and the (b) basic solution systematic load store based approach are compared with the performance of a CPU in terms of number of cycles. The low-power cpu chosen is a Or1K [START_REF] Lampret | Openrisc 1000 architecture manual. Description of assembler mnemonics and other for OR1200[END_REF]. The results are obtained with OVPsim [START_REF] Ovp | Open virtual platform[END_REF]. The binary is obtained with the toolchain provided by OVPsim. The simulator is instruction-accurate, and we assume one cycle per instruction to be in line with one cycle per operation in the CGRA. The performance comparison of standalone execution in CGRA and CPU, is done for -O0, -O1, -O2 and -O3 optimizations for CPU. Secondly, we compare area and energy consumption of the post synthesis implementation of CGRA with that of CPU in STMicroelectronics 28nm UTBB FD-SOI technology. They were synthesized using Synopsys design compiler, and Synopsys PrimePower was used for Fig. 6. Performance of proposed mapping approach in a CGRA with infinite band-width power analysis. Table II refers the area of the information including 1kB of instruction memory for the CPU and 32 20-bit words of instruction memory per tile for CGRA. We performed timing analysis and power analysis at 0.6V supply voltage at the temperature of 25 • C. In this operating point, the processor can achieve 45 MHz, with a power density of 3.54 µW/MHz, while a 4x4 CGRA achieves 100 MHz and a power density of 1.78 µW/MHz thanks to the much simpler structure of the tiles architecture with respect to a CPU.

B. Results

We have carried out a first set of experiments on the two approaches presented in this work: (a) systematic load store and (b) register allocation. We have first considered a 4x4 CGRA with "infinite bandwidth". Each PE in this case has a LSU and the number of load store per cycle is not limited, since this represents the theoretical worst case for the register allocation approach and the best case for the systematic load store approach we want to compare with. Fig. 6 shows the performance of the proposed register based approach and the basic load-store based approach normalized to cpu execution, for different optimization options. For all the cases, register based mapping approach achieves best performances. Systematic load store based approach sometimes (for matrix multiplication and masque) performed even worse than cpu.

Fig. 6 sums up the performance gain for different applications. The speed-up decreases with the compilation option as very aggressive compilation optimizations on loops are performed on the cpu with -03. Even if we do not implement such aggressive passes in our flow, still we are able to accelerate.

In Fig. 7, to show the effect of a more realistic number of load-store units on the mapping approaches we limit the number of load-store units to 4 (top row) [START_REF] Bouwens | Architectural exploration of the adres coarse-grained reconfigurable array[END_REF], and we compare the results with respect to a CPU. Systematic load-store based approach performs not up to the mark, whereas register based approach gets much less effected by the limit of aggregated bandwidth. The speed-up with respect to a general-purpose Fig. 7. Performance of proposed mapping approach in a CGRA with limited band-width processor decreases with the compilation option, due to strong CPU-dependent optimization passes performed by GCC. Table III presents energy consumption for several kernel execution in a 4x4 CGRA and a CPU, showing that the proposed approach outperforms the sequential execution on a CPU by up to 21x and 50.42x in terms of performance and energy efficiency, respectively. The results show that with the proposed approach we can execute CDFGs with much more parallelism than a single CPU, leading to significant speedup and energy efficiency boost, even with very moderate assumptions on the available bandwidth to memory. In addition, the area overhead with respect to a CPU is moderate, leading to higher silicon area efficiency (∼20x). When we compare the proposed approach with state of the art, full predication and partial predication approaches, we achieve an average of 1.44x and 1.6x energy improvement (Table IV), respectively. As we did not implement any power management techniques, the energy results include dynamic, static and clock tree power of the idle PEs for all the presented techniques. This demonstrates that even if theoretically, predication can expose more parallelism and leads to faster execution, in practice it leads to waste of resources and inefficiency compared to synchronized execution, making the latter more suitable for low-power, deeply embedded applications where the primary target is energy efficiency.

VII. CONCLUSION

Control flow in the applications is a significant bottleneck in CGRA architectures, avoiding to exploit their full potential. In this paper we have presented a CGRA architecture and mapping approach to implement full control flow onto a CGRA in an ultra-low-power environment. The proposed approach overcomes limitations and inefficiencies of state of the art predications methods, achieving 1.44x and 1.6x energy gain over par- tial and full predication techniques, respectively. The proposed approach also achieves a speed-up up to 21x and an energy improvement up to 50x with respect to an embedded CPU with an area overhead of 2.7x, demonstrating it suitability for next generation IoT applications.

Fig. 1

 1 Fig. 1. Sample program and corresponding CDFG

Fig. 3 .

 3 Fig. 3. The proposed mapping flow

Fig. 4 . 3 ×

 43 Fig. 4. 3 × 4 CGRA with mesh torus topology

Fig. 5 .

 5 Fig. 5. Design of processing element

TABLE III ENERGY

 III CONSUMPTION IN µJ, IN CPU AND CGRA

		Opt -O0	opt -O1	opt -O2	Opt -03
	kernels	CGRA CPU CGRA CPU CGRA CPU CGRA CPU
	FFT	0.021 5.016	0.021 0.589 0.018 0.582 0.018 0.582
	Convolution 1.256 14.493 0.556 2.632 0.556 2.184 0.556 2.183
	Non sep filter 6.373 269.817 5.275 36.713 2.061 31.89 2.061 32.158
	FIR	0.103 1.358	0.051 0.206 0.051 0.162 0.051 0.162
	Matrix mul 0.002 0.022	0.001 0.004 0.001 0.003 0.001 0.003
	Sep filter	5.083 166.419 4.318 24.129 1.932 21.179 1.931 21.179
	Masque5x5	0.003 0.01	0.001 0.002 0.001 0.002 0.001 0.002

TABLE IV ENERGY

 IV CONSUMPTION IN µJ FOR DIFFERENT APPROACHES

	kernels	Proposed approach Partial Pred Full Pred
	FFT	0.021	0.051	0.057
	Convolution	1.256	1.396	1.467
	Non sep filter	6.373	8.877	9.338
	FIR	0.103	0.13	0.136
	ManhDist	0.046	0.058	0.065
	Matrix mul	0.002	0.003	0.004
	Sep filter	5.083	6.542	7.349
	Masque5x5	0.003	0.003	0.004


Patricia Bouyer

Samy Jaziri

Nicolas Markey

Efficient timed diagnosis using automata with timed domains

We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed autmata, 2002].

Introduction

Formal methods in verification. Because of the wide range of applications of computer systems, and of their increasing complexity, the use of formal methods for checking their correct behaviours has become essential [START_REF] Henzinger | The embedded systems design challenge[END_REF][START_REF] Clarke | Model checking: algorithmic verification and debugging[END_REF]. Numerous approaches have been introduced and extensively studied over the last 40 years, and mature tools now exist and are used in practice. Most of these approaches rely on building mathematical models, such as automata and extensions thereof, in order to represent and reason about the behaviours of those systems; various algorithmic techniques are then applied in order to ensure correctness of those behaviours, such as model checking [START_REF] Clarke | Model checking[END_REF][START_REF] Clarke | Handbook of Model Checking[END_REF], deductive verification [START_REF] Antony | An axiomatic basis for computer programming[END_REF][START_REF] Filliâtre | Deductive software verification[END_REF] or testing [START_REF] Tretmans | Conformance testing with labelled transition systems: Implementation relations and test generation[END_REF].

Fault diagnosis. The techniques listed above mainly focus on assessing correctness of the set of all behaviours of the system, in an offline manner. This is usually very costly in terms of computation, and sometimes too strong a requirement. Runtime verification instead aims at checking properties of a running system [START_REF] Leucker | A brief account of runtime verification[END_REF]. Fault diagnosis is a prominent problem in runtime verification: it consists in (deciding the existence and) building a diagnoser, whose role is to monitor real executions of a (partially-observable) system, and decide online whether some property holds (e.g., whether some unobservable fault has occurred) [START_REF] Sampath | Failure diagnosis using discrete-event models[END_REF][START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF]. A diagnoser can usually be built (for finite-state models) by determinizing a model of the system, using the powerset construction; it will keep track of all possible states that can be reached after each (observable) step of the system, thereby computing whether a fault may or must have occurred.

The related problem of prediction, a.k.a. prognosis, (that e.g. no fault may occur in the next five steps) [START_REF] Genc | Predictability of event occurrences in partially-observed discrete-event systems[END_REF], is also of particular interest in runtime verification, and can be solved using similar techniques.

Verifying real-time systems. Real-time constraints often play an important role for modelling and specifying correctness of computer systems. Discrete models, such as finite-state automata, are not adequate to model such real-time constraints; timed automata [START_REF] Alur | A theory of timed automata[END_REF], developed at the end of the 1980's, provide a convenient framework for both representing and efficiently reasoning about computer systems subject to real-time constraints. Efficient offline verification techniques for timed automata have been developed and implemented [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF][START_REF] Behrmann | Uppaal 4.0[END_REF]. Diagnosis of timed automata however has received less attention; this problem is made difficult by the fact that timed automata can in general not be determinized [START_REF] Tripakis | Folk theorems on the determinization and minimization of timed automata[END_REF][START_REF] Finkel | Undecidable problems about timed automata[END_REF]. This has been circumvented by either restricting to classes of determinizable timed automata [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF], or by keeping track of all possible configurations of the automaton after a (finite) execution [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF]. The latter approach is computationally very expensive, as one step consists in maintaining the set of all configurations that can be reached by following (arbitrarily long) sequences of unobservable transitions; this limits the applicability of the approach.

Our contribution. In this paper, we (try to) make the approach of [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF] more efficiently applicable (over the class of one-clock timed automata). Our improvements are based on two ingredients: first, we use automata over timed domains [START_REF] Bouyer | On the determinization of timed systems[END_REF] as a model for representing the diagnoser. Automata over timed domains can be seen as an extension of timed automata with a (much) richer notion of time and clocks; these automata enjoy determinizability. The second ingredient is the notion of timed sets: timed sets are pairs (E, I) where E is any subset of R, and I is an interval with upper bound +∞; such a timed set represents a set of clock valuations evolving over time: the timed set (E; I) after a delay d represents the set (E + d) ∩ I. As we prove, timed sets can be used to finitely represent the evolution of the set of all reachable configurations after a finite execution.

In the end, our algorithm can compute a finite representation of the reachable configurations after a given execution, as well as all the configurations that can be reached from there after any delay. This can be used to very quickly update the set of current possible configurations (which would be expensive with the approach of [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF]). Besides diagnosis, this can also be used to efficiently predict the occurrence of faults occurring after some delay (which is not possible in [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF]). We implemented our technique in a prototype tool: as we report at the end of the paper, our approach requires heavy precomputation, but can then efficiently handle delay transitions.

Related works. Model-based diagnosis has been extensively studied in the community of discrete-event systems [START_REF] Sampath | Diagnosability of discrete-event systems[END_REF][START_REF] Sampath | Failure diagnosis using discrete-event models[END_REF]28]. This framework gave birth to a number of ramifications (e.g. active diagnosis [START_REF] Sampath | Active diagnosis of discrete-event systems[END_REF], fault prediction [START_REF] Genc | Predictability of event occurrences in partially-observed discrete-event systems[END_REF], opacity [START_REF] Lafortune | On the history of diagnosability and opacity in discrete event systems[END_REF]), and was applied in many different settings besides discrete-event systems (e.g. Petri nets, distributed systems [START_REF] Benveniste | Diagnosis of asynchronous discrete event systems: A net-unfolding approach[END_REF], stochastic systems [START_REF] Lunze | State observation and diagnosis of discreteevent systems described by stochastic automata[END_REF][START_REF] Bertrand | Foundation of diagnosis and predictability in probabilistic systems[END_REF], discrete-time systems [START_REF] Chen | Modeling and diagnosis of timed discrete event systems -a factory automation example[END_REF], hybrid systems [START_REF] Narasimhan | Model-based diagnosis of hybrid systems[END_REF]).

Much fewer papers have focused on continuous-time diagnosis: Tripakis proposed an algorithm for deciding diagnosability [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF]. Cassez developed a uniform approach for diagnosability of discrete and continuous time systems, as a reduction to Büchi-automata emptiness [START_REF] Cassez | A note on fault diagnosis algorithms[END_REF]. A construction of a diagnoser for timed systems is proposed in [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF]: the classical approach of determinizing using the powerset construction does not extend to timed automata, because timed automata cannot in general be determinized [START_REF] Tripakis | Folk theorems on the determinization and minimization of timed automata[END_REF][START_REF] Finkel | Undecidable problems about timed automata[END_REF]. Tripakis proposed the construction of a diagnoser as an online algorithm that keeps track of the possible states and zones the system can be in after each event (or after a sufficiently-long delay), which requires heavy computation at each step and is hardly usable in practice. Bouyer, Chevalier and D'Souza studied a restricted setting, only looking for diagnosers under the form of deterministic timed automata with limited resources [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF].

Definitions

Intervals

In this paper, we heavily use intervals, and especially unbounded ones. For r ∈ R, we define

→ r = [r; +∞) → r = (r; +∞) → r = (-∞; r) → r = (-∞; r]. We let R ≥0 = { → r, → r | r ∈ R ≥0 }
for the set of upward-closed intervals of R ≥0 ; in the sequel, elements of R ≥0 are denoted with r. Similarly, we let R ≥0 = { → r, → r | r ∈ R ≥0 }, and use notation r for intervals in R ≥0 . The elements of R ≥0 can be (totally) ordered using inclusion: we write r ≺ r whenever r ⊂ r (so that r < r entails → r ≺ → r ).

Timed automata

Let Σ be a finite alphabet.

Definition 1. A one-clock timed automaton over Σ is a tuple A = (S, {s 0 }, T, F ), where S is a finite set of states,

s 0 ∈ S is the initial state, T ⊆ S × R ≥0 × R ≥0 × (Σ { }) × {0, id} × S is the set of transitions, and F ⊆ S is a set of final states. A configuration of A is a pair (s, v) ∈ S × R ≥0 . There is a transition from (s, v) to (s , v ) if -either s = s and v ≥ v.
In that case, we write (s, v)

d -→ (s, v ), with d = v -v,
for such delay transitions (notice that we have no invariants); or there is a transition e = (s, l, u, a, r, s ) s.t. v ∈ l ∩ u and v = v if r = id, and v = 0 otherwise. For those action transitions, we write (s, v) → e (s , v ).

We assume that for each transition e = (s, l, u, a, r, s ), it holds l ∩ u = ∅.

Fix a one-clock timed automaton A; we write T id for the set of non-resetting transitions, i.e., having id as their fifth component, and T 0 for the complement set of resetting transitions.

For a transition e = (s, l, u, a, r, s ), we write e and e for l and u, respectively. We write src(e) = s and tgt(e) = s , and lab(e) = a ∈ Σ. We extend these definitions to sequences of transitions w = (e i ) 0≤i<n as src(w) = src(e 0 ), tgt(w) = tgt(e n-1 ), and lab(w) = (lab(e i )) 0≤i<n .

Let w be a sequence (e 2i+1 ) 0≤2i+1<n of transitions of T , and d ∈ R ≥0 . We write (s, v)

d -→ w (s , v ) if there exist finite sequences (s i , v i ) 0≤i≤n ∈ (S × R ≥0 ) n+1 and (d 2i ) 0≤2i<n ∈ R n/2 ≥0
such that 0≤2i<n d 2i = d, and (s 0 , v 0 ) = (s, v) and (s n , v n ) = (s , v ), and for all 0 ≤ j < n, (s j , v j )

dj -→ (s j+1 , v j+1 ) if j is even and (s j , v j ) → ej (s j+1 , v j+1 ) if j is odd. We write (s, v) → (s , v ) when (s, v) d -→ w (s , v ) for some w ∈ T * and some d ∈ R ≥0 .
For any λ ∈ Σ * and any d ∈ R ≥0 , we write (s, v) d -→ λ (s , v ) whenever there exists a sequence of transitions w such that λ = lab(w) and (s, v)

d -→ w (s , v ). Notice that 3 (s, v) d -→ ⊥ (s , v ) (sometimes simply written (s, v) d -→ (s , v )) indi- cates a delay-transition (hence it must be s = s ). The untimed language L(A) of A is the set of words λ ∈ Σ * such that (s 0 , 0) d -→ λ (s , v ) for some s ∈ F and d ∈ R ≥0 .
We borrow some of the formalism of [START_REF] Bouyer | On the determinization of timed systems[END_REF], in order to define a kind of powerset construction for timed automata. For a one-clock timed automaton A = (S, {s 0 }, T, F ) on Σ, we write M = (P(R ≥0 )) S for the set of markings, mapping states of A to sets of valuations for the unique clock of A. For a marking m ∈ M, we write supp(m) = {s ∈ S | m(s) = ∅}. For any l ∈ Σ, we define the function O l : M → M by letting, for any m ∈ M and any s ∈ S,

O l (m) : s → {v ∈ R ≥0 | ∃s ∈ S. ∃v ∈ m(s). (s, v) → l (s , v )}.
Similarly, for any d ∈ R ≥0 , we let

O d (m) : s → {v ∈ R ≥0 | ∃s ∈ S. ∃v ∈ m(s). (s, v) d -→ (s , v )}.
Notice that O d simply shifts all valuations by d.

Definition 2 ([7]

). The powerset automaton of a timed automaton A = (S, {s 0 }, T, F ) is a tuple DA = (P(S), {{s 0 }}, PT, PF ), where P(S) is the set of states, {s 0 } is the initial state, PT = {(q, m, a, q ) ∈ P(S) × M × Σ × P(S) | q = supp(m), q = supp(O a (m))} is the set of transitions, and PF = {E ∈ P(S) | E ∩ F = ∅} is a set of final states.

Configurations of DA are all pairs (q, m) ∈ P(S) × M for which q = supp(m). There is a transition from a configuration (q, m) to a configuration (q , m ) labelled with l ∈ Σ ∪ R ≥0 whenever m = O l (m). We extend this definition to sequences alternating delay-and action transitions, and write (q, m) d -→ w (q , m ) when there is a path from (q, m) to (q , m ) following the transitions of w in d time units. Similarly, we write (q, m)

d -→ σ (q , m ) if (q, m) d -→ w (q , m ) and lab(w) = σ.
Following [START_REF] Bouyer | On the determinization of timed systems[END_REF], the automaton DA is deterministic, and it simulates A in the sense that given two marking m and m and a word σ of Σ * , we have (supp(m), m)

d -→ σ (supp(m ), m ) if, and only if, m (s ) = {v ∈ R ≥0 | ∃s ∈ S. ∃v ∈ m(s). (s, v) d -→ σ (s , v )} for all s ∈ S.

Timed automata with silent transitions

The work reported in [START_REF] Bouyer | On the determinization of timed systems[END_REF] only focuses on the case when there are no silent transitions. In that case, for any d ∈ R ≥0 , the operation O d can be computed easily, since it amounts to adding d to each item of the marking (in other terms, for any marking m, any state s ∈ S, and any

v ∈ R ≥0 such that v + d ∈ R ≥0 , we have v ∈ m(s) if, and only if, v + d ∈ O d (m)(s))
. This leads to an efficient expression of a (deterministic) powerset automaton simulating A.

However fault diagnosis should deal with timed automata with unobservable transitions (unobservable transitions then correspond to internal transitions). So we now assume that Σ contains a special silent letter , whose occurrence is not visible. This requires changing the definition of lab: we now let

lab(⊥) = ⊥ lab(w • e) = lab(w) if lab(e) = lab(w • e) = lab(w) • lab(e) if lab(e) =
Notice that lab(w) ∈ (Σ \ { }) * . We may write → in place of → ⊥ , to stick to classical notations and make it clear that it allows silent transitions.

In that case, DA still is a (deterministic) powerset automaton that simulates A, and hence is still a diagnoser, but the function O d cannot be computed by just shifting valuations by d. In its raw form, the function O d can be obtained by the computation of the set of reachable configurations in a delay d by following silent transitions. This is analogous to the method proposed by Tripakis [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF], and turns out to be very costly. However, a diagnoser must be able to simulate all possible actions of the diagnosed automaton quickly enough, so that it can be used at runtime. In this paper, we introduce a new data structure called timed sets, which we use to represent markings in the timed powerset automaton; as we explain, using timed sets we can compute O d more efficiently (at the expense of more precomputations).

-3 -2 -1 0 1 2 3 4 5 r = 1 E F (0) = [1; 2] -3 -2 -1 0 1 2 3 4 5 E + 3 r = 1 F (3) = [1; 2] ∪ [3; 5]

(Regular) timed sets

Timed sets

For a set E and a real d, we define the set

E + d = {x + d | x ∈ E}.
We introduce timed sets as a way to represent sets of clock valuations (and eventually markings), and their evolution over time.

Definition 3. An atomic timed set is a pair (E; r) where E ⊆ R and r ∈ R ≥0 . With an atomic timed set F = (E; r), we associate a mapping F : R ≥0 → 2 R defined as

F (d) = (E + d) ∩ r.
We define the union of two timed sets F and F , denoted as F F , as their pointwise union:

(F F )(d) = F (d) ∪ F (d). Definition 4. A timed set is a countable set F = {F i | i ∈ I} (intended
to be a union, hence sometimes also denoted with i∈I F i ) of atomic timed sets. With such a timed set, we again associate a mapping F : R ≥0 → 2 R ≥0 defined as

F (d) = i∈I F i (d).
A timed set is finite when it is made of finitely many atomic timed sets. We write T (R) for the set of timed sets of R.

Given two timed sets F and F , we write F F whenever F (d) ⊆ F (d) for all d ∈ R ≥0 . This is a pre-order relation; it is not anti-symmetric as for instance

({1}; → 0) ({1}; → 1) and ({1}; → 1) ({1}; → 0). We write F ≡ F whenever F F and F F . Example 1. Figure 1 displays an example of an atomic timed set F = (E; → 1), with E = [-3; -1] ∪ [0; 2]. The picture displays the sets F (0) = [1; 2] and F (3) = [1; 2] ∪ [3; 5].

Regular timed sets

In order to effectively store and manipulate timed sets, we need to identify a class of timed sets that is expressive enough but whose timed sets have a finite representation.

Definition 5. A regular union of intervals is a 4-tuple E = (I, J, p, q) where I and J are finite unions of intervals of R with rational (or infinite) bounds, p ∈ Q ≥0 is the period, and q ∈ N is the offset. It is required that J ⊆ (-p; 0] and I ⊆ → (-q • p). The regular union of intervals E = (I, J, p, q) represents the set (which we still write

E) I ∪ +∞ k=q J -k • p.
Regular unions of intervals enjoy the following properties: Proposition 6. Let E and E be regular unions of intervals, K be an interval, and d ∈ Q. Then E ∪ E , E, E + d and E -K are regular unions of intervals.

Definition 7. A regular timed set is a finite timed set F = {(E i ; r i ) | i ∈ I}
such that for all i ∈ I, the set E i is a regular union of intervals.

Computing the powerset automaton

In this section, we fix a one-clock timed automaton A = (S, {s 0 }, T, F ) over alphabet Σ, assumed to contain a silent letter . We assume that some silent transitions are faulty, and we want to detect the occurrence of such faulty transitions based on the sequence of actions we can observe. Following [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF], this can be reduced to a state-estimation problem, even if it means duplicating some states of the model in order to keep track of the occurrence of a faulty transition. In the end, we aim at computing (a finite representation of) the powerset automaton DA, which amounts to computing the transition functions O l for any l ∈ Σ and O d for any d ∈ R ≥0 . Computing O l (m) for l ∈ Σ is not very involved: for each state s ∈ S and each transition e labelled with l with source s and target s , it suffices to intersect m(s) with the guard e ∩ e, and add the resulting interval (or the singleton {0} if e is a resetting transition) in O l (m)(s ).

From now on, we only focus on computing O d , for d ∈ R ≥0 . For this, it is sufficient to only consider silent transitions of A: we let U = U 0 U id be the subset of T containing all transitions labelled , partitioned into those transitions that reset clock x (in U 0 ), and those that do not (in U id ). We write A for the restriction of A to silent transitions, and only consider that automaton in the sequel. All transitions are silent in A , but for convenience, we assume that transitions are labelled with their name in A, so that the untimed language of A is the set of sequences of consecutive (silent) transitions firable from the initial configuration.

Linear timed markings and their -closure

We use markings to represent sets of configurations; in order to compute O d , we need to represent the evolution of markings over time. For this, we introduce timed markings. A timed marking is a mapping M : S → (R ≥0 → 2 R ≥0 ). For any s ∈ S and any d ∈ R ≥0 , M (s)(d) is intended to represent all clock valuations that can be obtained in s after a delay of d time units. For any delay d ∈ R, we may (abusively) write M (d) for the marking represented by M after delay d (so that for any s ∈ S and any d ∈ R ≥0 , both notations M (d)(s) and M (s)(d) represent the same subset of R).

A special case of timed marking are those timed markings that can be defined using timed sets; timed markings of this kind will be called linear timed markings in the sequel. As we prove below, linear timed markings are expressive enough to represent how markings evolve over time in one-clock timed automata. Atomic (resp. finite, regular) timed markings are linear timed markings whose values are atomic (resp. finite, regular) timed sets (we may omit to mention linearity in these cases to alleviate notations). Union, inclusion and equivalence of (timed) markings are defined statewise.

With any marking m, we associate a linear timed marking, which we write -→ m (or sometimes m if no ambiguity arises), defined as

- → m(s)(d) = {v+d | v ∈ m(s)}.
This timed marking is linear since it can be defined e.g. as -→ m(s) = (m(s); → 0). This timed marking can be used to represent all clock valuations that can be reached from marking m after any delay d ∈ R ≥0 .

Given a marking m, a delay d and a sequence w ∈ U * of silent transitions of A , we define the marking m ⊕ w d as follows: The definition is extended to timed markings as follows: for a timed marking M and a delay d, we let

m ⊕ w d : s → {v ∈ R ≥0 | ∃s ∈ S. ∃v ∈ m(s). (s, v) d -→ w (s , v )}
M ⊕ w d : s → {v ∈ R ≥0 | ∃s ∈ S. ∃d 0 ≤ d. ∃v ∈ M (d 0 )(s). (s, v) d-d0 ---→ w (s , v )},
Again, this gives rise to a timed marking M w : d → M ⊕ w d. Observe that for any linear timed marking, we have M ⊥ ≡ M . Notice also that for any marking m, it holds ( -→ m) w ≡ m w . We let M ⊕ d be the union of all M ⊕ w d when w ranges over U * , and M be the associated timed marking.

Definition 8. Let M be a timed marking. A timed marking N is an -closure of M if N ≡ M . The timed marking M is said -closed if it is an -closure of itself. s0 s1 x < 1; x ≥ 2; ; x := 0 -3 -2 -1 0 1 2 r = 0 -3 -2 -1 0 1 2 r = 0 Fig. 2. A silent timed automaton
Our aim in this section is to compute (a finite representation of) an -closure of any given initial marking (defined using regular unions of intervals).

Example 2. Consider the (silent) timed automaton of Fig. 2. The initial configuration can be represented by the timed marking M with M (s 0 ) = ([0; 0]; → 0) and M (s 1 ) = (∅; → 0), corresponding to the single configuration {(s 0 , x = 0)}. This timed marking is not closed under delay-and silent-transitions, as for instance configuration (s 1 , x = 0) is reachable; however, this configuration cannot be reached after any delay: it is only reachable after delay 0, or after a delay larger than or equal to 2 time units. In the end, an -closed timed marking for this automaton is M (s 0 ) = M (s 0 ), and M (s 1 ) = ((-∞; -2] ∪ [0; 0]; → 0).

Computing -closures

Let E and F be two subsets of R. We define their gauge as the set

E F = (E -F ) ∩ R ≤0 . Equivalently, E F = {d ∈ R ≤0 | F + d ∩ E = ∅}. Lemma 9. -If E ≤ F (in particular, if E ⊆ R ≤0 and F ⊆ R ≥0 ), then E F = E -F . -if E > F , then E F = ∅.
-If E and F are two intervals, then E F is an interval.

-IF E is a regular union of intervals and J is an interval, then E F is a regular union of intervals.

-

If F ⊆ R ≥0 , then (E F ) F = (E F ) -F .
We now define a mapping : T (R) × U * → T (R), intended to represent the timed set that is reached by performing sequences of silent transitions from some given timed set. We first consider atomic timed sets, and the application of a single silent transition. The definition is based on the type of the transition:

((E, r), (s, e, e, , op, s Finally, we extend this definition to unions of atomic timed sets by letting (F 1 F 2 , w) = (F 1 , w) (F 2 , w). We now prove that this indeed corresponds to applying silent-and delay-transitions from a given timed set.

)) =      (∅; → 0) if r ∩ e = ∅ (E ∩ e; p) if r ∩ e = ∅
Lemma 10. Let F be a timed set and w ∈ U * . Then for any d ∈ R ≥0 and any

v ∈ R ≥0 , v ∈ ( (F, w))(d) ⇔ ∃d 0 ∈ [0; d]. ∃v ∈ F (d 0 ). (src(w), v ) d-d0 ---→ w (tgt(w), v).
Proof. We carry the proof for the case where F is an atomic timed set. The extension to unions of atomic timed sets is straightforward. The proof for atomic timed sets is in two parts: we begin with proving the result for a single transition (the case where w = ⊥ is easy), and then proceed by induction to prove the full result.

We begin with the case where w is a single transition e = (s, e, e, , op, s ). In case F is empty, then also (F, e) is empty, and the result holds. We now assume that F is not empty, and consider three cases:

if r ∩ e = ∅, then (F, e) = (∅; → 0). On the other hand, for any d 0 and any v ∈ F (d 0 ), it holds v ∈ r, so that v / ∈ e, and the transition cannot be taken from that valuation. Hence both sides of the equivalence evaluate to false, and the equivalence holds. We now extend this result to sequences of transitions. The case where w = ⊥ is straightforward. Now assume that the result holds for some word w, and consider a word w • e. In case tgt(w) = src(e), the result is trivial.

The case of single transitions has been handled just above. We thus consider the case of w • e with w ∈ U + . First assume that v ∈ ( (F, w • e))(d), and let F = (F, w). Then v ∈ ( (F , e))(d), thus there exist 0 ≤ d 0 ≤ d and

v ∈ F (d 0 ) s.t. (src(e), v) d-d0 ---→ e (tgt(e), v ). Since v ∈ F (d 0 ), there must exist 0 ≤ d 1 ≤ d 0 and v ∈ F (d 1 ) such that (src(w), v ) d0-d1 ----→ w (tgt(w), v). We thus have found 0 ≤ d 1 ≤ d such that (src(w), v ) d-d1 ---→ w•e (tgt(e), v ). Conversely, if (src(w), v ) d-d1 ---→ w•e (tgt(e), v ) for some 0 ≤ d 1 ≤ d and v ∈ F (d 1 ), then we have (src(w), v ) d0-d1 ----→ w (tgt(w), v) d-d0
---→ e (tgt(e), v ) for some d 0 ∈ [d 1 ; d] and some v. We prove that v ∈ ( (F, w))(d 0 ): indeed, we have

d 1 ∈ [0; d 0 ], and v ∈ F (d 1 ) such that (src(w), v ) d0-d1 ----→ w (tgt(w), v), which by induction hypothesis entails v ∈ ( (F, w))(d 0 ). Thus we have d 0 ∈ [0; d] and v ∈ F (d 0 ), where F = (F, w), such that (tgt(w), v) d-d0
---→ e (tgt(e), v ), which means v ∈ (F , e)(d), and concludes the proof.

Thanks to this semantic characterization of (F, w), we get: Corollary 11. For any sequence w of transitions, and any two equivalent timed sets F and F , the timed sets (F, w) and (F , w) are equivalent. It follows that the closure of any marking can be represented as a linear timed marking. However, this linear timed marking is currently defined as an infinite union over all sequences of consecutive silent transitions. We make the computation more effective in the next section.

Finite representation of the closure

In this section, we prove that we can effectively compute a finite representation of the closure of any regular timed marking. More precisely, we show how to compute such a closure as a regular timed marking.

Finiteness. Indeed, let M be (a finite representation of) a regular timed marking: then M can be written as the finite union of atomic regular timed markings M (s,E, r) , defined as M (s,E, r) (s) = (E; r) and M (s,E, r) (s ) = (∅; → 0) for all s = s. In the end, any regular timed marking M can be written as the finite union i∈I M i of atomic regular timed markings. Thus we have (M ) ≡ i∈I (M i ), and it suffices to compute for atomic regular timed markings M (s,E, r) . We prove that those closures can be represented as regular timed markings.

We write 1 ((E; r), w) and 2 ((E; r), w) for the first and second components of ((E; r), w). Notice that 2 ((E; r), w) does not depend on E (so that we may denote it with 2 ( r, w) in the sequel). In particular,

-2 ((E; r), w) = → 0 if w ∈ U * × U 0 is a sequence of consecutive transitions ending with a resetting transition; -2 ((E; r), w) = r ∩ i<k e i if w = e 1 . . . e k ∈ U id
* is a sequence of consecutive non-resetting transitions.

Letting J r = { → 0, r} ∪ { e | e ∈ U id }, it follows that 2 ((E; r), w) ∈ J r . for any (E; r) and any w. Thus (M ) can be written as a finite union of atomic timed markings.

Regularity. To prove regularity, we first introduce some more formalism:

-we let G id = { e | e ∈ U id } and G id = { e | e ∈ U id }. We thus have J r = { → 0, r} ∪ G id ;
for r ∈ R ≥0 and e ∈ U , we write Φ( r, e) for the interval r ∩ e ∩ e; we define a mapping J r : U * → N J r ×U0 that counts the number of occurrences of certain timing constraints at resetting transitions along a path: precisely, it is defined inductively as follows (where represents addition of an element to a multiset):

J r (⊥) = {0} J r ×U0 J r (w • e) = J r (w) {( 2 ( r, w), e)} if e ∈ U 0 J r (w • e) = J r (w) if e ∈ U id .
By induction on w, we prove:

Lemma 14. Let (E; r) be a timed set with E ⊆ R ≤0 , and w ∈ U * . Then

1 ((E; r), w) = E - J=( g,e)∈J r J r (w)(J) × Φ( g, e) ⊆ R ≤0 .
Now, we fix an atomic regular timed marking M (s,E, r) . For any state s of A , we let L(s, s ) be the set of all sequences of consecutive transitions from s to s in A . Then (M (s,E, r) ) =

s ∈S (M (s,E, r) , L(s, s )).

Hence we need to prove that 1 (M (s,E, r) , L(s, s )) is regular.

For any set L of sequences of consecutive transitions, and for any r and r in R ≥0 , we let L r r = {w ∈ L | r = 2 ( r, w)}. One easily observes that for any r ∈ R ≥0 and any L, it holds L = r ∈J r L r r , so that

1 (M (s,E, r) , L(s, s )) = r ∈J r 1 (M (s,E, r) , [L(s, s )] r r ).
The following property entails that this set is a regular union of intervals:

Lemma 15. Let E be a regular union of intervals, r and r be two elements of R ≥0 , and L ⊆ L(A ) be a regular language. Then 1 (M (s,E, r) , L r r ) is a regular union of intervals.

Experimentations

In order to evaluate the possible improvement of our approach compared to the diagnoser proposed in [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF], we implemented and compared the performances of both approaches. Sources can be downloaded at http://www.lsv.fr/ ~jaziri/ DOTA.zip

Comparison of the approaches

In the approach of [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF], the set of possible current configurations is stored as a marking. If an action l occurs after some delay d, the diagnoser computes the set of all possible configurations reached after delay d (possibly following silent transitions), and applies from the resulting markings the set of all available transitions labelled l. This amounts to computing the functions O d and O l at each observation. There is also a timeout, which makes the diagnoser update the marking (with O d ) regularly if no action is observed. The computation of O d is heavily used, and has to be performed very efficiently so that the diagnoser can be used at runtime.

In our approach, we use timed markings to store sets of possible configurations. Given a timed marking, when an action l is observed after some delay d, we can easily compute the set of configurations reachable after delay d, and have to apply O l and recompute the -closure. Following [START_REF] Bouyer | On the determinization of timed systems[END_REF], O l can be performed as a series of set operations on intervals. The -closure can be performed as a series of subtractions between an interval and regular unions of intervals (see Lemma 14). Those regular unions can be precomputed; while this may require exponential time and space to compute and store, this makes the simulation of a delay transition very efficient.

Implementation

In our experimentations, in order to only evaluate the benefits of the precomputation and of the use of -closures in our approach compared to that of [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF], we use the same data structure for both diagnosers. In particular, both diagnosers are implemented as automata over timed domains [START_REF] Bouyer | On the determinization of timed systems[END_REF], where the timed domain is the set of timed markings. The only difference lies in the functions computing the action-and the delay transitions. As a consequence, both implementations benefit from the data structure we chose for representing timed intervals, which allows us to compute basic operations in linear time. Also, both structures use the same reachability graphs for either computing the sets of reachable configurations or the Parikh images.

Our implementation is written in Python3. One-clock timed automata and both diagnosers are instances of an abstract class of automata over timed markings; timed markings are implemented in a library TILib. Simulations of those automata are performed using an object called ATDRunner, which takes an automaton over timed markings and simulates its transitions according to the actions it observes on a given input channel. It may also write what it does on an output channel. A channel is basically a way of communicating with ATDRunners.

In order to diagnose a given one-clock timed automaton, stored in an object OTAutomata, we first generate a diagnoser object, either a DiagOTA or a TripakisDOTA, depending of which version we want to use. Then we launch two threads: one is an ATDRunner simulating the timed automaton, listening to some channel object Input, and writing every non-silent action it performs on some other channel object Comm. The other one is another ATDRunner simulating the diagnoser and listening to the Comm channel.

In a DiagOTA object, which corresponds to our approach, we have already precomputed the relevant timed intervals; action transitions are then made by operations over timed markings, and delay transitions are encoded by increasing a padding information on the timed markings, which is applied when performing the next action transition. In such a simulation, we can thus keep track of which states may have been reached, but also predict which states may be reached in the future and the exact time before we can reach them.

In a TripakisDOTA object, which corresponds to the approach of [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF], action and delay transitions are simulated by computing all configurations reachable through that action or delay, also allowing arbitrarily many silent transitions. This does not allow for prediction.

Results

Table 3 reports on the performances of both implementations on a small set of (randomly generated) examples. Those examples are given in Appendix B, and are distributed with our prototype. In Table 3, we give the important characteristics of each automaton (number of states and of silent transitions), the amount of precomputation time used by our approach, and the average time (over 400 random runs) used in the two approaches to simulate action-and delay transitions.

As could be expected, our approach outperforms the approach of [START_REF] Tripakis | Description and schedulability analysis of the software architecture of an automated vehicle control system[END_REF] on delay transitions by several orders of magnitude in all cases. The performances of both approaches are comparable when simulating action transitions.

The precomputation phase of our approach is intrinsically very expensive. In our examples, it takes from less than a second to more than 13 minutes, and it remains to be understood which factors make this precomputation phase more or less difficult. We may also refine our implementation of the computation of Parikh images, which is heavily used in the precomputation phase.

Conclusion and future works

In this paper, we presented a novel approach to fault diagnosis for one-clock timed automata; it builds on a kind of powerset construction for automata over timed domains, using our new formalism of timed sets to represent the evolution of the set of reachable configurations of the automaton. Our prototype implementation shows the feasibility of our approach on small examples.

There remains space for improvements in many directions: first, our implementation can probably be made more efficient on the precomputation phase, and at least we need to better understand why some very small examples are so hard to handle.

A natural continuation of this work is an extension to n-clock timed automata. This is not immediate, as it requires a kind of timed zone, and an adaptation of our operator . Another possible direction of research could target priced timed automata, with the aim of monitoring the cost of the execution in the worst case.

A Appendix

A.1 Proof of Proposition 6 Proposition 6. Let E and E be regular unions of intervals, K be an interval, and d ∈ Q. Then E ∪ E , E, E + d and E -K are regular unions of intervals.

Proof. Write E = (I, J, p, q) and E = (I , J , p , q ), so that

E = I ∪ +∞ k=q J -k • p E = I ∪ +∞ k=q J -k • p .
We can write p = a b and p = a b , with a, b, a and b in N. Let

N = min{n ∈ N | n • b • a ≥ q and n • b • a ≥ q }.
Then we can write

E =   I ∪ N •b•a -1 k=q J -k • p   ∪ +∞ k=N     b•a -1 r=0 J -r • p   -k • a • a   . and E =   I ∪ N •b •a-1 k=q J -k • p   ∪ +∞ k=N     b •a-1 r=0 J -r • p   -k • a • a   .
Since J ⊆ (-p; 0], we have We now prove the result for E: again writing E = I ∪ +∞ k=q J -k • p, thanks to the constraints imposed on I and J, we have

E = ( → (-q • p) \ I) ∪ +∞ k=q ((-p; 0] \ J) -k • p.
The proofs for E + d and E -K follow similar arguments.

A.2 Proof of Lemma 9

Lemma 9.

-

If E ≤ F (in particular, if E ⊆ R ≤0 and F ⊆ R ≥0 ), then E F = E -F . -if E > F , then E F = ∅.
-If E and F are two intervals, then E F is an interval.

Finite automaton for L r r . We assume that L is accepted by the automaton B = (S, {s}, U, {s }) obtained from A by imposing an initial state s and a single accepting state s ; this is enough for our purpose, and is easily generalized to any regular L ⊆ L(A ). We decorate all states with elements of R ≥0 in order to derive a finite automaton accepting L r r . More precisely, we consider the automaton B r r = (S × J r , (s, r), U , (s , r )) where U ={([q, g], e, e, ( g, e, → 0), 0, [q , → 0]) | e = (q, e, e, 0, , q ) ∈ U and g ∩ e = ∅} ∪ {([q, g], e, e, ( g, e, g ), id, [q , g ]) | e = (q, e, e, id, , q ) ∈ U and g ∩ e = ∅}.

This automaton accepts words in ( R ≥0 × U × R ≥0 ) * . Writing π U : R ≥0 × U × R ≥0 → U for the projection on the second element of this alphabet (and extending it to sequences in the natural way), it is easily observed that π U (L(B r r )) = L(B) r r .

Defining 1 (M (s,E, r) , [L(s, s )] r r ) as a regular union of intervals. We now focus on 1 (M (s,E, r) , [L(s, s )] r r ) = 1 ((E, r), [L(s, s )] r r ), which we write η for the sake of readability.

For any g ∈ J r = { → 0, r} ∪ G id and any g ∈ G id , we define

W id g, g = {w = ( g 1 , e 1 , g 1 ) • ( g 2 , e 2 , g 2 ) • • • ( g n , e n , g n ) | g n = g and min 1≤i≤n e i = g }.
We decompose [L(s, s )] r r as the union of

g ∈ G id [L(s, s )] r r ∩ W id r , g
(all runs that do not contain resetting transitions) and

g ∈ G id ( g,e)∈J r ×U0 [L(s, s )] r r ∩ W id g, g × {( g, e, → 0)} × (J r × U × J r ) *
where the right-hand side of the intersection contains all paths containing at least one resetting transition labelled ( g, e, → 0). Using this decomposition, we get η = g ∈ G id w∈[L(s,s )] r r ∩W id r , g 1 ((E, r), π U (w)) ∪ g ∈ G id ( g,e)∈J r ×U0 w∈[L(s,s )] r r ∩W id r , g ×{( g,e, → 0)}×(J r ×U ×J r ) * 1 ((E, r), π U (w))

In the first part, π U (w) contains only non-resetting transitions, so that we have 1 ((E, r), π U (w)) = E ∩ g . This is a finite union of regular intervals.

As for the second part, decomposing w ∈ W id r , g × {( g, e, → 0)} × (J r × U × J r ) * as u • ( g, e, → 0) • v, we have 1 ((E, r), π U (w)) = 1 ( ( ((E, r), π U (u)), e), π U (v)).

20

Since π U (u) contains non-resetting transitions, we have ((E, r), π U (u)) = E ∩ g ⊆ R ≤0 , and since e is a resetting transition, we get 1 ((E, r), π U (w)) = 1 (((E ∩ g ) Φ( g, e), → 0), π U (v)).

Hence it remains to prove that for all g ∈ G id , the set η =

( g,e)∈J r ×U0

1 ((E ∩ g ) Φ( g, e), → 0), π U (Q) ,

where Q = (W id g, g × {( g, e, → 0)})\[L(s, s )] r r is the left-quotient of [L(s, s )] r r by W id g, g × {( g, e, → 0)}, is a regular union of intervals. Write E e, g, g = (E ∩ g ) Φ( g, e) ⊆ R ≤0 . From Lemma 14, we derive We write Γ e, g, g for the second term, so that η = E e, g, g -Γ e, g, g . For 1 ≤ i ≤ c and 0 ≤ j ≤ d i , we let

K i j =
( n,e)∈J r ×U0 n ∈J r p i j ( n, e, n ) × Φ( n, e).

We now consider two cases:

first assume that for some i 0 and j 0 and some ( n 0 , e 0 ) ∈ J r × U 0 , it holds p i0 j0 ( n 0 , e 0 , → 0) > 0 and Φ( n 0 , e 0 ) has positive length. Let L n = K i0 0 + n • K i0 j0 for any n ∈ N. Then clearly L n ⊆ Γ e, g, g for all n. Moreover, by definition of i 0 and j 0 , the length of K i0 j0 is positive, so that the length of n • K i0 j0 tends to infinity. It follows that for some α ∈ R ≥0 , → α ⊆ n∈N L n ⊆ Γ e, g, g . Then Γ e, g, g ∩ → α ⊆ [0; α], and it has finite granularity, so that it is a finite union of intervals.

-We now assume that for all i and j and all ( n, e) ∈ J r ×U 0 , either p i j ( n, e, → 0) = 0, or Φ( n, e) has length 0. All Then for all 1 ≤ i ≤ n and 1 ≤ j ≤ d i , K i j is a finite union of punctual intervals, so that η is a regular union of intervals.

B Examples definition

Fig. 1 .

 1 Fig. 1. Example of an atomic timed set F = ([-3; -1] ∪ [0; 2]; → 1).

(

  remember that w here represents a sequence of silent transitions). This corresponds to all configurations reachable along w from a configuration in m with a delay of exactly d time units. By definition of the transition relation → w , for m ⊕ w d to be non-empty, w must be a sequence of consecutive transitions. With this definition, for any sequence w of silent transitions and any marking m, we can define a timed marking m w : d → m ⊕ w d. In particular, for the empty sequence ⊥, the timed marking m ⊥ is equivalent to the timed marking -→ m (hence it is linear). For any d ∈ R ≥0 , we define m ⊕ d as (m ⊕ d)(s) = w∈U * (m ⊕ w d)(s). The marking m ⊕ d represents the set of configurations that can be reached after a delay d through sequences of silent transitions. This gives rise to a timed marking, which we write m . By definition of O d , we have O d (m) = m (d) for any marking m and any delay d.

  and op = id (E ( p ∩ e); → 0) if r ∩ e = ∅ and op = 0 where p = r ∩ e. We extend to sequences of transitions inductively by letting ((E; r), ⊥) = (E; r) and, for w ∈ U + , ((E; r), w • e) = ( ((E; r), w), e) if tgt(w) = src(e)

-

  now assume that r ∩ e = ∅, and consider the case where e does not reset the clock. Then v ∈ ( (F, w))(d) means that v ∈ (E + d) ∩ ( e + d) ∩ p. If such a v exists, then p ∩ e ∩ [v -d; v] is non-empty: indeed, this is trivial if either v ∈ e, or v -d ∈ p, or d = 0; otherwise, we have e ⊆ → v and p ⊆ → v -d, so that p ∩ e ⊆ (v -d; v). Moreover, p ∩ e = ∅ since r ∩ e = ∅ and e ∩ e = ∅. Then for any v in that set p∩ e ∩ [v -d; v], letting d 0 = v -(v -d), we have v ∈ E + d 0 . In the end, v ∈ F (d 0 ), and v ∈ e ∩ e, so that (src(e), v ) d-d0 ---→ e (tgt(e), v). Conversely, if d 0 ∈ [0; d] and v ∈ F (d 0 ) exist such that (src(w), v ) d-d0 ---→ w (tgt(w), v), then v ∈ E + d 0 ∩ r, and for some d 1 ≤ d -d 0 , v + d 1 ∈ e ∩ e. Then letting v = v + d -d 0 , we have v ∈ E + d and v ∈ r + (d -d 0 ) ⊆r and v ∈ e + (d -d 0 -d 1 ) ⊆ e and v ∈ e + (d -d 0 -d1) ⊆ e + d. This proves our result for this case. we finally consider the case where r∩ e = ∅ and e resets the clock. In this case, v ∈ ( (F, w))(d) means that v ∈ → 0 and v -d ∈ E ( p ∩ e), which rewrites as 0 ≤ v ≤ d and (E +d-v)∩( p∩ e) = ∅. Let d 0 = d-v. The property above entails that 0 ≤ d 0 ≤ d, and that there exists some v ∈ (E + d 0 ) ∩ ( p ∩ e), so that 0 ≤ d 0 ≤ d, v ∈ F (d 0 ) and (src(e), v ) d-d0 ---→ e (tgt(e), v). Conversely, if those conditions hold, then for some 0 ≤ d 1 ≤ d -d 0 , we have v + d 1 ∈ e ∩ e, and v = d -(d 0 + d 1 ) (remember that e resets the clock). Then v + d 1 ∈ E + (d 0 + d 1 ) ∩ r ∩ e ∩ e, so that -(d 0 + d 1 ) ∈ E ( p ∩ e), and finally v ∈ (F, w)(d).

Finally, we extend

  to linear timed markings in the expected way: given a linear timed marking M , and a sequence w of transitions, we let(M, w) : s → (M (src(w)), w) if s = tgt(w), s → (∅; → 0) otherwise. Again, we have (M 1 M 2 , w) ≡ (M 1 , w) (M 2 ,w) for any w ∈ U * . Then: Lemma 12. (M, w) ≡ M w for all w ∈ U * and all linear timed marking M . Letting (M, L) = w∈L (M, w) for any subset L of U * , and (M ) = (M, U * ), we immediately get: Theorem 13. For any linear timed marking M , it holds (M ) ≡ M .

b•a - 1 r=0J

 1 -r • p ⊆ (-b • a • p; 0] = (a • a ; 0], and similarly for J . Taking the union of the equalities above, we get an expression of E ∪ E under the form I ∪ +∞ k=N (J -k • (a • a ), which proves that E ∪ E is a regular union of intervals.

1

  ((E e, g, g , → 0), π U (w)) = E e, g, g -J∈J r ×U0 J → 0 (π U (w))(J) × Φ(J). Hence η = w∈Q E e, g, g -J∈J r ×U0 J → 0 (π U (w))(J) × Φ(J) = E e, g, g -w∈Q J∈J r ×U0 J → 0 (π U (w))(J) × Φ(J)= E e, g, g -P ∈p(Q) ( n,e)∈J r ×U0 n ∈J r P ( n, e, n ) × Φ( n, e),where p(Q) is the set of Parikh vectors of Q (i.e., for each w ∈ Q, p(w) is the multiset of states visited along w, and p(Q) is the set of all those multisets). The latter equality is obtained by observing that J → 0 (π U (w))( n, e) is the number of occurrences of a state of the form ( n, e, n ) (for some n ) along w. Now, the set Q = (W id g, g × {( g, e, → 0)})\[L(s, s )] r r is regular, so that by Parikh's theorem, p(Q) is a semi-linear set; it can be written p(Q) = c i=1 (p i 0 + di j=1 p i j × N), where p i j ∈ N J r ×U0×J r for all 1 ≤ i ≤ c and 0 ≤ j ≤ d i . Then:η = E e, g, g -c i=1(n,e)∈J r ×U0 n ∈J r p i 0 ( n, e, n ) × Φ( n, e) + (nj ) 1≤j≤d i ∈N d i di k=1 ( n,e)∈J r ×U0 n ∈J r n k • p i j ( n, e, n ) × Φ( n, e)

B. 1 B

 1 Example2 # States. Size : 3 q0;q1;q2 # Transitions q0;[0,2];0;q0;a q0;[1,1];0;q1;a q1;[1,2];0;q1;a q1;[2,2];0;q2;a q2;[0,inf[;0;q0;a q0;]0,2];0;q0;b q0;[0,inf[;0;q1;b q1;]1,2];0;q0;b q1;[0,2[;0;q1;b q2;[0,0];0;q1;b q2;]0,1];0;q2;b q0;]2,inf[;0;q0;e q0;[1,2[;0;q1;e q0;[0,2[;1;q2;e q1;]0,2];0;q0;e q1;]2,inf[;0;q1;e q2;[1,1];0;q0;e

In this paper, we write ⊥ for the empty word (or empty sequences) over any alphabet.

Work supported by ERC project EQualIS.

-IF E is a regular union of intervals and J is an interval, then E F is a regular union of intervals.

-

Proof. The first three claims are trivial from the definition of E F . The fourth claim follows from Prop. 6. Finally, the last claim is a consequence of the first one (because E F ⊆ R ≤0 ).

A.3 Proof of Lemma 12

Lemma 12. (M, w) ≡ M w for all w ∈ U * and all linear timed marking M .

Proof. For d ∈ R ≥0 and s ∈ S, we have

---→ w (s, v)}. By Lemma 10, this corresponds to (M, w)(s)(d).

A.4 Proof of Lemma 14 Lemma 14. Let (E; r) be a timed set with E ⊆ R ≤0 , and w ∈ U * . Then

Proof. The proof is by induction on w. The result is straightforward for w = ⊥. Now, assume the result holds for some w ∈ U * , and consider w = w • e.

First, if e ∈ U id , then 1 ((E; r), w • e) = 1 ((E; r), w) ∩ e (by definition of ). Since 1 ((E; r), w) ⊆ R ≤0 ⊆ e, we have 1 ((E; r), w • e) = 1 ((E; r), w). Since J r (w • e) = J r (w) when e ∈ U id , our result follows.

For e ∈ U 0 , we have

This precisely corresponds to the effect of adding {( 2 ( r, e), e)} to the multiset J r (w).

A.5 Proof of Lemma 15

Lemma 15. Let E be a regular union of intervals, r and r be two elements of R ≥0 , and L ⊆ L(A ) be a regular language. Then 1 (M (s,E, r) , L r r ) is a regular union of intervals.

Proof. The proof of this result is in two parts: we first express L r r as the language of a finite automaton, and then-by a tedious proof-express 1 (M (s,E, r) , L r r ) as a regular union of intervals.