Clara Benac Earle

Lars-Åke Fredlund
email: lfredlund@fi.upm.es

Clara Benac
email: cbenac@fi.upm.es

Verification of Timed Erlang Programs Using McErlang

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

Introduction

Timed semantics for concurrent formalisms is by now a very well-studied field. In the field of real-time semantics a very successful technique for specifying and verifying systems are the timed automata [START_REF] Alur | A theory of timed automata[END_REF]. Similarly there exist numerous discrete-timed specification formalisms, or timed formalisms for which a discrete time domain has been extensively studied, e.g., in process algebra for Timed CSP [START_REF] Ouaknine | Discrete analysis of continuous behaviour in real-time concurrent systems[END_REF], TCCS [START_REF] Moller | Behavioural abstraction in TCCS[END_REF], TPCCS [START_REF] Hansson | A calculus for communicating systems with time and probabitilies[END_REF], LOTOS [START_REF] Léonard | A formal definition of time in LOTOS[END_REF], to mention but a few.

Uppaal [START_REF] Larsen | Uppaal in a nutshell[END_REF] is the currently most well-known model checker for real-time systems. It provides an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays etc.).

While tools and specification formalisms like Uppaal are quite successful at real-time verification, there is still a need to reason about timed behaviour in other specification and programming languages, using dedicated model checkers. However, many of these model checkers do not implement tailored real-time verification algorithms like Uppaal. Rather, they are used to check timed behaviour by discretizing time, and by using normal model checking algorithms for the LTL and CTL logics. The SPIN [START_REF] Holzmann | The model checker SPIN[END_REF] model checker is perhaps the most well-known explicit-state model checker that follows this approach.

In recent years the approach of checking timed behaviour using "untimed" model checkers has received renewed attention, with the publication of Lamport's article [START_REF] Lamport | Real-time model checking is really simple[END_REF] on real-time model checking using the TLC model checker. Other recent works along the same lines include [START_REF] Wang | Verifying real-time systems using explicit-time description methods[END_REF] and [START_REF] Van Den Berg | Introducing time in an industrial application of model-checking[END_REF].

In this work we address the verification of timed programs written in the Erlang functional concurrent programming language using the McErlang model checker [START_REF] Fredlund | McErlang: a model checker for a distributed functional programming language[END_REF]. The approach taken is similar to Lamport's approach to real-time model checking in [START_REF] Lamport | Real-time model checking is really simple[END_REF], and also inspired by the timed automata framework, but with a few notable differences. As in Lamport's work, the transitional semantics is defined over a global system state. In contrast to that article there is no explicit clock tick (the minimum observable "time quanta"), rather the tick is derived from the time constraints for the processes in the system, and the granularity of the tick can even vary through the lifetime of the verified system. Moreover, there is no explicit clock process which is responsible for the progress of time.

As demonstrated, such processes can be programmed, and if desired, included in a verification.

In related work for Erlang, Guo et.al. [START_REF] Guo | Verifying Erlang telecommunication systems with the process algebra muCRL[END_REF], verify untimed Erlang programs by translating Erlang into the µCRL process algebra. However, the translation addresses only the high-level concurrency libraries of Erlang. In [START_REF] Guo | Verification of timed Erlang/OTP components using the process algebra mucrl[END_REF], Guo and Derrick consider the verification of timed Erlang/OTP components by means of translating Erlang into µCRL, however without considering the problem of generating finite models (state graphs).

In Sect. 2 and 3 we provide a brief introduction to the Erlang programming language and the McErlang model checker. Then, in Sect. 4, we provide an intuition for the timed semantics for Erlang, and Sect. 5 defines a high-level formal semantics. In Sect. 6 we evaluate the efficiency of the timed semantics; Sect. 7 summarizes the results.

Erlang

Erlang [START_REF] Armstrong | Concurrent Programming in Erlang[END_REF][START_REF] Cesarini | Erlang Programming -A Concurrent Approach to Software Development[END_REF] is a functional concurrent programming language created by the Ericsson company in the 1980s. Ericsson is still maintaining the main Erlang implementation, but it is available as open source since 1998. The chief strength of the language is that it provides excellent support for concurrency, distribution and fault tolerance on top of a dynamically typed and strictly evaluated functional programming language. Concurrency is achieved by lightweight processes communicating through asynchronous message passing. Although Erlang is not a new language, it has experienced considerable growth in users in recent years. This is due in most part to its focus on message passing instead of variable sharing as the main communication mechanism, which enables programmers to write robust and clean code for modern multiprocessor and distributed systems.

Today Erlang is used by Ericsson and many other companies (T-Mobile (UK), and many smaller start-up companies such as e.g. LambdaStream in Spain and Klarna in Sweden) to develop industrial applications, often implementing crucial internet server-side applications. Examples include a high-speed ATM switch developed at Ericsson with over a million lines of Erlang code which had to meet very challenging requirements on software reliability and overall system availability [START_REF] Blau | AXD 301: A new generation ATM switching system[END_REF][START_REF] Wiger | World-class product certification using Erlang[END_REF], parts of Facebook chat, Apache CouchDB -a distributed, faulttolerant and schema-free document-oriented database accessible via a RESTful HTTP/JSON API, etc.

Handling a large number of processes easily turns into an unmanageable task, and therefore Erlang programmers mostly work with higher-level language components. The OTP component library is the most used, it offers design patterns such as: a generic server component (for client-server communication), a finite state machine component, generic TCP/IP communication, and a supervisor component for easy structuring of fault-tolerant systems.

Handling Time in Erlang

As Erlang is relatively well known, we will just describe the main language features which concern timing, i.e., the receive statement and timestamps.

The receive Statement. The basic mechanism for handling time dependent behaviour in Erlang is the timeout clause of a receive statement: The intuitive semantics of the receive statement is as follows. If a message matches a pattern PatI, and the guard GuardI (which may contain variables bound by the match) evaluates to true (and moreover no earlier pattern Patj matches, or the guard GuardJ does not evaluate to true), the message is removed from the mailbox and evaluation continues with expression ExprI under the matching binding.

Concretely, the oldest message in the process mailbox is first matched against the clauses according to the above procedure. If no pattern and guard match this message, the same sequence of tests continues with the second oldest message, and so on. If no message matches, the process waits for the reception of a matching message for at least Deadline milliseconds, until it times out and starts executing the expression TimeoutExpr.

A zero deadline corresponds to the case when, if no matching message is in the mailbox, the timeout can happen at once. The special atom infinity may also be used as a time deadline, signifying waiting forever without timing out.

