Asma Ben

Hadj Mohamed

Amal Baghdadi
email: amal.baghdadi@enis.rnu.tn

Thierry Val
email: thierry.val@univ-tlse2.fr

Laurent Andrieux
email: laurent.andrieux@univ-tlse2.fr

Abdennaceur Kachouri
email: abennaceur.kachouri@enis.rnu.tn

Edges detection in depth images for a gesture recognition application using a Kinect WSN

Keywords: Kinect;3D images, depth images, people edge detection, gestures recognition

The detection of persons in an image has been the subject of several studies. Most of these works were done on images taken by cameras in visible light (RGB). In this paper,we are interested in people contours detection on the Kinect3D images. We investigate the application of Gradient approach and optimal filters on depth images. We also use this detection to monitor the person via her gestures. Results show that edge detection of Canny is good for people in both light condition but, the performance of Sobel algorithm was better for the images taken in the dark depths.

Introduction

Images acquisition and processing are taking significant growth especially in the evolution of technologies and the audio-visual communications tools in the last years.Recognition and identification in digital images constitutes an important part which does not lack importance in this field. However, the processing of these images is not as easy as in 2D. Indeed these are less complex since each pixel has a level of color (RGB or gray level), while a pixel in a depth image has the coordinates in space of an object in the scene being shot.

The detection of persons in an image has been the subject of several studies [START_REF] Ben Hadj Mohamed | Assisting people with disabilities through Kinect Sensors into a smart house[END_REF] [START_REF] Ben Hadj Mohamed | Using a Kinect WSN for home monitoring : principle, network and application evaluation[END_REF]. Most of these works were done on images taken by cameras RGB [START_REF] Baghdadi | Image Processing depth from the Kinect[END_REF]. Methods of detection and recognition generally used to imitate the same detection process as humans [START_REF] Evans | A morphological gradient approach to color edge detection[END_REF]. They use features based on gradients or determine interest points of the image. The purpose of edge detection is to identify the points of a digital image correspond to abrupt changes in light intensity. These changes in image properties generally reflect significant events or changes in the properties of the world. These include discontinuities in depth, in the orientation of a surface, the material properties and the lighting of a scene.

The new technology of intelligent video sensors has generated depth images with the advantage of capturing in different environments where light conditions are poor or ambiguous [START_REF] Demigny | On optimal linear filtering for edge detection[END_REF]. Processing 3D images invades many fields such as, industry, military and security applications, mobile technology, video games etc.

In this paper we are interested in processing 3D images to detect person's edges using some approaches and monitoring the person detected as well as recognizing her gestures. Actually, this work is part of a medical application of monitoringpeople with disabilities into their own homes [6] [7]. Indeed, it allows them to control their environments (state of the lights, air conditioning, opening and closing doors etc) via gestures recognition. We use Matlab to extract the depth of images and to perform transformations at these digital images. The data acquisition system which we used is the Kinect sensor. In fact, it is an intelligent video sensor made by PrimeSense company semiconductor fables.This device is originally designed for the Microsoft console 360 which aims to control the video game controller without using joystick [START_REF] Webb | Beginning Kinect programming with the microsoftKinect SDK[END_REF].It consists of horizontal bar connected to the base via a small motor. This allows the camera to perform small up and down movements in order to adapt the perception of the camera depending on the position in the room. The horizontal bar is the main element of the Kinect technology. It contains a series of multi-microphones,an RGB camera, and finally a 3D depthsensor which is the main interesting element in this subject (Figure1). Thus, the device can not only detect the color through the video camera, but also the depth of the data. Thanks to the infrared projector which projects a pattern into the entire room. The sensor collects at first the infrared image obtained. Thanks to the IR projector, the Kinect can work on darkness. Then, it analyses the deformation of the patterns using a highly parallel SOC called "PS1080" and finally infers a depth map of the image. This technical is called "light coding" is specification of the Kinect [START_REF] Papin | Comparative Analysis for images processing d'algorithmes[END_REF]. Therefore, the device transmits to the computer the frames containing the depth map, the color map and an audio streamall synchronized and whose size are VGA and with an average rate of 30 frames per second. These features make the Kinect available in many applications such as robotic, industry, etc [10]. In this paper, we will talk at a first time about the construction of 3D mesh with this sensor. In a second time, we willinvestigate the application of several filters and approach to edge detection in these images in aim to detect human body edges and finally we will represent how to monitor this person through her gestures.

People detection in depth images

Construction of 3D mesh in Kinect

The infrared camera provides an image representing the thermal releases emitted by the observed object (Figure 2). This type of image was widely popularized by legendary movie Predator and infrared vision. However, the resulting images are not colored; it is the users who decide to add color levels based on the measured temperature. The IR or depth camera has a field of view just like any other camera. The field of view of Kinect is limited as illustrated in Figure 3. The view angles are 57 degrees horizontal and 43 vertical and the depth map returned by the Kinect associated with each pixel its distance from the sensor in mm [START_REF] Cruz | Kinect and RGBD Images: Challenges and Applications[END_REF]. From this distance, which is equivalent to the z coordinate of the point represented by the real pixel, we can calculate its abscissa and ordinate. X p and Y p : Pixel coordinates X res and Y res : The horizontal and vertical resolution of the depth map. fov H et fov V :The horizontal and vertical field of view of Kinect (in radians). Thus, the coordinates (x, y, z) corresponding to the actual points of the pixel depth map are known. This allows obtaining a 3D point cloud of the scene seen by the Kinect whose dimensions are the same as the actual dimensions.Since weknow the depth values, we can determine the width and height of a player using trigonometry, as illustrated in figure 4 where we calculate a player's width. The normal depth vision of the sensor ranges from around two and ahalf feet (800mm) to just over 13 feet (4000mm) [START_REF] Cruz | Kinect and RGBD Images: Challenges and Applications[END_REF]. The purpose of edge detection is to identify the points of a digital image that correspond to a sudden change in light intensity. These changes in image properties generally reflect significant events or changes in the properties of the world. These include discontinuities in depth, in the orientation of a surface, the material properties and the lighting of a scene. To extract the contour of people in the 3D images we tried different approaches. However, in this second part, we will present only two filters which are the most efficient in our researches [START_REF] Tölgyessy | The Kinect Sensor in Robotics Education[END_REF].

Application of Edge detection Approach (The Gradient Approach)

The gradient is a vector, the more traditional approach to estimate the gradient is to choose two orthogonal preferred directions, on which we project the gradient [START_REF] Ni | RGBD-HuDaAct: A color-depth video database for human daily activity recognition[END_REF]. It can be described in the following flow chart. Operator Roberts described in a rectangular image (see Figure 5), with a contour ramp, the first derivatives, they are of limited value because the maximum slope is unlikely to be on one of the two directions considered. What matters is the length of the gradient vector of which they are components. This length is calculated in principle by the Pythagorean Theorem by computing on real and accelerating considerably using a full approximation:

çG ç= çE -Wç + çN -Sç (4)
Where: E, W, N and S are the pixels in the rectangular image Regardless of the accuracy of the calculation, this result must be transformed into a digital filter. The physical notion of filter corresponds to the mathematical concept of convolution. In the case of digital data as in the case of image processing, the relationship between output pixel values and the input t pixels value is described by an array of numbers called convolution matrix [START_REF] Munoz-Salinas | People Detection and Trackingusing Stereo Vision and Color[END_REF]. Calculated on 4 points, this filter consists of the application of the double mask as follows: The Sobel filter computes an approximation rather inaccurate of intensity gradient, but enough practice in many cases. In fact, it uses a neighborhood (usually 3 × 3) around each point to calculate the gradient, and the weights used to calculate the gradient are integers [START_REF] Munoz-Salinas | People Detection and Trackingusing Stereo Vision and Color[END_REF]. Also calculated on 9 points, this filter allows focus on the calculation following several directions (horizontal, vertical, diagonal). Filters are the following:

Laplacian approach

A priori, the use of second derivatives is more convenient than first derivatives: instead of seeking the maximum intensity gradient, we seek cancellation of second derivatives [START_REF] Ni | RGBD-HuDaAct: A color-depth video database for human daily activity recognition[END_REF]. In the case of an image, there is no second derivative but only four partial derivatives (in x ², y ², xy and yx). In practice, it removes this ambiguity by using the Laplacian operator which is the sum of the two partial derivatives. Being an image I with 2 variables x and y I = I (x,y) The Laplacian is calculated by the following formula:

Optimal filters

Actually, the main disadvantage of the Laplacian approach is that the derivative operators of first order exaggerate the noise effects and second derivatives are exaggerating it twice. Another type of most recent approach is based on the definition of optimality criteria of edge detection; these criteria leading to optimal smoothing filters [START_REF] Green | The detection and quantification of persons in cluttered beach scenes using neural network-based classification[END_REF]. a) Canny filter.

If we talk about the one-dimensional case, it is assumed that the detection is performed by convolving the signal by a filter with impulse response "h", the contours being characterized by the extreme of the filter output [START_REF] Green | The detection and quantification of persons in cluttered beach scenes using neural network-based classification[END_REF]. The edges are considered here types on and the noise is assumed to be white (zero mean). Optimality criteria are: ─ Detection: the edge must be detected, it must minimize false answers. ─ Localization: the edge must be located with accuracy; it comes to minimize the distance between the detected and the true contour. ─ Single response: to minimize the number of responses for a single edge.

The minimization of these criteria in the context of the proposed model leads to a differential equation whose solution is of the form: Figure 9 shows an example of edge detection by Canny.

Edge detection of depth images in light and darkness

