Bernard Monjardet
email: monjarde@univ-paris1.fr

Social choice theory and the "Centre de Mathématique Sociale": Some historical notes

Keywords: distributive lattice, effet Condorcet, Guilbaud's theorem, median, metric, permutoedre, simple game, ultrafilter JEL classification number: D71, B21

In this paper we describe some research directions in social choice and aggregation theory taken at the "Centre de Mathématique Sociale" since the fifties. We begin by presenting some institutional aspects concerning this center. Then we sketch a thematic history by considering the following questions about the "effet Condorcet" ("voting paradox"): What is it? How is it overcome? Why does it occur? These questions were adressed in Guilbaud's 1952 paper (Les théories de l'intérêt général et le problème logique de l'agrégation) which will mark the beginning of our inquiry. The conclusion outlines some more recent research developments linked to these questions.

1 1 Introduction Arrow's book Social Choice and Individual Values appeared in 1951 and immediately caused a considerable interest as well as critical discussions. In May 1952 Arrow went to the Conference on Risk held at Marseille and then to Paris where François Perroux head of the "Institut des Sciences Économiques Appliquées (ISEA)" had asked him to make a presentation of his work. The lecture entitled The rationality principle in collective decisions was given on 9 June 1952 at the Institute. Translated into French under the title Le principe de rationalité dans les décisions collectives it was published in a special issue of Économie appliquée 1 devoted to welfare economics and called L'avantage collectif. This same issue contained Guilbaud's paper Les théories de l'intérêt général et le problème logique de l'agrégation (Theories of the general interest and the logical problem of aggregation) 2 . Guilbaud, a mathematician 3 , was then one of the two assistant heads of the ISEA. Although Guilbaud's appointment to the 6th section of the "Ecole Pratique des Hautes Études" (EPHE now EHESS) took place only three years later, this paper must be taken as our departure point for our historical inquiry on the theory of social choice at the center created by Guilbaud. Indeed as we will see almost all the work in this field made at the center had its origin in ideas presented in this paper.

We have just spoken of "historical inquiry". But there are several ways to do the history of science. Here we will begin by the institutional history and then we will develop a thematic history. For the first one, we will first present the institutions and their members, then some scientific activities of these members (seminars, conferences, publications...) and in particular those related to the theories of decision and voting. The thematic history will be presented by considering the following questions about the "effet Condorcet": What is it? How is it overcome? Why does it occur? In our conclusion we will outline some developments of researches linked to these questions.

Institutional history

The "École des Hautes Études en Sciences Sociales (EHESS) 4 " is probably the most highly reputed French institution for social sciences researches (from history to linguistics through economy, demography, cognitive science, social psychology, sociology, anthropology, ethnology, geography....). Until 1975 when the École took its independance, it was just the sixth section of the "École Pratique des Hautes Études (EPHE)" 5 . In 1955 the president of the sixth section was the historian Lucien Febvre and secretary, the historian Fernand Braudel. Guilbaud, then 44 years old, was just leaving Perroux's Institute (ISEA). Claude Levi-Strauss and Charles Morazé, two members of the sixth section, asked him to join them as "directeur d'études" at the École (a position equivalent to a position of full professor at university) and he was elected this same year. Guilbaud presented to Febvre his project to do "de la mathématique sociale, à la Condorcet" 6 . He proposed to call his research group "Groupe de Mathématique Sociale", but Braudel asked him to add "et de Statistique" (so the acronym was GMSS) 7 . The group grew regularly by the addition of new members 8 of which we give only the names of those (more or less) concerned with social choice theory: Marc Barbut (1956), Pierre Rosenstiehl (1960), Bernard Monjardet (1963), Bruno Leclerc (1967) and Jacqueline Feldman (1967-1969). There were also (and there are still) more or less closely associated members like Jean-Pierre Barthélemy (now member) or Olivier Hudry. Note that all these persons, except J. Feldman who was a physicist, were mathematicians sometimes working also in computer sciences.

The first task of a "directeur d'études" to the École is to give seminars for advanced students and researchers. The title of Guilbaud's first seminar was Modèles mathématiques dans les sciences sociales (Mathematical models in social sciences) and he or others like Barbut gave such seminars up to now. In the sixties there was a great interest among many social scientists in the use of mathematical models 9 and several of them attended regularly these seminars. At the same time the mathematicians of the CAMS (see footnote 7) worked, or tried to work, since it was not necessarily easy, as well with historians (as Emmanuel Leroy-Ladurie), teaching of the sciences than the one given by the universities. In 1975 it contained six sections of which the most important were the sixth (created in 1947) and in 2002 it has only three sections (life and earth sciences, history and philology sciences, religious sciences). 6 See Mathématique sociale, Entretien avec G.Th. Guilbaud, Savoir et Mémoire n°4, Éditions de l'EHESS, Paris, 1993, and Rosenstiehl P, La mathématique et l'École. In Revel J, Wachtel N (eds) Une École pour les sciences sociales. Cerf and Éditions de l'EHESS, Paris, 1996. 7 When the "groupe" grew it became a "centre", and after some terminological variations it is now called "Centre d'Analyse et de Mathématique Sociale (CAMS)". Henceforth we will use only (so sometimes anachronistically) this acronym CAMS in our text. 8 The center has presently 25 members, plus some retired former members but still working at the center. 9 See for instance Armatte M, Feldman J, Leclerc B, Monjardet B, Schiltz MA, Selz Laurière M, (1989) ethnologists (as Claude Levi-Strauss), linguists and psycholinguists (as François Bresson). The relations with economists either of the École as Edmond Malinvaud or associated member of the École as André Nataf were important during the sixties 10 . Traditional seminars with presentations by invited lecturers were also created like Méthodes mathématiques dans les sciences sociales (Mathematical methods in social sciences) by Guilbaud and Barbut (1960-1963) To organize meetings is another classic scientific activity. Among the many conferences organised (completely or partially) by CAMS members the following were in the fields of choice and decision theory (the name of organizers and the place of the meeting are in parentheses): 1960, "La décision I" (Georges Darmois and G.Th. Guilbaud, Paris); 1967, "La décision II" (G.Th.Guilbaud and M. Barbut, Aix-en-Provence); 1971, "Ordres totaux finis" (M. Barbut Many centers of the École have created journals in their fields of research. The CAMS journal Mathématiques et Sciences humaines was created by Barbut in 1962 15 . Among the special issues of this journal one 10 For the relations between the mathematicians and some social scientists of the École see the references given in footnote 6. 11 The present organizers of this seminar are J.P. Barthélemy,O. Hudry,Marc Demange,B. Leclerc,and B. Monjardet. 12 Presently Michel Armatte, Bernard Bru and Thierry Martin are also organizers of this seminar. 13 TRAP is the acronym of "Table Ronde sur l'Agrégation des Préférences". 14 Although J. Feldman was no longer a member of CAMS at this time, one can mention also the Conference organized in 1991 at the École: "Moyenne, Milieu, Centre" (J. Feldman, G. Lagneau and B. Matalon, Paris). 15 An aim of this journal was also to promote exchanges between people teaching mathematics and statistics for social sciences and those teaching these sciences. In fact CAMS members and especially Guilbaud and Barbut played a significant role in the starting and the development of mathematical training courses for students in economics, psychology and sociology. In particular Barbut was one of the initiators of the creation of a new curriculum "Applied Mathematics and Social Sciences" presently existing in more than 30 french universities. can quote: "Opinions et scrutins" (Opinions and votes, 1973), "Modélisation des préférences et quasiordres" (Preferences modelization and semiorders, 1978), "Métriques et relations" (Metrics and relations, 1979), "Condorcet" (1990). Note that another special issue "Cinquante ans de théorie du choix social" (Fifty years of social choice theory) will appear in 2003. On the other hand, for instance between the years 1962 and 1980, 49 papers were published in the fields "Décisions, préférences, procédures de vote". 16

Thematic history

As said above our leading clue for this historic inquiry will be Guilbaud's 1952 paper Les théories de l'intérêt général et le problème logique de l'agrégation. But we have first to recall one of the major contributions of this paper. By dragging from the deep oblivion where it had fallen Condorcet's " Essai sur l'application de l'analyse à la probabilité des décisions rendues à la pluralité des voix" 17 (Paris, 1785) and by recalling Condorcet's significant approaches to the topic adressed by Arrow, Guilbaud was knotting again the broken thread of a history, which was in fact a long history 18 . Indeed the Essai had been read only by a few people including Daunou, Lhuillier 19 and Lacroix. But in France reputed mathematicians like Joseph Bertrand found the book unreadable and anyway without interest, an opinion shared by Todhunter who at least had read the Essai 20 . Guilbaud was the first to read again the Essai and more generally Condorcet's works on "la mathématique sociale". Moreover he suggested to his colleague epistemologist Gilles Granger to do researches on this topic, researches which led to Granger's book "La mathématique sociale du marquis de Condorcet" (1956). 16 One must point out that during these years the quasi totality of these papers were published in French, a fact that didn't favor their knowledge by an international audience. 17 Henceforth we will call Condorcet 's book simply the Essai. 18 The famous "Annales's school" of historians of the École (and in particular Braudel) supported the notion of the "long history". 19 Daunou and Lhuillier worked on voting procedures at the end of 18th century and the beginning of 19th century and both quote the Essai (see McLean I (1995) The first golden age of social choice 1784-1803. In: Barnett W, Moulin H, Salles M, Schofield N (eds) Social choice, Welfare and Ethics. Cambridge University Press, pp 13-33). 20 In his book An history of the mathematical theory of probability from the time of Pascal to that of Laplace (MacMillan, London, 1865), In fact Todhunter devotes a chapter to a detailed analysis of the Essai but he completely misses the significance of Condorcet's study on the systems of propositions and their possible contradictions ("these results however appear of too little value to detain us any longer", page 375).

Guilbaud's paper was published in "Économie Appliquée", an economics journal, but it was written both for economists and mathematicians, a not so easy task 21 . The paper, like Arrow's book, uses finite mathematical structures, in particular binary relations and families of sets on finite sets 22 . We recall now the classical notations used in social choice theory for such structures. A = {x,y,z,...} is a finite set of m elements called alternatives (or issues, decisions, outcomes, candidates, objects, etc.). N = {1,2,.....n} is a finite set of n elements called voters (or agents, persons, individuals, criteria, etc.). The preference of a voter on the set A is given by a linear order 23 L = x 1 ...x k ...x m , where x 1 is the most preferred alternative, x 2 the second one, etc. If alternative x is preferred to alternative y in the linear order L, we write xLy or (x,y) L. More generally, if R is an arbitrary binary relation on A, we write xRy or (x,y) R when x is in the relation R with y. We denote by L the set of all linear orders on A:

L L L L = {linear orders L on A}. 21 Economists (with sufficient mathematical training) appreciated the paper (in the second edition of his book, Arrow describes it as a "remarkable exposition of the theory of collective choice and the general problem of aggregation"). But few mathematicians, -too often unaware or even contemptuous of social sciences-read it. 22 It is interesting to mention that Arrow had been introduced to such mathematics by Tarski. 23 Condorcet and most of his followers expressed the preference of a voter by such a linear order, i.e. by a transitive, antisymmetric and complete binary relation. Arrow expressed this preference by a weak order (called by him ordering and by others quasiordering or complete preorder or etc.), i.e. by a transitive and complete binary relation. We can now define Condorcet's majority rule(s) and the "effet Condorcet".

A profile ¡ = (L 1 ,...,L n ) is a function ¡ of N into L,

1 The Condorcet effect and its frequency

As is well known Condorcet proposed to adopt as a voting procedure the method retaining for each pair of alternatives the one (or the ones) supported by a majority of voters24 . For a given profile ¥ , we denote by R MAJ (¥ ) (respectively R SMAJ (¥ )) the binary relation obtained by using the majority (respectively the strict majority). Formally

x R MAJ (¥ ) y if N¤ (x,y) ¨ MAJ (i.e. if n¤ (x,y) ¦ n/2), x R SMAJ (¥ ) y if N¤ (x,y) ¨ SMAJ (i.e. if n¤ (x,y) > n/2)).
We call Condorcet's rule (respectively Condorcet's strict rule) the aggregation rule obtained by associating with each profile ¥ the relation R MAJ (¥ ) (respectively R SMAJ ). Note that when the number of voters is odd there is a single majority rule. Now Condorcet's majority rules are not L-preference aggregation functions since the majority preference relations can have cycles of length k (called k-cycles) greater than 2 (i.e. there can exist k ¦ 3 distinct alternatives