Timestamps. The API call now() returns the time elapsed since 00:00 GMT, January 1, 1970 as a tuple {MegaSeconds,Seconds,MicroSeconds}.

McErlang [START_REF] Fredlund | McErlang: a model checker for a distributed functional programming language[END_REF][START_REF]McErlang[END_REF] is an explicit-state model checker for programs written in Erlang. Similarly to most explicit state model checkers, McErlang checks concurrent programs against specifications in full linear temporal logic (LTL) using on-the-fly state space exploration algorithms.

The main idea behind the design of McErlang is to re-use as much of the normal Erlang language implementation as possible, but adding a model checking capability. To achieve this, the tool replaces the part of the Erlang runtime system which implements concurrency and message passing, while still using the runtime system for the evaluation of the sequential part of the input programs.

McErlang has built-in support for some Erlang OTP component behaviours that are used in almost all serious Erlang programs such as the supervisor component (for implementing fault-tolerant applications) and the generic server component (implementing a client-server component). The presence of such high-level components in the model checker significantly reduces the gap between original program and the verifiable model, compared to other model checkers.

McErlang has been used in several complex case studies: in the model checking of a Video-on-Demand-server [START_REF] Fredlund | Model checking a VoD server using McErlang[END_REF], in the verification of agent based RoboCup teams [START_REF] Benac Earle | Verifying robocup teams[END_REF], and for the verification of an industrial Erlang process supervision component [START_REF] Castro | A case study on verifying a supervisor component using McErlang[END_REF]. The timed extension of McErlang described in this paper is available at GitHub [22].

A Timed Extension

In the following subsections we first provide an intuition for the untimed Erlang semantics in McErlang, then introduce the timed extension and timestamps.

An Untimed Semantics

Previously, there was only an untimed semantics implemented in McErlang. In the untimed semantics, if a receive statement cannot be executed because there is no matching message in the process mailbox, the timeout is enabled (unless the deadline is infinity). However, another process can send a receivable message to the process and thus disable the timeout. This corresponds to treating timeouts as nondeterministic choices. As an example, consider code below.

P1 = spawn ( fun () -> receive Msg -> ok

after 1000 -> bad end end ) , spawn ( fun () -> P1 ! hello end ).

Two processes are spawned, the first (P1) waiting to receive a message, and timing out after one second (1000 milliseconds) if no message can be received, and the second process sending the message hello to the first.

The state graph of the above program as generated by McErlang is depicted in Fig. 1 below. Note that only side effects are depicted; as the receive statement is not considered a side effect it is not shown. We colour the states where the hello message was received light grey, whereas states where a timeout occurred first are grey, and the arrow of the timeout transition is bold. Clearly there is a race condition in the program: if the message hello is sent first from P1 to the second process a timeout never happens. Alternatively the timeout can happen first; in this case the message is sent anyway but is never received.

Non-Timed Actions are Infinitely Fast. A semantics option, implemented in McErlang, provides a semantics where non-timeout actions are infinitely fast compared to timeouts, i.e., always giving precedence to non-timeout actions. In practice this turns out to be a useful abstraction in many scenarios where the actions of the verified program can be safely assumed to be infinitely fast compared to timed (external) actions.

The state graph for the above program, when this option is enabled, is shown in Fig. 2. Since a timeout is infinitely slow compared to other actions, the timeout never happens since it is disabled by the reception of the hello message.

Adding Explicit Time

The main changes needed in McErlang to implement a timed semantics are to record the current time in the state representation of a running program, and to modify the behaviour of the receive statement in the model checker so that when handling timeouts, the current time is taken into account.

To keep compatibility with normal Erlang code we let the current time be a tuple {MegaSeconds,Seconds,MicroSeconds}, and its initial value is {0,0,0}.

Clearly the presence of a non-infinity timeout clause in a receive statement specifies a minimum waiting period until a timeout happens. In the Erlang documentation there is of course no guarantee for exactly when, after a timer has elapsed, the corresponding timeout happens (as it depends on the operating system, the hardware, etc). However, in this work, as is usual for timed calculi, we also want to be able to specify a maximum waiting period until a timeout happens (a notion sometimes called urgency in timed calculi).

To specify the urgency of a state the function mce_erl:urgent(MaximumWait) is provided. The parameter MaximumWait specifies the maximum number of milliseconds the process can remain in the current state, if it has transitions enabled.

Moreover we reinterpret the notion of an infinitely fast computation (i.e., where normal actions are infinitely fast compared to timeouts) as one where every state has an associated implicit call to mce_erl:urgent(0) signifying that no time can pass if the state has a transition enabled.

For instance, we can add the line mce_erl:urgent(1500) to the running program example (see Fig. 3) to force a timeout to happen before some moment in time. The first process will now wait between 1 and 1.5 seconds for a message to arrive before timing out. Since we have not specified when the second process sends a message both possibilities (timeout or no timeout) remain possible. Its state graph is depicted in Fig. 4; each state is labelled by the current time value in milliseconds. It may be surprising to see that time does not progress in Fig. 4 after the timeout, and that the timeout occurs exactly at the earliest possible moment. This is because the semantics discretizes the progress of time: time makes a discrete jump between two consecutive time values. So what are the consecutive time values? In normal discrete-time semantics there is often an implicit clock, with a tick value which defines the minimum distance between two time values:

t 0 = 0 t 1 = 1 * tick t 2 = 2 * tick • • •
where the t i 's are the time values at different states. In our semantics, in contrast, there is no implicit clock process nor a hard-wired tick clock value increment. Rather, each timeout clause in a receive statement represents a clock tick. However, we can easily implement an explicit clock process, which constantly increments the time value with a tick increment as seen in Fig. 5. Note that if we add an unbounded clock process to the program in Fig. 3, then its state clock ( Tick ) -> mce_erl : urgent (0) , receive after Tick -> clock ( Tick ) end . Fig. 6: A bounded clock graph becomes infinite. To obtain a finite state graph for now (in Sect. 5.1 we overcome this restriction) the bounded clock in Fig. 6 is used instead.

The state graph of program 2, where we add a clock process with a 500ms tick and a duration of 2500ms with the call spawn(fun () -> clock(500,2500) end), is shown in Fig. 7. The timeout transitions in the graph are either timeouts by a process (corresponding to bold arrows as usual) or timeouts by the clock process. In the graph we can see that the timeout behaviour (the bold transition) is enabled after 500ms, and stays enabled until after 1500ms. Note also the white state labelled with 1500 (ms); since the timeout transition with value 0 is urgent, the clock process cannot make a transition which increases time.

