Shoyeb Al

Mamun Shohag

An Observation and Analysis of IPTV and Multicasting Traffic

Keywords: Computer Network, Information and Communication Technology IPTV, Multicasting, STB (Set-to Box), GOP (Group of Picture), ST (Transport Stream), PIM (Protocol Independent Module), IGMP (Internet Group Message protocol), CGMP

. This paper describes the functionality of IPTV protocol and Multicasting with a short background of its. We also have studied on various compression techniques of audio and video file and format. Our main intention was to observed how various protocols works with IPTV services like Protocol independent module (PIM), Internet group messages protocol (IGMP), and Cisco group management protocol (CGMP) when packets are interchanged with in router, switch, video server and clients. To observe these, a lab work on IPTV has been conducted and the findings have been discussed.

INTRODUCTION

Packets are traverse from one host to another host which is normally referred as unicast transmissions or from one host to all hosts that is referred to as broadcast. IP Multicast provides a third communication allowing a host to send packets to a group that is made up of a subset of the hosts on the network. IP Multicast is a bandwidth-conserving technology specifically designed to reduce traffic by simultaneously delivering a single stream of information to potentially thousands of corporate recipients or homes. By replacing copies for all recipients with the delivery of a single stream of information, IP Multicast is able to minimize the burden on both sending and receiving hosts and reduce overall network traffic.

BACGROUND STUDY 2.1 Literature Review

The authors in [START_REF] Pajdušáková | Triple play service and IPTV services offered within it[END_REF] mainly focused on triple play services (voice, data and video) and demonstrates the architecture of its. They also points out various services of IPTV and especially works on video on demand service (VoD). The authors has showed architecture of VoD services and describes working principles of its.

According to [START_REF] Tilovska | Performance Model of Key Points at the IPTV Networks[END_REF], the authors have developed an analytical model for the key points of IPTV networks (head-ends, network transport monitoring, last mile, set-top-box). Finally they summarized as their test result with this model has given an important result in terms of IPTV performance measurement. They also finds few factors (encoding and compression, jitter, packet loss, limited bandwidth) those effects IPTV networks.

In [3], the authors worked with error resilience methods and data partitioning for IPTV video stream over IEEE 802.16e Channel. They have proposed a FEC protection scheme for data partitioning of video stream by retransmission of additional data as and when it is required. They also have tested their proposed scheme and remarked as, it is not sufficient to apply just application FEC with poor channel condition that comes from slow and fast fading. The authors also remarked that a number of measurements required on their proposed schemes to deliver a good quality video in realistically.

The tendency of the authors in [START_REF] Gonzalez-Miranda | Converging Multidomain Services in an IMS environment for IPTV and 3G Networks[END_REF], was to develop a convergence service environment so that service requester can get access on various services (IPTV, ENUM and IMS) from various devices and multiple domains and even from different networks. Finally, they have proposed a compound modular architecture to define and provision the future internet service to a common platform, and tested their proposed architecture by the interconnection of different prototype deployed with this project work.

QoS management mechanism for IMS network component control and service delivery have been proposed by 3GPP but that mechanism only focused on the steps of service provisioning and didn't have any mechanism to monitor QoS dynamically. The authors in [START_REF] Leghroudi | ETOM process to Manitor and Corelat IPTV QoS in IMS[END_REF], has developed a QoS mechanism for the next generation IMS network and for IPTV service specific QoS policies, and this mechanism has been designed based on eTOM process. They have said and proof that their created platform will acts as proactive supervisor of the IMS network. It will correct and anticipate the QoS degradations before failures occur at customer premises.

The authors in [START_REF] Xiao | Internet Protocol Television (IPTV): The Killer Application for the Next-Generation Internet[END_REF] In [7], the authors discussed that traditional unicast is not adequate for IPTV. XDSL can support limited number of TV channels. Author analyse that using multicast in core network avoids multiple copies in core, but still we have multiple copies at the access network. To provide IPTV with high QoS, multicast mechanism is essential. This paper has also analysis on the communication scenarios for IGMPv1 and IGMP v2.

The authors in [START_REF] She | IPTV over WiMAX: Key Success Factors, Challenges, and Solutions[END_REF]

MPEG-2

Figure 1: MPEG packet format It's a standard that define the generic coding of moving picture and associated audio information. It describes a lossy video compression and lossy audio data compression method that permit storage and transmission of video data using currently available storage media and transmission bandwidth. Lossy compression is a method where data is compressed and then decompressed; the received data is different one from the original but it is close enough to be useful in some way [9]. MPEG-2 allows two forms of multiplexing one is MPEG program stream and the other is MPEG transport stream.

MPEG Transport Stream

It consists of a sequence of fixed sized transport packet of 88 bytes, where each packet takes 184 bytes of payload and a 4 byte header. A 13 bit packet identifier (PID) include in the 4 byte header that play a key role in the operation of the transport layer. According to [10], the packet format looks like as fig- 1.

The header field start with a byte called synchronisations that has a bit pattern like 0x47(01000111). Three flag fields also there in the packet format in fig- 1. The first flag is used to indicate transport error (1 bit), second flag is used to denote the start of payload and third flag is for transport priority (1 bit). A 13 bit packet identifier (PID) is used to uniquely identify the stream to which the packet belongs to. Two scrambling bit are also used to encrypt the payload of some TS packets. Adaptation field (2 bit) is used with the combinations like 01 for payload only, 10 indicate no payload, 01 followed by payload and 00 reserved for future use. Lastly, there is a 4 bit continuity counter.

Video Stream

The MPEG-2 video coding standard is primarily aimed at coding of CCIRR-601 or higher resolution video with fairly to support a challenging bitrates of 4 to 9 Mbps. The video stream data hierarchy look like as fig-2 [START_REF]A beginner's guide for MPEG-2[END_REF]. According to [START_REF]A beginner's guide for MPEG-2[END_REF], video stream data hierarchy consist of four layers those are GOP, Picture, Slice, macro block and block .Video sequence, begins with a sequence header, include one or more group of picture and ends with an ends of sequence code. Group of pictures (GOP), a header used to take a series of one of more pictures intended to allow random access into the sequence. Picture, it consists of three rectangular matrices representing luminance (Y) and two chrominance (Cb and Cr) values. Y matrix has an even number of rows and columns.

IPTV

The short form of Internet protocol television is IPTV. The video signals are converted into a stream of data which pass over the network in the same way as other traffic.

Background of IPTV Multicasting

Today's most of the distribution of television is running over a wire line distribution medium network based on analogue technologies. This network usually builds separate network islands. Each network provides their services using their own terrestrial and satellite receivers and, a shared coaxial cable. TV channel management was wide-meshed and often inadequate in such networks. Mix of multiple channels was distributed to end user using a STB (Set-Tob-Box) that is either hardwired or configured by means of the periodic distribution to end user. The problem with this STB box was the inability to create a mechanism of restricting access to premium subscriber channels such as movie channels. Few factor that have created the need to reassess the situation, those factor includes revolution of internet, a rapid increase in the performance of fiber infrastructure and a corresponding fall in price, and the new generation IP telephony [12].

MULTICASTING

It is a bandwidth-conserving technology that reduces traffic because it simultaneously delivers a single stream of information to thousands of corporate recipients and homes. For example, an application that takes advantage of multicast include video conferencing, corporate communications, distance learning, and distribution of software, stock quotes, and news. [13].

Multicast Addressing Scheme

The Internet Engineering Task Force (IETF) has developed the IPv4 address scheme with four categories (classes), those are A, B, and C and D. First three addresses are used for unicasting traffic and Class D addresses are reserved for multicast traffic, and are allocated dynamically. The address scheme looks like as Figure 4 Figure 4: Multicasting address scheme

Multicast Routing Protocol

To do multicasting, we need to run special protocol on router and switches, those protocols are IGMP (Internet group Management protocol) and PIM (Protocol Independent module) [14]. The original IGMP version host membership model was defined in RFC1112 [START_REF] Deering | [END_REF]. At present there are three version of IGM. Version-1 provide the basic query-response mechanism, According to RFC-2236 [START_REF] Fenner | Xerox PARC[END_REF], version-2 has the IGMP leave process, group specific queries and an explicit maximum query response time. Version provides source filtering. multicast packet and has no directly connected member or PIM neighbor present, a prune messages is sent back to the source so that subsequent multicast packets are not flooded to this router on this prune branch. In spare mode, a router assumes that other router don't want to forward multicast packets for a group, unless there is an explicit request for the traffic. The RP (rendezvous' point) is used in spare mode. It keeps track of multicast groups. Host that send multicast packets are registered with the RP by the first hop router of that host. [14].