x 1 ,x 2 ,....x k such that for instance x 1 R MAJ x 2 R MAJ x 3 .......x k R MAJ x 1 ).This fact discovered by Condorcet has been called "l'effet Condorcet" by Guilbaud. It is also known as the "paradox of voting". But we prefer the term "Condorcet effect" since as it will be shown in section 3.3 this effect is unavoidable and thus not really paradoxical.

The simplest case of such an effect is obtained for three alternatives x,y,z and three voters with the preferences xyz, yzx and zxy. The collective preference is then the 3-cycle shown in Figure 1.

Figure 1. HERE A 3-cycle

Before trying to deal with the Condorcet effect a preliminary question has to be asked: is it frequent? 25 Guilbaud studies the case of three alternatives. He gives the frequency of the Condorcet effect for a number of voters respectively equal to 3 (5,6%), 4 (7%), 9 (7,8%) and 25 (8,4%) and a formula for this value when n goes to infinity: (1-3/© )Arccos(1/

)) = 0,08774. Since this formula was given in a footnote without explanation it intrigued somehow. But since Guilbaud's result there has been a considerable amount of work studying the probability of the effect or the weaker probability to have no Condorcet winner 26 . The general conclusion of these investigations is that the Condorcet effect is frequent especially when the numbers of alternatives and/or the number of voters is large. For instance if this frequency remains always small for three alternatives, it is 49% for 3 voters and 6 alternatives and about 96% for 25 voters and 9 alternatives (a situation quite possible in academic committees). Then if one is inclined to use majority rules as much as possible one must find ways to overcome this effect when it occurs. This was the real question raised by Condorcet and we will see below (in section 3.2.2) what was probably his answer. But more generally we will consider three approaches presented in Guilbaud's paper to overcome this effect. 25 In Black's book (The Theory of Committees and Elections (1958) Cambridge University Press, Cambridge) the answer is given for three voters and three alternatives. In 1803 Daunou writes that the Condorcet effect "is by no means a rare occurence", but his assertion is based on wrong computations (See Mémoire sur les élections au scrutin, published in English translation In McLean I, Urken AB (eds) Classics of social choice. The University of Michigan Press, Ann Arbor, 1995, pp 237-276, page 243). 26 See for instance a review of such works in Gehrlein WV (1983) Condorcet's paradox. Theory and Decision 15: 161-197. Note that the computation of the frequency is equivalent to computing the probability of the effet Condorcet under the so-called probabilistic model of "impartial culture" where each linear order has the same probability (1/m!) of being adopted by each voter. In this case Guilbaud's formula has been generalized (for instance in Gehrlein WV, Fishburn PC (1976) Probabilities of election outcomes for large electorates. Journal of Economic Theory 13: 14-25). More generally the probability of the effect has been studied when the preferences of the voters follow various probability models (see again Gehrlein's 1983 paper).

T o o v e r c o m e t h e C o n d o r c e t e f f e c t ?

T o o v e r c o m e t h e C o n d o r c e t e f f e c t ? the generalized majorities rules

Condorcet's majority rule is defined by taking in each pairwise comparison of alternatives the preference supported by a majority, where a majority has been defined as a set of at least half of the voters. One can ask if by changing the size of majorities one can get a rule which will avoid the Condorcet effect. It is certainly possible in some sense. For instance if one requires now unanimity in order to have x preferred to y, then the collective preference obtained has no cycles since it is the partial order intersection of the linear orders of the voters. But this collective preference has no reason to be complete, i.e. to be a linear order and so we don't get a L-preference aggregation function. In fact such a unanimity rule can often lead to an indecisiveness that is not very satisfying. Guilbaud proposes to call such a simple game a family of generalized majorities and he considers the associated generalized majority rules:

The preference aggregation function f associated with the simple game is given by: for every L N , f ( ) = R ( ), where for all x,y A, xR ( )y N (x,y) . The term simple game to name this mathematical structure was justified in the context of Von Neumann and Morgenstern's book. But in fact such a structure appears in many fields of mathematics where to use the term simple game would be absurd. Unfortunately such an terminological absurdity has became unavoidable in social choice theory (note that from a mathematical point of view a simple game is nothing more than an order filter in the Boolean lattice of all subsets of S). n/2}. The unanimity rule is also a generalized majority rule since it is obtained by taking = {N}. More generally one can call "oligarchic" the generalized majority rule obtained for the simple game V = {W N : V W} where ! V N. Indeed such a rule amounts to take as collective preference the unanimous preferences of the voters belonging to V and ignoring the preferences of the other voters. A particular case is obtained for V = {i}. Then {i} is the family of subsets of N containing i and the associated rule can be called a dictatorial rule since the collective preference is always the preference of the voter i. Now the problem is to determine among all these generalized majority rules those that always induce a linear order, i. e. to determine the preference aggregation functions f that are L-preference aggregation functions. The answer is given in Guilbaud's paper and we will call it Guilbaud's theorem 29 : Observe that = {i} is equivalent to saying that is an ultrafilter 30 since when N is finite the ultrafilters on N are exactly the n families {i} (i

Let

# N).
It is instructive to sketch the very simple proof. First one checks that the collective preference R ($ ) is antisymmetric and complete (i.e. a so- 29 In fact this theorem is a consequence of a more general result proved by Guilbaud and concerning a logical problem already raised by Condorcet. Let a set of binary ("yes or no") questions be logically linked in the sense that the answers to some imply the answers to others. A coherent opinion of an individual is defined as a set of answers to these questions respecting their links. What are the rules allowing one to aggregate several coherent individual opinions into a coherent collective opinion ? Guilbaud proves that if the aggregation rule must preserve all the possible logical links between these questions, then it must be dictatorial (page 306). A contrario, the use of, for instance, the majority rule can lead to an incoherent collective opinion, a fact called also "Condorcet effect" by Guilbaud. It is interesting to observe that this much more general Condorcet effect has been rediscovered in the eighties under the name of the "doctrinal paradox" and has led to results similar to Guilbaud's results (see List C, Pettit P (2002) Aggregating Sets of Judgments: An Impossibility Result. Economics and Philosophy 18: 89-110 and a bibliography at http://www.nuff.ox.ac.uk/users/list/ doctrinalparadox.htm). 30 A filter on a set N is an order ideal (U % and U & V imply V % ), is stable by intersection (U, V % imply U' V % ) and does not contain the empty set. An ultrafilter is a maximal filter, i.e. a filter which is not strictly contained in another filter.