After presenting some approach in edge detecting on color images, we will apply iton depth images. An example of 3D images produced by the Kinect sensor is shown is figure 10 and11. We should note that color in this figure represents a distance and the user can program the Kinect to display his color choice depending on the distance. We made testes on these images in an indoor environment once when exposed to light and once in darkness. By comparing images taken in deep darkness and those taken in good lighting conditions, we note that the quality is the same. As edge detection of Canny is good for people in both conditions. But the performance of Sobel algorithm was better for the images taken in the dark depths. Results are summarized in table I below.

Gesture detection

The tests we made on the depth images aim to detect and locate people then the monitor. We applied two approaches (Canny and Sobel filters) in the presence of light and darkness to check the efficiency of depth sensor and see the difference between the two approaches used. In this part, we made a gesture recognition using hands position. The Kinect sensor can detect 20 joints in human body.

When we calculate the coordinates (x,y,z) of each joint in the space we could make an idea about the position of each body part referred to the head or spin joint. In our application, we put sensors on the smart home building located in the University of Blagnac Toulouse such presented in figure 12. Therefore, we programmed the sensor to recognize hands user positions depending on the head and spin joints. Indeed, we can identify a focus gesture based on Z coordinates in the space. The sensor is being in an idle mode if the person already detected is not moving in the scene. However, when there is an action, the Kinect focus on hands position to see if there a focus gesture that exceeds a threshold distance. Thus, it triggers a recognition part. When a gesture is recognized, the monitored person can handle devices through a domestic bus where there are a large number of KNX actuators [START_REF] Phung | Detecting People in Images: An Edge Density Approach[END_REF] such as lights, blinds, heating, air conditioning system, opening doors and windows, alarm, luminous path at night etc. Some recognized gestures are represented in figure 14. In a previous work, we already investigate the use of a wireless network with Mesh topology [START_REF] Yli | OLSR Mesh Networks for Broadband Access: Enhancements, Implementation and Deployment[END_REF]. Indeed, we test the application of OLSR routing protocol [START_REF] Chrétien | 2A Project speciality 2A "real time 3D Reconstruction of hands motion[END_REF] and 802.11s standard. Besides, we demonstrate that there is difficult to transport Kinect data (depth images) through the network because of the high Baud rate required in the network which was about 180Mbits/s. Therefore, it is easier in our application to communicate a simple text or alert. So, when we gesture is detected, we don't need to communicate all the frames through the network. The communication of a message within the network seems a more discreet and does not present a sort of spying on the patient in their own home.

Conclusion

The detection of persons in an image has been the subject of several studies. Most of these works were done on images taken by cameras in visible light (RGB). In this paper, we are interested in the Kinect depth images.We first presented the video sensors considered as a smart camera as well as the construction of 3D mesh. Secondly, we applied edge detection filters on its 3D images, we extracted people contours and we did a performance comparison between filters. Results show that edge detection of Canny is good for people in both light condition but, the performance of Sobel algorithm was better for the images taken in the dark depths. Finally, we presented the gesture recognition part based on hand motions. We develop a program which detects people gestures and to recognize it. An automatic monitoring system seems to be interesting in the medical side. In a further work, we will implement Unistroke recognizer to use with Kinectin aim to find more gesture to command the smart house. Also, as perspectives, it is important to present a new approach for detecting people in images using depth contour models in 2D and 3D surface models.

Fig. 1 .

 1 Fig. 1.Kinect sensor elements

Fig. 2 .

 2 Fig. 2. Image obtained by the Kinect infra-red camera

Fig. 3 .

 3 Fig.3.. Calculation of the coordinate "y" of the point[START_REF] Pishchulin | Learning people detection models from few training samples[END_REF]

Fig. 4 .

 4 Fig.4. Finding the player real world width[START_REF] Cruz | Kinect and RGBD Images: Challenges and Applications[END_REF]

Fig. 5 .

 5 Fig. 5.Flow chart of the Gradient ApproachApplied to an image, regarded as a function of two variables, we can define two partial derivatives along x as a function of y. Let's consider an image I with 2 variables x and y; I = I (x, y) The gradient is calculated by the following formula:

Fig. 6 .

 6 Fig. 6.Mask to apply in Robert filter

Fig. 7 .

 7 Fig. 7.Sobel filter.

Fig. 8 .

 8 Fig. 8.. Example of edge detection using the Sobel filter

Fig. 9 .

 9 Fig. 9..Edge detection using Canny filter on grayscale image

  Results are illustrated in figures 10.a, 10.b, 11.a and 11.b.

Fig. 10 .Fig. 11 .Fig. 11 .

 101111 Fig. 10.Depth images of the Kinect sensor

Fig. 12 .

 12 Fig. 12.The smart house where testing our application

Fig. 13 .

 13 Fig. 13.Gesture recognition using Kinect

Table 1 .

 1 I. Table Type Styles

		Edge'sthickn	Localization	Sensibility to	Detectability
		ess		noise
	Sobel	Augmentation	Average	High	Low
	Canny	Preserved	High	Low	High


Philippe Balbiani
email: philippe.balbiani@irit.fr

Andreas Herzig
email: andreas.herzig@irit.fr

Nicolas Troquard
email: troquard@loa.istc.cnr.it

Dynamic logic of propositional assignments: a well-behaved variant of PDL

We study a version of Propositional Dynamic Logic (PDL) that we call Dynamic Logic of Propositional Assignments (DL-PA). The atomic programs of DL-PA are assignments of propositional variables to true or to false. We show that DL-PA behaves better than PDL, having e.g. compactness and eliminability of the Kleene star. We establish tight complexity results: both satisfiability and model checking are EXPTIME-complete.

I. Introduction

Dynamic logics are logics to reason about imperative programs. Their language extends that of propositional logic by modalities π , one per program π. Programs are either atomic or complex, the latter being built by means of sequential and nondeterministic composition, test and iteration ('Kleene star'). The models of PDL are transition systems: each transition is labeled with the name of an atomic program and indicates the possible execution of an atomic program from one state to another. The modal formula π ϕ is true at state s if there is an execution of π from s leading to a state satisfying ϕ.

The basic dynamic logic is Propositional Dynamic Logic (PDL). Its atomic programs are abstract: they are just letters a, b, . . . from some alphabet. Thus "PDL abstracts away from the nature of the domain of computation and studies the pure interaction between programs and propositions" [1, p. 147]. In contrast, the atomic programs of first-order dynamic logic are concrete, viz., assignments of object variables to terms [1, ch. 11]. They capture assignments as used in programming languages. We are here interested in a different kind of assignments: assignments of propositional variables to truth values, for short: propositional assignments. We write +p and -p for such assignments, where p is a propositional variable.