IGMP

PIM

SETTING UP LAB OF IPTV

The network topology that we have used in test lab of IPTV has given bellows in the Figure 5. The equipments used with this lab were two Cisco Router (1800 series) and one Cisco Switch (2900 series), two hub, two client computer and one video stream server. We have only used hub in between router to router and router to switch to catch the multicasting traffic. A computer has been configured as a streaming server with VLC Player; two computers are connected to the switch as clients to receive the streaming data. Routers and switch are configured and enabled IGMP, PIM and CGMP protocols to support Multicasting. Wireshark network protocol analyzer has been used to capture and analyze multicasting traffic. We have considered four cases to capture the multicasting traffic. From the Packets captured between server and router (R2), it is found that UDP is used as transport protocol with the source port 1821 and destination port 1234. The other important thing is IGMP is used as multicast protocol and PIM is used as a multicast support protocol which looks like as Fig 6. In this scenario, UDP is used as the transport protocol. PIM is also used as a multicast support protocol. CDP (Cisco Discovery Protocol) is used between two routers that looks like as Fig 7. Again UDP is used as the transport protocol and PIM is used as a multicast support protocol. The other packets include IGMP packets of query & report messages as mentioned above. In addition to this, there was another packet named CGMP (Cisco Group Management Protocol) which indicates we have used CGMP technique instead of IGMP Snooping. Captured packets contents have given in Figure 9. Again, UDP is used as the transport protocol. But here there is no PIM packet is captured. Along with this, there is no IGMP packet with Membership query message because it is usually sent by multicast routers.

We have only found IGMP packets with Membership report and leave group messages because they are sent by the hosts and it has shown below in Figure 11.

FINDINGS AND ANALYSIS

Few parameters those includes Hello, Hold timer, Generation ID, Length, Checksum, DR Priority have found from the captured packet between router 2 and video steam server (Fig 6). Hello messages will send a router as soon as PIM enabled and configured to detect other PIM enabled router. In this case router 2 sends this Hello message but didn't receive any Hello message from other end because other end of this link is a streaming server and it's not PIM enabled. Hold time indicates the time period by which a receiver must response to the originator. The Generation ID is a random number which is generated whenever PIM is enabled to any router interface; the checksum is a calculated value of 16 bit one's complement of the one's complement sum of the entire PIM message used in data communication to check the packet has been transmitted successfully or not [START_REF] Adams | Request for Comments: 3973[END_REF]. DR indicates the designated router of a network that can be changed by assigning value within the range of 1 to 65535 and 0 is the default value.

From the captured packet of router 1 and router 2 interaction (Fig 7, Fig 8 and Fig 11), we have got few message of IGM those are header checksum, max response time, multicast address and type of message (leave group, query and response). Checksum is a 16 bit value which is calculated and insert with the message by sender. At the receiver end before processing this packet the checksum must be checked that ensure successful delivery of the messages. Maximum response time will only be noted during membership query message, for leave group and response message it will always set to zero by the sender and that's why we have got max response time for query message 10 sec where member ship response time and leave group time 0 sec (Fig 7 and Fig 8). We also have found multicast address 0.0.0.0 for general membership query message, 239.255.255.250 for membership report message and 224.10.0.1 for leave group message. This is because for query message the group address field is set to 0 , leave group message and report messages holds the multicast group address [START_REF] Fenner | Request for Comments: 2236, Internet Group Management Protocol[END_REF].

In Fig 9, we have seen another protocol named CGMP. It's only used in the IGMP enabled router interface. As soon as its enabled, router will send join messages to advertise themselves to switches with in this network. CGMP works with IGMP messages to keep updated cisco switch port, to forward IP multicast traffic to only those port that are belongs to IP multicast host. When a CGMP router receives an IGMP control messages, its creates a CGMP packet that holds join or request message, multicast group address and actual MAC address of the host and only Cisco router sends this message instead of any host. When a switch receives a CGPM messages changes the forwarding behaviour and send it to only that port associated with IP multicast client [START_REF]IP CGMP, IP multicasting Command[END_REF] [START_REF]Cisco Group Management Protocol[END_REF].

CONCLUSION

Initially, a specific study on compression technique of audio video file format has been done that allows IPTV to consume less bandwidth. We also studied on various protocol of IPTV those includes IGMP, PIM, and CGMP that helps us to run the IPTV lab. Few factor have been remarks those includes revolution of internet, a rapid increase in the performance of fiber infrastructure and a corresponding fall in price, and the new generation IP telephony from the back ground study of IPTV and multicasting that aware us to think about the present situation of IPTV services. Mainly, what we have done with this paper work was to find out the protocols that are used with IPTV and Multicasting. It has been done capturing multicasting traffic considering four possible cases and discussed. Finally, it can be said this paper works gives us a clear understanding how various protocols of IPTV works and interact with each other.

Figure 2 :

 2 Figure 2: Video stream file format

Figure 3 :

 3 Figure 3: Group of pictures Slice consists of one or more contiguous macro blocks. Within a slice the macro block is count from left-to-right and top-tobottom. Slices are important in the handling of error. Block represents the smallest coding unit in macro block or slice. It can be of three types such as luminance (Y), red chrominance (Cr), blue chrominance (Cb).

  .0.0 -247.255.255.255 224.0.0.0 -239.255.255.255 192.0.0.0 -223.255.255.255 0.0.0.0 -127.255.255.255 128.0.0.0 -191.255.25521), length: 4, value: 0x1000000 Internet Group Management Protocol IGMP version: 2 Type: Membership Report (0x16) Max Response Time: 0.0 sec (0x00) Header Checksum: 0xfa04 [correct] Multicast Address: 239.255.255.250 (239.255.255.250) Internet Group Management Protocol IGMP version: 2 Type: Membership Query (0x11) Max Response Time: 10.0 sec (0x64) Header Checksum: 0xee9b [correct] Multicast Address: 0.0.0.0 (0.0.0.0) Internet Group Management Protocol IGMP version: 2 Type: Leave Group (0x17) Max Response Time: 0.0 sec (0x00) Header Checksum: 0x08f4 [correct] Multicast Address: 224.10.0.1 (224.10.0.1)

Figure 5 :

 5 Figure 5: IPTV lab 6. RESULT OF IPTV LAB Case 1: (Server & Router R2)

Fig 6: PIM messages Case 2 :

 2 Fig 6: PIM messages Case 2: Router R1 & Router R2 (by using Hub 2)

Figure 7 :

 7 Figure 7: Packets between R1 & R2 We also find two kinds of packet from the captured traffic those are membership query and membership report messages of IGMP as shown in the Fig 8.

Figure 8 :

 8 Figure 8: Member ship query and report message

Figure 9 :

 9 Figure 9: CGMP messages We also found information which is related to STP (Spanning Tree Protocol) as shown in Fig 10.

Figure 10: STP protocol Case 4 :

 4 Figure 10: STP protocol Case 4: (Client C1, C2 and Switch)

Figure 11 :

 11 Figure 11: Message transaction between host computer and switch

  Fig 9 holds the CGMP messages are Join, group destination address and unicast source address. From Fig 7 and Fig 10, we have found two another protocols named CDP (cisco discovery protocol) and STP (Spanning Tree Protocol).CDP is used to get the information of neighbouring devices like platform, IP address and is a Cisco proprietary protocol. STP is used to make a loop free path for multicasting traffic.

  primarily discussed on the high throughput of IEEE 802.11N wireless LAN and its performance. This paper next discuss about the technical challenges of IPTV which

	includes QoS, Traffic management, Multicasting admission
	control, admission control for Ethernet, WLANs, Security and
	Privacy etc. But it emphasise on QoS, because services are
	provided by the public internet so video quality depends on the
	network traffic condition.
	MPEG 2
	Transport
	Stream
		Header		Payload
	Sync.	Trans	Paylo	Trans	PID Trans	Adapta	Contin	Adapta
	Byte	port	ad	port	port	tion	uity	tion
		error	unit	priorit	scram	field	Counte	field
		indica	start	y	bling	control	r
		tor	indica		contro
			tor		l