called tournament) for all profiles ( if and only if is a so-called proper and strong simple game, i.e. satisfies the following condition:

U ) 0 N\U 1 (1)
Now easy and well known results on tournaments say that a tournament is transitive (i.e. a linear order) if and only if it has no cycles and if and only if it has no 3-cycles (as in Figure 1). But to avoid a 3-cycle in R (( ) it is necessary and sufficient that satisfies the following condition:

for all U, V, W 1 , U2 V2 W 3 4 (2)
Indeed in this case one cannot have three (generalized) majorities U,V,W and three alternatives x,y,z, with x preferred to y (respectively y preferred to z and z preferred to x) for each voter of U (respectively of V and W) since then a voter belonging to U2 V2 W would have a 3-cycle in his (her) linear order of preference. And conversely if there exists U, V, W 1 such that U2 V2 W = 4 , it is easy to construct a profile for which there will be a 3-cycle on a set {x,y,z} of three alternatives. It remains now to prove that a simple game satisfying condition (1) and ( 2) is an ultrafilter, which is easy.

Remarks 1) Recall that Arrow's theorem says that an independent and Paretian 31 social welfare function W N 5 W (set of all weak orders on A) is dictatorial (in the sense that the strict preference of the dictator is the collective strict preference). One can get Arrow's theorem from Guilbaud's theorem. First one shows that an independent and Paretian L-preference aggregation function f is a preference aggregation function f associated with a simple game ( is the family of the decisive sets of f). By applying Guilbaud's theorem one gets that f is dictatorial. This result is extended to weak orders by using a domain restriction standard argument, probably found in Blau 32 for the first time. But obviously Arrow's proof in the second edition of his book or in his 1952 paper in French is direct and quicker. 31 A social welfare function is independent (of irrelevant alternatives) if the social preference on two alternatives depends only on the individual preferences on these alternatives and it is Paretian if x is socially (strictly) preferred to y if all the voters prefer (strictly) x to y. 32 See Blau JH (1979) Semiorders and collective choice. Journal of Economic Theory 29: 195-206. Wilson (Wilson RB (1972) Social choice theory without the Pareto principle. Journal of Economic Theory 5: 478-486) proved also that Arrow's theorem could be obtained from the linear order version of this theorem, but his proof of this version which results from his general theory of aggregation is remarkably complicated.

2) The term ultrafilter does not appear explicitly in Guilbaud's paper. But it suffices to read his proof to see that "followers of Bourbaki will notice an ultrafilter in the background" as Blau 33 would have said and as I observed it later: "then it is immediate that in the Boolean algebra of subsets of N, must be a maximal filter" 34 .

3) The characterization of ultrafilters given above can be improved. Indeed one has the following result: a family on an arbitrary set N is an ultrafilter if and only if it is strong and satisfies condition (2) 35 . Note also that this last condition can be written 6 7 ) > 3, where 6 7 ) is Nakamura's number of so that Nakamura's theorem on simple games can be seen as a generalization of Guilbaud's theorem (a point of view developped in my 2003 paper quoted in the Annex). 4) Guilbaud's theorem is in fact a characterization of the functions L N 8 L that are projections. This is an interesting mathematical result which can have links with other such projection characterization results for mathematical structures like vector spaces and posets 36 .

T o o v e r c o m e t h e C o n d o r c e t e f f e c t ? the Condorcet (median) procedure

A big problem of Condorcet was to remedy the defect of his majority rule and he addressed it in several places in the Essai. Since his proposals are not necessarily very clear and can vary, several interpretations of what he has in mind have been given 37 . Let us quote Guilbaud's interpretation: "Condorcet could not resign himself to conclude that it is impossible to attribute any coherent opinion 38 to the electoral body (......). He looks for lesser evil, that is to say among all the coherent opinions the one which is supported by the largest possible number of votes" 39 .

33 See Blau's paper in footnote 32. 34 37 See for instance Black's book quoted in footnote 25. 38 In the Essai "coherent opinion" means linear order. 39 Page 265 in the English translation of Guilbaud's paper quoted in footnote 2.

One can give a formal description of this procedure. For 9 = (L 1 ,...,L n ) an arbitrary profile in L N and L an arbitrary linear order in L, one sets:

@

(9 ,L) = A {nB (x,y), (x,y) C L}. @ (9 ,L) is a measure of agreement between the profile 9 and the possible collective preference L, since it counts the number of pairwise agreements between the preferences of the voters and the linear order L. Now the procedure described in Guilbaud's sentence consists to:

Take as the collective preference a linear order L that solves the discrete optimisation problem:

MAX{ @ (9 ,L), L C L L L L}.
For reasons that we will explain below we call this procedure the median procedure and we call median orders of a profile the corresponding linear orders obtained by applying it to this profile.

One can make several remarks on this median procedure. First this optimisation problem has at least one solution (since the set L is finite) but it can have several (an even many) solutions. It is easy to see that if there is no Condorcet effect, these solutions are given by Condorcet's majority rules. More precisely in this case and when the number of voters is odd there is a unique median order given by the two Condorcet's rules. Always in this case and when the number of voters is even one notes first that the strict majority relation R SMAJ ( 9) is a partial order contained in the majority relation R MAJ (9 ). Then there exists (at least) one linear order between (in terms of set-inclusion) these two majority relations and it is easy to understand that the median orders are all such linear orders. This is the "easy" case, whereas in the general case the computation of the solutions is a "difficult" problem40 .

Guilbaud's quotation (above) identifies Condorcet's procedure to overcome the Condorcet effect as the median procedure. In the case of three alternatives and of a Condorcet effect, Condorcet proposes to take as collective preference the linear order obtained by inverting the preference supported by the weakest majority. This is clearly equivalent to adopting the median procedure. When there are more than three alternatives, Condorcet's ambiguous proposals lead to several possible algorithms. And one can find profiles with a Condorcet effect for which none of these algorithms lead to a median order. But this is not very surprising considering the difficulty of the problem to find the median orders. On the other hand for Condorcet there is an objective linear order between the alternatives (for instance a true order of merit between candidates). The aim of the voting procedure is to find this objective order from those given by the voters and containing errors. Then, in the search for this true order, he introduces a probabilistic model to find what we would call the "maximum likelihood" order. Young's analysis of this Condorcet model led him to conclude that the orders obtained by the corresponding procedure are the median orders41 . So following Guilbaud's and Young's interpretations we will consider that Condorcet has been the creator of the median procedure for profiles of linear orders and we will call this procedure the Condorcet generalized rule.

Now we should explain why we have called it the median procedure. To do that we have to define what is a median in a metric space. Let (E,d) be an arbitrary (finite) metric space, and (x 1 ,...,x n ) an n-tuple of points in this space.

A (metric) MEDIAN of (x 1 ,...,x n ) in the metric space (E,d) is any point m of E minimizing the sum D {d(x i ,x), i = 1,...n} Here also since E is finite it is clear that the n-tuple (x 1 ,...,x n ) has at least one median. In fact it has often several medians.

It remains then to show that the median orders described above are medians in a metric space, which is easy. We take as the metric space E the set of all linear orders L endowed with the following distance:

for L,L' E L, d K (L,L') = |{pairs {x,y} such that xLy and yL'x, or xL'y and yLx}|.

Thus this quantity measures the disagreement between the two linear orders L and L' and it is a distance since it is nothing more than half of the classical symmetric distance |L\L'| + |L'\L| between these two orders 42 .

We denote this distance by d K since it has been implicitly used by Kendall as early as 1938 (the well-known Kendall "correlation coefficient" tau is nothing more than the normalization of this distance between -1 and +1) as well that by Kemeny (see below). finite any subset X of L has a meet denoted by U X and a join denoted by V X. A lattice is distributive if for all x,y,z W L, xX Y y`z) = (xX y) `(xX z). The lattice (2 E , a ) of all the subsets of a set ordered by set inclusion is a distributive lattice with intersection and union as meet and join operations (in fact it is a special kind of distributive lattice, namely a Boolean lattice). In particular (2 A 2 , a ) is the distributive lattice of all the binary relations defined on the set A. Now in a distributive lattice L there exists a "natural" distance d L generalizing the symmetric difference distance in the lattice of the subsets of a set46 . So one can consider the metric space (L,d L ) and the medians of an n-tuple b = (x 1 ,...,x n ) of elements of L. The following proposition generalizing Birkhoff and Kiss's result is due to Barbut and Monjardet 47 :

The medians of an n-tuple b = (x 1 ,...,x n ) of elements of the metric space (L, d L ), L being a distributive lattice, are all the elements of the interval

[m 1 (b ), m 2 (b )] = {x W L : m 1 (b ) c x c m 2 (b )} where m 1 (b ) = V d d U {x i , i W W}, W a {1,...n}e |W| > n/2}} and m 2 (b ) = V d d U {x i , i W W}, W a {1,...n}e |W| f n/2}}.
These two elements m 1 (b ) and m 2 (b ) (which are equal if n is odd) can be called the algebraic medians of b . The result on the medians of a profile b of linear orders in the metric space (2 A 2 , dg ) is a particular case of the above result since in the Boolean lattice

(2 A 2 , a ) one has clearly R SMAJ (b ) = h d d i {L i , i W W}, W a Ne |W| > n/2}} and R MAJ (b ) = h d d i {L i , i W W}, W a Ne |W| f n/2}}.
Another particular case of this result is the case where L is totally ordered. Then the meet and join operations are the minimum and maximum operations and one gets the usual statistical median of numbers. For instance if x 1 <x 2 <x 3 the median of these three

numbers is x 2 = Max{Min{x 1 ,x 2 }, Min{x 2 ,x 3 }, Min{x 3 ,x 1 }} = Min{Max{x 1 ,x 2 }, Max{x 2 ,x 3 }, Max{x 3 ,x 1 }}.
The fact that the majority rule is a median rule appears informally several times in Guilbaud's paper (see for instance pages 279 and 291). But it induces consequences linked to the third approach to overcome the Condorcet effect, the so-called Condorcet (or restricted or coherent) domains.

T o o v e r c o m e t h e C o n d o r c e t e f f e c t ? the restricted domains

We will use the following definition of a restricted domain of linear orders.

A set D p L of linear orders is a Condorcet domain if the use of Condorcet's strict majority rule for profiles of D never induces the Condorcet effect, i.e.:

q N finite set, q sr t D N , R SMAJ ( r ) is without cycles.

Thus a set of linear orders is a Condorcet domain if the strict majority rule applied to any profile of linear orders of the domain leads always to an asymmetric relation without cycles. Note that if |N| is odd such a relation is a linear order and that in the general case it can be always completed into a linear order. Moreover an easy consequence of this definition is that R SMAJ ( r ) is always a partial order.