Only few authors studied such propositional assignments. The first were Meyer and Winklmann, who considered both assignments of object variables and assignments of propositional variables [START_REF] Meyer | On the expressive power of dynamic logic (preliminary report)[END_REF]. Tiomkin and Makowsky focused on propositional assignments [START_REF] Tiomkin | Propositional dynamic logic with local assignments[END_REF]. They augmented the language of PDL with two kinds of propositional assignments: local and global. Local assignments modify the truth value of a propositional variable at the actual state of a Kripke model and leave its value unchanged elsewhere. Global assignments modify the value of a propositional variable everywhere in a Kripke model. Besides these two distinct kinds of assignments, their logic still contains abstract atomic programs a, b, . . . They establish that the logic embeds first-order dynamic logic [START_REF] Tiomkin | Propositional dynamic logic with local assignments[END_REF]. It is perhaps due to the ensuing undecidability result that dynamic logics with propositional assignments did not gain much traction, despite their putative usefulness for modelling concrete properties of computational systems. A notable exception is Wilm's decidable Propositional Program Logic PPL [START_REF] Wilm | Determinism and non-determinism in PDL[END_REF]. PPL is a dynamic logic with deterministic atomic programs (alias 'Strict PDL'), plus nondeterministic composition "∪", plus Tiomkin and Makowsky's global propositional assignments. (So PPL has abstract atomic programs just as Tiomkin and Makowsky's logic.) Wilm showed that the Kleene star operator can be simulated in PPL.

More recently, dynamic logics with assignments but without abstract programs were investigated, chiefly in logics of agents, as variants of dynamic epistemic logics (DEL). The basic version of DEL is Public Announcement Logic (PAL). PAL extends multi-agent epistemic logic with dynamic operators whose arguments are truthful public announcements of propositions. Epistemic riddles and cryptographic protocols were successfully modelled in PAL (see e.g. [START_REF] Ditmarsch | The Russian cards problem[END_REF]). It was extended by public assignments in [START_REF] Ditmarsch | Dynamic epistemic logic with assignment[END_REF]- [START_REF] Ditmarsch | From Situation Calculus to Dynamic Logic[END_REF], which model how agents' knowledge changes when some propositional variable is publicly assigned to true or to false. None of these papers explored the program operators of PDL. Again, the designated culprit is an issue of computability: Miller and Moss showed that the addition of the PDL program connectives to PAL yields an undecidable logic [START_REF] Miller | The undecidability of iterated modal relativization[END_REF].

In this paper we revisit the logic of propositional assignments. Contrarily to Tiomkin and Makowsky, our language has no abstract programs; Contrarily to the approaches in the PAL tradition, it does not have epistemic operators. We call our logic Dynamic Logic of Propositional Assignments, abbreviated DL-PA. We present it in Section II. We briefly compare it to PDL in Section III, showing that it can be viewed as an instantiation of PDL with assignment programs.

The star-free version of DL-PA was previously studied by van Eijck [START_REF] Eijck | Making things happen[END_REF] and recently put to use in [START_REF] Herzig | A dynamic logic of normative systems[END_REF]. Van Eijck gave an axiomatisation of star-free DL-PA and stated that the addition of the Kleene star does not increase the expressivity because "an arbitrary [program] π * only affects a finite number of atomic propositions". He however observes that "[f]inding an efficient method for translating π * [programs] into * -free form is another matter". In Section IV we show that the Kleene star can be constructively eliminated in DL-PA, providing thus a procedure reducing DL-PA to its star-free fragment. From this, decidability of the satisfiability problem follows. Our result contrasts with both Miller and Moss's undecidability result for the extension of PAL by the PDL program connectives and with Tiomkin and Makowsky's undecidability result for the extension of PDL by local assignments.

But the decidability of DL-PA is not to be doubted given the nature of its models: its semantics does not require a transition system, given that there is no need for an accessibility relation interpreting abstract actions. Models are in fact made up of a single state, i.e., a valuation of classical propositional logic. Propositional assignments then update these valuations in the obvious way. Being able to do PDL-style reasoning whilst relying on such 'degenerate', succinctly specified models, has an immediate practical advantage when modelling a computational system. Indeed, it is folklore that modelling a distributed system is typically achieved by a transition system of size exponential in the number of variables. The applicability of verification via model checking is then immediately compromised: a system designer cannot realistically be expected to even represent the model, let alone verify it. Instead, the modelling of a system in view of verification with DL-PA is confined to the initial state of affairs. Naturally, quite some modelling effort is shifted to the query, which needs to represent the dynamic constraints of the relevant variables. But it happens that it often does not impact much the size of the whole input to a model checking procedure. We exemplify this by efficiently mapping the instances of a variant of a decision problem concerning the game Peek [START_REF] Stockmeyer | Provably difficult combinatorial games[END_REF] into instances of the DL-PA model checking. Stockmeyer and Chandra showed that deciding the former is provably difficult. Thus, unfortunately, it also means that there is a price to pay for this comparatively effortless modelling task: the computational complexity of model checking with DL-PA is EXPTIME-complete. In contrast, the complexity of model checking a transition system with PDL is PTIME-complete. As we shall show, the complexity of DL-PA satisfiability checking remains EXPTIME-complete, which is also the complexity of PDL. 1 Under a commonly accepted conjecture in complexity theory, this indicates that van Eijck's problem does not have a full solution: there is probably no efficient method to eliminate the Kleene star from DL-PA. We introduce Peek in Section V, and provide the lower bounds for the model checking and satisfiability checking problems. Section VI addresses the upper bounds.

In Section VII we discuss the extensions of DL-PA with assignments of any formula as atomic programs (and not just true and false) and with converse as a new program construct. In Section VIII we investigate the tight relationship of DL-PA with Coalition Logic of Propositional Control and Delegation (DCL-PC) [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF], correcting a mistake in [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF] about the complexity of DCL-PC.

II. DL-PA: dynamic logic of propositional assignments

In this section we define syntax and semantics of dynamic logic of propositional assignments DL-PA.

A. Language

Throughout the paper, P = {p, q, . . .} denotes a (fixed) countable set of propositional variables. The language of DL-PA is defined by the following grammar:

π +p | -p | π; π | π ∪ π | π * | ϕ? ϕ p | ⊤ | ⊥ | ¬ϕ | ϕ ∨ ϕ | π ϕ
where p ranges over P. So atomic programs are of the form +p or -p. In a few places we will use the expression ±p to talk economically about +p and -p. The operators of sequential composition (";"), nondeterministic composition ("∪"), unbounded iteration (" * ", the Kleene star), and test ("?") are familiar from PDL.

The program skip abbreviates ⊤? ("nothing happens"). We use the abbreviation π n with the obvious meaning. We also use bounded iteration "π ≤n ", i.e., iteration up to integer n, as a macro for k≤n π k . A program is said to be sequential if it is built up from atomic programs and tests by means of the operator ";".

We abbreviate the logical connectives ∧, → and ↔ in the usual way. Aside the dynamic operator π , we also use its dual: [π]ϕ abbreviates ¬ π ¬ϕ.

The length of a formula ϕ, noted |ϕ|, is the number of symbols used to write down ϕ in the primitive language, without , , and parentheses. For example, |q ∧ r| = |¬(¬q ∨ ¬r)| = 6. The length of a program π, noted |π|, is defined in the same way. For example, |-p; p?| = 5. Also | +q (q ∧ r)| = 2+6 = 8. We define P ϕ to be the set of variables from P occurring in formula ϕ, and we define P π to be the set of variables from P occurring in program π. For example, P -p∪+q = {p, q} = P -p q .

B. Semantics

Models of DL-PA are nothing but models of classical propositional logic. Definition 1. A valuation is a subset of the set of propositional variables P. The size of a valuation v is the cardinality of v.

DL-PA programs are interpreted by means of a (unique) relation between valuations: atomic programs +p and -p update valuations in the obvious way, and complex programs are interpreted just as in PDL by mutual recursion. Table I gives the interpretation of the DL-PA connectives.

Definition 2. A formula ϕ is DL-PA valid if ||ϕ|| = 2 P , and ϕ is DL-PA satisfiable if ||ϕ|| ∅.
DL-PA validity and DL-PA satisfiability are defined as usual. For example, the formulas +p ⊤ and +p ϕ ↔ ¬ +p ¬ϕ are DL-PA valid. Other examples of DL-PA validities are +p p and -p ¬p. Observe that if p does not occur in ϕ then both ϕ → +p ϕ and ϕ → -p ϕ are valid. This is due to the following semantical property that we will use a few times in this paper.

||+p|| = (v, v ′ ) : v ′ = v ∪ {p} ||-p|| = (v, v ′ ) : v ′ = v \ {p} ||π; π ′ || = ||π|| • ||π ′ || ||π ∪ π ′ || = ||π|| ∪ ||π ′ || ||π * || = k∈N 0 (||π||) k ||ϕ?|| = {(v, v) : v ∈ ||ϕ||} ||p|| = {v : p ∈ v} ||⊤|| = 2 P ||⊥|| = ∅ ||¬ϕ|| = 2 P \ ||ϕ|| ||ϕ ∨ ψ|| = ||ϕ|| ∪ ||ψ|| || π ϕ|| = {v : there is v ′ s.t. (v, v ′ ) ∈ ||π|| and v ′ ∈ ||ϕ||}

C. Example: the n-bit counter

Here is a DL-PA program implementing an n bit counter. We need n propositional variables q 0 , . . . , q n-1 . The conjunction

time(0) = ¬q n-1 ∧ • • • ∧ ¬q 1 ∧ ¬q 0 encodes that the counter has value zero; time(1) = ¬q n-1 ∧• • •∧¬q 1 ∧q 0 encodes value one; time(2 n -1) = q n-1 ∧ • • • ∧ q 1 ∧ q 0 encodes 2 n -1. Let time(N) encode that the counter has value N.
Here is a program incr n incrementing the n bit counter until 2 n -1 is attained and then fails:

incr n = ¬(q n-1 ∧ • • • ∧ q 0 )?;         0≤k≤n-1 (¬q k ∧ q k-1 • • • ∧ q 0 ?; +q k ; -q k-1 ; • • • ; -q 0 )        
Observe that the length of incr n is quadratic in n. Observe moreover that the formula

time(0) → [incr n * ] N<2 n-1 time(N) → ( incr n ⊤ ∧ [incr n ]time(N+1))
and the formula

[incr n * ] time(2 n -1) → [incr n ]⊥)
are both DL-PA valid. The reader may check that the counter indeed runs from zero to 2 n -1 and then fails: the formula

¬q n-1 • • • ∧ ¬q 0 → incr n * q n-1 • • • ∧ q 0 ∧ [incr n ]⊥ is DL-PA valid.

III. Relation with PDL

Let us briefly recall PDL. Its grammar has exactly the same form as that of our DL-PA, except that PDL has a countable set Π 0 of abstract atomic programs instead of the DL-PA assignments +p and -p. The models of PDL are triples M = (W, R, V) where W is a nonempty set of states, R : Π 0 -→ 2 W×W associates with every atomic program π 0 ∈ Π 0 an accessibility relation R(π 0 ) on W, and V : W -→ 2 P associates with every state a subset of P. We write M, w ϕ when the PDL formula ϕ is true at state w of model M.

For the sake of comparison, suppose the set of atomic programs Π 0 contains {+p : p ∈ P} ∪ {-p : p ∈ P}. Then the set of DL-PA validities obviously contains the set of PDL validities. To see this, build the Kripke model

M DL-PA = (W, R, V) such that W = 2 P , V is the identity function, and such that if π 0 is of the form +p or -p then (v 1 , v 2 ) ∈ R(π 0 ) iff (v 1 , v 2 ) ∈ ||π 0 ||;
we can prove that for every valuation v and DL-PA formula ϕ we have v ∈ ||ϕ|| iff M DL-PA , v ϕ. So when ϕ ↔ ϕ ′ is PDL valid then ϕ and ϕ ′ are formula-equivalent in DL-PA. The converse does not hold: for instance, +p ⊤ ↔ ⊤ is valid in DL-PA, but not in PDL.

As to program equivalence, let us say that programs π and π ′ are program-equivalent in PDL if for every model M = (W, R, V) we have R(π) = R(π ′ ). Clearly, when π and π ′ are program-equivalent in PDL then π and π ′ are also programequivalent in DL-PA. Again, the converse does not hold; to witness, +p; +q and +q; +p are program equivalent in DL-PA, but not in PDL.

We are going to show in Sections V and VI that both the model checking and the satisfiability problem of DL-PA have the same complexity as the satisfiability problem of PDL. The proof involves a polynomial embedding of DL-PA into PDL (Section VI, Proposition 16).