Médésu Sogbohossou
email: medesu.sogbohossou@epac.uac.bj

Antoine Vianou
email: antoine.vianou@epac.uac.bj

ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets

Keywords: Time Petri Net, timed grafcet, state class, partial order execution, synchronous modelling MOTS-CLÉS : Réseau de Petri temporel, grafcet temporisé, classe d'état, exécution ordre partiel, modélisation synchrone

    ϵ-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets Médésu Sogbohossou, Antoine Vianou

Introduction

Formal specification of a critical system at the early stage of conception is often needed to achieve their reliability in working, by means of languages allowing simulation or formal verification on the established model of this system [START_REF] Clarke | Model checking[END_REF]. Graphical statetransition modeling formalisms in engineering are appreciated because of their intuitiveness. They are based on the automata theory, ensuring an unambiguous description of the behaviours of a system. Petri nets (PN) are one of these formalisms, used to model in a compact and explicit way the concurrency and the synchronization between the dynamic components of the so-called discrete-event systems [START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF]. In PNs, firing of transitions (with possibly multiple concurrent firings in the same instant) changes the state and express the dynamics of the modeled system. Time Petri nets (TPN) [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF] are one of its extensions, suitable when quantitative time analyses are required for the real-time specifications.

Otherwise, the engineering pratices often promote less formal graphical languages, because of their increased semantic richness (for instance, litteral formulae and hierarchical modeling do not exist in the ordinary PNs) favoring more compact and fluent modeling to the detriment of unambiguous interpretations. These are the cases of formalisms derived from PNs, such as GRAFCET 1 (IEC 60848 standard) [9] and SFC (Sequential Function Chart, IEC 61131-3 standard) [START_REF]Programmable controllers -part 3: Programming languages[END_REF], used mainly in the world of the manufacturing control. Whereas simultaneous fireable transitions are always done by their total interleaving with PNs, the semantics of these two IEC standards considers only synchronous firings; a consequence is that the notion of transitions in conflict does not exist in GRAFCET and SFC formalisms. GRAFCET is intended for specification purposes (event-driven modeling), contrary to SFC for implementation uses (clock-driven modeling), and is considered in the sequel.

To allow a formal verification of GRAFCET (or SFC) models integrating quantitative time informations, many authors proposed to translate them into formal and well-reputed languages such as timed automata [START_REF] Her | Proving sequential function chart programs using timed automata[END_REF] or TPN [START_REF] Wightkin | Formal modeling of Sequential function Charts with Time Petri nets[END_REF][START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF]. The work in [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF] is focused on defining some transformation rules which are used to translate the entities composing a timed and not necessarily sound grafcet chart (steps, transitions, literal variables, actions) into connected blocks to obtain the resulting TPN. The method exploits the similarity between TPN and GRAFCET to avoid exponential size of the translation, and implicitly relies on a clear choice about the GRAFCET semantics.

To deal with synchronous firings inherent to GRAFCET formalism, the authors [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF] introduced transitions with infinitesimal ε delays, however without redefining formally the resulting extended TPN. The first goal of this paper is to palliate this lack, by specifying a formal semantics for the so-called ε-TPN; the slight differences with the definition in [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF] are also presented. Basing on this new definition, the second goal is to provide how to build the state space abstraction of an ε-TPN (which is just sketched in [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF]) with the ε delays. Particularly, it is shown how to take advantage from this kind of TPN to cope with the state-space explosion problem, by avoiding useless interleaving of concurrent firings and by abstracting some state classes during the state-space construction.

In the next section are mainly recalled definitions about TPNs and GRAFCET charts. Section 3 summarizes and illustrates how the entities of a grafcet are converted into the connected subnets forming the corresponding TPN; also, a rule of translation is enhanced (concerning stored action modelling), and various definitions used in the subsequent sec-tions are introduced. Formal definitions about the syntax and semantics of ε-TPN are given in Section 4, completed with a characterisation of the ε-TPN model in the form of a list of features used in the next section throughout the proposal of state-space abstractions. Then, Section 5 extends the definition of a TPN state class and justifies the partial-order approach to compute a ε-TPN state-space abstraction, before presenting the algorithm of the all situations state-space and the stable situations state-space. Finally, this paper contribution is summarized and some perspectives are sketched in Section 6.

Definitions: time Petri nets and GRAFCET charts

In this section is recalled the syntax and semantics definitions about (classic) time Petri nets (TPN). Then, GRAFCET charts are presented and the related semantics choices are remembered, concerning especially the synchronous assumptions on which the subsequent sections are relied on. The classic definition about Petri nets with no time information ranges from items 1 to 5.

Time Petri nets (TPN) and state-space abstractions

Graphically, no regular arc between two nodes (one place and one transition) means that the weight is 0, and a regular arc without a weight label means that the weight is 1. Similarly, no read arc directed from p ∈ P to t ∈ T means W R (p, t) = 0, and no inhibitor arc directed from p ∈ P to t ∈ T means W I (p, t) = ∞.

A transition t is enabled by a marking M : P -→ N when:

∀p ∈ P, (M (p) ≥ W (p, t) ∧ M (p) ≥ W R (p, t)) ∧ p ∈ P, M (p) ≥ W I (p, t).
The set of transitions enabled by M is denoted En(M ).

Items 6 and 7 add quantitative time informations: each transition t bears a static interval [ED(t), LD(t)], with ED(t) ≤ LD(t), specifying the delay after which t is fireable since the instant it becomes enabled or re-enabled.

Semantics

The chosen operational semantics of TPN is the standard semantics (as in the references [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF][START_REF] Bucci | Compositional validation of time-critical systems using communicating time Petri nets[END_REF]).

The well-known two characterizations of TPN state [START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF] are interval state and clock state: the second one is used here since it is more general than the first one for building all kinds of abstractions.

TPN semantics is formally defined by means of a timed transition system. Let be a vector v ∈ (R + ) T : v(t i ) denotes the local clock of transition t i ∈ T , that is the quantity of elapsed time since transition t i becomes fireable 2 . q = (M, v) is a state of the timed transition system. Definition 2. The timed transition system (Q, {q 0 }, T, →) of a marked TPN is defined by:

1) the initial state is q 0 = (M 0 , v 0 ) ∈ Q, with v 0 def = (0) T ;
2) the set of the states reachable from q 0 are Q ⊆ (N) P × (R + ) T ;

3) the alphabet of the discrete transitions is T ; 4) the relation of the timed and instantaneous transitions is → ⊆ Q×(T ∪R + * )×Q, with:

a) a timed transition by a delay d ∈ R + * such as (M, v) d → (M, v ) iff: v (t i ) def = v(t i ) + d, ∀t i ∈ T t i ∈ En(M ) ⇒ v (t i ) ≤ LD(t i )
b) and an instantaneous firing by a transition

t i ∈ En(M ) such as (M, v) ti → (M , v ) iff:            M def = M \ • t i ∪ t • i ED(t i ) ≤ v(t i ) ≤ LD(t i ) ∀t j ∈ T, v (t j ) def =    0 if t j ∈ En(M ) ∧ (t j / ∈ En(M \ • t j ) ∨ t j = t i ) v(t j ) else In Item 4.b of the definition 2, the notation • t i (resp. t • i )
represents the multiset3 of the input (resp. output) places for transition t i , by the relation W of the regular arcs.

In a state q, any enabled transition is fireable (item 4.b) if its clock value is within the static interval. Thus, an enabled transition t i must be fired with no more delay if the clock reaches LD(t i ) (item 4.a); otherwise each enabled transition t i may be delayed by d, as long as any local clock is not increased beyong LD(t i ).

After a firing of some transition t i , the clock value of each transition in En(M ) is updated (item 4.b): it is reset for a newly enabled transition t j / ∈ En(M \ • t j ) ∨ t j = t i , and it is not changed for a persistent enabled transition t j ∈ En(M \ • t j ).

Notice that the clock value of disabled transitions in a state does not mind.

State space abstractions

When time progression is continuous (or dense), the representation of the state-space by a timed transition system is generally infinite. For a bounded TPN (i.e. a marking of a place is always finite), different finite abstractions were proposed [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF][START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF]