One can show that a set of linear orders is a Condorcet domain if and only if the strict majority rule applied to any profile of n linear orders of the domain with n an odd integer leads always to a linear order 48 . In fact we are going to consider Condorcet domains satisfying the stronger condition of stability, namely that this linear order must belong to the domain.

The best known example of stable domain is the single-peaked domain B defined by Black 49 . Since its definition needs to take a reference linear order L considered as the "objective" order between the alternatives it is also called the domain of L-unimodal linear orders. Now one finds in Guilbaud's paper an analysis of the single-peaked domain showing that the set of single-peaked linear orders has a distributive lattice structure and that the majority relation of a profile in this domain is the median of the elements of the profile in this lattice (see page 289 and the figure showing the distributive lattice of the 16 single-peaked linear orders on a set of cardinality 5).

Using another paper by Guilbaud and Rosenstiehl 50 , one can generalize this result. Indeed Guilbaud and Rosenstiehl show that the set L of linear orders can be endowed with a lattice structure called the "permutoèdre" lattice. This lattice has an arbitrary linear order L as the greatest element and the dual of L as the least element. The unoriented covering relation of this lattice is the adjacency relation where the linear order L is adjacent to the linear order L' if they differ on a unique pair of elements. The permutoèdre lattice is not distributive but it contains distributive sublattices. We say that a sublattice of L is covering if the covering relation in this sublattice is the same as the covering relation in L.

The following result is due to Chameni-Nembua 51 : Any distributive covering sublattice of the permutoèdre lattice L is a stable domain and thus a Condorcet domain.

Indeed in this distributive lattice to take the majority relation of a profile of n (odd integer) linear orders reduces to taking the (metric or algebraic) median of these n elements. More generally the lattice interval [m 1 (u ), m 2 (u )] associated with an arbitrary profile u of linear orders in this lattice is exactly the set of linear orders containing the strict majority relation R SMAJ (u ).

Figure 2 Figure 3 shows a covering distributive sublattice of the permutoèdre lattice on 6 elements. It has 45 elements. When I discovered it in 1988 52 it was interesting since the best lower bound on the size of a Condorcet domain was then given by an Abello and Johnson's construction [START_REF] Abello | How large are transitive simple majority domains?[END_REF] which for n = 6 was 44. On the other hand Figure 3 illustrates in the case of n = 6 a general construction of Condorcet domains found later independently by Craven and Fishburn [START_REF] Craven | Majority consistent preference orderings[END_REF] .

Figure 3 HERE A Condorcet domain sublattice of the permutoèdre lattice on 6 elements.

W h y t h e C o n d o r c e t e f f e c t ?

Another significant contribution of Guilbaud's paper was to bring together the Condorcet effect and some other "paradoxes" like the paradox raised by Quetelet's "homme moyen". The statistician and social scientist Quetelet proposed to extend the notion of mean to a population of individuals [START_REF] Quetelet | Sur l'homme et le développement de ses facultés ou Essai de physique sociale[END_REF] .To do that he considers the measures of several characteristics of these individuals (size, weight, strength...) and he calculates the means of these measures for each characteristic. The problem is that a mean man so defined could be an impossible man. This fundamental objection is well presented by Cournot who writes: "When one applies mean operations to various parts of a complicated system, one must be aware that these mean values can be incompatible: the state of the system where all elements take the mean values separately determined for each could be an impossible state" 56 . And Cournot gives the example of the triangle obtained by taking the means of the lengths of the three sides of rectangular triangles, a triangle which in general is not rectangular. More generally Guilbaud considers a method of aggregation of complex objects that can be called a component-wise (algebraic) mean method. It consists first of decomposing complex objects into their simple elements, then of applying to each series of such elements an algebraic mean operation. By definition an essential property of this method is its property of independence: each series of simple elements is aggregated (by the same or by different mean operations) independently of the other series. Now as soon as the complex objects considered are defined by some relations between their simple elements, the aggregated complex object does not necessarily satisfy these same relations. In Condorcet's case the simple elements are the ordered pairs forming the linear orders and the mean operation is the majority relation taken on each pair. One can represent any binary relation R on A = {a 1 , .... a m } by a boolean vector b ij , where b ij = 1 (respectively 0) if (a i ,a j ) v R (respectively (a i ,a j ) w R).

Then linear orders are defined by the properties b ii = 1 (reflexivity), b ij + b ij = 1 (antisymmetry), b ij + b jk + b k1 x 2 (transitivity). To take the majority on each pair keeps always the first (trivial) reflexivity property. It keeps always the second one if the number of voters is odd, but it need not maintain the transitivity one, which is exactly the Condorcet effect. Note that it is no more paradoxical than the fact that the majority rule applied to a even number of complete relations can induce an incomplete relation. Formally one can consider that the objects to be aggregated are defined as p-tuples of a set X of elementary objects (or more generally as elements of a direct product y X i ).The set of all the possible objects is then X p . If all these objects are admissible the component-wise mean method for aggregating them causes no problem. But if the set S of admissible objects is a subset of X p defined by a set of formulas linking the components of the objects, then to use this method requires closure properties of the aggregation operator m with respect to : x 1 , .... x n v S (i.e. satisfy ) implies m(x 1 , .... x n ) v S (i.e. satisfy ). If not the contradictions (the socalled "paradoxes") are unavoidable.

Another merit of Guilbaud's analysis was to show that the same logical problem of aggregation was occurring in several domains. Nevertheless it was only more than thirteen years later that it was shown that the use of an independence axiom in consensus problems arising in data analysis leads to state impossibility theorems57 resulting from similar unavoidable contradictions.

Finally, Guilbaud mentioned as a possible solution to the general aggregation problem the metric method illustrated above in the case of aggregating linear orders: to calculate (metric) medians. In fact this method belongs to the classes of methods proposed by Maurice Fréchet in the forties. In his paper Réhabilitation de la notion statistique de l'homme moyen 58 , quoted by Guilbaud, Fréchet presented informally how to apply some of his mathematical results on the "typical elements" (a generalization of the central values of random variables) of arbitrary random elements in an arbitrary abstract metric space 59 . It is interesting to add that as early as 1914 the median method has been also proposed in the case of subsets of (what are now called) Euclidean spaces by the well-known Italian statistician Corrado Gini and still about "l'homme moyen" 60 .

C o n c l u s i o n

As we said in our introduction most of the researches conducted at CAMS in the domain of social choice theory and more generally of consensus theories were developments of ideas found in Guilbaud's paper. But as it is usual in science these researches of CAMS members met researches led independently elsewhere or/and inspired researches led by other people (in cooperation or not with CAMS members).