IV. Constructive eliminability of the Kleene star

In this section we show how dynamic operators can be eliminated from formulas. The key step is the elimination of the star operator. This allows us to establish decidability of satisfiability (Section IV-C) and compactness (Section IV-D).

A. Some remarkable properties

We now state some properties of DL-PA that already hold for PDL. We say that a program is star-free if it does not contain the Kleene star " * ". We recall that in star-free PDL, the program operators can be entirely eliminated from formulas.

Proposition 3. The following formula equivalences are

DL-PA valid. π; π ′ ϕ ↔ π π ′ ϕ π ∪ π ′ ϕ ↔ π ϕ ∨ π ′ ϕ ψ? ϕ ↔ ψ ∧ ϕ π ≤0 ϕ ↔ ϕ π ≤n+1 ϕ ↔ ϕ ∨ π π ≤n ϕ
Program equivalence is a congruence relation w.r.t. ';' and '∪': if

π 1 ≡ π ′ 1 and π 2 ≡ π ′ 2 then both π 1 ; π 2 ≡ π ′ 1 ; π ′ 2 and π 1 ∪ π 2 ≡ π ′ 1 ∪ π ′ 2 . Proposition 4. The following program equivalences are DL-PA valid. π ; (π ′ ; π ′′ ) ≡ (π; π ′ ) ; π ′′ (1) π ; (π ′ ∪ π ′′ ) ≡ (π; π ′ ) ∪ (π; π ′′ ) (2) (π ∪ π ′ ) ; π ′′ ≡ (π; π ′′ ) ∪ (π ′ ; π ′′ ) (3) ϕ? ; ψ? ≡ ϕ ∧ ψ? (4) skip; π ≡ π (5) π ; ϕ? ≡ π ϕ? ; π if π is sequential (6) (ϕ?; π) ∪ π ≡ π (7)
ϕ? ∪ ¬ϕ? ≡ skip (8) Proof: The proof is a routine induction on the length of the expression ǫ. For the case ǫ = ϕ? we use Proposition 5, and for the case ǫ = π ϕ we use Proposition 6.

π ≤0 ≡ skip (9)
π ≤n+1 ≡ skip ∪ π; π ≤n (10)
We call a program a conditioned sequence of assignments if it is of the form

ϕ?; π 1 ; • • • ; π n , for n ≥ 0
where every π k is an atomic program. When n = 0 we identify the sequence with ϕ?. Proposition 8. In DL-PA, every star-free program π is program-equivalent to the nondeterministic composition of conditioned sequences of assignments.

Proof: We start by distributing ";" over '∪', applying the program equivalences (2) and (3) of Proposition 4. The result is a nondeterministic composition of sequential programs. In each of these sequences we shift tests to the left and then group together test sequences into a single test, applying the program equivalences ( 6) and ( 4) of Proposition 4. The result is a nondeterministic composition of conditioned assignment sequences of the form (ϕ 1 ?; π 1 ) ∪ • • • ∪ (ϕ n ?; π n ) where each π k is a (possibly empty) sequence of atomic programs.

The next proposition is pivotal: it states a sufficient condition for the eliminability of the Kleene star. Proposition 9. Let π be a program of the form ϕ 1 ?;

π 1 ∪ • • • ∪ ϕ n ?; π n such that for every k, m ≤ n we have π k ; π m ≡ π m . Then π * ≡ π ≤n .
Proof: It suffices to prove that π ≤n+1 ≡ π ≤n . Consider any sequence of length n + 1; such a sequence necessarily contains a repetition of some ϕ k ?; π k . Take for example the following sequence σ of length n + 1 wherein ϕ 1 ?; π 1 occurs twice: σ = ϕ 1 ?; π 1 ; ϕ 2 ?; π 2 ; ϕ 3 ?; π 3 ; • • • ; ϕ n ?; π n ; ϕ 1 ?; π 1 . We show that σ is subsumed by π ≤n , in the sense that σ∪π ≤n ≡ π ≤n . Our proof makes extensive use of Proposition 7.

We first use the program equivalence π 1 ; ϕ 2 ? ≡ π 1 ϕ 2 ? ; π 1 (which is an instance of program equivalence (6) of Proposition 4) to push the second test to the left: we rewrite σ to ϕ 1 ?; π 1 ϕ 2 ? ; π 1 ; π 2 ; ϕ 3 ?; π 3 ; • • • ; ϕ n ?; π n ; ϕ 1 ?; π 1 . Pushing the third test leftwards we obtain: ϕ 1 ?; π 1 ϕ 2 ?; π 1 ; π 2 ϕ 3 ? ; π 1 ; π 2 ; π 3 ; • • • ; ϕ n ?; π n ; ϕ 1 ?; π 1 . Pushing all the tests leftwards in this way, we obtain a sequence of tests that is followed by π 1 ; • • • ; π n ; π 1 , namely:

ϕ 1 ?; π 1 ϕ 2 ?; • • • ; π 1 ; • • • ; π n-1 ϕ n ?; π 1 ; • • • ; π n ϕ 1 ? ; π 1 ; • • • ; π n ; π 1 .

By hypothesis, π

1 ; • • • ; π n ; π 1 ≡ π 1 . Therefore our program σ is equivalent to ϕ 1 ?; π 1 ϕ 2 ?; • • • ; π 1 ; • • • ; π n ϕ 1 ?
; π 1 . Proposition 4(4) allows us to group all the tests from the second test on into a single test: Note that each of the above steps is correct thanks to Proposition 7.

ϕ 1 ? ; ( π 1 ϕ 2 ∧ • • • ∧ π 1 ; • • • ; π n ϕ 1 )? ; π 1 . Let us abbreviate π 1 ϕ 2 ∧ • • • ∧ π 1 ; • • • ; π n ϕ

Proposition 13 ( [10]

). The following formula equivalences are DL-PA valid.

±p ⊤ ↔ ⊤ ±p ⊥ ↔ ⊥ ±p ¬ϕ ↔ ¬ ±p ϕ ±p (ϕ 1 ∨ ϕ 2 ) ↔ ±p ϕ 1 ∨ ±p ϕ 2 +p q ↔        ⊤ if q = p q otherwise -p q ↔        ⊥ if q = p q otherwise B.

Elimination of the Kleene star

We now give a procedure eliminating the Kleene star from formulas. This contrasts with PDL where elimination is impossible. Our procedure has three steps. 1) Take some innermost star-operator, i.e., some π * such that π is star-free. Transform π into the nondeterministic composition of conditioned sequences of assignments

π ′ = (ϕ 1 ?; π 1 ) ∪ • • • ∪ (ϕ n ?; π n )
where every π k is a sequence of assignments. 2) Make all the assignment sequences π k assign exactly the same variables: replace π k by (p?; +p; π k )∪(¬p?; -p; π k ) whenever p P πk and p ∈ P πl for some l ≤ n, and put the result again in the form of a nondeterministic composition of conditioned assignment sequences. We obtain therefore a program of the form

π ′′ = (ϕ ′′ 1 ?; π ′′ 1 ) ∪ • • • ∪ (ϕ ′′ m ?; π ′′ m ) with P π ′′ 1 = • • • = P π ′′ m . 3) Replace (π ′′ ) * by (π ′′ ) ≤m .
The first step preserves program equivalence by Proposition 8. The second step does so because of Proposition 12 (to be applied at most n times per assignment sequence). The third step is guaranteed by Proposition 9, which applies because of Proposition 11: when the assignment sequences π and π ′ have exactly the same variables then π; π ′ ≡ π ′ . All three steps preserve formula equivalence: the formulas resulting from replacement of the program equivalences are formula-equivalent thanks to Proposition 7.

Summing up, in the first three steps we have succeeded in eliminating an innermost star-operator. By iterating these three steps we eliminate star operators entirely from formulas.

Theorem 1. For every DL-PA formula ϕ there exists a formula ϕ ′ without the Kleene star such that ϕ and ϕ ′ are formula equivalent in DL-PA.

C. Deciding satisfiability Definition 4. The problem of satisfiability checking SAT has the following input and output.

• Input: a formula ϕ;

• Output:

true, when ||ϕ|| ∅; false, otherwise.

The decision procedure is as follows: 1) Eliminate the Kleene star from ϕ.

2) Eliminate the sequential and the nondeterministic composition operators as well as the test operators. 3) Eliminate all the dynamic operators with assignments. The first step uses Theorem 1. The second step uses the standard PDL equivalences of Proposition 3 that we have recalled in the beginning of Section IV-A. We therefore end up with formulas having only atomic programs, i.e., assignments. We can then distribute these dynamic operators over the boolean operators (using in particular the equivalence for negation of Proposition 13) and finally eliminate them by the DL-PA equivalences for assignments of Proposition 13. The resulting formula has no more dynamic operators, it is equivalent to the original formula, and its validity or satisfiability may be checked by means of any theorem prover for classical propositional logic. Theorem 2. For every DL-PA formula ϕ there is a propositional formula ϕ ′ such that ϕ ↔ ϕ ′ is DL-PA valid.

Corollary 1. The problem of satisfiability of a DL-PA formula is decidable.

Observe that the only principles beyond those of star-free PDL that we have used in our decision procedure are propositions 5 and 6 (that allow us to prove Proposition 7 and that can be viewed as inference rules), the formula equivalences of Proposition 13 (though the one for disjunctions is already provable in star-free PDL), and the program equivalences of Proposition 4. The latter axiom schemes are a bit unusual: they do not have the form of formulas but that of program equivalences. Together, these principles provide a complete but somewhat non-standard axiomatisation of DL-PA.