Supporting Timestamps

Clocks have an important role to play in decidable real-time calculi, recording the moment an event takes place, relative to other clocks and the general progress of time. In Erlang the function now() returns the time elapsed since 00:00 GMT, January 1, 1970 as a tuple {MegaSeconds,Seconds,MicroSeconds}. Most Erlang programs that handle time simply call now, store the result somewhere, and later compare the old value with the current time. This programming discipline is reminiscent of the use of clocks in timed automata formalisms. The discussion on how to obtain finite models with time is deferred to Sect. 5.1; however, a crucial requirement is that only a finite number of values returned from calls to now() are "alive" (i.e., accessible from some program variable) in any state. It would be possible to tailor a static analysis to track calls to now(), and the flow of the resulting values. Instead we provide the programmer with a new API to obtain time stamps, and to directly manipulate the lifetime of timestamps. Direct calls to now() are forbidden. In general adapting a program to use this new API is trivial; an example is provided below, and Sect. 6.2 contains a further discussion.

The new API located in the module mce_erl_time has the following functions: -returns the time stored in a clock reference forget(Ref) -explicitly destroys an old clock reference There are a number of restrictions on the use of this API. First, times obtained from calls to now() may never be remembered by the program, but only used in comparisons against previously recorded clocks. Moreover, for the soundness of model checking it is forbidden to compare a clock (or the current time) against an absolute time value, only relative comparisons are permitted, e.g., checking how much time has passed since some system event occurred. That is, it is not allowed to check whether now() returns some concrete date and time.

To illustrate the clock API we show below the coding of a fragment of the lamp example [START_REF] Behrmann | A tutorial on uppaal[END_REF] of real-time calculi. A lamp is initially off, and when a button is pressed shines with low intensity. If a button is pressed again within 5 milliseconds, the lamp shines with bright intensity, otherwise if the new button press arrives later, the lamp is switched off. In the code fragment below we show the lamp controller, which receives button presses from a user, and operates the lamp hardware by sending messages to PhysicalLamp. The function compareTimeStamps_ge(T1,T2) returns true if T1 is a later or identical timestamp as T2; addTimeStamps(T1,T2) computes a new time stamp which is the sum of its argument time stamps, and milliSecondsToTimeStamp(N) computes the time stamp corresponding to N milliseconds.

A Semi-Formal Timed Semantics

In the following we describe how a timed semantics can be obtained by modifying an untimed semantics. We assume the presence of a non-hierarchical "global" structured operational semantics for Erlang states, which is the basis of the implementation of the McErlang model checker (unpublished work). For a nonglobal state, hierarchical, semantics of Erlang programs see [START_REF] Fredlund | A Framework for Reasoning about Erlang Code[END_REF][START_REF] Svensson | A more accurate semantics for distributed Erlang[END_REF].

In the untimed "global" semantics, an Erlang state s is, informally, a tuple Nodes, Ether consisting of a set of nodes (Nodes) and a datastructure (Ether ) storing the messages in transit between nodes. To obtain a timed Erlang state we add the current time Time ≡ MegaSeconds, Seconds, MicroSeconds and a set of clocks, i.e., tuples ClockId , Time created by calling nowRef(), to the tuple:

Nodes, Ether , Time, Clocks . A node Processes, Dictionary, Registry, Links, Monitors is a collection of processes, a node global variable store, a process registry (for associating symbolic names to processes), and process links and monitors (for handling fault tolerance). Finally a process Pid , Dictionary, Mailbox , Expr has a mailbox, a process dictionary (an imperative memory), a unique process identifier, and the currently executing expression Expr . The contents of a typical Erlang system state is depicted symbolically in Fig. 8. Solid lines depict inter-node message passing, dashed lines intra-node message passing.

An Erlang untimed action is, informally, a side effect (e.g., a message sent between two processes, registering a symbolic name for a process, etc) or a process internal action. To the untimed actions we add the timed actions corresponding to timeouts, which cause time to progress, and actions corresponding to creating and modifying clocks. We let α range over the actions.

Given that we can compute the untimed transition relation written s α -→ s , which is defined as an structural operational semantics, we obtain the timed transition relation s The first side effect free rule simply replaces a time relative deadline with an absolute deadline; to clarify the semantics we introduce the new synthetic keyword absreceive for such time absolute receive statements.

In the second rule, in a state s, if there is a process p which is executing a receive statement, and which cannot receive a message, then there is a transition labelled by the action timeout(deadline) to a new state where the current time has increased, and where the currently executing expression of p has been replaced. Similar transition rules are added for handling clocks.

Finally we constrain the resulting transition relation to enforce global urgency constraints on the progress of time, using the following high-level Erlang function which first calculates the transitions for a state using the function transitions, and then returns a reduced set of transitions compatible with the notion of urgency introduced in Sect. 4.2. The timeRestrict function is called with the following arguments: a list of transitions which is reduced, the current system time (Now), a list of untimed transitions (Untimed), the time when the most urgent transition seen so far must be taken (MostUrgent), and a list of transitions which are enabled to be executed sometime before the MostUrgent deadline. The function first classifies a timed transition: informally the minimum waiting period is the timeout value in a receive statement, whereas the maximum waiting period is the urgency (specified using a call to mce_erl:urgent). Having infinity as the wait limit signifies that the process will wait forever.

Finite Models

To obtain finite models, i.e., finite state graphs, for timed programs, we note that the actions of a timed program normally depends only on the passage time, not on the absolute value of the time parameter of the system state. Similarly, in the specification logic we make statements only about the relative value of clocks and the system time parameter. Thus, for any given system state there is typically an infinite number of equivalent states, which differ only in that the time system parameter is distinct, but the relative values of clocks and the system time parameter is the same for all these "equivalent" states.

Thus, to obtain finite models, the obvious strategy is to normalize system states, and to generate the state space modulo such normalization. During state space generation, before adding a new node to the state graph, we should check whether its normalization (another state) is already in the graph. If it is, we do not need to consider the new state further. If it is not, we add the normalized state to the state graph, and continue exploring the behaviour of the new state. In [START_REF] Lamport | Real-time model checking is really simple[END_REF] this procedure is referred to as model checking under symmetry.

It turns out to be trivial to add such a normalization to McErlang. The untimed McErlang tool already provided an "abstraction" feature, whereby a user-defined state abstraction function can be used to transform a state before storing it in the state table ; exactly what is needed to implement time normalization. The normalization procedure modifies a state according to the following:

-The system time parameter is reset to {0,0,0} -The values of clocks (created using nowRef()) are decreased by the old time -Timeouts in (absolute) receive statements are decreased by the old time (but greater or equal to the new time)

As an example, the state graph for the program in Fig. 3, with the unbounded clock in Fig. 5, and using the above normalization, is depicted in Fig. 9. Note that states are no longer labeled by the current time, as the normalization collapses many states with distinct times into a single state. To evaluate the resulting semantics and its implementation we below provide some initial benchmark results, and report on the challenges in obtaining a verifiable timed model from a crucial Erlang software component used in industry.

Efficiency

We evaluate the efficiency of the resulting implementation by checking Fischer's mutual exclusion algorithm [START_REF] Gafni | Analysis of timing-based mutual exclusion with random times[END_REF]. Fig. 10 contains an implementation of the algorithm in Erlang. The global node dictionary extension of McErlang is used to implement reading and writing to the shared variable; see the functions read and write. The entering of the critical region of a process Id is indicated by a synthetic probe action mce_erl:probe({enter,Id}). The latest(Tick,Wait,F) function calls the function parameter F at most Wait milliseconds later; the time interval is partitioned into slices of maximum size Tick (the slices could be smaller if other clocks are defined).

We check mutual exclusion in a range of experiments characterized by the parameters of the start(N,Tick,D,T) function: N is the number of processes, Tick is the time tick, D is the maximum time to wait until writing to the shared variable, and T is the minimum time to wait until reading from the shared variable. Note that in this experiment we do not assume that internal actions are infinitely fast compared to timers. As seen in Table 1 the size of the state space is exponential in the number of processes (N). In the last four rows the effect of an increase in the values of the timers is indicated. To verify the correctness of the algorithm a simple monitor checks that enter and exit probe actions strictly alternate. As expected, if writing is slower than reading, e.g., D > T, the algorithm works correctly and otherwise a counterexample is quickly found. Overall, the size of state spaces and the execution times are reasonable.

These functions define the restarting policies of the supervisor. The function add_restart is called when a child process should be restarted due to having terminated abnormally. However, a constraint on restarting is that the child process may not have been restarted more than MaxR times within MaxT seconds. If this constraint is violated, the supervisor terminates all child processes and then itself.

Correctness properties are specified as safety monitors that inspect the actions of a the supervisor and processes interacting with the supervisor; see [START_REF] Castro | A case study on verifying a supervisor component using McErlang[END_REF] for details. Using untimed McErlang we were not able to verify time dependent properties for the supervisor component, but had to resort to expressing the timing checks as a nondeterministic choice.

Using timed McErlang there is no need to change any of the 760 lines of code, although a few lines of code had to be added to delete the time clocks created using nowRef(). Of course we still need to create verification scenarios that explore the behaviour of the supervisor in detail, i.e., programming child process terminating abnormally and being restarted in narrow time intervals.

Conclusions

We have implemented a timed semantics for the Erlang programming language in the McErlang model checker, and have demonstrated that the resulting tool is capable of verifying timed systems. Compared to other similar semantics our semantics has a few interesting characteristics such as e.g. the absence of a dedicated time tick.

Currently the timed implementation is undergoing a study as to its suitability as a workbench for analysing Timed Rebeca programs. Earlier work [START_REF] Aceto | Modelling and simulation of asynchronous real-time systems using Timed Rebeca[END_REF] has implemented a translation from Timed Rebeca to Erlang, and has used untimed McErlang to simulate and test the resulting programs against correctness properties specified as safety monitors. In recent work, the new timed McErlang model checker, and the language extensions to specify urgency and clocks, are being used to verify Timed Rebeca programs.

Fig. 1 :Fig. 2 :

 12 Fig. 1: State graph with no precedence

  mce_erl : urgent (1500) , receive Msg -> ok after 1000 -> bad end end ) , spawn ( fun () -> P1 ! hello end ).

Fig. 3 Fig. 4 :

 34 Fig. 3: Program 2

Fig. 5 :

 5 Fig. 5: An unbounded clock

Fig. 7 :

 7 Fig. 7: State graph with an explicit bounded clock process

  now () , addTimeStamps ( m il l iS ec o nd s To Ti m eS ta m p (5) , mce_erl_time : was ( PressTime ))) of true -> PhysicalLamp ! off , mce_erl_time : forget ( PressTime ) , ...; false -> PhysicalLamp ! bright , mce_erl_time : forget ( PressTime ) , ... end end end .

Fig. 8 :

 8 Fig. 8: An Erlang multi-node system

  timeRestrict ( State ) -> Now = State # state . time , Transitions = transitions ( State ) , timeRestrict ( Transitions , Now , [ ] , infinity , [ ] ). timeRestrict ( [ ] ,_ , Untimed ,_ , Timed ) -> Untimed ++ Timed ; timeRestrict ( Transitions , Now , Untimed , MostUrgent , Timed ) -> [ Transition | Rest ] = Transitions , MinWait = calculate_minwait ( Transition ) , MaxWait = calculate_maxwait ( Transition ) , if MinWait == infinity orelse MinWait > MostUrgent -> timeRestrict ( Rest , Now , Untimed , MostUrgent , Timed ); MaxWait == infinity andalso MinWait == Now -> NewNonTimed = [ Transition | NonTimed ] , timeRestrict ( Rest , Now , NewNonTimed , MostUrgent , Timed ); MinWait = < MaxWait < MostUrgent -> NewTimed = [ Transition | restrict ( MaxWait , TimerEntries ) ] , timeRestrict ( Rest , Now , NonTimed , MaxWait , Newtimed ); MinWait = < MostUrgent = < MaxWait -> NewTimed = [ Transition | TimerEntries ] , timeRestrict ( Rest , Now , NonTimed , MostUrgent , NewTimed ) end . restrict ( MaxWait , [ ] ) -> [ ] ; restrict ( MaxWait , [ Transition | Rest ] ) -> MinWait = calculate_minwait ( Transition ) , if MinWait = < MaxWait -> [ Transition | restrict ( MaxWait , Rest ) ] ; MinWait > MaxWait -> restrict ( MaxWait , Rest ) end .

Fig. 9 :

 9 Fig. 9: State graph for the program in Fig. 4 with an explicit unbounded clock process, and finite model abstraction