Let us mention quickly some of the research directions and results. A first direction concerns preferences and social choice theory with for instance the study of the permutoèdre and of restricted domains, or the use of ultrafilters for Arrowian or Gibbard and Satterthwaite theorems. A second direction concerns axiomatic or metric consensus theories in other fields and particularly in data analysis (consensus of partitions, classification trees etc.). Transversely to these directions many researches have concerned medians. In particular the link has been made with works made completely independently since the forties in "pure" lattice or graph theories. It is now clear what are the "good" discrete metric spaces for medians, i.e. the spaces where medians can be easily computed from algebraic formulas: they are the so-called median semilattices which contain in particular the distributive lattices and the tree semilattices 61 . The computation of medians in the "bad" cases (like those of linear orders) lead 58 Les Conférences du Palais de la Découverte, Paris, 1949. 59 Recall that the notion of distance i.e. of metric space goes back to Frechet in 1904. 60 Gini C (1914) L'uomo medio. Giornali degli economiste e revista de statistica 48: 1-24. The notion of the metric median in Euclidean spaces goes back to a problem raised by Fermat in 1629 and it has been used for location problems since Weber's 1909 book Uber den Standort der Industrien (see Monjardet B., Éléments pour une histoire de la médiane métrique, In Moyenne, Milieu, Centre. Histoires et usages (1991) Coll. Histoire des Sciences et Techniques, n°5. Éditions de l'EHESS, Paris). 61 See references in Barthélemy, Leclerc and Monjardet's 1986 paper in the Annex. to many researches to find exact algorithms and (since the problem is NPcomplete) "good" heuristics. From an axiomatic point of view the median rule has been axiomatized in many spaces [START_REF] Mcmorris | The median function on median graphs and semilattices[END_REF] . On the other hand it has for instance been shown only recently that this rule satisfies the Paretian property in the metric space defined by the symmetric difference distance between partial orders on a set, although it does not satisfy it for other distances defined between partial orders [START_REF]See Leclerc's[END_REF] . More abstractly, axiomatic or metric consensus theories have been developed in lattices, semilattices or posets, since for instance these theories allow one to derive from an Arrowian theorem in such "abstract" structures several known or new Arrowian theorems in various "concrete" domains 64 . The annex below contains the papers on the above topics written by at least a CAMS member or associate member since Guilbaud's paper in 1952. They are ranked by year of publication.

Social choice theory and the "Centre de Mathématique Sociale": Some historical notes. A Condorcet domain sublattice of the permutoèdre lattice on 6 elements.

  , Aix-en-Provence); 1981, "TRAP I 13 : Analyse et Agrégation des Préférences" (Pierre Batteau, Eric Jacquet-Lagrèze and B. Monjardet, Aix-en-Provence); 1982 "TRAP II" (Marc Roubens, Mons); 1988, "TRAP III: Modélisation, Analyse et Agrégation des Préférences et des Choix" (Louis-André Gerard-Varet and B. Monjardet, Luminy) 14 .

  describing the state of preferences of the voters on the set of alternatives. L N denotes the set of all such profiles. A L-preference aggregation function is a map f: L N ¢ L which assigns a linear order f(¡ ) -the collective preference-to each profile ¡ of individual preferences. For all x,y A, and ¡ L N , we define N£ (x,y) = {i N : xL i y}, n£ (x,y) = |N£ (x,y)|.

  So N¤ (x,y) is the set of voters preferring x to y in the profile ¥ and n¤ (x,y) is the number of these voters. A subset S of N is called a majority if |S| ¦ n/2 and a strict majority if |S| > n/2. We define MAJ = {majorities of N} = {S § N : |S| ¦ n/2}, SMAJ = {strict majorities of N} = {S § N : |S| > n/2}.

  More generally Guilbaud proposes to see if by changing the form of majorities one can obtain L-preference aggregation functions. He considers what Von Neumann and Morgenstern 27 have called a simple game 28 : A simple game on N is a non-empty set of subsets of N satisfying : [S and S U] [U ].

  Thus x is collectively preferred to y according to the generalized majority rule f if and only if the set of voters preferring x to y in the profile belongs to the family of generalized majorities. Obviously these rules generalize Condorcet's majority rules which are obtained with = MAJ = {S N : |S| n/2} and = SMAJ = {S N : |S| > 27 in Von Neumann J, Morgenstern O (1944) Theory of games and economic behaviour. Princeton, University Press.

  28

  be a simple game on N and L L L L be the set of all linear orders on A (n, m " 3). The map f is an L L L L-preference aggregation function if and only if is dictatorial (i.e., there exists i # N such that = {i} = {W N : i # W}).

  Translation of my sentence "Il est alors immédiat que dans l'algèbre de Boole des parties de N, doit être un filtre maximal" in Monjardet B (1969) Remarques sur une classe de procédures de vote et les théorèmes de possibilité In La décision, Éditions du CNRS, Paris, pp 177-184. 35 See Monjardet B (1978) Une autre preuve du théorème d'Arrow. R.A.I.R.O. 12: 291-296 and Monjardet B (1981) On the use of ultrafilters in social choice theory In Pattanaik PK, Salles M (eds) Social Choice and Welfare. Amsterdam, North-Holland, pp 73-78. 36 See for instance Pouzet M (1998) A projection property and Arrow's impossibility theorem. Discrete Mathematics 192(1-3): 293-308.

  represents the permutoèdre lattice L on a set A = {a,b,c,d}. The covering sublattice of the single-peaked orders (w.r.t. the linear order abcd) is represented on this Figure by squares. It has 8 elements. One can find another covering distributive sublattice with 9 elements (search for it!).

Figure 2 HERE

 2 Figure 2 HEREThe permutoèdre lattice on four elements

  Figure 1 A 3-cycle

,

  Mathématiques discrètes et sciences sociales (Discrete mathematics and social sciences) initiated in 1978 by Monjardet 11 and Histoire du calcul des probabilités et de la statistique (History of probability and statistics) initiated in 1982 by M. Barbut and Ernest Coumet 12 .

Économie appliquée 5(4): 469-484 (October-December 1952).

This method had been already proposed in the thirteenth century by Ramon Lull (seeMcLean I, London J (1990) The Borda and Condorcet principles: three medieval applications. Social Choice and Welfare 7: 99-108).

The fact that the median problem is NP-complete can be found for example inOrlin (1981) unpublished note or Hudry O (1989) Recherche d'ordres médians : complexité, algorithmique et problèmes combinatoires. Thèse ENST, Paris.

See Young HP (1988) Condorcet's Theory of Voting. American Political Science Review 82: 1231-1244.

This distance is nothing more than the "path length" distance in the unoriented graph associated with the covering relation of the lattice (see for instance Birkhoff G (1967) Lattice theory. Amer. Math. Soc., Providence or Barbut M, Monjardet B (1970) Ordre et Classification, Algèbre et Combinatoire, tomes I et II. Hachette, Paris).

Barbut M (1961) Médianes, distributivité, éloignements. Note CAMS, EHESS, Paris and (1980) Mathématiques et Sciences Humaines 70: 5-31, Monjardet B (1980) Théorie et application de la médiane dans les treillis distributifs finis. Annals of Discrete Mathematics 9: 87-91.

This definition is also equivalent to saying that D has no cyclic triples, i.e. that there do not exist a subset {x,y,z} of three alternatives and three linear orders in D such that the restrictions of these orders to {x,y,z} is a cyclic permutation like xyz, yzx and zxy (such a set D has been also called a consistent or an acyclic or a majority-consistent set, see the references in footnotes 53 and 54).

See Black D (1948) On the rationale of group decision-making. Journal of Political Economy 56: 23-34 and Black's book quoted in footnote 25.

The following first such result has been followed by many others: MirkinBG (1975) On the problem of reconciling partitions In Quantitative Sociology, International Perspectives on mathematical and Statistical Modelling. Academic Press, New-York, pp 441-449 (in the case of partitions as in the case of partial orders the independence and unanimity axioms lead to "oligarchic" consensus functions).

Acknowledgements.

The author wish to thank M. Barbut, J.P. Barthélemy, B. Leclerc and M. Salles for their suggestions. He is particularly grateful to G.Th. Guilbaud and W. H.E. Day to have corrected many content and/or form errors contained in a preliminary version of this paper. All these contributions have greatly improved the paper. ANNEX 2 B. Leclerc, The median procedure in the semilattice of orders, Discrete Applied Mathematics 127 (2), 285-302. B. Monjardet and V. Raderinirina, Lattices of choice functions and consensus problems, to appear in Social Choice and Welfare. B. Monjardet, De Condorcet à Arrow via Guilbaud, Nakamura et les "jeux simples", to appear in Mathématiques et Sciences Humaines, 163. [Version 1/10/04]

Now an old result of Barbut 43 proves our claim:

For F = (L 1 ,...,L n ) G L N , the medians of F in the metric space (L, d K ) are the solutions of the discrete optimisation problem: MAX{H (F ,L), L G L}.

One can note that as early as 1959 Kemeny proposed to take as collective preference(s) for a profile of linear orders its medians in the metric space (L, d K ) defined above 44 . This proposal was later published in Kemeny and Snell's famous book Mathematical Models in the Social Sciences and so this procedure is widely known as Kemeny's procedure 45 . One can now add that Kemeny's procedure, the median procedure and Condorcet's generalized rule are all the same.

We have not yet finished with medians since we are turning now to the notion of algebraic medians, a notion closely related to the notion of majority. Note first that a profile F = (L 1 ,...,L n ) of linear orders is in particular a profile of n binary relations on A. Take now as a metric space (E,d) the set 2 A 2 of all binary relations on A endowed with the symmetric difference distance dI (R,R') = |(R\R') P (R'\R)|. What are the medians of F in this metric space? The answer is easily found. Since one always has

of all binary relations contained between the two majority relations. Then one has:

The medians of a profile F of linear orders in the metric space (2 A 2 , dI ) are all the binary relations of the interval

Now this result is a special case of a general result on distributive lattices. Recall that a lattice (L, R ) is a partially ordered set such that each pair {x,y} of elements of L has a greatest lower bound (or meet) denoted by xS y and a least upper bound (or join) denoted by xT y. Then if L is 43 Barbut M (1967)


Belgacem Amira Methni
email: amira.methni@cea.fr

Ben Hedia

Matthieu Lemerre
email: matthieu.lemerre@cea.fr

Serge Haddad
email: haddad@lsv.ens-cachan.fr

Kamel Barkaoui
email: kamel.barkaoui@cnam.fr

State Space Reduction Strategies for Model Checking Concurrent C Programs

Model checking is an effective technique for uncovering subtle errors in concurrent systems. Unfortunately, the state space explosion is the main bottleneck in model checking tools. Here we propose a state space reduction technique for model checking concurrent programs written in C. The reduction technique consists in an analysis phase, which defines an approximate agglomeration predicate. This latter states whether a statement can be agglomerated or not. We implement this predicate using a syntactic analysis, as well as a semantic analysis based on abstract interpretation. We show the usefulness of using agglomeration technique to reduce the state space, as well as to generate an abstract TLA+ specification from a C program.

Model checking, TLA, State space reduction, Agglomeration predicate.

INTRODUCTION

Model checking is an attractive formal verification technique because it is automatic. It offers extensive and thorough coverage by considering all possible behaviors of a system, unlike traditional testing methods. Given a set of properties expressed in a temporal logic and a model, model-checking automatically analyzes the state space of the model and checks whether the model satisfies the properties [START_REF] Clarke | Model Checking[END_REF]. However, the main obstacle of model checking is the state explosion problem and concurrency is a major contributor to this problem.

Many solutions have already been investigated for reducing the complexity of model checking. For instance, by getting a simpler model from the original one using abstraction technique [START_REF] Clarke | Model Checking and Abstraction[END_REF]), or by using on-the-fly model checking to eliminate part of the search to the automaton representing the (negation of the) checked property [START_REF] Fernandez | On-the-fly verification of finite transition systems[END_REF].

Contribution

In this paper, we present a state space reduction technique for model checking concurrent programs written in a low level language. We apply this technique to the verification of C programs by an explicit model checker. We use TLA+ [START_REF] Lamport | The Temporal Logic of Actions[END_REF]) as a formal specification language for our concurrent C programs and we base ourselves on previous work reported in [START_REF] Methni | Specifying and Verifying Concurrent C Programs with TLA+[END_REF]. The reduction technique is based on an analysis phase, which defines an approximate agglomeration predicate. This latter states whether a statement can be agglomerated or not. We implement this predicate using a syntactic analysis, as well as a semantic analysis based on abstract interpretation of C code. The particularity of our method is that we apply the reduction technique during the generation of TLA+ code and by using the abstract interpretation technique. We show the usefulness of using this technique to reduce the state space during the verification of C programs, as well as to generate an abstract TLA+ specification from a C program.

Outline

The rest of the paper is organized as follows. We give an overview of TLA+ in Section 2. Section 3 presents how we specify the semantics of C in TLA+. Section 4 describes the reduction technique and how we implement it on C programs. Experimental results are presented in Section 5. We discuss related work in Section 6. Section 7 concludes and illustrates future research directions.

OVERVIEW OF TLA