D. Compactness and interpolation

In PDL, there are two ways to define the consequence relation | = between a set of formulas Γ and a formula ϕ. In contrast, in DL-PA there is only one way to do so: ϕ is a consequence of Γ iff ψ∈Γ ||ψ|| ⊆ ||ϕ||. In other words, for every valuation v, if v ∈ ||ψ|| for every ψ ∈ Γ then v ∈ ||ϕ||. Compactness of the DL-PA consequence relation immediately follows from Theorem 2.

Theorem 2 also helps us to prove the interpolation property for DL-PA. We actually need a slightly stronger version guaranteeing that the propositional formula that is equivalent to ϕ has the same propositional variables as ϕ.

Theorem 3. For every DL-PA formula ϕ there is a propositional formula ϕ ′ such that P ϕ ′ = P ϕ , and ϕ ↔ ϕ ′ is DL-PA valid.

Proof: All the rewriting rules of the procedure underlying Theorem 2 preserve the variables, except those for subformulas of the form ±p ⊤, ±p ⊥, +p q, and -p q. The equivalences for the latter eliminate propositional variables. Fortunately they have variants that preserve variables and that are also valid:

±p ⊤ ↔ p ∨ ¬p ±p ⊥ ↔ p ∧ ¬p +p q ↔        p ∨ ¬p if q = p q ∧ (p ∨ ¬p) otherwise -p q ↔        p ∧ ¬p if q = p q ∧ (p ∨ ¬p) otherwise
Now an interpolant of ψ | = ϕ can be obtained by rewriting ϕ and ψ to propositional ϕ ′ and ψ ′ in a way such that their respective languages are preserved. By the interpolation property for propositional logic, there exists an interpolant χ of ψ ′ | = ϕ ′ . As the new equivalences are language-preserving, χ is also an interpolant of ψ | = ϕ.

V. Complexity of decision problems: lower bounds

We now give complexity results for our logic DL-PA. We have already defined the problem SAT in Section IV-C; it remains to define model checking.

Definition 5. The problem of model checking MC has the following input and output.

• Input: a model v and a formula ϕ such that v ⊆ P ϕ ;

• Output:

true, when v ∈ ||ϕ||; false, otherwise.

Note that the constraint v ⊆ P ϕ implies that v is finite. We are now going to provide lower bounds for both problems. Proof: The result is established for model checking in Section V-A, and for satisfiability checking in Section V-B.

A. Lower bound for model checking: encoding PEEK

We prove that model checking with DL-PA is EXPTIMEhard by means of a logarithmic-space reduction of the problem PEEK-G 5 [START_REF] Stockmeyer | Provably difficult combinatorial games[END_REF] into the problem MC.

PEEK-G 5 is in terms of two players E ('Eloise', the existential player) and A ('Abelard', the universal player). Definition 6. An instance of Peek is a tuple PE = (X E , X A , Φ, v 0 , τ) where

• X E and X A are finite sets of propositional variables such that X E ∩ X A = ∅, where the idea is that Player E controls the variables in X E and Player A controls the variables in X A ;

• Φ is a propositional formula over X E ∪ X A ; • v 0 ⊆ X E ∪X A

indicates which variables are currently true;

• τ is either A or E, indicating which player makes the next move.

Informally, each instance PE = (X E , X A , Φ, v 0 , τ) of Peek is played as follows. Agents' turns strictly alternate. At their respective turn, Player E (resp. A) moves by changing the truth value of at most one variable of X E (resp. X A ) in the current valuation, either adding or withdrawing it from the valuation. The game ends when Φ first becomes true. We are considering PEEK-G 5 , where Player A cannot move from a situation where Φ is true, and Player E wins the game if Φ ever becomes true. We say that Player E has a winning strategy in PE if she can make a sequence of moves at her turns and ensure to win whatever the moves made by Player A at his turn. Let us make this more precise.

The game tree associated with PE is a tree labeled by valuations such that the root is labeled v 0 , starting with the agent τ at the root, all nodes are obtained by E and A alternatively performing all possible moves. A node is an E node if it is Eloise's turn to move, and it is an A node if it is Abelard's turn.

A (memoryless) strategy of Eloise is a function from valuations to actions of E. A branch (n 0 , n 1 , n 2 , . . .) of the game tree is compatible with Eloise's strategy s E if and only if for every E-node n k , the valuation v k+1 labeling n k+1 is obtained by applying E's action s E (n k ) to the valuation v k .

Eloise has a winning strategy if and only if there is a strategy s E such that every branch (n 0 , n 1 , n 2 , . . .) of the game tree that is compatible with s E has a node n k such that v k ∈ ||Φ||.

Definition 7. The decision problem PEEK-G 5 is the following:

• Input: an instance PE = (X E , X A , Φ, v 0 , τ) of Peek;

• Output:

true, when Player E has a winning strategy in PE; false, otherwise.

Theorem 5 ( [12]). PEEK-G 5 is EXPTIME-complete.

We prove that deciding the model checking problem MC for DL-PA is EXPTIME-hard by reducing PEEK-G 5 to it. Beyond the variables of X E ∪X A , we use the propositional variables elo and nowin. The intended meaning of elo is that it is Player E's turn to play, whereas the intended meaning of nowin is that Player E has no winning strategy. Let PE = (X E , X A , Φ, v 0 , τ) be an instance of the Peek problem. We associate with it an instance (v, ϕ) of the MC problem as follows. First, the valuation v is defined by: if

τ = A then v = v 0 ∪ {nowin} else v = v 0 ∪ {nowin, elo}.
Second, in order to define the formula ϕ, we need to introduce the following abbreviations:

ϕ def = [move * ] nowin → (¬Φ∧(elo → [move]nowin)∧ (¬elo → move nowin))
Obviously, given PE, the computation of (v, ϕ) can be done in logarithmic space. Moreover,

Lemma 1. PEEK-G 5 (PE) returns false iff MC(v, ϕ) returns true.
Informally, the idea is that PEEK-G 5 (PE) returns false iff when we assume that Eloise does not have a winning strategy (by putting nowin in v along with the the initial situation of PE described by v 0 ), then we can verify that the following is an invariant in the game-tree starting at v:

"if Eloise has no winning strategy, then (1) at Eloise's turn, she has no winning strategy after any move, (2) at Abelard's turn, there is a successor node where Eloise has no winning strategy."

Proof: Suppose PEEK-G 5 (PE) returns false: Eloise does not have a winning strategy in PE. Therefore the nodes of the game tree associated with PE can be further labeled by nowin in the following way:

• The root is labeled nowin;

• For E-nodes labeled nowin, each of E's moves leads to a node that it labeled nowin; • For A-nodes labeled nowin, some move of A's moves leads to a node that it labeled nowin; • A node whose valuation satisfies Φ cannot be labeled Proof: This follows directly from Lemma 1.

B. Lower bound for satisfiability checking: encoding MC

We finally establish that the problem of satisfiability checking is EXPTIME-hard. Since we have proved in Section V-A that the model checking problem MC is EXPTIME-hard (Proposition 14), it suffices to reduce MC to the problem of satisfiability checking.

Proposition 15. The problem of DL-PA satisfiability checking is EXPTIME-hard.

Proof: This follows directly from propositions 2 and 14.

We already know that star-free DL-PA is PSPACEcomplete [START_REF] Herzig | A dynamic logic of normative systems[END_REF]. We can then state the following: Corollary 2. A logarithmic-space reduction from the DL-PA satisfiability problem to the satisfiability problem of its starfree fragment exists iff PSPACE = EXPTIME.

So van Eijck's problem of finding an efficient method for translating DL-PA programs into star-free programs has a positive answer if and only if PSPACE = EXPTIME.

VI. Complexity of decision problems: upper bounds

We are now going to provide upper bounds for the problems MC and SAT. This establishes that the lower-bounds of Section V are tight. While our rewriting procedure of Section IV-C could be turned into decision procedures for both problems, it would however lead to upper bounds far beyond those we are going to establish now. Theorem 6. The problems of DL-PA model checking and DL-PA satisfiability are both in EXPTIME.

The proof uses a satisfiability preserving polynomial transformation tr PDL (.) from the formulas and programs of DL-PA to the formulas and programs of PDL. Our translation replaces each assignment ±p by an abstract program a ±p . Precisely it is defined by recursion as follows:

tr PDL (p) def = p if p ∈ P tr PDL (+p) def = a +p tr PDL (-p) def = a -p
and homomorphic for the other formula and program connectives. Observe that the length of every translated formula tr PDL (ϕ) is linear in the length of ϕ.

The abstract programs a ±p that occur in a formula ϕ should behave in the same way as the original assignment ±p. We achieve this by means of the following set of formulas.

Γ ϕ = {[a +p ]p : p ∈ P ϕ } ∪ {[a -p ]¬p : p ∈ P ϕ } ∪ { a ±p ⊤ : p ∈ P ϕ } ∪ {q → [a ±p ]q : p, q ∈ P ϕ , p q} ∪ {¬q → [a ±p ]¬q : p, q ∈ P ϕ , p q}
Observe that for every ϕ, the set Γ ϕ is finite; its cardinality is quadratic in the length of ϕ. Each element of Γ ϕ having constant length, the length of Γ ϕ is quadratic in the length of ϕ.

Let U ϕ be the program p∈Pϕ (a +p ∪ a -p ) *

. The modal operator [U ϕ ] plays the role of a master modality in our proof: given a valuation v, the program U ϕ relates v to every valuation that is examined during the evaluation of ϕ at v. Proposition 16. For every DL-PA formula ϕ, ϕ is DL-PA satisfiable if and only if