Grafcet

A GRAFCET chart [9] is a graphical representation to model the behaviour of an automation control part. A GRAFCET chart is made up of two components:

-the structure comprises the steps, the transitions and the directed links. The structure describes the possible evolutions between the situations, a situation being the set of active steps at a given time;

-the interpretation is allowed by the literal variables (inputs, outputs, delays, internal variables, ...) related to the structural elements (steps and transitions). It is done through the transition conditions (containing: inputs, rising/falling edges of boolean inputs, delays, ...) and the actions (continuous or stored actions attached to steps) updating output or internal variables. The simple example of grafcet Fig. 1 has two steps (square blocks numbered 1 and 2,

Step 1 with double square being an initial step), two transitions (1) and ( 2) respectively with conditions I 1 (an input variable) and 1s/X 2 (a timed variable on Step 2), and a continuous action block which sets the output O 1 when Step 2 is active. The four directed links connect a step to a transition, or a transition to a step. Some syntax restrictions are applied to the grafcets for the translation into TPN previously proposed: no hierarchical concepts of forcing and enclosure, no source transition, predicates concern only positive counters (as internal variables), timed variables of the simple form T 1 /X n /T 2 or T 1 /X n .

A grafcet transition is enabled when each of its input steps is active, and is fireable4 when it is enabled with a true transition condition: the firing provokes simultaneously the activation of all the output steps, and the deactivation of all the input steps (which are not reactivated by the same firing stage). Several simultaneously fireable transitions are simultaneously fired, in the so-called same firing stage: this synchronous property is to oppose to the asynchronous firings with Petri nets.

A situation is stable when no transition is fireable. Only external events may cause an evolution, meaning iterated firing stages, from a stable situation. An external 5 event is either an input change, or a timed variable change (after some corresponding delay) called timed event (or delay event).

The algorithm describing the succession of the execution phases of a grafcet is recalled in the work [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF]. Likewise, some ambiguous aspects of the standard [9] requiring clarifications and how to carry out stored and continuous actions were presented in this reference.

About synchronous assumption

Some assumptions about synchronous semantics found the translation principle and are reminded here to prelude the summary about the translation rules.

Every external event may start an evolution, a succession of transition firing stages. An evolution is achieved instantaneously to reach a stable situation, before any next external event which may occur. Thus, the control part of the system which fulfils an evolution, is supposed to be infinitely faster than the rhythm of the environment producing external events. Consequently, the elementary time elapse of the control part is inconsiderable compared to the one of the external clock governing the environment rhythm.

Another consequence of this assumption is that two external events may not occur in the same instant: the reaction of the control part is always completed between two consecutive occurrences of external events. In the specific case when two timed events are synchronous, it is supposed that the control handles them in a total order. It should be noticed that this assumption does not call into question the possibility of parallel execution of several grafcet branches derived from a selection divergence, if the transition conditions allow it.

Translation of grafcet into TPN

The principle

With Petri nets, firings must always be done in a total order: so, the transitions of a firing stage are totally interleaved in the same instant. To allow the simulation of consecutive synchronous firing stages without interference between them, an infinitesimal delay (ε) is introduced, without calling into question the infinitely faster character of the control part [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF].

Concretely, two consecutive synchronous firing stages of grafcet transitions are separated by a delay 2ε 0 , and the updating of variables (step variables and variables updated by stored actions) occurs ε 0 delay after each instant of firing stage of grafcet transitions, and so occurs ε 0 delay before the next firing stage of grafcet transitions in the same evolution phase.

When no more firing stage is possible (meaning the end of an evolution phase), the stable situation is reached a delay 3ε 0 after the last firing stage (that is a delay 2ε 0 after the last updating): only one occurrence of an external event allows returning to a new evolution phase, possibly empty of firing stage.

To help an overall understanding of the translation rules reminded in the sequel, a Petri net at Fig. 2 depicts how a grafcet dynamic is interpreted. For the transitions with structural conflict in Fig. 2, the choice condition is indicated into brackets. An italic text shows the action of a transition to perform within some delay. Notice that an input rising or falling edge state is just available a delay 2ε 0 , thereby only for the conditions of the first firing stage of the next evolution phase.

Let make clear the general concept of stage after the translation into TPN. A TPN firing stage is a set of firings performed in the same instant which simulates a grafcet firing stage. More generally, a stage may also correspond to:

-the set of TPN firings done as variables updating (related to step states or stored actions) during an evolution phase: it is called update stage, -or the synchronous firings done in the instant of coming into a stable situation, to set outputs for continuous actions: it is called into-stability stage, -or in the instant of leaving a stable situation, to set an external event occurrence and to reset outputs for continuous actions: it is called out-stability stage.

Thus, a grafcet execution is a cyclic succession of an occurrence of an external event followed by an evolution phase. This cyclic execution is broken down into the four kinds of stages. At the system start-up, a early evolution phase is computed: a first update stage initializes diverse variables, which may trigger a firing stage, then another update stage, and so on, until reaching a stable situation. Entering a stable situation allows setting the outputs for continuous actions via the into-stability stage. At the occurrence of an external event, the out-stability stage updates related variables (changing an input or a timed variable) before beginning a new evolution phase: a sub-cycle of a firing stage followed by the subsequent update stage, and so on.

The head firing of a stage is the first firing to begin this stage. These new denominations are used in the sequel to manage the state-space abstractions.

Translation rules

The application of translation rules follows a suitable order to complete the resulting ε-TPN of a grafcet: the grafcet elements are converted into connected TPN modules composing the ε-TPN. An additional and first module called phase sequencer (Fig. 3) allows alternation between an occurrence of an external event (the place Stable is marked to denote a stable situation before producing an external event) and the subsequent reaction phase (marking of the place Evolution denotes the transient evolution phase following an external event occurrence), without any interference: especially, no input as external event may not be modified during a transient evolution. The place Occurrence is marked every time a grafcet transition model is fired or when a timed event occurs, allowing to stay in (or to restart) an evolution phase. After adding this first module, creation of the TPN modules may follow this suitable order: steps, inputs, timed variables, outputs, counter variables, continuous actions, stored actions, grafcet transitions.

The static time interval beared by every transition t of a module gets the form of a simple delay δ(t): δ(t) = ED(t) = LD(t); except for the transiion named Change_input in Fig. 3 Here, the translation rules are not modified, except slighty for the extra module of the phase sequencer (Fig. 3): ED(Change_input) which previously has ε 0 value is now replaced by 0. The former value was a trick to make firings related to continuous actions to occur ε 0 delay before a next input change, which is useless now since the transition Change_input has lesser priority (see Section 4). Moreover, in the previous work [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF], it was possible in a stable situation for an input event to occur just before a timed event in the same instant to start a subsequent evolution phase, whereas the converse (i.e. a timed event followed in the same instant by an input event) was not possible. This contradiction is emended here, since the respect of the synchronous assumptions (cf. subsection 2.3) prevents multiple occurrences of external events between two evolution phases.

An example of translation

As an illustration, the translation into TPN of the example of grafcet at Fig. 1 is provided Fig. 5(b). Two modules are simplified to get the resulting TPN: the step modules because the grafcet model is safe, and the input module for I 1 since the rising and falling edges are useless. Definition 3. T input and T G denote respectively the transitions modelling input changes and grafcet transitions.

For the given example, T input = {I_1_to_true, I_1_to_f alse} and T G = {tr_1, tr_2}. Incidentally, T T = {1s_X_2_to_true}.

Enhancement on stored action modeling

Here, the goal is to modify the modelling of the ordering of a stored action on a boolean variable (internal or output). Indeed, the actual model given at Fig. 6(c

Formal definitions on ε-TPN

In this section is formally defined the TPN extension, called ε-TPN, used as the target model of the grafcet to translate. Moreover, the specificity of the grafcet semantics and how the ε-TPN modules translate the entities of a grafcet justify some stated features: the subsequent algorithms about state-space abstraction are based on these features.

Syntax

Let ε 0 be an infinitesimal constant delay comparable to 0

+ . For n ∈ N, ε n def = ε 0 × (n + 1), and E def = {ε n | n ∈ N}. For ε n ∈ E and any d ∈ R + * , it is assumed that: 0 < ε n < d and d ± ε n ≈ d. And E 0 def = E ∪ {0} by extension.
Definition 4. An ε-TPN is a TPN with specific static firing intervals for transitions:

1) the earliest firing delays of transitions, ED : T -→ E ∪ Q + ;
2) the latest firing delays of transitions, LD :