TLA+ [START_REF] Lamport | Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers[END_REF] is the specification language of the Temporal Logic of Actions (TLA). TLA is The syntax of TLA is given in Figure 1 (the symbol means equal by definition). TLA+ formulas are built up from actions and predicates using boolean operators (¬ and ∧ and others that can be derived from these two), quantification over logical variables (∀, ∃), and the unary temporal operator (always) of the linear temporal logic [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems[END_REF].

f ormula predicate | [ action ] state f unction | ¬ f ormula | f ormula ∧ f ormula | f ormula
The predicate "ENABLED A", where A is an action, is defined to be true in a state s iff there exists some state t such that the pair of states s, t satisfies A. The formula [A] vars , where A is an action and vars the tuple of all system variables, is equal to (A ∨ (vars ′ = vars)) where vars ′ is the expression obtained by priming all variables in vars. It asserts that every step (pair of successive states) is either an A step or else leaves the values of all variables vars unchanged. TLA+ defines the abbreviation "UNCHANGED vars" to denote that vars ′ = vars.

While TLA+ permits a variety of specification styles, the specification that we use is defined by:

Spec Init ∧ [N ext] vars ∧ F airness (1)
where:

• Init is a state predicate describing the possible initial states by assigning values to all system variables,

• N ext is an action representing the program's next-state relation,

• vars is the tuple of all variables,

• F airness is an optional formula representing weak or strong assumptions about the execution of actions.

Formula Spec is true of a behavior σ iff Init is true of the first state of σ and every step of σ is either a N ext step or a "stuttering step", in which none of the specified variables change their values, and F airness holds. The behaviors satisfying the specification formula given by Equation ( 1) are the ones that represent correct behaviors of the system, where a behavior represents a conceivable history of a universe that may contain the system.

The TLA+ formula Spec ⇒ φ is valid when the model represented by Spec satisfies the property φ, or implements the model φ.

TLA+ has an explicit model checker called TLC that can be used to check the validity of safety and liveness properties. TLC handles specifications that have the standard form of the formula (1). For this reason, we only use specification formula of the form of Equation (1). TLC requires a configuration file which defines the finite-state instance to analyze. It begins by generating all states satisfying the initial predicate Init. Then, it generates every possible next-state t such that the pair of states s, t satisfies N ext and the F airness constraints, looking for a state where an invariant is violated. Finally, it checks temporal properties over the state space.

TRANSLATION FROM C TO TLA+

Our approach to checking a concurrent C program is to first translate it into a TLA+ specification, to which the TLA+ tools can be applied. In what follows, we briefly present how we specify the semantics of C in 1 int x = 3; 2 int y = 0; TLA+ by describing the memory layout considered and how we model the control flow of a C program.

Memory Layout

C file is parsed and normalized according to CIL (C Intermediate Language) [START_REF] Necula | CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs[END_REF] which transforms complicated constructs of C into simpler ones. This transformation makes programs more amenable to analysis and transformation.

According to the Abstract Syntax Tree (AST) of the C program, C2TLA+ generates automatically a TLA+ specification according to a set of translation rules detailed in our previous work [START_REF] Methni | Specifying and Verifying Concurrent C Programs with TLA+[END_REF].

In C2TLA+, a concurrent program consists of many interleaved sequences of operations called processes, corresponding to threads in C. Each process has a unique identifier id. The set of all processes is determined by the TLA+ constant P rocSet.

Figure 2 presents a C program and the content of the memory as modeled by C2TLA+. We consider that the C code is executed by two processes. One process executes p1() function and the other one executes p2() function.

The memory is separated into four areas that do not overlap:

• a shared memory called data that stores global (and static) variables. In the example of Figure 2a, the x variable is shared by the two processes.

• a local memory for each process, called stack and stores local variables and function parameters. The memory stack[id] specifies the local memory of process id and is composed of stack frames. Each stack frame corresponds to a call to a function. In the example of Figure 2a, stack[1] is composed of two stack frames, one of p1() function and one of inc() function. When a function call terminates, its stack frame is removed.

• a local memory for each process called register modeled as a sequence and stores the program counter of each process. The head of this sequence contains the statement being currently executed by the process id.

• a local memory called ret which contains values to be returned by processes.

The memory is modeled in TLA+ by a variable called memory. It is a record whose four fields represent the four memory areas. The global memory data behaves like an array of values, whereas stack and register behave like a FIFO (First In, First Out) queues. Access to those memory areas is addressed using offsets. So, a memory address is a couple [loc,of f s] of memory location loc, (data or stack area) and an offset of f s in this location. For instance, Addr x specified in Figure 2b defines the memory address of x variable.

The main operations that manage the memory are load() and store():

• load() is the function that given the current state of memory mem and a memory address addr (in the form of [loc, of f s]), returns the value stored at the address addr in the memory mem,

• store() is the function that given the current state of memory mem, a memory address addr and a value val, returns the new copy of the memory after storing the value val at the memory address addr.

Specifying the C control-flow

Each C statement i is identified in C2TLA+ by a label assigned by CIL and is modeled by a TLA+ function, noted stmt i (), which takes as arguments the process identifier id and the memory mem, and returns the new content of the memory after executing the statement.

Each stmt i () updates the program counter register of the process id and may change the content of mem, stack, and/or ret memory areas depending on the type of the statement (assignment, jump statements, etc.). For instance, the statement on line 20 is translated into the TLA+ function p2 20(id, mem) defined as follows:

p2 20(id, mem)

∆ = LET mcopy ∆ = load(id, Addr x, [val → 3]) IN [data → mcopy.mem, stack → mcopy.stack, register → [mem.register EXCEPT ![id] = [pc → "p2 21" , f p → Head(mem.register[id]).f p] • T ail(mem.register[id]), ret → mem.ret]
The definition of p2 20() function uses the TLA+ construct LET/IN to define a temporary variable that stores the value of the memory after affecting the value 3 to the memory address Addr x. The symbol • defines the concatenation operator for TLA+ sequences. Head(s) is a TLA+ function that returns the head of the sequence s and T ail(s) returns the tail of the sequence s. Then, the register [id] is updated by the label value of the successor statement given by the control flow graph (CFG) of the C program (provided by CIL).

The control flow of the C program in C2TLA+ is ensured by the dispatch() function. For the example of Figure 2a, this function is defined as follows: Head(mem.register[id]).pc = "inc 6" → inc 6(id, mem) Head(mem.register [id]).pc = "inc 7" → inc 7(id, mem) Head(mem.register [id]).pc = "p1 11" → p1 11(id, mem) Head(mem.register [id]).pc = "p1 12" → p1 12(id, mem) Head(mem.register [id]).pc = "p1 13" → p1 13(id, mem) Head(mem.register [id]).pc = "p1 14" → p1 14(id, mem) Head(mem.register [id]).pc = "p2 19" → p2 19(id, mem) Head(mem.register [id]).pc = "p2 20" → p2 20(id, mem) Head(mem.register [id]).pc = "p2 21" → p2 21(id, mem) OTHER → mem

dispatch(id, mem) ∆ = CASE
The dispatch() function calls, according to the value of the pc field contained at the top the process register (determined by the expression Head(mem.register[id]).pc), the corresponding TLA+ function to execute, i. e., the C instruction to execute.

The C program is thus simulated by the Spec formula given by equation ( 1). The Init predicate specifies the initial values of the memory and the N ext action is defined as follows:

N ext ∆ = ∨ ∃ id ∈ P rocSet : ∧ memory.regsiter[id] = ∧ memory ′ = dispatch(id, mem) ∨ ∀ id ∈ P rocSet : ∧ memory.regsiter[id] = ∧ UNCHANGED memory
It states that one of the processes that has not finished execution (its register[id] is not empty) is nondeterministically chosen to execute one action until all processes finish execution, i. e., all registers become empty. Executing an action consists in calling dispatch() function. For example, when Head(mem.register [id]).pc equals to "inc 6", calling the function inc 6(id, mem) will update the value of stack[id] (as tmp is stored in the local memory) as well as the top of register [id]. As the register[id] is • a finite set of states Q,

• a set I ⊆ Q of initial states, specified by the Init predicate,

• a transition relation δ ⊆ Q × Q that links two states. This latter corresponds to satisfying the predicate N ext.

The state transition system encodes the state space of the corresponding TLA+ specification of the C program.

Figure 3 illustrates the state space of the corresponding TLA+ specification of the C code given in Figure 2a. It consists in all the possible interleaving of process execution. In order to simplify, we represent only the content of pc field contained at the top of the register[1] and register[2] memories. Each state of the graph matches a valuation of memory variable, i. e., its four fields.

Process Synchronization

All processes interact with each other through the shared memory data. Concurrent access to this latter is ensured via synchronization mechanism. There are many different ways to implement concurrency synchronization in C. For instance, by using locks and semaphores, or by providing low level hardware instructions (e. g., test-and-set and compareand-swap). To support synchronization mechanism, generated TLA+ specifications by C2TLA+ can be completed with manually written TLA+ specifications to provide concurrency primitives and atomic instructions. More detailed information about integrating synchronization primitives in TLA+ specifications can be found in our previous work [START_REF] Methni | Specifying and Verifying Concurrent C Programs with TLA+[END_REF].

APPLYING REDUCTION ON C PROGRAMS

The process of generating an optimized TLA+ specification is illustrated in Figure 4. To apply reduction on C programs, it is necessary to define the agglomeration predicate. The C program is first analyzed. This analysis phase defines an approximate agglomeration predicate which takes as argument a C statement and returns true or false depending on whether the statement can be agglomerated or not. This predicate can be safe or unsafe. The meaning of safe predicate depends on how the analysis is performed.

• The predicate is said safe when the analysis is a safe approximation. Its definition is as follows:

-if the statement does not modify the shared memory, the predicate returns true,

-if the statement modifies the shared memory or it is unknown, it returns false.

The unknown predicate states that we have no idea if the statement modifies the memory or not.

• The predicate is called unsafe when a statement is agglomerated and we are not sure if it modifies the global memory or not. In this Section, we introduce the agglomeration technique by an example. Then, we describe the implementation of a safe agglomeration predicate by using a syntactic and semantic analysis on C programs. Then, we show the interest of using an unsafe agglomeration predicate to generate an abstract TLA+ specification of a C program.

In what follows, we use the expression agglomerating TLA+ actions, to designate agglomerating the corresponding statements in the C program.

An introducing example

As the semantics of a TLA+ is expressed through a state transition system, where transitions between states are ensured by TLA+ actions, the reduction technique consists in agglomerating consecutive actions into one atomic action which performs the effects of the original ones. The reduction idea based on agglomeration has been widely used in Petri Nets [START_REF] Haddad | New Efficient Petri Nets Reductions for Parallel Programs Verification[END_REF][START_REF]Checking properties of nets using transformation[END_REF]).

Figure 5 shows three consecutive states linked by two actions x ′ = x +1and x ′ = x +2. The result of this agglomeration (represented by -→ ), is two states linked by one atomic action which is the result of executing the action x ′ = x +1, then x ′ = x +2.

x =2

x =3

x =5

x ′ = x +1

x ′ = x +2 → x =2
x =5

x ′ =(x + 1) +2

Using syntactic and semantic analysis

Syntactic analysis

A syntactic analysis is performed to detect statements on which reduction can be applied. Often, C functions make use of local variables, and when a statement refers only to local variables, the value for which the statement is executed by a process cannot change the execution of other processes. Furthermore, we assume that statements involving local pointer variable cannot be agglomerated as they may reference shared memory.

Moreover, we consider that jump statements, namely goto, break and continue, can be agglomerated with its successor (designated by computing the CFG), as they only change the local register of the process (register[id] in TLA+ specification).

Semantic analysis

In many scenarios, a concurrent C program could contain, in its global memory, data blocks that are accessed only by one process at a time. In that case, syntactic analysis is insufficient. Therefore, we use a semantic approximation predicate. The C program is thus analyzed and an approximation of memory access is computed using the Mthread Frama-C plugin (Mth). This latter provides information about the memory zones that are accessed concurrently by more than one process and those that are not. In this case, the agglomeration predicate is safe as the analysis is based on an over-approximation of the memory.

We consider the example given by Figure 2a.

To illustrate the agglomeration technique on this example, we represent the C program by its control flow graph, illustrated by Figure 6a, where each state of the graph represents a C statement and edges represent the control flow. After applying the syntactic and semantic analysis on this example, the control flow graph is transformed into a smaller graph, given in Figure 6b. Each state of the graph corresponds to one statement or a block of statements. As the inc() function uses only local memory, its block definition is combined into one basic block. For p1() function, statement on line 11 is agglomerated with statement on line 12 and statement on line 14 is agglomerated with the return instruction.

Generating an abstract specification

Agglomerating statements can also be useful to generate an abstract TLA+ specification of a C program. The user can define which C statements can be agglomerated using an unsafe predicate. The resulting TLA+ specification can be viewed as an abstract formal specification of the C program.

As TLA+ is a fragment of LTL \x (Linear Temporal Logic without the "next operator"), it is well known that the equivalence between checking a property given in LTL \x on an abstract model and checking it on the original model is ensured by the preservation [START_REF] Goltz | Propositional Temporal Logics and Equivalences[END_REF].

Example: Agglomerating critical sections

Consider the following fragment of C code (Figure 7) implementing an example of the producer/consumer model. The two processes share a buffer protected by a mutex m. The synchronization between processes is ensured by two semaphores empty and full. Mutex and semaphores are implemented as an integer values and are only accessible through two atomic operations P() and V().

Translating this implementation into a TLA+ specification and model checking results in verifying all interleavings of actions between processes. We define the agglomeration predicate that states that statements protected by mutex (namely by P() and V() primitives) can be agglomerated. After reduction, the control flow graph of this example is illustrated in Figure 8b.

Therefore, the block statements from line 12 to line 14 and that from line 12 to 26 are agglomerated into one state. The state space of the TLA+ specification generated after agglomerations contains fewer states than the one without agglomerations as the reduction inside the critical section restricts the amount of interleaving allowed between processes. We define the mutual exclusion property in TLA+ as follows:

mut exclusion(lbl1, lbl2) Head(memory.regsiter[id1]).pc = lbl1))