tr PDL (ϕ) ∧ [U ϕ ] Γ ϕ is PDL satisfiable.
Proof: From the left to the right, let v 0 be a DL-PA valuation such that v 0 ∈ ||ϕ||. Define M ϕ = (W, R ϕ , V) where W = 2 P is the set of all valuations, V is the identity function (i.e., V(v) = v for every v ∈ W), and where the accessibility relation is as follows for the relevant atomic programs a ±p such that p ∈ P ϕ :

R ϕ (a +p ) = (v, v ′ ) : v ′ = v ∪ {p} R ϕ (a -p ) = (v, v ′ ) : v ′ = v \ {p}
Furthermore, we set R ϕ (π 0 ) = ∅ for all atomic programs π 0 for which there is no p ∈ P ϕ with π 0 = a +p or π 0 = a -p . Observe that M ϕ is indeed a model of PDL as defined in Section III. We are going to prove that

M ϕ , v 0 tr PDL (ϕ) ∧ [U ϕ ] Γ ϕ
First, by construction of M ϕ we have M ϕ , v Γ ϕ for every v ∈ W. (In particular, each of the accessibility relations R ϕ (a ±p ) is serial.) Therefore M ϕ , v 0 [U ϕ ] Γ ϕ . It remains to establish that M ϕ , v 0 tr PDL (ϕ). We prove by simultaneous induction on the form of subformula ψ and program π occurring in ϕ that

1) v ∈ ||ψ|| iff M ϕ , v tr PDL (ψ) and 2) (v, v ′ ) ∈ ||π|| iff (v, v ′ ) ∈ R ϕ (tr PDL (π)).
for all valuations v and v ′ . When the subformula ψ of ϕ is atomic then

v ∈ ||p|| iff p ∈ v iff M ϕ , v p.
When the program π occurring in ϕ is of the form +p then

(v, v ′ ) ∈ ||+p|| iff v ′ = v ∪ {p} iff (v, v ′ ) ∈ R ϕ (a +p );
and similarly for -p. For the induction step, the only interesting case is that of the modal operator. We have:

v ∈ || π ψ|| iff there is v ′ such that (v, v ′ ) ∈ ||π|| and v ′ ∈ ||ψ|| iff there is v ′ such that (v, v ′ ) ∈ R ϕ (tr PDL (π))
and

M ϕ , v ′ tr PDL (ψ) (by I.H., twice) iff M ϕ , v tr PDL (π) tr PDL (ψ) iff M ϕ , v tr PDL ( π ψ)
From the right to the left, let M = (W, R, V) be a PDL model and let w 0 be a state in M such that M, w 0 tr PDL (ϕ)

∧ [U ϕ ] Γ ϕ . First, observe that M, w [U ϕ ]
Γ ϕ for every w such that (w 0 , w) ∈ R(U ϕ ). We therefore have:

• if (w, w ′ ) ∈ R(a +p ) then V(w ′ ) ∩ P ϕ = V(w) ∪ {p} ∩ P ϕ • if (w, w ′ ) ∈ R(a -p ) then V(w ′ ) ∩ P ϕ = V(w) \ {p} ∩ P ϕ .
for every p ∈ P ϕ and every w such that (w 0 , w) ∈ R(U ϕ ). This allows us to prove by induction on the form of subformula ψ and program π occurring in ϕ that 1) M, w tr PDL (ψ) iff V(w) ∈ ||ψ|| and 2) (w, w ′ ) ∈ R(tr PDL (π)) iff (V(w), V(w ′ )) ∈ ||π|| for every w such that (w 0 , w) ∈ R(U ϕ ) and for every w ′ . For the three base cases: when the subformula ψ of ϕ is atomic then M, w tr PDL (p) iff p ∈ V(w) iff V(w) ∈ ||p||;

when the program π occurring in ϕ is of the form +p then

(w, w ′ ) ∈ R(a +p ) iff V(w ′ ) = V(w) ∪ {p} iff (V(w), V(w ′ )) ∈ ||+p||;
and similarly for -p. For the induction step the only interesting case is that of the modal operator. We have:

M, w tr PDL ( π ψ) iff M, w tr PDL (π) tr PDL (ψ) iff there is w ′ s.t. (w, w ′ ) ∈ R(tr PDL (π))
and M, w ′ tr PDL (ψ) iff there is

w ′ s.t. (V(w), V(w ′ )) ∈ ||π|| and V(w ′ ) ∈ ||ψ|| (by I.H.) iff V(w ′ ) ∈ || π ψ||
This ends the proof of Proposition 16.

To conclude, Theorem 6 follows from Proposition 16, the fact that tr PDL (.) is a satisfiability preserving polynomial transformation, and Proposition 2.

VII. Extensions

We now discuss some extensions of our basic logic DL-PA.

A. More general assignments

Our assignments are more restricted than those of [START_REF] Ditmarsch | Dynamic epistemic logic with assignment[END_REF]- [START_REF] Ditmarsch | From Situation Calculus to Dynamic Logic[END_REF]. There, assignments take the form p←ϕ: to p the truth value of ϕ is assigned, where ϕ is any formula (and not just ⊤ or ⊥ as in our DL-PA).

Programs p←ϕ can be simulated in our language by (ϕ?; +p)∪(¬ϕ?; -p). This may result in an exponential increase of formula size. However, an inspection of our proofs shows that all our complexity results also hold for the richer language with assignments p←ϕ. It remains to find out whether the language with general assignments is more succinct.

B. Other program connectives

Our logic can be extended as well by other program connectives that are familiar from PDL. We briefly discuss the properties of DL-PA extended with the converse operator " -". Its interpretation is ||π -|| = (||π||) -1 , where (||π||) -1 is the inverse of the relation ||π||.

Consider an innermost occurrence π -. Thanks to the program equivalences of Section IV, we may suppose that π is star-free. The converse operator distributes over sequential and nondeterministic composition in the usual way:

(π 1 ; π 2 ) -≡ π - 2 ; π - 1 (π 1 ∪ π 2 ) -≡ π - 1 ∪ π - 2
and when it meets a test or an atomic program it can be eliminated by means of the following equivalences:

(ψ?) -≡ ψ?

(+p) -≡ p? ∪ (p?; -p) (-p) -≡ ¬p? ∪ (¬p?; +p)

Converse DL-PA can therefore still be reduced to propositional logic.

As to complexity, the extension of DL-PA by the converse operator can be mapped into PDL with converse by extending the polynomial transformation of Section III in a straightforward way. Converse PDL being still in EXPTIME [START_REF] De Giacomo | Combining deduction and model checking into tableaux and algorithms for converse-PDL[END_REF], it follows that the satisfiability problem of converse DL-PA is EXPTIME-complete, too.

VIII. Relationship with the logics of propositional control

It was shown in [START_REF] Herzig | A dynamic logic of normative systems[END_REF] that star-free DL-PA embeds the logics based on the idea of propositional control that were recently studied in the multi-agent literature ( [START_REF] Hoek | On the logic of cooperation and propositional control[END_REF], [START_REF] Gerbrandy | Logics of propositional control[END_REF]). We give their embedding in Section VIII-A (adapting the presentation to our notation) and extend it in Section VIII-B in order to show how full DL-PA relates to Coalition Logic of Propositional Control and Delegation [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF].

A. Coalition logic of propositional control

Models of Coalition Logic of Propositional Control (CL-PC) have a twofold interpretation of propositional variables: besides the valuation function v mapping propositional variables to truth values, there is a control function ξ mapping each propositional variable to some agent in a finite set of agents A. Saying that the agent ξ(p) controls p, we mean that i can set p to true and can set p to false. As ξ is a function, control is exclusive: for every p there is at most one i controlling p. As the function ξ is total, control is also assumed exhaustive: for every p there is at least one i controlling p.

With CL-PC one can model the capabilities of agents and groups of agents to achieve a state of affairs: in the model (v, ξ), agent i is capable to achieve ϕ if there exists a valuation v ′ that differs from v only in the interpretation of the variables that are under i's control, and is such that ϕ is true in (v ′ , ξ). Formally:

|| i ϕ|| = { (v, ξ) : there is v ′ such that (v ′ , ξ) ∈ ||ϕ|| and for every p, if ξ(p) i then v(p) = v ′ (p) }
The interpretation of the coalition operator J straightforwardly generalises this truth condition.

In star-free DL-PA we can encode agent i's control over p by means of a special propositional variable c i,p . Then exclusivity and exhaustivity of control over a set of variables P ⊆ P are expressed by:

Exc(P) def = p∈P i, j∈A,i j ¬(c i,p ∧ c j,p ) Exh(P) def = p∈P i∈A c i,p
Finally, we set a translation tr such that:

tr(p) def = p if p ∈ P tr( i ϕ) def = skip ∪ (c i,p1 ?; +p 1 ) ∪ (c i,p1 ?; -p 1 ) • • • skip ∪ (c i,pn ?; +p n ) ∪ (c i,pn ?; -p n ) tr(ϕ) if P ϕ = {p 1 , . . . , p n }
and homomorphic for the boolean operators.

The following result corresponds to Theorem 4 in [START_REF] Herzig | A dynamic logic of normative systems[END_REF].

Proposition 17. A CL-PC formula ϕ is CL-PC satisfiable iff Exc(P ϕ ) ∧ Exh(P ϕ ) ∧ tr(ϕ) is (star-free) DL-PA satisfiable.

It is also clear that the lengths of Exc(P ϕ ), Exh(P ϕ ), and tr(ϕ) are all polynomial in the length of ϕ. Our translation therefore provides a polynomial embedding of CL-PC into DL-PA.