Table 1 :

 1 Execution times for Fischer's algorithm

	N Tick D T Time (secs.) Number of states
	4	1	1	2	0.1s	2034
	5	1	1	2	0.7s	13738
	6	1	1	2	7.6s	89051
	7	1	1	2	50.3s	580080
	5	1	2	3	4.4s	81452
	5	1	3	4	12.7s	268793
	5	1	4	5	36.7s	704901
	5	1	5	6	73.7s	1522179

This work has been partially supported by the following projects: DESAFIOS10 (TIN2009-14599-C03-00), PROMETIDOS (P2009/TIC-1465), pSAFECER (GA 269265) and nSAFECER (GA 295373).

Expressive Power

As a final example we consider the verification of the nos supervisor library [START_REF] Castro | A case study on verifying a supervisor component using McErlang[END_REF]; this is a crucial software component used in several industrial projects at the LambdaStream company [START_REF] Lambdastream | [END_REF].

A supervisor is a process in charge of starting, stopping and monitoring a set of children (processes). Basically whenever a child process terminates the supervisor should restart it, i.e., spawn a new process executing the task of the terminated child. A supervisor typically supervises not only process workers, but also other supervisors, defining a hierarchical structure as shown in Fig. 11.

Supervisor1 Worker1 Supervisor2

Worker3 Supervisor3

Worker4 Worker5

Worker2

Fig. 11: A supervision tree.

The nos supervisor is implemented in around 760 lines of Erlang code. To enable untimed verification of part of its functionality in [START_REF] Castro | A case study on verifying a supervisor component using McErlang[END_REF] we had to modify the functions below:


Brice Effantin

A note on Grundy colorings of central graphs *

Keywords: Vertex coloring, Grundy coloring, Central graph. 2010 Mathematics Subject Classification: 05C15

A Grundy coloring of a graph G is a proper vertex coloring of G where any vertex x, colored with c(x), has a neighbor of any color 1, 2, . . . , c(x)-1. A central graph G c is obtained from G by adding an edge between any two non adjacent vertices in G and subdividing any edge of G once. In this note we focus on Grundy colorings of central graphs. We present some bounds related to parameters of G and a Nordhaus-Gaddum inequality. We also determine exact values for the Grundy coloring of some central classical graphs.

Introduction

We consider connected graphs without loops or multiple edges. In a graph G = (V, E), the set V (G) is the set of vertices (|V (G)| = n is the order of G) and E(G) is the set of edges (|E(G)| = m is the size of G). The number of neighbors of a vertex x in G is its degree, denoted d G (x), and the maximum (resp. minimum) degree of the graph is denoted ∆(G) (resp. δ(G)). The set of neighbors of x in G is denoted N G (x).

For a graph G = (V, E), a k-coloring of G is defined as a function c on V (G) into a set of colors C = {1, 2, . . . , k} such that for each vertex x i , 1 ≤ i ≤ |V (G)|, we have c(x i ) ∈ C. A proper k-coloring is a k-coloring satisfying c(x i ) = c(x j ) for every pair of adjacent vertices x i , x j ∈ V (G). For a given proper k-coloring, a vertex x i adjacent to a vertex of every color q, q < c(x i ), is called a Grundy vertex for the color c(x i ). A Grundy k-coloring is a proper k-coloring where any vertex is a Grundy vertex. In 1979 Christen and Selkow [START_REF] Christen | Some perfect coloring properties of graphs[END_REF] introduced the Grundy number, denoted by Γ(G), as the maximum number of colors among all Grundy colorings of G. It is obvious that Γ(G) ≤ ∆(G)+1 but the determination of the Grundy number is NP-complete in general. This parameter was then 2 Nordhaus-Gaddum inequality type for the Grundy number of central graphs

In this section we present an upper bound for Nordhaus-Gaddum inequality Γ(G c ) + Γ(G c ). Different studies consider Nordhaus-Gaddum inequalities type for the Grundy number (see the survey [START_REF] Aouchiche | A survey of Nordhaus-Gaddum type relations[END_REF] where such inequalities are presented for several parameters). Zaker [START_REF] Zaker | Results on the Grundy chromatic number of graphs[END_REF] proposed some results in 2006 and he conjectured that Γ(G) + Γ(G) ≤ n + 2 for any graph G. This conjecture was confirmed by Füredi et al. [START_REF] Füredi | Inequalities for the First-Fit Chromatic Number[END_REF] for general graphs with n ≤ 8 and disproved for n ≥ 9 and they give the following result.

Theorem 2.1. ( [START_REF] Füredi | Inequalities for the First-Fit Chromatic Number[END_REF]) Let G be a graph of order n, then

Γ(G) + Γ(G) ≤    n + 2 if n ≤ 8, 12 if n = 9, 5n+2 4
otherwise.

We start our study with bounds for the Grundy numbers of G c and its complement.

Proposition 2.2. Let G be a graph of order n. Then 1 + Γ(G) ≤ Γ(G c ) ≤ min{n, n+2-δ(G)} if G is connected and Γ(G) ≤ Γ(G c ) ≤ min{n, n+2-δ(G)} otherwise. Proof. The bound Γ(G c ) ≥ Γ(G) is obvious since G ⊆ G c . Consider a connected graph G and a Grundy coloring C of G. In G c put the coloring C on V 1 (G c )
shifted by 1 and put the color 1 on all the vertices of V

2 (G c ). Then Γ(G c ) ≥ Γ(G) + 1. Next, since ∆(G c ) ≤ n -1 we have Γ(G c ) ≤ ∆(G c ) + 1 ≤ n. Moreover every vertex x i of V 1 has degree d G c (x i ) = n -1 and it follows that the maximum number of colors in N G c (x i ) is (n -1) -d G (x i ) + 2 because d G (x i ) neighbors of x i in G c
are vertices of V 2 which can be colored only by 1 or 2. Therefore Γ(G c ) ≤ (n -1) -δ(G) + 2 + 1 and the result holds.

Corollary 2.3. Let G be a graph of stability number α(G). Then Γ(G c ) ≥ α(G) + 1. Proof. Let S be a stable set in G of size α(G) (S is a clique in G). By Proposition 2.2 we have Γ(G c ) ≥ Γ(G) + 1 ≥ α(G) + 1.
Proposition 2.4. Let G be a graph of order n and size m.