∆ = ((∀ id1, id2 ∈ P rocSet : ∧ (id1 = id2) ∧ (Head(memory.register[id1]) = ) ∧(Head(memory.register[id2]) = ) ∧(
⇒ Head (memory.register[id2]).pc = lbl2) This property expresses that critical sections cannot be executed simultaneously. This property was verified on the TLA+ specification after reduction. Thus, we can deduce that the property is also verified on the specification generated without the reduction technique.

Integrating the reduction into TLA+ specification

In what follows, we show how we implement the reduction on TLA+ specification. As described in Section 3, each execution of N ext action corresponds to executing an atomic C statement. The reduction in C programs, consists in translating a sequence of C statements into one action instead of multiple ones. Let i be the identifier of a statement and j be the identifier of its successor. To do that, we generate for each statement i a new function that we call stmt long i () defined below.

stmt long i (id, mem) ∆ = stmt long j (id, dispatch(id, mem))
The definition of stmt long i (id, mem) consists in calling the function of the successor statement j, noted by stmt long j () and passing as argument the memory state returned by dispatch(id, mem). To generate a reduced TLA+ specification, we iterate over all statements and when the agglomeration predicate returns true for a statement i, its translation consists in calling the function stmt long j (id, dispatch(id, mem)). Otherwise, we call dispatch(id, mem) function.

The C program is thus specified by the formula Spec given by equation (1), except that the N ext action calls a new function dispatch red(), instead of dispatch() function. For the example of figure 2a, the dispatch red() function is defined in Figure 9:

The dispatch red(id, mem) function calls according to the value the program counter pc contained at the head of mem.register[id] the corresponding TLA+ function to execute.

EXPERIMENTS

The reduction technique is totally automatic and was integrated in C2TLA+ which is a Frama-C [START_REF] Cuoq | Frama-C: A Software Analysis Perspective[END_REF]) plugin, implemented in OCaml. This Section is concerned with our practical experience. We use the Mthread plugin results and the syntactic analysis as described in Section 4 to implement our agglomeration technique.

We consider one sequential C program and four concurrent programs: Head(mem.st[id]).pc ="inc 6" → inc long 6(id, mem) Head (mem.register[id]).pc ="inc 7"

dispatch red(id, mem) ∆ = CASE
→ inc long 7(id, mem) Head (mem.register[id]).pc ="p1 11" → p1 long 11(id, mem) Head (mem.register[id]).pc ="p1 12" → p1 long 12(id, mem) Head (mem.register[id]).pc ="p1 13" → p1 long 13(id, mem) Head (mem.register[id]).pc ="p1 14" → p1 long 14(id, mem) Head (mem.register[id]).pc ="p2 19" → p2 long 19(id, mem) Head (mem.register[id]).pc ="p2 20" → p2 long 20(id, mem) Head (mem.register[id]).pc ="p2 21" → p2 long 21(id, mem) OTHER → mem • Zunebug which is a bug in the internal clock driver of Zune 30GB music player. The source code is taken from [START_REF] Weimer | Automatic Program Repair with Evolutionary Computation[END_REF]).

• Lamport's Bakery and Peterson algorithms obtained from [START_REF] Raynal | Concurrent Programming: Algorithms, Principles, and Foundations[END_REF] and Dekker mutual exclusion algorithm presented in (Dijkstra 1968).

• Dining philosopher problem. We use the solution that appears in Tanenbaum's book [START_REF] Tanenbaum | Modern Operating Systems[END_REF].

These programs make typical examples for demonstrating the strength of the state space reduction. C2LTA+ takes as input a C program and generates for each one the corresponding TLA+ specification.

Using the TLC model checker, we compute the total number of generated states and we verify a set of properties on the two specifications.

Results of experiments are shown in Table 1, where #Proc denotes the process number, #St denotes the numbers of states and #T denotes the time for model checking in seconds. Columns 3 to 6 give information about the state space generated with and without applying the reduction technique. The last column indicates the reduction factor, the ratio between the state space generated without reduction and the one after applying the reduction technique.

All experimental results were performed on an Intel Core Pentium i7-2760QM machine with 8 cores (2.40GHz each), with 8Gb of RAM memory.

For zunebug, one property to verify is program termination, which is a liveness property that we express as follows:

termination ∆ = ⋄(Head(memory.register[1]) = )
This property asserts that the register of the program will eventually be empty. For the TLA+ specification without agglomeration, checking this property causes TLC to report an error. This error occurs when the code takes as input the last day of a leap year, causing the code to enter into an infinite loop. After applying the reduction technique for the zunebug program, the state space size of its corresponding TLA+ specification equals 2. This is due to the fact that the program is sequential. Model checking the TLA+ code with the last day of a leap year causes the TLC model to report an incorrect recursive function definition.

For the concurrent programs, the mutual exclusion property has been successfully verified on Peterson, Bakery, Dekker and Philosophers benchmarks. As expected, the size of the state space with agglomerations is always smaller than the one without agglomerations. For the philosopher example with 5 processes, the state space without agglomeration takes more than 7 hours to be model checked. However, using the reduction technique the specification is verified in 6 minutes. The reduction factor in this cas reaches 99.32. The reduction technique obtains good results on these benchmarks due to the elimination of some intermediate states.

RELATED WORK

There are a wealth of research contributions on formal verification of software as well as techniques for the reduction of the state space.

Program slicing is a technique introduced by [START_REF] Weiser | Program Slicing[END_REF] for simplifying sequential programs for debugging and program understanding. It consists in removing from the program features that are irrelevant for the property to be verified. Recently, slicing technique has been used to reduce the state space of a system in model checking. It has been applied to Promela [START_REF] Millett | Issues in Slicing PROMELA and its Applications to Model Checking, Protocol Understanding, and Simulation[END_REF], the input language for the Spin model checker [START_REF] Holzmann | The Model Checker SPIN[END_REF]). The interested reader can refer to [START_REF] Tip | A Survey of Program Slicing Techniques[END_REF] for a detailed description of the different approaches used in the program slicing.