T -→ E ∪ Q + ∪ {∞};
3) the set of transitions is made of three subsets,

T = T E0 ∪ T T ∪ T ∞ such as: a) ED(t) = LD(t) ∈ E 0 when t ∈ T E0 ; b) ED(t) = LD(t) ∈ Q + * when t ∈ T T ; c) ED(t) = 0 and LD(t) = ∞ when t ∈ T ∞ .
Thus, definition 4 extends the classic definition 1 with use of the infinitesimal delays (here, E def = {ε 0 , ε 1 , ε 2 }) in the transition bounds, but restricts the form of the static firing intervals for transitions which mostly allow only fixed delays.

In the sequel, T ∞ = {Change_input} is a single transition denoted by t ∞ : the variable delay experienced before such a firing represents the time spent in a stable state before the occurrence of the next external event.

Transitions in T E model synchronous firings done in an evolution phase. External events to the control part depend on the transitions {t ∞ } (an input event occurs in the same instant of this firing) and T T (delay events for the timed variables): two transitions of these kinds may never occur simultaneously in the same instant, as imposed by the operational semantics. Thus, only one firing in the set {t ∞ }∪T T should trigger a reaction, that is a sequence of firings in T E0 . The transitions with zero delay value (i.e. with static interval [0, 0]) may also be used to produce an external event, in order to update some variables instantaneously.

Subsequently, the fixed delay of a transition t ∈ T E0 ∪ T T is denoted δ(t).

Operational semantics

If transitions are enabled in both the sets T E0 and T ∞ ∪ T T , then transitions in T E0 always have priority to be fired, contrary to the previous work [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF] which considers no such priority. When a transition in T ∞ ∪T T is really fireable, dense time elapse is allowed in a stable state, by a non-infinitesimal delay. After such an external event, a reaction phase is entered where only firings in T E0 are possible, before to reach a next stable state.

Compared to previous definition 2, a vector v gets its values in E ∪R + : v ∈ (E ∪R + ) T .

Definition 5. (Q, {q 0 }, T, →) for a marked ε-TPN is defined by:

1) the initial state is q 0 = (M 0 , v 0 ) ∈ Q, with v 0 def = (0) T ;
2) the set of states reachable from q 0 are Q ⊆ (N) P × (E ∪ R + ) T ;

3) the alphabet of the discrete transitions is T ;

4) the relation of the timed and instantaneous transitions is

→ ⊆ Q×(T ∪E ∪R + * )× Q, with: a) a timed transition by a delay d ∈ E ∪ R + * such as (M, v) d → (M, v ): i) if ∃d ∈ E (infinitesimal time elapse), then:            ∃t ∈ En(M ) ∩ T E ∀t j ∈ T,        t j ∈ En(M ) ⇒ v(t j ) + d ≤ LD(t j ) if t j ∈ T E then v (t j ) def = v(t j ) + d, else v (t j ) def = v(t j ) ii) if ∃d ∈ R + * (non-infinitesimal time elapse), then:    t ∈ En(M ) ∩ T E0 v def = v + d ∀t j ∈ En(M ) ⇒ v (t j ) ≤ LD(t j )
b) and an instantaneous firing by a transition

t i ∈ En(M ) such as (M, v) ti → (M , v ) iff:                    t i ∈ T E0 ∨ ( t j ∈ En(M ) ∩ T E0 ) ∧(t i ∈ T T ∪ T ∞ ) M def = M \ • t i ∪ t • i ED(t i ) ≤ v(t i ) ≤ LD(t i ) ∀t j ∈ T, v (t j ) def =    0 if t j ∈ En(M ) ∧ (t j / ∈ En(M \ • t j ) ∨ t j = t i ) v(t j ) else
Thus, when the set En(M ) ∩ T E0 is not empty in a given state q, a transition t in this set is fired instantaneously if the clock value v(t) = δ(t), or the least infinitesimal elapse is observed to make one of them fireable. Meanwhile, clock values do not change for enabled transitions in T T ∪ T ∞ . Otherwise, only transitions in T T ∪ T ∞ are enabled, and the common semantics for TPN is applied (definition 2). After a firing, the clocks value of the transitions En(M ) are updated in accordance with the standard semantics.

Adequate features on the ε-TPN

Here is highlighted some features resulting from the translated grafcet into ε-TPN, features on which the subsequent developments rely on, the state-space abstractions especially.

The equivalence between a GRAFCET chart and the TPN resulting from the translation was shown [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF]. In particular, an induced first feature is the boundness of the TPN, which determines the construction of a finite state-space. Boundness implies that each modelled variable ranges in a finite domain: only an unbounded counter in a grafcet may call into question this feature.

Deadlock-freeness

This feature results from the phase sequencer (Fig. 3): evolution phase and stable phase alternate indefinitely, even if an evolution phase between two external events may be empty of grafcet transition firing (and so empty of internal variables updating): the transition Evolution_End is just fired.

A stage is finite

This feature results from the structure of the generated finite and bounded TPN. Indeed, only a structural loop of transitions with zero static delay may cause an infinite stage. That is to be check locally on modules of translation, because it is not difficult to apprehend graphically that firings allowed by interconnections between two modules always imply a non zero static delay transition. Modules with loop by zero static delay transitions are:

-the phase sequencer, with the transition F iring (Fig. 3): only firings from a grafcet transition or a transition in T T (in a timed variable module), which are in finite number, allow this firing; -an input module (Fig. 4(b)): one token put in the place One_Input_Changing by the transition t ∞ causes only one transition firing in all input modules (T input ); -a continuous action module (Fig. 4(d)): a firing depends on the related step state (X i or X i ), so only one is possible;

-a stored action module on a boolean variable (the new proposal at Fig. 6(d)): the subsection 3.4 justifies the finiteness of a such execution.

A non-finite evolution phase is always detectable

A total instability is when an evolution phase lasts indefinitely. It compromises the synchronous assumption since this evolution will not end before some next external event. By saving and comparing states reached by each finite firing or update stage constituting a current evolution, a loop is detectable.

A sequence of firings during an evolution phase may not be interfered with the occurrence of an external event

Initially, a first evolution phase is executed, and transitions T T ∪T input are not fireable. Then, every time a stable state is reached, an external event t e ∈ T T ∪ {t ∞ } is produced to begin a new evolution phase. No interference with the first firing stage (after a delay ε 0 ) of the evolution phase is possible because the remaining firings due to the produced external event are done in the same instant of the related out-stability stage: the transition T ime_out if t e ∈ T T , or one of the transition T input if t e = t ∞ . In short, priority avoids possible interference.

In a stable state, besides transitions T T ∪ {t ∞ }, only transitions with static interval [0, 0] may be enabled

Before producing an external event in a stable state, one token in the place Stable (caused by the transition Evolution_end, when leaving the evolution phase) may allow firings of zero static delay transitions of continuous action modules 6 . Indeed, no more grafcet or update transition enabled in an evolution phase remains fireable before firing Evolution_end.

Besides, a firing in T T makes the zero static delay transition T ime_out to be enabled, transition of which firing causes leaving the stable state; whereas the firing of t ∞ causes immediate leaving of the stable state.

6. Notice that in an evolution phase, a firing in a continuous action module is impossible because it depends on the marking of the place Stable.

When the transition t ∞ is fireable, its clock value does not change by a concurrent firing in T T

t ∞ is fireable after zero-delay firings for stored actions (during an into-stability stage); then, it remains a priori persistent when a transition in T T is fired at first (to head an outstability stage). But a firing in T T causes the enabling of T ime_out having priority on t ∞ and fired without delay. Since this firing is in conflict with t ∞ (by sharing the place Stable), t ∞ is disabled. Not doing a firing in T T means t ∞ will necessarily be fired: an observed delay is only due to waiting this firing.

State space abstractions

Specificity of ε-TPN abstractions