Then m ≤ Γ(G c ) ≤ m + n -2. Proof. By construction, vertices of V 2 (G c ) form a clique in G c . Thus Γ(G c ) ≥ |V 2 (G c )| = m. Moreover in G c , each vertex of V 2 (G c ) has the maximum degree ∆(G c ) = (m -1) + (n -2) = n + m -3 and Γ(G c ) ≤ ∆(G c ) + 1 = n + m -2.
We then present an upper bound for Γ(G c ) + Γ(G c ) which improves the bound of Theorem 2.1 for central graphs when n ≥ 10 and m is large enough. Theorem 2.5. Let G be a graph of order n and size m.

Then Γ(G c ) + Γ(G c ) ≤ min{m + 2n -2, m + 2n -δ(G)}.
Proof. Deduced from Propositions 2.2 and 2.4.

Remark. Note that G c is of order n ′ = n + m. Consider δ(G) ≥ 2. Thus from Theorem 2.5, if n ≥ 10 and m ≥ 3n + 5 -4δ(G) then

m ≥ 3n + 5 -4δ(G), m + (4m + 5n -1) ≥ 3n + 5 -4δ(G) + (4m + 5n -1), 5n ′ -1 ≥ 4m + 8n + 4 -4δ(G), 5n ′ + 2 4 ≥ 5n ′ -1 4 ≥ m + 2n + 1 -δ(G) > m + 2n -δ(G),
and the upper bound of Theorem 2.1 is improved for central graphs. By the same way if we consider δ(G) = 1, n ≥ 10 and m ≥ 3n -3, we have a similar

relation 5n ′ +2 4 > m + 2n -2.
3 The Grundy number of some central graphs

In the above section we showed that α(G)

+ 1 ≤ Γ(G c ) ≤ min{n, n + 2 -δ(G)}.
Now we present exact values for the Grundy number of central graphs for some classical graphs where the both bounds are reached. In particular we consider the central graphs of complete graphs, complete bipartite graphs, complete kary trees, paths and cycles. Before studying these classes of graphs we can do some remarks on the Grundy number of a central graph G c versus the Grundy number of G. Indeed we have G ⊆ G c which gives the following bounds.

Proposition 3.1. Let G be a graph. Then, Γ(G) + 1 ≤ Γ(G c ) ≤ Γ(G) + 2 if G is connected and Γ(G) ≤ Γ(G c ) ≤ Γ(G) + 2 otherwise.
Proof. The lower bounds are given by Proposition 2.2. And if we suppose a Grundy coloring of

G c with k ≥ Γ(G) + 3 colors, then a vertex x colored by c(x) ≥ Γ(G) + 3 has a neighbor in V 2 (G c ) with color c ′ ≥ 3 which cannot be satisfied, a contradiction. Therefore Γ(G c ) ≤ Γ(G) + 2
From this relation we see that it is possible to determine the Grundy number of a central graph G c from the Grundy number of the complement graph G in polynomial time. Proposition 3.2. Let G be the complement graph of a connected graph G with a Grundy coloring of Γ(G) colors. Then a coloring of G c can be determined in polynomial time.

Proof. By Proposition 3.1 we see that Γ(G c ) can have two possible values. For the lower value, a polynomial coloring algorithm is given in Proposition 2.2. Then note that Zaker [START_REF] Zaker | Results on the Grundy chromatic number of graphs[END_REF] introduced the concept of t-atom which is a sufficient and necessary condition to have a Grundy coloring of t colors (i.e. a minimal induced subgraph of G, Grundy colorable with t colors). Moreover in [START_REF] Zaker | Results on the Grundy chromatic number of graphs[END_REF], Zaker shows how to construct the set of t-atoms (from (t -1)-atoms) and he proves (Theorem 1 and its corollary) that there exists a polynomial time algorithm to determine whether Γ(G) ≥ t for any given graph G and integer t by determining if one of the t-atoms (generated above) exists in G. If exists, the coloring of such a t-atom can be extended in a polynomial time algorithm to the remaining of G by a greedy algorithm and Γ(G) ≥ t. Therefore in a polynomial time algorithm we can determine if Γ(G c ) ≥ Γ(G) + 2 (and by Proposition

3.1, Γ(G c ) = Γ(G) + 2).
Despite the relation between central and complement graphs, for general central graph the problem of determining the Grundy number stays a NP-complete problem. This is why we focus on particular classes of central graphs. Firstly we consider complete and bipartite graphs.

Theorem 3.3. Let K n be a complete graph of order n ≥ 4. Then Γ(K c n ) = 3.
Proof. In K c n there exits an induced subpath P 4 colorable with colors 1-2-3-1 (a Grundy coloring). Then remaining vertices are colorable in a proper coloring and Γ(K

c n ) ≥ 3. Moreover δ(K n ) = n -1 and Proposition 2.2 gives Γ(K c n ) ≤ n + 2 -δ(K n ) = 3.
Theorem 3.4. Let K p,q be a complete bipartite graph of order p + q, with p ≥ q ≥ 2. Then Γ(K c p,q ) = p + 2.

Proof. Denote by S p = {x 1 , x 2 , . . . , x p } and S q = {x p+1 , x p+2 , . . . , x p+q } the partitions of K p,q . Vertices of S p form a clique in K c p,q . Color these vertices with colors 3, 4, . . . , p + 2. Then put c(x p+1 ) = 1 and color the vertices of V 2 (K c p,q ) as follows: c(x i,p+1 ) = 2 for any 1 ≤ i ≤ p and the others with color 1. Thus each vertex of S p is adjacent to all the colors (except its own color). Moreover vertices x i,p+1 (1 ≤ i ≤ p) are also satisfied because c(x p+1 ) = 1. Remaining vertices can be properly colored and the coloring is a Grundy coloring. Thus Γ(K c p,q ) ≥ p + 2. Furthermore we have δ(K p,q ) = q and Proposition 2.2 gives Γ(K c p,q ) ≤ (p + q) + 2 -δ(K p,q ) = p + 2.

Secondly we consider complete rooted trees. In a rooted tree of height h, the root is on the level 0 while the leaves are on level h. Moreover for a vertex x on level i (0 ≤ i < h), a son of x is a neighbor of x on level i + 1. Theorem 3.5. Let T k,h be a complete k-ary tree of height h ≥ 4, with k ≥ 2. Let L(i) be the number of vertices on the level i (L(i) = k i ). Then Γ(T c k,h ) = 1 + i∈I L(i) where I = {0, 2, . . . , h} if h is even and I = {1, 3, . . . , h} if h is odd.