Predicate abstraction [START_REF] Graf | Construction of Abstract State Graphs with PVS[END_REF] is a technique in which a set of predicates over the programs variables is used to construct an abstract program. This technique is being used in SLAM [START_REF] Ball | The SLAM project: Debugging System Software via Static Analysis[END_REF], BLAST (Henzinger et al. 2003) and MAGIC [START_REF] Chaki | Modular verification of software components in c[END_REF]).

Other approaches perform reduction during exploration of the state space of the program. For example, partial order reduction [START_REF] Valmari | Stubborn Sets for Reduced State Space Generation[END_REF]) is a technique which explores only a representative subset of the state space of a model. The basic idea is to exploit the commutativity caused by the interleavings of transitions, which result in the same state. This technique was first introduced for checking the absence of deadlock. Subsequently, a number of variants of this technique have been developed and integrated in verification tools, like Spin [START_REF] Holzmann | The Model Checker SPIN[END_REF] and Verisoft [START_REF] Godefroid | Model Checking for Programming Languages using VeriSoft[END_REF]).

Although we have mentioned some projects in the C context, there are also significant works interested in model checking the Java language. For example, JPF [START_REF] Visser | Model Checking Programs[END_REF] uses state compression technique to handle big states, partial order and symmetry reduction, slicing, abstraction and runtime analysis techniques to reduce the state space.

In this work, the state space reduction technique that we propose is closer to that originally introduced by [START_REF]Checking properties of nets using transformation[END_REF] in Petri nets formalism. Berthelot developed a large set of reduction rules for reducing the complexity of verification. Extended work has been proposed by [START_REF] Haddad | New Efficient Petri Nets Reductions for Parallel Programs Verification[END_REF].

Our work differs from this latter by the fact that the model of our TLA+ specification is a state transition system and the agglomeration predicate depends on the analysis of the C program. Our reduction technique is applied during the generation of TLA+ code unlike the partial order reduction technique which performs reduction during the construction of the state space. Besides, we use TLA+ as formal framework which provides an expressive power to specify the semantics of a programming language and can reason about concurrent systems and can express safety and liveness properties unlike SLAM and BLAST which have limited support for concurrent properties as they only check safety properties.

CONCLUSION AND FUTURE WORK

We have proposed a technique to reduce the state space for model checking C programs. We used C2TLA+ to translate the semantics of C to the formal specification language TLA+. This reduction technique is based on an analysis phase, which defines an approximate agglomeration predicate that states whether a statement can be agglomerated or not. We implemented this predicate by applying a syntactic and semantic analysis on C Programs. We illustrated the effectiveness of applying the agglomeration technique to reduce the state space during the verification of C programs and also as well as to define an abstract TLA+ specification that model the behavior of C programs.

We aim to integrate a mechanism for structuring large TLA+ specifications from C programs using a refinement process between different levels of abstraction. Finally, we are planning to apply the methodology on a critical part of the microkernel of the PharOS [START_REF] Lemerre | Method and Tools for Mixed-Criticality Real-Time Applications within PharOS[END_REF]) real-time operating system (RTOS).

Figure 2 :

 2 Figure 2: Example of a C code in which one process (with id equals to 1) executes p1() function and the second one executes p2(). The top of the stack[1] indicates that process 1 is executing the statement with label 6 of inc() function. U ndef represents an undefined value such as the value of an uninitialized variable.

Figure 3 :

 3 Figure 3: Example of a state space

Figure 4 :

 4 Figure 4: Reduction process

FigureFigure 6 :

 6 Figure 5: Agglomerating actions

Figure 7 :

 7 Figure 7: Example of a producer/consumer model using locks

Figure 8 :

 8 Figure 8: The control flow graph of the Producer() and Consumer() functions before and after reduction

Figure 9 :

 9 Figure 9: Example of the dispatch red() function definition

  action boolean valued expression containing constant symbols, variables, and primed variables predicate f ormula with no primed variables | ENABLED action state f unction nonboolean expression containing constant symbols and variables

	Figure 1: TLA syntax (Lamport 2002)
	a variant of linear temporal logic introduced by
	(Lamport 1994) for specifying and reasoning about
	concurrent systems. Readers interested in a more
	detailed presentation of TLA+ can refer to Lamport's
	book (Lamport 2002).
	TLA+ specifies a system by describing its possible
	behaviors. A behavior is an infinite sequence
	of states. A state is an assignment of values
	to variables.

A state function is a nonboolean expression built from constants, variables and constant operators and it assigns a value to each state. For example, y + 3 is a state function that assigns to state s the value 3 plus the value that s assigns to the variable y. An action is a boolean expression containing constants, variables and primed variables (adorned with " ′ " operator). Unprimed variables refer to variable values in the current state and primed variables refer to their values in the next-state. Thus, an action represents a relation between old states and new states. A state predicate (or predicate for short) is an action with no primed variables.

Table 1 :

 1 Comparing Model Checking Results with & without Reduction (time in seconds)

	Prorgam #Proc	Without reduction	With reduction	Factor
			#St	#T	#St	#T
	Zunebug	1	389	0.147	2	0.136	99.48
	Dekker	2	173	0.128	70	0.109	59.53
	Peterson	2 4	107 1.080.161	1.37 59.2	22 31.221	0.131 4.82	79.43 97.10
	Bakery	2 4	2.389 50.515.927	1.91 1560	223 835.355	1.67 76.6	90.66 98.36
	Philos	4 5	9.791.509 >619.309.984	366 25340	146.106 4.179.520	12 352	98.5 99.32


The many facets of the urban night time

Cities and Lighting n°7, juin 2018, p.23

Luc Gwiazdzinski (*)

The urban nighttime, as we just saw, has multiple dimensions. Leading policy-makers, lighting professionals and researchers from around the world talk to Cities & Lighting on their view of the nighttime in cities -its essence, its challenges, and its future.

Nighttime is a caricature of daytime in that everything seems to be intensified. The night reveals people and has a lot of things to say to daytime and to tomorrow.

A space and time that has been neglected for a long time, now under pressure, taken over by daytime activities, nighttime is rebuilding itself, for better or worse. Thinking about the city at night with these contradictions and paradoxes can help us to "experience" a complex world in which the answers can no longer be caricatured. It has always been a time and space for creativity where artists, designers and agitators come to seek refuge or inspiration from their nocturnal muses.

There is no one night but a continuum of nights. Nighttime is an opportunity and an obligation in terms of social dialogue, democracy and town-planning. The responsibility of everybody and nobody, a sensitive question that concerns all of us, a complex time and space which requires a shared inter-disciplinary, cross-cutting approach, nighttime is an effective and perceptible key to reconsidering our cities and inspiring society, far from the cold certainties of the day.

It requires a time-space and "chronotopic" approach and encourages us to rethink the rhythms and modes of occupation of a malleable city. By allowing experiences which involve all of the senses, nighttime can reveal other ways of being in the world and increase the sustainable development of creative and ethical dimensions.

Starting to study and work on urban nights means experiencing "a nocturnal way of thinking", integrating the knowledge specific to these time-spaces, and learning how to manage inevitable tensions between commercial areas, areas of creativity and escapism, and areas in which people can seek privacy.

The solutions developed for nighttime in our cities (night charters between residents, owners of establishments and consumers, night mayors, mediators …) are of interest in that they offer mediation rather than regulations.

Light is at the heart of a "nocturnal way of thinking" which compels us to incorporate a paradox: without light, there is no city at night but too much light kills the night. It is therefore necessary to retain a sense of moderation and ask ourselves the question "how much is too much?" If we want to enhance nighttime through the use of lighting, this task could concern four specific points: the first is equality of lighting in terms of the various districts of our cities, given the current discrepancy between centres and outskirts; the second concerns the intensity of lighting, given the risk of light pollution; the third concerns adjustment of lighting at night according to the presence of people; the fourth concerns a lighting approach on individual terms by rethinking portable lighting and the traditional torch.

Future urban nights remain to be invented together with, at first, some rules: ensure that they remain spaces of freedom and innovation by making way for improvisation, mystery and the unorganised. Let's make sure that nighttime retains what makes it different and that it does not simply become the equivalent of daytime. Let's not put an end to shadows. Let's keep away from harsh, prison-like lighting. This original change must be retained by heeding the warnings of chrono-biologists: without rhythm, there is no life.

In a space and time where notions of safety and freedom are essential, we can devise "nighttime urban planning" based on hospitality, quality, equality, sensitivity, variety and the unexpected; safety by increasing human presence and delight. Applied to daytime, these principles of "giving consideration to nighttime" could contribute to urban planning strategies based on connections, interaction and mediation rather than on separation and zoning.

  Sharing rather than separating. Contractualising rather than imposing. One can yet dream of cities which are more liveable, human, accessible and welcoming at nighttime and daytime by continuing to be inspired by Situationists: "Open the underground at night, after the trains have finished running (…). Leave public gardens open at night. Keep their lights switched off. Equip street lights in all the streets with switches". Tomorrow is another night. Luc Gwiazdzinski est géographe, directeur du Master Innovation et territoire à l'université Grenoble Alpes. Il a dirigé une vingtaine de colloques et programmes de recherche sur la nuit et les temps urbains. Il est l'auteur de nombreux articles et ouvrages sur ces questions parmi lesquels : La nuit dernière frontière de la ville (L'aube) ; la Ville 24h/24 (L'Aube) ; La Nuit en questions (Hermann) ; Nuits d'Europe (UTBM), L'hybridation des mondes (Elya) ; Chronotopies (Elya).

	Citer cet article :
	Gwiazdzinski L., 2018, The many facets of the urban night time, Cities and Lighting n°7, juin
	2018, p.23
	(*)