Each of the four kinds of stages, presented in subsection 3.1, is made of a finite number of firings (sequential and/or concurrent) done in the same instant (according to feature 4.3.2 in the previous subsection), and the possible interleavings of the synchronous firings should lead up to the same state. So, to manage the state explosion problem, only one interleaving should be dealt with, while insuring (if necessary) that the stage always ends up in a unique and coherent state, by an unexpensive way of checking it: subsection 5.5 suggests a way to check a coherent execution of a stage, so-called the consistency check.

The first level of abstraction, called partial-order state-space, consists in computing all the reachable state classes by the computed stages, from the initial class C 0 . In addition to this first level of abstraction, two subsequent levels more relevant for a grafcet point of view are considered, by abstracting the informations too specific to the target ε-TPN model:

-the all situations state-space, containing all the stable and unstable situations of the grafcet: every firing stage followed by an update stage are merged into one stage, -and the stable situations state-space, only containing the stable situations of the grafcet: all consecutive stages between two stable states are merged into one. In practice, informations in the classes and in the merged stages of these two kinds of abstraction should be filtered and simplified (as far as renaming places and transitions modelling the grafcet) to only keep relevant informations about the original grafcet. However, these conveniences which purpose is to improve the transparence of the state-space towards the TPN formalism, are taken into account only partially in the sequel: namely for the transitions of these two high level state-spaces.

The boundness of the ε-TPN may be called into question only by an unbounded counter variable modelling. So, the test of the state-space finiteness in this eventuality should be easily integrated in the algorithms, in the classical manner with TPNs [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF]: here, a state-space abstraction is finite iff the ε-TPN is bounded.

Composite classes

Before presenting the three levels of abstractions, some accommodations are necessary on the usual ways to compute the state class graph (SCG), because of the specificity of an ε-TPN.

So, an extended definition of class is justified by integration of discrete infinitesimal time delay ε 0 for T E transitions. In fact, for a domain interval such as [0, ε 0 ], time could only take two values, 0 or ε 0 , and intermediate values are nonsensical since time is no more dense. Here, we choose to keep the classic definition of a class domain by considering 0 instead of ε n for the enabled T E transitions. But, another time informations about discrete clock values of the enabled transitions in T E0 are needed to know which transitions are really fireable among ones having priority.

A composite state class C is a tuple of a marking M , a clock domain D (a conjunction of dense time binary constraints between the clock values of all enabled transitions) and a set of discrete clock values V for the enabled transitions in T E0 . The clock variable of a transition t i appearing in a global domain D (resp. in the set V ) is denoted by τ

i (resp. ν i ). The initial class is C 0 = (M 0 , D 0 , V 0 ), such as D 0 = ti∈En(M0) τ i = 0 and V 0 = {ν i = 0 | t i ∈ En(M 0 ) ∩ T E0 }.
For a current class C, if En(M ) ∩ T E0 is empty (the set V is empty), the fireability check of each t i ∈ En(M ) and the next class C reached by fireable t i are computed as usual [START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF]. Else (i.e. En(M ) ∩ T E0 = ∅), a transition t f having priority must be fired, in the set {t f | ∀(t f , t i ) ∈ (En(M ) ∩ T E0 ) 2 , δ(t f ) -ν f ≤ δ(t i ) -ν i }; the next class domain D is still computed as usual (by considering 0 bounds for T E transitions) and the set V as follows:

∀t i ∈ En(M ) ∩ T E0 , ν i = 0 if newly enabled, ν i = ν i + (δ(t f ) -ν f ) else. Indeed, a discrete delay (δ(t f ) -ν f ) is observed between the classes C and C .
An ε-TPN gets an unbounded static interval, the only one of the transition t ∞ . Thus, the risk is an infinite SCG exits, justifying the relaxation operation when using clock state based abstraction [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF], which is necessary for ASCG. Fortunately, transition t ∞ may not induce an infinite number of domains: feature 4.3.8 justifies no need of relaxation, thanks to mutual exclusion firing between t ∞ and T T transitions.

As an illustration, the SCG (without partial order execution of the stages) of the example Fig. 5(b) is made of 41 classes and 50 transitions.

Abstraction of level 0: Partial-order state-space

To get the level 0 SCG (L0-SCG), a transition between two classes C and C is a multiset T s of the firings in a stage (C Ts → C ): the intermediate states during a stage are not saved.

The initial class C 0 corresponds to the initial state of the grafcet (the initial situation begins in an evolution phase, with the setting of the initial value of the diverse variables). So, the first stage to fire is a firing stage if the initial situation is not stable; otherwise, the transition Evolution_end is fired to trigger the first into-stability stage. The head firing of a stage is always the transition Evolution_end (denoted t ε2 in the sequel) for an into-stability stage, and is a transition t ∞ or a delay transition in T T (modeling external events) for an out-stability stage.

For a partial-order state-space of an unambiguous grafcet, it should be noticed that only classes from which an external event is fireable may get multiple outgoing stage transitions in L0-SCG. Every firing interleaving of a stage should lead up to the same class, except when the head firing is a transition t ∞ for an out-stability stage: the real input event is produced by one change among the possibly multiple inputs in T input (feature 4.3.7). Therefore, a class from which a transition t ∞ is enabled will get as many outgoing transitions as the number of existing inputs. Algorithm 1: Construction of the L0-SCG Algorithm 1 describes the construction of the L0-SCG. It is globally structured like the classical algorithm computing a PN state graph, but with lines 7-13 specialized to the computing of the stages (only classes reached by the stages are saved) as macrotransitions instead of simple transition firings. Stages are computed by calls to procedures FromEvolution at line 8 and FromStable at line 12. FromEvolution (resp. FromStable) implicitely deals with firing stages, update stages and into-stability stages (resp. outstability stages). None of these procedures needs to be provided with test of execution finiteness (or loop detection) thanks to the feature 4.3.2. Moreover, because of the deadlock-freeness (feature 4.3.1), a head firing t is always found to begin a stage from a new class C to process from the stack: either a transition having priority at line 7, or an external event at line 11.

1 Find any fireable transition t from C; 2 Compute the successor class C ; Ts := {{t }}; 3 while ∃t ∈ En(M ) ∩ TE 0 , with t and t fireable at the same time do Procedure FromStable Lines 7-10 of Algorithm 1 deal with any stage, except the out-stability stage which is managed at line 12 with the call to the procedure FromStable: the if block of the procedure (lines 3-8) deals with firing t ∞ followed by a firing in the set T input in the same instant (feature 4.3.7); the else block (lines 9-15) deals with a timed event firing in T T followed by firings of transition with zero static delay (feature 4.3.6), in fact a singleton set made of the transition T ime_out (feature 4.3.5) to return to an evolution phase.

The usage of a stack by Algorithm 1 to save classes is pertinently justified when interleavings are necessary for possible multiple external events in a stable state (lines 6 and 13 of the macro FromStable). The AddSCG procedure call at lines 7 and 14 of the macro FromStable allows to save relevant classes and the related transitions as stages.

The consistency check of a stage evoked in subsection 5.1 may be useful, especially for an update stage: the procedure is presented in the subsection 5.5.

The procedures FromEvolution, FromStable, and AddSCG are reused for the following levels of abstraction in the next subsection. Notice that it is supposed SCG data in Algorithm 1 are shared, as the current class informations (C, C , T s , ...), with the macros FromStable and FromEvolution.

Besides, it may be observed that the stack used for Algorithm 1 contains as well stable states as unstable (i.e. evolution) states. And the possibility of a total instability of the grafcet model evoked in subsection 4.3, does not mind yet here; this is taken into account in the sequel.

As illustration, the L0-SCG of the example Fig. 5(b) is made of 18 classes and 21 transitions, detailed in Table 1.

Abstractions of levels 1 and 2: grafcet situations state-space

Algorithm 2 describes the constructions of the L1-SCG (level 1 SCG, with the sets C L1 and T L1 ) and L2-SCG (level 2 SCG, with the sets C L2 and T L2 ), which are worth doing as grafcet state-space. These constructions are more largely based on the knowledge of the possible succession order of the different stages induced by a grafcet semantics:

-a firing stage is always followed by an update stage: these consecutive stages are merged in practice for a grafcet, and the intermediate state between them does not need to be saved (lines 6-8 and 22-24); -any total instability should be detected (at lines 10 and 26) to abort the SCG computing.