Proof. Let q = i∈I L(i) with I = {0, 2, . . . , h} if h is even and I = {1, 3, . . . , h} if h is odd. Note that q corresponds to the number of vertices in the even levels if h is even (resp. odd levels if h is odd) of the tree T k,h . In T k,h we have α(T k,h ) ≥ q and by Corollary 2.3 we deduce Γ(T c k,h ) ≥ 1 + q. The upper bound can be proved by contradiction. Suppose there exists a Grundy coloring of T c k,h with q ′ colors such that q ′ ≥ 2 + q. We see that T k,h can be decomposed into two cliques K o and K e (due to respectively odd and even levels) where there exists an edge between each vertex of a set and at most k + 1 vertices of the other set (corresponding to its neighbor in the previous level, if exists, and its k neighbors in the next level in T k,h , if exist). The graph T c k,h is the same one where each edge between cliques is splitted by a vertex of V 2 . Note that since h ≥ 4 and k ≥ 2 we have q > max{4, k + 1}. Thus we have q

= |K o | > |K e | if h is odd while q = |K e | > |K o | otherwise.
Without loss of generality, consider h is odd and q = |K o | > |K e |. We see that color 2 cannot be on a vertex of K o , otherwise any vertex of K o with color c > 3 must have a neighbor in V 2 colored by 3, a contradiction. Then K o contains colors 3 to q + 2 and these vertices need colors 1 and 2 on V 2 . Thus at least q vertices of V 2 have color 2. Since each vertex of K e has at most k + 1 neighbors of V 2 and q > k + 1, then at least two vertices of K e are adjacent to vertices of V 2 colored by 2 and must be colored with color 1. This implies a non proper coloring because K e is a clique, a contradiction. Therefore Γ(T c k,h ) ≤ 1 + q. Finally we focus on central graphs of paths and cycles. Paths and cycles are classical graphs. Several graphs based on them have been studied. For instance the Grundy number of power paths and power cycles was studied in [START_REF] Germain | Grundy numbers of powers of graphs[END_REF]. Power graphs G p are obtained from G by adding edges between vertices at distance at most p in G. A central graph is then a power graph (where p is the diameter of G) with new added vertices. Moreover recently central paths and central cycles were considered for another maximal coloring called the b-coloring [START_REF] Thilagavathi | b-colouring of central graphs[END_REF].

We start with some results on the number of colors used on Grundy colorings. Lemma 3.6. Let G be either a path P n or a cycle C n of order n ≥ 6. In G c , denote by C i the set of colors used on V i , with i ∈ {1, 2}. In any Grundy coloring of G c only the color c = 1 can satisfy c ∈ C 2 and c / ∈ C 1 .

Proof. Suppose that two distinct colors c 1 and c 2 appear only on

V 2 , i.e. c 1 , c 2 ∈ C 2 and c 1 , c 2 / ∈ C 1 (assume c 1 > c 2 ).
To satisfy a vertex colored by c 1 the color c 2 must be repeated on V 1 . This is a contradiction and a unique color c can appear only on V 2 . Suppose that c > 1. To satisfy the vertices of V 2 and since n ≥ 6 (so |V 2 | ≥ 4), there exist two vertices of V 1 colored by 1 such that the distance between them is 2 or more (i.e. they are adjacent in G c ). This contradicts the property of the coloring. Hence all vertices of V 2 are colored with color 1. Proof. Colors 2 to k are on vertices of V 1 (by Lemma 3.6). Let n u and n r be the numbers of respectively unique and repeated colors on V 1 (note that n u + n r = k -1). Moreover two vertices with unique colors must be adjacent to satisfy the largest one (i.e. they cannot be on consecutive vertices of

V 1 ), thus n r ≥ n u . a) Suppose that n r < k-1 2 . Then we have k-1 2 > n r ≥ n u = k -1 -n r ≥ k-1 2
, a contradiction. Thus at least k-1

2 vertices of V 1 have repeated colors.
b) Since we have at least k-1 2 repeated colors, suppose the coloring has exactly n r = k-1

2 repeated colors. If k is even then n r = k-2 2 and k-2 2 = n r ≥ n u = k -1 -n r = k 2 , a contradiction. If k is odd (thus k ≥ 2q + 3) then we have n r = k-1 2 and n u = k -1 -n r = k-1 2 .
Since the colors of n u (put once) and n r determination of the partial Grundy number is also NP-complete in general but it is obvious that δΓ(G) ≥ Γ(G). The results presented above on Grundy colorings give first bounds for the partial Grundy number of central graphs.

Corollary 4.1. Let G be a graph of order n and size m. Then, a)

1 + Γ(G) ≤ δΓ(G c ) ≤ n, b) δΓ(G c ) ≥ α(G) + 1, c) m ≤ δΓ(G c ) ≤ m + n -2, d) δΓ(G c ) + δΓ(G c ) ≤ m + 2n -2.
Proof. This is deduced from the fact that Γ(G) ≤ δΓ(G) ≤ ∆(G) + 1 for any graph G. For case c, see Proposition 2.4.

However even for such a coloring we can find classes of central graphs for which the upper bound δΓ(G c ) ≤ n is reached (for instance central chordal graphs) while it is not for some others (for instance central even paths). A graph is a chordal graph if each induced cycle of length 4 or more has a chord (an edge connecting two non adjacent vertices). Chordal graphs are sometimes called triangulated graphs. Proof. By Corollary 4.1 we have δΓ(G c ) ≤ n. The lower bound is given by construction. Color the vertices of V 1 with colors 1, 2, . . . , n. Then in G c , for every triangle {x i , x j , x k }, with c(x i ) > c(x j ) > c(x k ), vertex x i does not reach colors c(x j ) and c(x k ) (and vertex x j does not reach color c(x k )). Then put c(x i,j ) = c(x k ) and c(x i,k ) = c(x j ) to make x i and x j Grundy vertices. Thus all the vertices of V 1 are Grundy vertices. If it remains non colored vertices of V 2 they can be properly colored with color 1, 2 or 3 since they have degree 2. Therefore δΓ(G c ) ≥ n. Theorem 4.3. Let P n be a path of order n ≥ 7. Then,

δΓ(P c n ) = n if n is odd, n -1 otherwise.
Proof. Consider n odd. Color c(x i ) = i for odd i and c(x i ) = i + 2 for even i, with 1 ≤ i ≤ n -2. Then put c(x n-1 ) = n and c(x n ) = 2. Vertices x i , with odd i, are already Grundy vertices. Finally color c(x i,i-1 ) = c(x i+1 ) and c(x i,i+1 ) = c(x i-1 ) for even i with 1 ≤ i ≤ n. Thus all the vertices are colored and each vertex of V 1 is a Grundy vertex (δΓ(P c n ) ≥ n). And by Corollary 4.1 we have δΓ(P c n ) ≤ n.