B. Coalition logic of propositional control and delegation

Coalition logic of propositional control and delegation (DCL-PC) extends CL-PC by dynamic operators of transfer of control over a propositional variable. They were called delegation programs in [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF], [START_REF] Hoek | On the dynamics of delegation, cooperation and control: a logical account[END_REF], but the term control transfer program appears to be more appropriate. Atomic control transfer programs are of the form i p j and are read "i transfers his control over p to j". The intuition is that i p j is applicable when i controls p and that it changes the control function ξ such that j gets control over p (and i looses it, control being exclusive). Complex delegation programs are defined by means of the standard PDL operators.

The interpretation of a delegation program is a binary relation on the set of models of propositional control. For atomic programs we have:

||i p j|| = ((v, ξ), (v, ξ ′ )) : ξ(p) = i, ξ ′ (p) = j, and ξ(q) = ξ ′ (q) for q p

The interpretation of complex programs and of formulas is as usual. The interpretation of π ϕ is: The other way round, DL-PA can also be translated into DCL-PC if the set of agents contains at least two agents. Let us call these agents t and f . We then encode truth of p as t controlling p and falsity of p as f controlling p. Then the atomic assignment +p corresponds to the control transfer program t p t ∪ f p t and -p corresponds to f p f ∪ t p f . The other program connectives and boolean operators of DL-PA are mapped homomorphically. It is then routine to prove that a DL-PA formula is DL-PA satisfiable if and only if its translation into the language of DCL-PC is DCL-PC satisfiable.

|| π ϕ|| = (v,
It follows that both the model checking problem and the satisfiability problem of DCL-PC are EXPTIME-hard. Provided that PSPACE EXPTIME, this contradicts the claim in [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF] that both are PSPACE-complete. 2

IX. Conclusion

Our logic DL-PA is an interesting alternative to PDL. On the one hand, we can basically reason about the same kind of phenomena as in PDL: programs changing the truths of the world. This is demonstrated by the example of the counter of Section II-C and also by our encoding of the PEEK problem in Section V-A; this is also demonstrated by the 2 The model checking algorithm in [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF] is claimed to work in nondeterministic space (NPSPACE, which is the same complexity class as PSPACE). The algorithm consists in two mutually recursive procedures calling each other that decompose formulas according to the truth conditions: a procedure deciding whether (v, ξ) ∈ ||ϕ|| [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF]Fig. 8] and a procedure deciding whether (ξ, ξ ′ ) ∈ ||π|| [START_REF] Hoek | On the logic of cooperation and the transfer of control[END_REF]Fig. 7]. However, that algorithm in fact requires alternating space (APSPACE). embeddings of Coalition Logic of Propositional Control that we have mentioned in Section VIII. On the other hand, the mathematical properties of DL-PA are better than those of PDL: DL-PA is compact, has the interpolation property, and the Kleene star can be eliminated.

Theorem 4 .

 4 The problems of DL-PA model checking and DL-PA satisfiability are both EXPTIME-hard.

  moveE def = elo?; x∈XE (-x ∪ +x); -elo moveA def = ¬elo?; ∪ y∈XA (-y ∪ +y); +elo move def = (moveE ∪ moveA) ; ((Φ?; -nowin) ∪ ¬Φ?) Now, we define

  nowin.The root is therefore now labeled by v 0 ∪ {nowin} if τ = A and byv 0 ∪ {nowin, elo} if τ = E. Then [move * ] nowin → (¬Φ∧(elo → [move]nowin)∧ (¬elo → move nowin)))is true at v because move correctly encodes the moves. ThereforeMC v, [move* ](nowin → (¬Φ∧(elo → [move]nowin)∧ (¬elo → move nowin))) returns true. The other way round, suppose MC v, [move * ](nowin → (¬Φ∧(elo → [move]nowin)∧ (¬elo → move nowin))) returns true. Consider the PDL model M DL-PA that we have built in Section III and focus on the relation R(move). The alternating application of the actions of E and A that it gives us directly provides a winning strategy for Abelard at v. Therefore Eloise cannot have a winning strategy. Proposition 14. The DL-PA model checking problem is EXPTIME-hard.

  ξ) : there is (v ′ , ξ ′ ) such that ((v, ξ), (v ′ , ξ ′ )) ∈ ||π|| and (v ′ , ξ ′ ) ∈ ||ϕ||We extend tr to provide a translation from the richer language of DCL-PC into the one of DL-PA. The key clauses are:tr( π ϕ) def = tr(π) tr(ϕ) tr(ϕ?) def = tr(ϕ)? tr(i q j) def = c i,p ? ; -c i,p ; +c j,p Theorem 7. A DCL-PC formula ϕ is DCL-PC satisfiable iff Exc(P ϕ ) ∧ Exh(P ϕ ) ∧ tr(ϕ) is DL-PA satisfiable.

  Two formulas ϕ and ϕ ′ are formula-equivalent (or logically equivalent) if ||ϕ|| = ||ϕ ′ ||, i.e., if ϕ ↔ ϕ ′ is DL-PA valid. Two programs π and π ′ are program-equivalent, in symbols π ≡ π ′ , if ||π|| = ||π ′ ||.

	TABLE I
	Interpretation of the DL-PA connectives
	Proposition 1. Suppose p P ϕ , i.e., p does not occur in ϕ.
	Then v ∪ {p} ∈ ||ϕ|| iff v \ {p} ∈ ||ϕ||.
	The next proposition shows that the model checking prob-
	lem can be reduced in logarithmic space to the satisfiability
	problem.
	Definition 3.

  The next proposition contains a sufficient condition for the applicability of Proposition 9.Proposition 11. Suppose the assignment sequences π and π ′ have exactly the same variables, i.e., P π = P π ′ . Then π; π ′ is program-equivalent to π ′ . Proof: This follows by iterated application of the program equivalences for assignments of Proposition 10.The next proposition tells us how we can add 'dummy' assignments in order to ensure that two assignment sequences are about the same variables. By Proposition 4(5), π is equivalent to skip; π.

	Proposition 12. Every program π is program-equivalent to
	(p?; +p; π) ∪ (¬p?; -p; π).
	By Proposition 4(8), the latter is equivalent to
	(p? ∪ ¬p?); π.
	By distribution of ";" over "∪" (Proposition 4(3)) this is
	equivalent to
	(p?; π) ∪ (¬p?; π).
	Finally, the above is program-equivalent to
		1 by χ. Proposi-
	tion 5 and Proposition 4(4) allow us to permute the two tests
	ϕ 1 ? and χ 1 ?:
	ϕ 1 ?; χ?; π 1
	is program equivalent to
	χ?; ϕ 1 ?; π 1 .
	Finally, the latter is subsumed by the program ϕ 1 ? ; π 1 , in the
	sense that
	(χ?; ϕ 1 ?; π 1 ) ∪ (ϕ 1 ?; π 1 )
	is program-equivalent to ϕ 1 ? ; π 1 by Proposition 4(7) .
	Proposition 10. The following program equivalences are
	DL-PA valid:
	p?; +p ≡ p?
	¬p?; -p ≡ ¬p?
	±p; +p ≡ +p
	±p; -p ≡ -p
	±p; +q ≡ +q; ±p	if p q
	±p; -q ≡ -q; ±p	if p q

Proof: (p?; +p; π) ∪ (¬p?; -p; π) due to the first two program equivalences of Proposition 10.

This corrects an error in the published version of[START_REF] Herzig | A dynamic logic of normative systems[END_REF] that was already signaled by an erratum of a few lines on the IJCAI website.

Acknowledgment

We are grateful to a reviewer whose detailed comments helped improve the presentation. First and second authors acknowledge the support of the ANR 11 BS02 011 03 grant (project DynRes), while the third author acknowledges the support of the program Marie Curie People Action Trentino (project LASTS).


!"# $$# %&# "!# "# &# ' '# ()*+,'-# +# *+#
The assembly loop

IP assembly = communications and reductions

Exact arithmetic sequential parallel

V (i) = D k V (i) subdomains D k , k = 1...p V (i) = a V (i1) = b V (i2) = c V (i) = b + c = a

IP assembly = communications and reductions

Floating point arithmetic sequential parallel

V (i) = D k V (i) subdomains D k , k = 1...p V (i) = a V (i1) = b V (i2) = c V (i) = b ⊕ c = a
Interface point assembly Interface node assembly:

AM1 in each iteration CV 2 = Bu -AuhH, CV 3 = Bv -AvhH.
Interface node assembly:

CV 2, CV 3 System equation Ay = b AM2, AM3 : diagonal matrices, AM1 = Ahh -AhuAM2 -1 Auh -Ahv AM3 -1 Avh, CV 1 = Bh -AhuAM2 -1 Bu -Ahv AM3 -1 Bv ,
Interface node assembly:

AM2, AM3, CV 1    A hh A hu A hv A uh Auu 0 A vh 0 Avv      H U V   =    B h Bu Bv    algebraic transformation   AM1 0 0 0 AM2 0 0 0 AM3     H U V   =   CV 1 CV 2 CV 3   Mesh (elements,
AM1 = Ahh -AhuAM2 -1 Auh -Ahv AM3 -1 Avh, CV 1 = Bh -AhuAM2 -1 Bu -Ahv AM3 -1 Bv , Interface node assembly: AM2, AM3, CV 1    A hh A hu A hv A uh Auu 0 A vh 0 Avv      H U V   =    B h Bu Bv    algebraic transformation   AM1 0 0 0 AM2 0 0 0 AM3     H U V   =   CV 1 CV 2 CV 3   Mesh (elements,
((a⊕b)⊕(c⊕d)) ⊕ ((e 1 ⊕ e 2 ) ⊕ e 3 ) = (((a⊕b)⊕c)⊕d) ⊕((f 1 ⊕ f 2 ) ⊕ f 3 ) IEEE binary64 (double): x 1 = 2 53 -1, x 2 = 2 53 and x 3 = -(2 54 -2).
Exact sum:

x 1 + x 2 + x 3 = 1.
Classic summation

2 54 -1 0 2 53 -1 2 53 -(2 54 -2) 2
Relative error = 1

Compensation of the rounding errors

2 54 0 -1 2 53 -1 2 53 -(2 54 -2) 1 2 -1
The exact result is computed

!" !!! "#$%!&! ! '%! (#$%!&! )*! + ! ' "#$%&"#$%*(#$% ) + '
,(!-../0123! 45'67$186$5'! %!957!/:/73!'5;/!0/.<!$!1/25'=$'=!65!/2/0/'6!/ /'!! 450>86-6$5'!-';!-??8082-6$5'!59!758';$'=!/7757.! 450>/'.-6$5'!59!6</!,(!-../0123!957!/:/73!0/.<!'5;/!@! The parallel case is easy to derive

!"# $$# %&# "# &# )#
678#.9:/",#;9:# ###678#.<=<>/",#;<=<># ########./0123#+.<=<>,#.9:-#### ########4+.-/4+.-5#?+.<=<>,#.9:-## Reproducible conjugate gradient Hardware and software env.

!"! !#$ !%! ! ! ! ! ! "#$%!&!"#$%!'!"#$%!'!"#$%! ! !!!(#$%!&!##(#$%!'!(#$%!')*%'!(#$%')+%!!!!!! "#$%!&!,-#./%!'!,-#.0%!'12'!,-#.3%! ! ! (#$%!&!4*'!4+'1'!43! "#$%&"#$%'(#$%!
Initialization: r 0 = AX 0 -B; a given d 0 ρ 0 = (r 0 , d 0 ) (Ad 0 , d 0 ) ; X 1 = X 0 -ρ 0 d 0 Iterations: r m = r m-1 -ρ m-1 Ad m-1 d m = r m + (r m , r m ) (r m-1 , r m-1 ) d m-1 ρ m = (r m , d m ) (d m , Ad m ) X m+1 = X m -ρ m d m A=[AM1, E AM1 ]
socket: Xeon E5-2660 (L3 cache = 20 M).

2 cores, 8 cores on each socket.

OpenMP 4.0 (Intra socket parallelism).

Compare vs. Intel MKL 11

To conclude

Feasibility ?

Do existing techniques easily provide reproducibility to large scale industrial scientific software?

Efficiency ?

Do correctly rounded summation algorithms provide efficient implementations of reproducible parallel BLAS routines?

A

  five year old dam break: 433 dead people and huge damage Simulation mesh: 26000 elements and 53000 nodes Simulation: 2200 seconds with a 2 sec. time step A rule → 10 18 flop/sec in 2020 Massive and heterogeneous parallelism : 1 million of computing units Numerical simulation of complex and sensitive physical phenomena Moore's rule → 10 18 flop/sec in 2020 Massive and heterogeneous parallelism : 1 million of computing units Numerical simulation of complex and sensitive physical phenomena Numerical reproductibility failure of finite precision computations Non associative floating-point addition Computed value depends on the operation order Reproducibility failures reported in numerical simulations for energy [12], dynamical weather science [4], dynamical molecular [11], dynamical fluid [8] When? why? Operation order uncertainty for consecutive executions of a given binary file Appears both in parallel and "sequential+SIMD" environments When? why? Operation order uncertainty for consecutive executions of a given binary file Appears both in parallel and "sequential+SIMD" environments Parallel reduction: SIMD, openMP, MPI, GPU Let p be the number of computing units When p varies, the partial computed values before the reduction also vary For a given p > 2, the computed reduced value depends on the dynamic scheduling of the reduction: omp, mpi, gpu Reproducibility = Portability Portability : one source → different binaries Parameters: compilers and their options, librairies, OS, comput. units Reproducibility may fail for a given set of portability parameters Reproducibility = Accuracy Reproducibility: bitwise identical results for every p-parallel run, p ≥ 1 Full accuracy = unit roundoff accuracy = bitwise exact result Improving accuracy up to correct rounding ⇒ reproducibility Reproducibility = Portability Portability : one source → different binaries Parameters: compilers and their options, librairies, OS, comput. units Reproducibility may fail for a given set of portability parameters Reproducibility = Accuracy Reproducibility: bitwise identical results for every p-parallel run, p ≥ 1 Full accuracy = unit roundoff accuracy = bitwise exact result

  for idp = 1, ndp //idp: triangular local numbering (ndp=3) for ielem = 1, nelem i = IKLE(ielem, idp) V(i) = V(i) + W(ielem, idp) //i: domain global numbering Assembly step principle: V (i) = elements W e (i) compute the inner node values accumulate W e for every ielem that contains i for idp = 1, ndp //idp: triangular local numbering (ndp=3) for ielem = 1, nelem i = IKLE(ielem, idp) <--LOOP INDEX INDIRECTION V(i) = V(i) + W(ielem, idp) //i: domain global numbering Parallel FE: subdomain decomposition

  non-reproducibility to compute reproducible system and solutions System equation Ay = b AM2, AM3 : diagonal matrices,

  Rounding errors are computed with EFT 2Sum (Knuth, 65), Fast2Sum (Dekker, 71) for base ≤ 2 and RTN. a + b = x + y , with a, b, x, y ∈ F and x = a ⊕ b. Algorithm (Knuth) function [x,y] = 2Sum(a,b) x = a ⊕ b z = x a y = (a (x z)) ⊕ (b z) Algorithm (|a| > |b|, Dekker) function [x,y] = Fast2Sum(a,b) x = a ⊕ b z = x a y = b z Existing techniques to recover numerical reproducibility in summation Accurate compensated summation [6

A=

  ;$3!<(!;==.:7>?2!! @93AB$76C93!,-#.D%!E9B!.F.B?!398.!:.=G!$!7.>93H$3H!A9!.>.:!./I12I!.3!! @9:J6A;C93!;38!;KK6:6>;C93!9E!B9638$3H!.BB9B=!4!! L3A.BE;K.!J9$3A!;==.:7>?! !$!M!$3A.BE;K.!J9$3A!7.AN..3!O*IO+IOP! QKK6:6>;C93!9E!.BB9B=!!4!;38!)!! @9:J.3=;C93!9E!AG.!<(!;==.:7>?!E9B!.F.B?!:.=G!398.!$! "#$%I!(#$%! "#$%I!(#$%! =$:$>;B! =$:$>;B! =$:$>;B! =$:$>;B!Interface Point assemblyTowards a reproducible conjugate gradientInitialization: r 0 = AX 0 -B; a given d 0 ρ 0 = (r 0 , d 0 ) (Ad 0 , d 0 ) ; X 1 = X 0 -ρ 0 d 0 Iterations: r m = r m-1 -ρ m-1 Ad m-1 d m = r m + (r m , r m ) (r m-1 , r m-1 ) d m-1 ρ m = (r m , d m ) (d m , Ad m ) X m+1 = X m -ρ m d m

  length n → sum of length 2n A correctly rounded result is reproducible A large panel of algorithms for faithful or correctly rounded sums Motivation How to benefit from these CR sums for reproducible BLAS? Is the over-cost acceptable in practice for reproducible BLAS? Current results BLAS 1 : asum, dot, norm2 openMP for shared memory Hybrid openMP-MPI for shared+distributed memory Parallel BLAS-1: Runtime overcost for reproducibility Runtime/size of parallel level 1 BLAS, up to 16 threads, cond=10 32

  Assembly step: example of reproducibility failure Sequential vs. p-parallel results differ for p = 2, 4, 8, 16Assembly with the classical floating-point accumulation sequential FPAss vs. p-parallel FPAss p

	Telemac2D finite element method (FE)
	Culprits: theory Solution U,V
	max |FPAssp -FPAss|/|FPAss| Building step: interface point assembly Basic ingredients wave equation
	10 Recovering reproducibility in a finite element resolution 20 30 40 50 60 70 Time step 10 -17 10 -16 10 -15 FPAss P=2 FPAss P=4 FPAss P=8 FPAss P=16 Compensation Reproducible parallel FE assembly Reproducible conjugate gradient Efficient and reproducible BLAS 1 Conclusion and work in progress Culprits: practice = optimizations Element-by-element storage of FE matrix and second member Wave equation and associated algebraic transformations Interface point assembly and system solving are merged Maximum Relative Error vs. Sequential Computation Sources of non reproducibility in Telemac2D conjugate gradient 10 -14 Finite element assembly: sequential and parallel cases Resolution with conjugate gradient: matrix-vector and dot products Solution H
	Mean frequency wave, Nice test case, Tomawac

 x 1 = 2 53 -1, x 2 = 2 53 andx 3 = -(2 54 -2). Exact sum:

Recovering reproducibility in Telemac2D Overview II Hardware and software env.

OCCIGEN: 26 th supercomputer in top500 list.

4212 cores, 12 cores on each socket.

OpenMP 4.0 (Intra socket parallelism).

OpenMPI (Inter socket communications).

Configurations

#sockets = 1 .. 128.

#threads = 12 per socket.

Dataset

Entry vectors size = 10 7 .

Condition number = 10 32 .

Results

Good scaling for large datasets.

Two communications cost limits ReprodDot and FastReprodDot.

We need only one communication for OneReduction, HybridSum and OnlineExact.

Time to conclude

Motivations