For L1-SCG, the procedure AddSCG1 replaces AddSCG (at lines 11, 27 and 31 in Algorithm 2, and at lines 7 and 14 in procedure FromStable2 replacing FromStable) by rather acting on the sets C L1 and T L1 (instead of the sets C and T with Algorithm 1). The first stable state class (i.e. a state class such as the place Stable is marked, meaning a state of a stable grafcet situation) is saved on STACK1 at line 14: STACK1 contains exclusively the stable state classes to be processed, by computing their successor classes. For each class pulled from STACK1 (line 16), the next classes reached by each possible external event with the related out-stability stage are saved on STACK2 by the macro FromStable2 replacing FromStable, with the same code lines but with some name substitutions. Indeed, lines 6 and 13 for the macro FromStable2 acts now on STACK2 (instead of Stack with Algorithm 1) which contains only classes reached by an out-stability stage, that is the beginning states of an evolution phase. Besides, the set Each item of the STACK2 is processed (lines 18-34 of Algorithm 2), allowing thereby to compute the successive classes until reaching the next stable state class, saved in STACK1 if new (line 32). To detect a possible total instability (always detectable according to the feature 4.3.3) which might prevent reaching some next stable state class, the following classes encountered (and only derived from the current stable state class C S to process) are stored in the set Loc_Classes: so, if a loop back is done before reaching an expected stable state, that would mean that the instability is never left, and therefore the algorithm is stopped (line 26). The same precaution is taken to reach the first stable state class from C 0 (line 10), by using directly the set C L1 which is not derived from multiple stable state classes meanwhile. Notice that constituting Loc_Classes is not subject to explosion since no interleaving is considered before reaching the next stable state class.

T ext = T s ∩ (T input ∪ {t ∞ }) (resp. T ext = T s ∩ T T ) replaces
L2-SCG is constituted only at the line 33 of Algorithm 2 with the macro AddSCG2: only the external event (T ext ) minds between two stable state classes. It should be mentioned that a transition T s between two classes, as well for L1-SCG as for L2-SCG, is now a simple set to only reflect the grafcet model elements: either T ext , or {t ε2 = Evolution_end} (from an evolution phase to a stable state, lines 12-14 and 29-31) or T s ∩ T G (for a firing stage, with the subsequent update stage, at lines 6-8 and lines 22-24).

If only L2-SCG minds as the state-space to generate, then the lines of the calls to the macro AddSCG1 should be discarded in Algorithm 2 and in procedure FromStable2.

The consistency check is done for an update stage at lines 9 and 25. At lines 14 and 31, although the transition T s = {t ε2 } is specific to ε-TPN, it expresses the leaving of an evolution phase, and it may be useful to detect a deadlock in the source grafcet (i.e. an always empty evolution phase) by model-checking.

As illustration, the L1-SCG of the example Fig. 5(b) is made of 14 classes and 17 transitions: it just saves the classes {C 3 , C 11 , C 13 , C 16 } in the L0-SCG. The L2-SCG is made of 4 classes and 7 transitions, detailed in Table 2.

In the second column of Table 2, only relevant variables are represented: X 1 , X 2 , O 1 and I 1 . In particular, the variable 1s/X 2 is obviously always false in a stable state. The Table 2. L2-SCG classes and transitions of the example Fig. 5(b).

Classes Some variables Transitions at true value

C1 X1 {t∞,I_1_to_true} -----------→ C5 C5 X2, O1, I1 {1s_X_2_true} ---------→ C5 {t∞,I_1_to_f alse} ------------→ C7 C7 X2, O1 {1s_X_2_true} ---------→ C1 {t∞,I_1_to_true} -----------→ C9 C9 X2, O1, I1 {1s_X_2_true} ---------→ C5 {t∞,I_1_to_f alse} ------------→ C7
domains of the stable state classes are such that all firings get the clock interval [0, 0], except transition 1s_X_2_true with clock interval [0, 1] in the classes C 7 and C 9 .

Consistency check of an update stage

Basing on the equivalence of behaviour between a grafcet and the corresponding ε-TPN, consistency check is only reserved for an update stage where ambiguity in a grafcet model may lead to contradictory actions. Indeed, incompatible update firings may concern stored actions on activation or deactivation:

-stored action on boolean output (or boolean internal variable): set and reset a given variable from a same situation. Subsection 3.4 deals with this case by preventing set and reset of a variable B i in the same update stage: places Set_B_i and Reset_B_i will remain marked at the end of the stage; -on nonnegative counter: reset, and increasing or decreasing a given counter C i from a same situation.

To detect such a contradiction after an update stage, a solution may be to make sure that activate or deactivate firings to update the states of various steps (for a step i, it is done by transitions Deactivate_Step_i and Activate_Step_i in the related ε-TPN) do not cause contradictory stored actions, by pairs of such update transitions. To implement this solution, from the structure of the ε-TPN, the set of update transitions for each variable (counter or boolean) may be established, before computing the state-space. For n activate or deactivate firings concerning the same variable, n(n -1)/2 pairs are possible. So, for m variables in the model related to some stored action and n max maximum number of update firings per variable, the complexity of an update stage test is in polynomial order: it is bounded by m × n max × (n max -1)/2.

The test fails when for some variable, two update firings are incompatible. However, the presented solution just gives a sufficient condition to detect an ambiguity in stored actions. For instance, multiple updates of a counter in a stage may always lead to the same state.

Taking into account CT L * model checking

With ε-TPN, a specific way for computing SCG is necessary to take into account CT L * model checking, similarly to the classic TPNs in general. This is justified by the transition t ∞ introducing convex domains, with multiple possible values of clock for a same firing in a class.

ASCG is computed from an intermediate SCG [START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF] (SSCG or CSCG), which may be one of the levels of abstraction presented previously. Obviously, the operation of splitting non-atomic state classes is worth doing only when no priority transition is fireable, that is from the classes reached by the into-stability stages: a head transition from such classes are in the set {t ∞ } ∪ T T . So, L0-SCG, L1-SCG and L2-SCG (in fact L0-SSCG, L1-SSCG and L2-SSCG respectively) will serve to create respectively L0-ASCG, L1-ASCG and L2-ASCG, using the algorithm described in the work [START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF]. No particular adaptation is necessary for that purpose, a firing t f from a class to split is just now a set including an external event and a zero delay transition.

As in the work [START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF], to reduce the size of the intermediate abstraction from which an ASCG is computed, comparing a new class with the stored classes will consist in inclusion test (to obtain CSCG) instead of equality test when computing an SSCG: it is again worth only from the classes reached by the into-stability stages.

The relaxation operation of a class when computing an SSCG or CSCG is justified when an unbounded delay transition (such as t ∞ ) may remain persistent after firing a delayed transition (such as an element of T T ): if the grafcet does not contain a non-zero delay transition (T T = ∅), then relaxation is always useless. The feature 4.3.8 makes anyway useless the relaxation operation.

Conclusion

The formal syntax and semantics for ε-TPN are proposed here, with some modifications made on the original description done in a previous work [START_REF] Sogbohossou | Formal modeling of grafcets with Time Petri nets[END_REF], mainly in order to simplify the construction of the ε-TPN state-space abstractions. Then, two algorithms are described to produce state-space abstractions, according to a partial-order semantics to cope with state explosion due to the concurrency inherent to a TPN formalism. A proposed consistency check should be applied to a stage (i.e. transition firings done in the same instant), especially for the update stages which may contain contradictory orders by the grafcet stored actions. The second algorithm generates the two abstractions relevant from a grafcet point of view: the all situations state-space and the stable situations state-space.

Based on the more clear definitions and characterisations about ε-TPN, a general perspective is to take into account the modelling of other concepts of the GRAFCET standard such as the hierarchical concepts of forcing and enclosure, by extending the translation rules.

Another extension of the current work is to allow model-checking for quantitative time properties. Indeed, TCTL [START_REF] Alur | Model-checking in dense real-time[END_REF] is a quantitative time temporal logic applicable to TPNs [START_REF] Boucheneb | TCTL model checking of time petri nets[END_REF], and a perspective may be to adapt it to ε-TPN.