Consider n even. The lower bound is given by construction. Put c(x i ) = i for any 1 ≤ i ≤ n -1, and c(x j,j+1 ) = c(x j-1 ) for any 2 ≤ j ≤ n -1. Thus every colored vertex of V 1 is a Grundy vertex. Remaining vertices can be properly colored and δΓ(P c n ) ≥ n-1. Next suppose there exists a partial Grundy coloring of P c n using q ≥ n colors. Note that c(x 1 ) ≤ c(x 2 ) and c(x n ) ≤ c(x n-1 ) to have a proper coloring of c(x 1,2 ) and c(x n-1,n ). Moreover we also observe that either c(x 1 ) < c(x 2 ) or c(x n ) < x n-1 (or both), otherwise the q -1 ≥ n-1 colors (only one color can appear only on V 2 ) are on the n -2 remaining vertices of V 1 , a contradiction. Then there exist four consecutive vertices x i , x i+1 , x i+2 , x i+3 such that c(x i ) < c(x i+1 ) < c(x i+2 ) and c(x i+2 ) > c(x i+3 ) (or c(x i+1 ) > c(x i+2 ) > c(x i+3 ) and c(x i ) < c(x i+1 )). In both cases vertices x i+1 and x i+2 are Grundy vertices in a proper coloring of P c n which implies c(x i+1,i+2 ) = c(x i ) (for x i+1 ) and c(x i+1,i+2 ) = c(x i+3 ) (for x i+2 ), a contradiction. Therefore δΓ(P c n ) ≤ n -1.

Lemma 3 . 7 . 2 + 1

 3721 Let P n and C n be respectively a path and a cycle of order n = 3q + r ≥ 6, with 0 ≤ r ≤ 2. Then, a) any Grundy coloring of P c n or C c n using k ≥ 2 n 3 + 1 colors has at least k-1 2 repeated colors. b) any Grundy coloring of C c n using k > 2 n 3 + 1 colors has at least k-1 repeated colors, if r ∈ {1, 2}.

Theorem 4 . 2 .

 42 Let G be a chordal graph of order n ≥ 3. Then δΓ(G c ) = n.

Acknowledgments

I would like to thank the referees for their valuable remarks that improved the clarity of the paper.

* Supported by the ANR-14-CE25-0006 project of the French National Research Agency 1

(put twice) allow to color V 1 , we have n ≥ n u + 2n r ≥ k-1 2 + k -1 ≥ 3q + 3, a contradiction. Therefore we have n r > k-1 2 .

We then propose the following exact value for the Grundy number of central paths.

Theorem 3.8. Let P n be a path of order n = 3q + r ≥ 6, with 0 ≤ r ≤ 2. The Grundy number of P c n is given by

3 + 2 otherwise. Proof. By construction only two consecutive vertices on V 1 can have the same color in a proper coloring of P c n . Suppose there exists a Grundy coloring of P c n on k colors where k > 2 n 3 + 1 if r = 0 and k > 2 n 3 + 2 otherwise. Lemma 3.7 shows that at least N ≥ k-1 2 colors are repeated on the vertices of V 1 (remaining colors are then put once). Since a color is repeated at most twice, the n vertices of V 1 are colored by at least (k -1) + N colors (color 1 on V 2 , see Lemma 3.6). We distinguish two cases:

We obtain a contradiction for each case. Therefore Γ(P c n ) ≤ 2 n 3 + 1 if r = 0 and Γ(P c n ) ≤ 2 n 3 + 2 otherwise. The lower bounds are given by construction. Let k = 2 n 3 + 2. We color all the vertices of V 2 with the color 1. Then we color c(

The coloring is then a Grundy coloring. Indeed first note that each vertex of V 1 is adjacent to the color 1 since it is put on all the vertices of V 2 . Then since every color c of the interval [2, n 3 + 1] is put twice, every vertex of V 1 can reach the color c (except the vertices colored by c). Moreover, since the distance in P n between two vertices with colors from [ n 3 + 2; k] (resp.

Finally we determine the exact value of the Grundy number of central cycles.

Theorem 3.9. Let C n be a cycle of order n, with n = 3q + r ≥ 6 and 0 ≤ r ≤ 2.

Then the Grundy number of C c n is given by

Proof. As in Theorem 3.8 we can prove the upper bound by contradiction. Suppose there exists a Grundy coloring of C c n with k colors where k > 2 n 3 + 1 if r = 0 and k > 2 n 3 + r otherwise. Lemma 3.7 shows that at least N colors are repeated on the vertices of V 1 (remaining colors are then put once), with N ≥ k-1 2 if r = 0 and N ≥ 1 + k-1 2 otherwise. Thus the n vertices of V 1 must be colored by at least (k -1) + N colors (color 1 is on V 2 , by Lemma 3.6). We distinguish three cases:

The lower bounds are deduced from the constructions given in Theorem 3.8 for the central graphs of paths. Let G be the induced subgraph of

By the same way, put the coloring of Theorem 3.8 (case r = 1) on G. Note that since x 1 is not adjacent to x n (which is the unique vertex of its color) in C c n , we recolor x n such that c(x n ) = c(x 1 ). Moreover since c(x n-1 ) = c(x n-2 ) then x n is a Grundy vertex. We complete the coloring of C c n by c(x n,1 ) = 1. Therefore Γ(C c n ) = Γ(C(P n )) -1 = 2 n 3 + 1. Finally consider r = 2. Put the coloring of Theorem 3.8 (case r = 2) on G and recolor x n such that c(x n ) = c(x 1 ) (x n is a Grundy vertex since x n and x n-1 are not adjacent in C c n and c(x n ) < c(x n-1 )). Note that x n-1 remains the last vertex of its color but it stays a Grundy vertex. We complete the coloring of C c n by c(x n,1 ) = 1 and we have Γ

Conclusion

We have presented some results on the Grundy colorings of central graphs. In particular we have given exact values for the central graphs of some classical graphs and have shown that lower and upper bounds given in Proposition 2.2 and Corollary 2.3 are reached.

A relaxed approach of the Grundy coloring, called the partial Grundy coloring, was introduced by Erdős et al. [START_REF] Erdős | On the equality of the partial Grundy and upper ochromatic numbers of a graph[END_REF] where every color has at least one Grundy vertex. The partial Grundy number, denoted δΓ(G), is then defined as the maximum integer k such that G admits a partial Grundy k-coloring. The