2. 1 . 1 . 1 ) 6 ) 7 )

 11167 SyntaxStructurally, a time Petri net is defined as follows: Definition 1. A Time Petri net (TPN) is a tuple (P, T, W, W I , W R , ED, LD, M 0 ) such as: the nodes: P is the set of places and T is the set of transitions (P ∩ T = ∅);2) the regular arcs and the corresponding weights between nodes, W : P × T ∪ T × P -→ N;3) the read arcs, W R : P × T -→ N; 4) the inhibitor arcs, W I : P × T -→ N * ∪ {∞}; 5) the TPN initial marking, M 0 : P -→ N; the earliest firing delays of transitions, ED : T -→ Q + ; the latest firing delays of transitions, LD : T -→ Q + ∪ {∞}.

Figure 1 .

 1 Figure 1. An example of grafcet.

Figure 2 .

 2 Figure 2. A Petri net simulating a grafcet behaviour.

Figure 3 .

 3 Figure 3. Phase sequencer.

  : the firing of this transition with interval [0, ∞[ allows the occurrence of an input change at any time. The given (non exhaustive) elements of translation are respectively, at Fig. 4: -(a): a step i with state variables X i and X i , -(b): an input I x with rising edge ↑ I x and falling edge ↓ I x , -(c): a timed variable T j /X i such as the firing T _j_X_i_to_true expresses an external timed event, -(d): an example of two continuous actions, with the condition X 1 in step 3, -(e): an example of two transitions, with one shared input step and the condition I 1 + I 2 on transition (2). For each figure, elements in gray are already contained in a previously generated module.

Figure 4 .

 4 Figure 4. Examples of translated elements of grafcet.

  ) allows an unpleasant behaviour: when the grafcet contains undesirably contradictory orders on set and reset the boolean variable B i in a same situation (one token marking of the places Set_B_i and Reset_B_i at Fig. (b) corresponds to the orders in Fig. (a)), the TPN translation at Fig. (c) allows to fire consecutively the transitions B_i__to_true and B_i__to_f alse in an infinite loop (in zero time), meaning that an evolution phase may last indefinitely.

Figure 5 .

 5 Figure 5. The example of grafcet at Fig. 1 (a) and the translation into ε-TPN (b).

Figure 6 .

 6 Figure 6. Stored action.To avoid such a behaviour involving specifically a non-finite update stage, two inhibitor arcs are added at Fig.6(d) representing the new modelling: a set (resp. reset) order prevents now resetting (resp. setting) B i in a current update stage. Of course, the model checking should spot the problem for afterward corrective action in the grafcet model.

4. 3 . 6 . 4 . 3 . 7 .

 36437 When a transition in T T ∪ {t ∞ } is fired, then only transitions with zero static delay are fireable in the same out-stability stage It is contained in the development of the features 4.3.4 and 4.3.5. When the transition t ∞ is fired, then one transition in T input for each input defined in the grafcet is fireable in the same out-stability stage It is contained in the development of the features 4.3.4 and 4.3.2.

1 8 FromEvolution

 8 Input: marked ε-TPN; 2 Output: sets CL 0 and TL 0 for L0-SCG; 3 CL 0 := {C0}; TL 0 := {}; 4 Stack C0; 5 while the stack is not empty do 6 Unstack C = (M, D, V ); 7 if ∃t ∈ En(M ) ∩ TE 0 then

4

  Compute C from C ; Ts := Ts ∪ {{t }}; C := C ; 5 end Procedure FromEvolution If the class reached by the stage computed by the procedure FromEvolution at line 8 of Algorithm 1 is a new one, then this class is stacked at line 9 to handle it later, and next at line 10 is saved the new transition caused by this stage with the call to the procedure AddSCG.

1 3 if t = t∞ then 4 foreach

 34 foreach t ∈ En(M ) fireable from C do 2 Compute C from C; Ts := {{t }}; transition t ∈ En(M ) ∩ Tinput do 5 Compute C from C ; Ts := Ts ∪ {{t }}; En(M ) ∩ TE 0 such as δ(t ) = 0 do 11 Compute C from C ; Ts := Ts ∪ {{t }}; C := C ;

  T s in the call AddSCG1 at line 7 (resp. line 14) of the macro FromStable2. Precisely, STACK2 saves a couple (T ext , C) instead of a simple class C at lines 6 and 13 in the macro FromStable2.

Table 1 .

 1 L0-SCG transitions of the example Fig. 5(b). Output: sets CL 1 and TL 1 (L1-SCG), sets CL 2 and TL 2 (L2-SCG); 3 CL 1 := {C0}; CL 2 := {}; C = C0; 4 TL 1 := {}; TL 2 := {}; 5 while tε 2 is not fireable from C do

	Transitions	Ts	Transitions	Ts	Transitions		Ts
	C 0	Ts → C 1	tε 2	C 6	Ts → C 7	tε 2	C 11	Ts → C 12	Activate_Step_1, Deactivate_Step_2,
									1s_X_2_f alse
	C 1	Ts → C 2	t∞ , I_1_to_true	C 7	Ts → C 8	t∞ , I_1_to_true	C 12	Ts → C 13	tr_1, F iring
	C 2	Ts → C 3	tr_1, F iring	C 7	Ts → C 15	1s_X_2_true,	C 13	Ts → C 14	Deactivate_Step_1,
						T ime_out			Activate_Step_2
	C 3	Ts → C 4	Deactivate_Step_1, Activate_Step_2	C 8	Ts → C 9	tε 2	C 14	Ts → C 5		tε 2
	C 4	Ts → C 5	tε 2 , O_1_true	C 9	Ts → C 6	t∞ , I_1_to_f alse	C 15	Ts → C 16	tr_2, F iring
	C 5	Ts → C 6	t∞ , I_1_to_f alse	C 9	Ts → C 10	1s_X_2_true	C 16	Ts → C 17	Activate_Step_1,
						T ime_out			Deactivate_Step_2,
									1s_X_2_f alse
	C 5	Ts → C 10	1s_X_2_true, T ime_out	C 10	Ts → C 11	tr_2, F iring	C 17	Ts → C 1	tε 2	, O_1_f alse
	1 Input: marked ε-TPN;
	6	FromEvolution();					// Firing Stage
	8	FromEvolution();					// Update Stage
	9	Make the consistency check of the stage Ts;
	10	if C ∈ CL 1 then exit (NEVER_STABILITY) ;
	11	AddSCG1(C * , T * ,s, C ); C = C ;
	12 end
	13 FromEvolution();				// Into-stability Stage
	14 AddSCG1(C, {tε 2 }, C ); Stack C in STACK1;
	15 while STACK1 is non empty do
	16	Unstack CS from STACK1; C = CS;
	17	FromStable2();				// Out-stability Stage
	18	while STACK2 is not empty do
	19		Unstack (Text, C) from STACK2;
	20		Loc_Classes := {C};
	21		while tε 2 is not fireable from C do
	22		FromEvolution();				// Firing Stage
	23		C * := C; C := C ; T * ,s := Ts ∩ TG;
	24		FromEvolution();				// Update Stage
	25		Make the consistency check of the stage Ts;
	26		if C ∈ Loc_Classes then exit (NO_STABILITY) ;
	27		if C * / ∈ CL 1 then AddSCG1(C * , T * ,s, C ) ;
	28		Loc_Classes := Loc_Classes ∪ {C }; C := C ;
	29		end
	30		FromEvolution();				// Into-stability Stage
	31		if C / ∈ CL 1 then AddSCG1(C, {tε 2 }, C ) ;
	32		if C / ∈ CL 2 then Stack C in STACK1 ;
	33		AddSCG2(CS, Text, C );
	34	end
	35 end
			Algorithm 2: Construction of the L2-SCG

2 7 C * := C; C := C ; T * ,s := Ts ∩ TG;

If transition t i is not enabled, v(t i ) does not mind: this value will not be of no use, to decide equality between two states for instance.

A multiset on a set X is a function Y : X → N; an equivalent notation is Y ∈ (N) X .

The concept of fireability with grafcets is thereby to be differentiated from the one of TPNs.Definition of a Time Petri Net Formalism Simulating the Behaviour of the Timed Grafcets 5

external to the processor of the control part of the system.

ARIMA -Volume 31 -2019

Input: C, Ts, C ;

if C / ∈ CL 0 then CL 0 := CL 0 ∪ {C } ;

TL 0 := TL 0 ∪ {(C, Ts, C )};Procedure AddSCG