Nesrine Khabou
email: nesrine.khabou@redcad.org

Ismael Bouassida Rodriguez

Ghada Gharbi

Mohamed Jmaiel

A Threshold Based Context Change Detection in Pervasive Environments: Application to a Smart Campus

Keywords: Ubiquitous computing, context awareness, adaptation, context analysis techniques

Context awareness is an essential feature of pervasive applications and runtime detection of context changes is necessary for enabling context awareness. Context aware applications are applications that are able to adapt their behavior (self adaptivity property) according to the available resources, environmental conditions, user needs, etc. The self adaptivity property is enforced by four phases. Monitoring/Collecting context parameters, analyzing the collected context parameters to detect changes, planning appropriate adaptation actions and finally executing the planned actions to respond to the changes. In this paper, we focus and discuss the second phase (Analysis phase). Contrary to the most research activities in which the analysis phase is performed by comparing context parameters against fixed thresholds, we propose an analysis approach that uses a threshold comparison technique. Fixed as well as adaptive thresholds are applied to detect changes and trigger notifications that are used to deal with the changes.

Introduction

The widespread of mobile devices (laptops, palmtops, smart phones) and sensors and the seamless connectivity between them have transcended the traditional computing era to the pervasive/ubiquitous computing. Pervasive/ ubiquitous computing aims at building smart environments where computing and communication are embedded in almost every surrounding object and can be accessed all the time and everywhere.

Context aware applications have thus emerged as one of the most important fields of pervasive/ubiquitous computing. These applications are those which can adapt their behavior in response to the context change without user intervention allowing to increase the application effectiveness by taking environmental context, user requirements into account ? .

The development of context aware applications is a complex process that requires the fulfilement of four phases. This process starts by collecting/monitoring context. This phase is considered a main phase of any context aware application. Collecting/monitoring context have a variety of sources such as sensors, networks, devices, users and other sources. The collected context parameters are analyzed in the second phase (Analysis) to detect the context changes. Several techniques such as threshold comparison, conditions or rules are used to detect changes. Once context changes are detected, adaptation actions are planned in the third phase (Planning). Finally, the planned actions are executed in the fourth phase (Execution) to react to the changes.

In this paper, we discuss the second phase (Analysis). This phase is divided into three consecutive steps: Context storage, context processing and classification, and finally, context change detection. The context storage is out of the scope of this paper. We first define the context classification step that attributes context categories for each context parameter. Second, we propose the context change detection step that targets detecting context changes and raising notifications when changes occur.

The rest of the paper is organized as follows. In section 2, we give an overview of some research studies dealing with context classification and context change detection in pervasive/ubiquitous environments. Then, in section 3, we introduce a case study named Smart Campus system. Its purpose is to provide suitable services to users according to the context changes. The analysis approach is presented in section 4. We define first the context classification step that takes into account the context parameter evolution. Then, we present the context change detection step that allows an application to analyze context and detect context changes using thresholds. In section 5, we motivate and illustrate the feasibility of our approach through an illustrative scenario. The last section concludes the paper and gives some directions for future work.

Related work

Many researchers have proposed several classifications of context. Some studies classify the context into two categories such as Schmidt ? , Prekop and Burnett ? and Mitchell ? . Schmidt ? , states two context categories such as physical environment and human factors. Mitchell ? divides the context into two categories. A personal environment and an environmental context. Other studies classify context to several categories such as the studies of Rodden et al. ? and Schilit et al. ? . In order to achieve a better understanding of the concept across a time span, Brown et al. ? add time context such as the time of the day, the week, the month and the season of the year.

Context classification is an important step to discover the possible context easily, simplify the context manipulation including context analysis. In fact, the context analysis's purpose is to analyze context parameters and identify context changes. In the context changes detection research direction, several techniques and models are proposed in order to detect the context changes.

In fact, Cioara et al. ? propose to use the context entropy concept for detecting the context changes and determining the degree of fulfilling a predefined set of policies. Moreover, context situation entropy defines the level of the systems self and execution envionment disorder which is measured by evaluating the degree of respecting a set of policies. Hence, once the context entropy exceeds a fixed threshold, then the system is in a critical state and it must execute adaptation actions. Although this approach allows a self adaptation following context changes, it does not consider many context parameters to study as it is restricted to context parameters related to the environment such as temperature, humidity and light, etc. In other studies, context changes are detected by comparing a context parameter value saved in a repository with a new context parameter value. In fact, Zheng et al. ? have addressed the issue of context change detection by proposing a context-aware middleware which conforms to the CORBA component model. The proposed middleware is composed of context aware services such as a context collector, a context interpreter, a context repository and a context analyzer. The latter is in charge of filtering and analyzing context information to determine relevant context changes and notifies the application afterwards. Furthermore, context filtering is based on a comparison of the context values stored in the context repository with the new context value in order to detect context changes. The proposed middleware enables to save the scare resources. In fact, the component deployment is performed just-in-time. However, this middleware does not specify context information to take into account. In the work of Baloch and Crespi, ? , they have proposed a framework for context acquisition, management and distribution in a ubiquitous environment. Context is collected from various sources and devices. Then, whenever a context change occurs, the device publishes its context in order to take the appropriate decision. However, the authors do not specify how context changes can be detected using their framework. Another approach for dynamic context management is proposed by Taconet et al. ? . Taconet et al. present CA3M, a context aware middleware, which enables applications to adapt their behavior by dynamically taking into account context changes. The authors model the application by entities, which represent a physical or a logical phenomenon (person, concept, etc.) and observable, which defines something to observe. For instance, a mobile device state is an example of an observable which may take a finite number of values (e.g low battery, almost low battery or normal battery). They consider that the change of an observable state or even the observation goes past a given threshold from the last notified value leads to a different application behavior. However, using a given threshold can cause false detections. Other approaches are used to analyze context. In fact, Bouassida Rodriguez et al. ? proposed a model driven approach for collaborative ubiquitous systems. In order to detect context changes, they specify predefined thresholds. Then, once context values remain below/under the threshold values, a notification is raised. Although this approach enables to detect instantly context changes, it may cause false detections as well as missing alarms by using fixed thresholds To illustrate the use of our approach, we describe in the following an example of a Smart Campus system illustrated in Fig. 1. Smart Campuses, with the ability to collect and analyze data, are built in order to benefit the institutions, the students, the teachers and the staff by providing services which facilitate interaction between the actors such as the teachers, the students and the staff. For instance, every actor is equipped with a personal device (PDA, smart phone, PC, tablet, etc) and the Smart Campus system provides different services to actors based on their current situations. To maintain the cooperation between students and teachers, the actors devices need to be aware of their environmental, execution context, etc. Consequently, Smart Campuses contain an infrastructure that allows devices and systems to be monitored and adapted automatically/autonomously according to the context. Our work focuses on several context parameters related to the environment and the user such as temperature, position and light which need to be monitored. Furthermore, a multitude of resources related to the devices and to the network such as the available memory, the energy, the CPU load and the available bandwidth should be considered and supervised to assess both the devices and the communication state.

Case study: Smart Campus

An efficient Smart Campus relies on the cooperation of smart devices. The campus architecture depicted in the Fig. 1 involves different kinds of participants. On the one side, two controlling servers called Smart Campus Servers (SCServers) namely SCServer1 and SCServer2 which are Ethernet connected and equipped with important storage and high computational capabilities. On the other side, fixed (Presence sensors, cameras, lamps, air conditioners) and mobile (laptop, PDA, phones) devices are placed. The mobile devices are usually resource constrained in terms of memory, bandwidth and energy for example. Hence, a periodic monitoring by the controlling servers is needed in order to check their state which changes according to context. Two gateways called Smart Campus Gateways (SCGateways), SCGateway1 and SCGateway2 implementing software interfaces are used to connect devices to the corresponding controlling servers (SCServers) to exchange relevant information. The campus space is composed of separate rooms (Research laboratory, Meeting room, Classroom1 and Classroom2). Each room is equipped with fixed devices as well as mobile devices that are carried by the different actors. Because of the complexity of the interaction between the different entities, we propose to focus our study on a part of the Smart Campus . It consists in the gateway SCGateway1 connected to both the SCServer1 and the devices located in the Classroom1.

The proposed approach

Context parameters classification step

With a wide range of context parameters, context parameters should be classified into categories towards using context effectively. We propose a context classification that takes into account the evolution of the context parameters. Three categories are distinguished. Context parameters which evolve in a trend way, context parameters which are characterized by peaks and context parameters which are characterized bu bursts. The three context categories are depicted in Fig. 3.

1 The term trend refers to a stable tendency of growth or decline exhibited in the data as illustrated in Fig. 3(a).

For example, each mobile device such as PDA, mobile phone, etc. mentioned in section 3 periodically monitors its resource state (Battery level, memory consumption) that belong to the trend category. 2 Peaks are defined as high values with sharp rise followed quickly by sharp fall implying a narrow period width ? .

We define a peak P by its amplitude "A p " and its period T as depicted in Fig. 3 narrow period of high values-That is, its amplitude "A p " exceeds for "n" times the average amplitude"A av " of the time series formed by the context parameter values. For example, the link load context parameter illustrated in Fig. 3(b) belongs to the peak category.So, a peak is defined by the following formulas:

A p = n × A av T ≤ m × T imeUnit
Where A p defines the peak's amplitude, A av defines the average amplitude of the parameter curve, n and m are constants fixed by the application designers. 3 A burst consists on a relatively wide contiguous region of values. A burst is defined as a large number of occurring events Klan et al. ? . As depicted in the Fig. 3(c), we can model the wide region by an ON-period and the other by an OFF-behavior Yang ? . The ON-period models a single flow such as the transfer of a single web page, and the OFF-period models the users thinking time. Noting that the ON-period and the OFF-period are strictly alternating. The message number is modeled as a burst as depicted in Fig. 3(c).

Context change detection step

Since the context parameters classification step is based on the context parameters evolution, we detail in the following the threshold calculation for each context category defined previously. For each context parameter belonging to a category, we propose to assign a number of thresholds. Each threshold is characterized by a level and for each level corresponds a notification type. When context parameters curve cuts the threshold, a notification is raised (See Fig. 4).

Threshold calculation for trend based context parameters evolution

For this category, the context parameters evolution is described by a trend. In order to avoid false detections as well as missing alarms, we need to define thresholds which are uncorrelated with the context parameter evolution. The notification raised when the context parameter value crosses the threshold is illustrated in Fig. 4. Different kinds of thresholds can be applied for this category, such as fixed thresholds, adaptive thresholds and step function thresholds. For instance, fixed thresholds may be defined by the application designers according to the context parameter characteristics. Then, a notification is raised once the context parameter value crosses the fixed threshold as depicted in the Fig. 4(a). For the adaptive threshold denoted in the Fig. 4(b), mathematical models need to be applied in order to update threshold values at runtime such as the Exponential Weighted Moving Average technique ? used by Lahyani et al. ? . However, for this kind of context parameters characterized by a trend, adaptive threshold must be uncorrelated with the parameter evolution in order to avoid false detections and missing alarms. Finally, for the step function threshold described in the Fig. 4(c), thresholds are defined per period and notifications are raised when the context parameter values crosse the thresholds. In our case study: Smart Campus, the memory consumption can be modeled by a trend. Each mobile device needs to monitor and analyze the memory consumption to evaluate its state. So each mobile device compares periodically its memory consumption state with the threshold. A notification is raised when there is an intersection between the threshold and the memory values as illustrated in Fig. 4.

Threshold calculation for peak based context parameters evolution

Identifying and detecting peaks in a given time series is important in order to react accordingly and to avoid undesirable effects. In this context category, the idea consists of specifying adaptive thresholds. In fact, using fixed thresholds in this category could cause false alarms. As mentioned in the Smart Campus case study (section 3),

Link Load values

Link load values Time Fig. 5. Threshold calculation for a context parameter whose evolution is characterized by a peak the servers receive periodically contextual information from the devices through the gateways. In case of a sudden large amount of data, the servers could be overloaded and need to perform an important processing. This overload is identified when the CPU load oversteps the adaptive threshold for this context category as illustrated in Fig. 5.

Threshold calculation for burst based context parameter evolution

In this category, our idea consists on transforming a bursty model into a peaked or a trend model. So, we propose to apply an aggregate function G in each ON-period. The aggregate function application is illustrated in Fig. 6(b). As depicted in the Fig. 6(b), the obtained model roughly coincides with a trend function. After applying thresholds, a notification is raised when the context parameter values cross the threshold calculated in an ON-period. For the Smart Campus case study (section 3), the gateway SCGateway1 analyzes the received data from the devices. The maximum queue size of the gateway is set by the application designer. So, if the traffic received by this gateway in a period T i exceeds a maximum, then a burst is identified in T i . Towards detecting bursty periods, the function G is applied. In our case study, the function G calculates the slope of the scatter diagram obtained in each ON-period. And, the intensity of each slope formed in each ON-period is computed (Result shown in Fig. 6(b)). Consequently, if the slope intensity exceeds the threshold, then a burst is detected and appropriate adaptation actions are launched as shown in Fig. 6(c).

Illustrative scenario

In this section, we consider the case of a Smart Campus as shown in section 3. We focus in the interaction of the actors of the Classroom1 and SCServer1 through SCGateway1. This Classroom1 is used by the researchers, the teachers, the students. The context parameters considered in this scenario are the following: The scenario starts as follows: At the beginning of each course session, the presence sensor captures and localizes the mobile actors. Their positions are then forwarded to SCServer1. SCServer1 runs the analysis algorithm based on thresholds on the context parameter (mobile actors position) and takes the appropriate desicion. Since the SCGateway1 communicates information received from the devices to the corresponding SCServer, in case of a large amount of data received by the gateway SCGateway1 at T i , the load of SCGateway1 increases rapidly reaching a high value (i.e a peak) and exceeding the adaptive threshold specified for this context parameter. The analysis algorithm integrated in SCGateway1 raises a notification and the gateway decides to split its load with its neighboring gateway namely SCGateway2.

Each student participating to a course uses a tablet device to which the course will be dispatched through bluetooth. The tablet device holds the analysis algorithm in order to detect context changes. During the course, the students tablet display appropriate slides and follow their courses. Furthermore, the students can write annotations on their tablets and publish their comments to share knowledge between all the group members to enrich the course and enhance the cooperation. A student holding a tablet is participating to the course by exchanging information and slides. For each amount of data received, the tablet device retrieves the memory consumption from the operating system using probes. Then, it compares each value with the threshold which can be either fixed, adaptive or step function since memory consumption belongs to the trend context parameter category as illustrated in Fig. 7. The tablet detects that at an instant T i , the memory consumption exceeds the threshold (Notification2). So, the device closes unecessary applications (Specified by the user). If this action is not enough (Notification3), the device displays a message proposing to the user to close some other running applications . This scenario highlights the interaction of the campus application with Fig. 7. An example of threshold application on the memory context parameter context in such a way that it can detect context changes using the analysis approach in order to adapt its behavior accordingly.

Conclusion

The challenges for context aware applications design and implementation are to handle monitoring/collection, analysis, planning and acting. In this paper, we have discussed the second phase (Analysis). The analysis phase is divided into three steps. We have defined first a context classification step based on context parameters evolution. Three categories have been identified. A trend category, a peak category and a burst one. Then, we have presented a context change detection step which aims at analyzing context and identifying context changes. In order to identify changes, we propose a threshold comparison technique. Different thresholds are used to detect changes such as fixed, adaptive and step function. As future work, we plan to stretch the context classification step. For further development, we intend to implement our analysis approach and to use it by generic applications.

Fig. 1 .

 1 Fig. 1. Case study: Smart Campus

Fig. 2 .

 2 Fig. 2. An overview of the self adaptivity process of a context aware application

  Fig. 3. The proposed context categories

  Fig. 6. An example of threshold application for burst based context parameters evolution

https://a2nets.erve.vtt.fi/

Acknowledgments

This research is supported by the Itea2's A2NETS (Autonomic Services in M2M Networks) project 1 .


Baptiste Poirriez

Aurélie Lemaitre

Bertrand Coüasnon

Visual perception of unitary elements for layout analysis of unconstrained documents in heterogeneous databases

Keywords: document layout analysis, heterogeneous documents, business documents, tables, forms

The document layout analysis is a complex task in the context of heterogeneous documents. It is still a challenging problem. In this paper, we present our contribution for the layout analysis competition of the international Maurdor Campaign. Our method is based on a grammatical description of the content of elements. It consists in iteratively finding and then removing the most structuring elements of documents. This method is based on notions of perceptive vision: a combination of points of view of the document, and the analysis of salient contents. Our description is generic enough to deal with a very wide range of heterogeneous documents. This method obtained the second place in Run 2 of Maurdor Campaign (on 1000 documents), and the best results in terms of pixel labeling for text blocs and graphic regions.

I. INTRODUCTION

This work addresses the problem of document layout analysis of heterogeneous and unconstrained documents. In an industrial context, automatic document processing has to face with a large variety of documents: there is no a priori about the possible content of the documents. The actual methods of document layout analysis are often trained to recognize a specific kind of document but the processing of heterogeneous databases of documents is still an open problem. Moreover, the modern layouts of documents can vary and it is not possible to predict a standard document organization.

In this context, an international competition called Maurdor Campaign [START_REF] Dga | Maurdor campaign dataset[END_REF] was led in November'2013 (second run). One of the tasks was the layout analysis of heterogeneous documents, such as those presented on figure 1. The images contain mixed printed and handwritten text, with three languages (French, English, Arabic). They sometimes contain graphics, logos, tables, forms... The goal was to localize homogeneous text regions (script and language), tables, and various kinds of graphic regions.

In this paper, we present our system for this competition. It is based on a grammatical description of the possible contents of the documents. The originality is to iteratively look for the most salient and structuring elements in the document, and to authorize a new segmentation of the document during the analysis.

This paper is organized as follows: after a study of the related works, our method will be presented on section III. Then, we will describe how we have implemented our system with the existing DMOS-P method. We will end in section V with the results that we have obtained in Maurdor Campaign and with a discussion on possible improvements.

II. RELATED WORK

Document understanding presents various challenges [START_REF] Dengel | Making documents work: Challenges for document understanding[END_REF]. In this work, we have to deal with two difficulties: the heterogeneity of the documents and the heterogeneity of the database. Those two aspects are often studied separately in the literature.

We call heterogeneous documents some documents that may contain various kinds of contents: handwritten text, printed text, graphics, tables, forms. Some works are proposed for pixel labeling of heterogeneous documents inside of a quite homogeneous collection. Recently, Cote et.al. [START_REF] Cote | Texture sparseness for pixel classification of business document images[END_REF] propose a method to label pixels in business documents. This approach is based on texture analysis, as many other approaches cited in their state of the art. Those approaches are convenient when we can rely on certain stability inside of the collection. For example, on the proposed business document collection, the text blocs are quite homogeneous.

On the other hand, the study of heterogeneous databases often leads to a problem of classification. For example, Medvet et. al. [START_REF] Medvet | A probabilistic approach to printed document understanding[END_REF] propose to analyze the layout of various kinds of printed documents. However their method requires learning a new class for each new kind of document. Many methods have been proposed for the classification of document image in heterogeneous images, as summarized in this survey [START_REF] Chen | A survey of document image classification: problem statement, classifier architecture and performance evaluation[END_REF].

In our case, we do not know a priori the kind of document that can be submitted to the layout analysis process. Then it is not possible to learn classes of documents. We have to focus on the analysis of structuring elements that might be present. In that context, the existing work often focus on one kind of element. For example, in [START_REF] Shafait | Table detection in heterogeneous documents[END_REF], the authors extract tables in documents with varying layout (company ). An extraction of tables is also proposed by LITIS lab [START_REF] Kasar | Learning to detect tables in scanned document images using line information[END_REF] on the Maurdor database. The particularity of this work is to combine the two difficulties: heterogeneous contents of documents and unconstrained databases. To our knowledge, there are few studies in the literature dealing with those two difficulties in the same time, except for Maurdor database [START_REF] Barlas | A typed and handwritten text block segmentation system for heterogeneous and complex documents[END_REF].

III. OUR METHOD FOR DOCUMENT LAYOUT ANALYSIS

In this section, we present our work for layout analysis, which begins after a pre-processing step.

A. Pre-processing: orientation detection

Due to the heterogeneity of the database, we have to apply a preprocessing tool to detect the orientation of the documents. Our strategy is to use an element of perceptive vision: when having a global vision of a document, a human can detect the main orientation of a document (with a precision of 180 ˚). The human vision is guided by the main direction of the writings. We use this idea for the orientation detection: we extract the line segments in a low resolution image (built by sub-sampling), which give indications on the document orientation. Indeed, the text-lines are perceived by the human eye as line segments at low resolution. If the number of vertical line segment is significantly higher than the number of horizontal line segment, then we rotate the document.

B. Overview of the method

We have to detect structuring elements, without knowing if they are present in the document. We propose to use two principles of perceptive vision that we used in the context of homogeneous databases [START_REF] Lemaitre | Interest of perceptive vision for document structure analysis[END_REF]:

• some contents are salient for the human vision inside of a document, which are often strongly structuring; • combining several points of view of a document enables a prediction/verification mechanism: the layout is predicted in a global vision of a document and verified with details. Our method is based on a grammatical description of the content. The strategy of analysis consists in iteratively finding the most structuring and salient elements: the tables and boxes, then the text blocs and at last the graphics. The originality of this analysis is to ask for a new segmentation of the document, during the analysis, to take into account the previously detected elements.

The figure 2 presents an overview of the different steps of analysis. Each step is detailed in the following sections. We use several kinds of primitives as terminal elements of our grammar:

• the line segments,

• the connected components,

• the printed words that are recognized by an OCR. Depending on the level of analysis, those elements are detected at different resolution levels of the image.

C. Tables, boxes, separators

The first part of our work consists in localizing tables, boxes and separators. Those elements are based on the presence of rulings. Consequently, we use the results of a line-segment detector (based on Kalman filtering) as an input of our grammatical description.

We first consider that a document can contain tables. A table must be composed of at least two crossing rulings (figure 3(a)). Then we look for parallel horizontal or vertical rulings having the same size. However, sometimes all the rulings are not present, or the tables are not rectangular, and it is not possible to find parallel rulings having the same size as the initial cross. Consequently, we compute some "virtual rulings" (figure 3(b)) that has the same length as the base crossing rulings. Once each ruling is detected, we compute the cells inside of the table (figure 3(c)). Our grammatical description expresses that we have to recursively analyze the content of the cells of a table or of the boxes. Indeed, inside of a cell, we can find another table or any constituent of a whole document. This method enables to easily deal with recursive tables.

The isolated boxes are made of four isolated rulings that constitute a rectangle. The remaining long enough rulings are considered as separators.

D. Latin printed text analysis

For printed text analysis, we use the commercial OCR Abbyy FineReader CLI. This OCR does not provide a correct layout on very unconstrained heterogeneous documents, but it enables to localize some printed words (figure 4(a)), even if documents also contain handwritten text and graphics.

Those words are used as input of our grammatical description. We select the words that we can trust, depending on various criteria given by the OCR: belonging to a dictionary, high enough recognition confidence, size of the word. These criteria enable to filter the handwritten words that are detected as printed by the OCR. The grammatical rules then describe a text bloc as a set of words that are organized into lines (figure 4(b)). The grammar checks among others the text alignment, the consistence of font-size. It also detects the presence of columns to build the final text-blocks.

E. New segmentation

At this step, the most structuring elements of the document have been detected: tables, boxes and printed text blocs. However, those elements sometimes interfere with the detection of the remaining elements (handwritten text or graphics). For example, in a form field, the ruling may cross the handwriting, which causes troubles to detect the connected components that compose the handwriting.

In order to deal with this problem, we propose to remove the previously detected elements before re-segmenting the analysis. The "removing" is done by replacing in the image all the black pixels by a gray level that corresponds to the estimated level of the local background color of the document. Then, the new extraction of connected components is realized.

F. Text-line extraction

The next step consists in extracting text lines in documents that now contain mixed graphic and text lines. The remaining text lines can be Latin or Arabic handwritten, Arabic printed and even the Latin printed text lines that have not been detected by the OCR. Our description of text lines must be robust enough to deal with all those cases. This is realized thanks to a mechanism of perceptive vision [START_REF]Use of perceptive vision for rulling recognition in ancient documents[END_REF]: at low resolution, the text lines can be perceived as line segments. We then apply our line segment detector to compute a prediction on the position of text line. Then, in the full image resolution, we can verify the presence of the text lines with the analysis of connected components: a text line is described as a set of regular aligned connected components. The difficulty is to sort the connected components between graphics and text lines when they overlap. We use thresholds on the size of the connected components to determine if they belong to a text-line or to a graphic region. This method can deal with slightly skewed text.

G. Graphic localization

The last step of analysis consists in localizing the graphic regions among the remaining components of the image. We use again a concept of the perceptive vision: the graphic regions are perceived as salient elements when we have a global view of the documents. Consequently, we work in a low resolution image (dimensions divided by 4 by subsampling). We consider that a graphic element is a big enough (more than 5 pixel edgewise) connected component in this image (figure 5).

IV. IMPLEMENTATION OF OUR METHOD

We have implemented our approach using the DMOS-P method.

A. DMOS-P method DMOS-P (Description MOdification of the Structure with Perceptive vision) [START_REF] Coüasnon | DMOS, a generic document recognition method: Application to table structure analysis in a general and in a specific way[END_REF] is a grammatical method for the recognition of structured documents. It is based on a specific grammatical language, EPF, which enables to express the physical, syntactical and semantic organization of a kind of document. Once the grammatical description has been realized, the associated parser is automatically produced by a compilation step.

The DMOS-P method has been validated on many kinds of documents (music scores, tables, forms, archive documents, mathematical formulas, business letters) and at a large scale (more than 700,000 document images). However, it has always been applied to relatively homogeneous databases.

B. Our implementation

In this work, the novelty is that we have to use DMOS-P method in the context of heterogeneous documents and unconstrained database. Consequently, we cannot describe precisely the content of each kind of document. Note that we had previously work on certain components of the documents: tables [START_REF] Coüasnon | DMOS, a generic document recognition method: Application to table structure analysis in a general and in a specific way[END_REF], text-lines [START_REF]Use of perceptive vision for rulling recognition in ancient documents[END_REF]. But as it was on a homogeneous context, our descriptions were not adapted for heterogeneous documents. We had to adapt them to describe all the unitary elements according to the strategy presented in section III. It was possible thanks to the powerful expressiveness of the EPF language. As the parser can deal with the presence or absence of each of these elements, this grammatical description is common for all the documents, even if they are heterogeneous.

Moreover, the DMOS-P parser is particularly adapted to this problem as it enables to ask for a new segmentation of the document during the analysis, which is required once we have detected the tables and rulings. This new segmentation is led by the grammatical description, which describes when it is necessary to remove elements.

At last, we have to combine several kinds of primitives: connected components, line segments, OCR words, extracted at various resolutions. This is very simple in DMOS-P method that offers the concept of perceptive layer. Indeed, each kind of primitive is stored in a layer and the grammatical description expresses which is the layer to study at each step of the analysis. Thus, the contents of the layers can be combined to produce some more complex results.

This implementation has been validated in the context of the international Maurdor Campaign. An example of produced result is presented on figure 6.

V. VALIDATION WITH MAURDOR CAMPAIGN

The Maurdor Campaign [START_REF] Dga | Maurdor campaign dataset[END_REF] is an international competition that aims at evaluating the various steps of document processing. It was led in November'2013 by the French lab LNE, Cassidian -an EADS company, and funded by the DGA. Several tasks were proposed in this campaign. We focus on the first one, called "Module 1", which evaluates the document layout analysis step.

A. Database and Metrics

The participants of the campaign were provided two sets of annotated data: a train set of 6,127 documents and a dev set of 1,000 documents. The competition results were evaluated on a third set: a test set of 1,000 documents. The database contains various kinds of documents (figure 1): blank forms and completed forms, typewritten commercial documents, handwritten personal letters, commercial letters, The documents have been manually labeled, following a guide of annotation. The annotations mainly contain homogeneous text blocs (with the same language and the same script), table regions, boxes, separators and various kinds of graphic regions (including signatures).

The evaluated systems must provide the best polygonal zones enclosing the regions of the ground truth, with the correct type. Two metrics have been used in the competition. The ZoneMap metric evaluates the quality of segmentation in terms of split and merge of polygonal zones. It is an error rate (the smaller is better). The Jaccard metric evaluates at pixel level if the correct type (text, graphic element, table. . . ) has been assigned to each pixel. The Jaccard score is a success value (the higher is better). Those two metrics are complimentary. They are fully described on the website of the campaign [START_REF] Dga | Maurdor campaign dataset[END_REF].

B. Obtained results

Three participants took part to this campaign. We present the global results of the campaign in table I. Our method obtains the second position in the global rates of the competition. Indeed, we mainly focused on finding the type of the elements in the image, more than building the ideal blocs. Consequently, our ZoneMap score, which evaluates split and merge, is not very good whereas our Jaccard Score, which evaluates to good classification of pixels, is very close to the best participant.

C. Discussion

The obtain results for this campaign show that the layout analysis of heterogeneous documents is a very difficult task. It is still an open topic, and our system meets a lot of confusing cases. We mainly have difficulties when graphics overlap text blocs. For example, the image 1(c) presents a high confusion between graphics and text blocs.

We also have difficulties to build homogeneous text blocs. As shows our bad score in ZoneMap, our method causes too much merge and split. In order to improve that, we need to detect in detail if a character is printed or handwritten and its language. For example, a handwritten field inside of a printed text must be isolated in a specific text bloc.

For that purpose, our future work will be to introduce some classifiers at connected component level to know if we have to aggregate a connected component to the current bloc. For example, we plan to use classifiers that separate printed Latin text vs Other, or Arabic text vs Other, or the different kinds of graphics. This should enable a cooperation between the grammatical symbolic description of the page and the statistic output of the classifiers.

VI. CONCLUSION

In this paper, we have presented our method for layout analysis of heterogeneous and mixed documents in the context of Maurdor Campaign. Our method is based on the following characteristics : a grammatical description of recognition rules based on the combination of points of view, an iterative analysis of most structuring elements which are salient in the document, the ability to re-segment the document during the analysis.

It is a new application of our DMOS-P method that had never been applied on such heterogeneous databases. We exploit its genericity and its ability to deal with elements that can be absent.

The results of Maurdor campaign shows that the layout analysis of heterogeneous documents is still an open problem. Our method is placed at the second rank of the competition for the global metric, and at the first place for the labeling of pixels of text and graphic regions.

The future work will be to introduce several classifiers (for script and language detection) and enrich the grammatical description by statistic features. This should enable to build homogeneous text blocs, which is required for the following steps of document recognition.

Figure 1 .

 1 Figure 1. Unconstrained database of heterogeneous documents

Figure 2 .

 2 Figure 2. Overview of the proposed method

  Figure 3. Table localization

  (a) Words located by the commercial OCR (b) Construction of text blocs with reliable words of OCR (c) Final text blocs after handwritten text analysis

Figure 4 .

 4 Figure 4. Text analysis based on OCR

Figure 5 .

 5 Figure 5. Graphic detection (a signature is a graphic element)

Figure 6 .

 6 Figure 6. Example of final segmentation: box in cyan, table in red, graphics and signature in orange, text blocs in green. This image obtains a score of 9.1% error rate with ZoneMap metric

  As our system focuses on some specific elements, such as text blocs, we present in table II the detailed results, on each category, with Jaccard metric. Those results show that our system obtains the best scores for the localization of text zones and graphic zones, at pixel level.

	Participant	ZoneMap(%) Jaccard
	Participant 1	48.7	0.45
	Our method	59.2	0.44
	Participant 2	73.5	0.28
			Table I
	RESULTS OF MAURDOR CAMPAIGN; LOWER ZONEMAP IS BETTER,
	HIGHER JACCARD IS BETTER
	Participant	Text zone	Graphic zone	Table
	Participant 1	0.552	0.394	0.363
	Our method	0.553	0.402	0.307
	Participant 2	0.307	0.176	0.174
			Table II
	RESULTS BY CLASS WITH JACCARD METRIC (HIGHER IS BETTER)

ACKNOWLEDGMENT

This work has been conducted in collaboration with Cassidian, an EADS company to study, develop and implement a prototype for automatic recognition of documents, for the French Ministry of Defence (DGA).


DiscoSNP

Discover Single Nucleotide Polymorphism (SNP) from nonassembled reads

TakeABreak

Detects inversion breakpoints without a reference genome by looking for fixed size topological patterns in the de Bruijn graph

GATB helps you as a NGS user

The GATB C++ library gives you the opportunity to quickly develop new NGS tools that fit your needs.

GATB helps you as a NGS developer

Here is a typical workflow when working with GATB GATB-CORE transforms the reads into a de Bruijn graph, saves it in a HDF5 file that can be opened by other tools developed with the GATB-CORE API.

The core data structure of GATB is a de Bruijn graph that encodes the main information from the sequencing reads.

Strength of GATB

GATB makes this graph compact by using a Bloom filter (a space efficient probabilistic data structure) and by using a CFP additional structure that avoids false positive answers from the Bloom filter due to its probabilistic nature.

The GATB philosophy proposes a 3-layer construction to analyze NGS datasets

GATB GATB

Objective

The Genome Assembly Tool Box (GATB)

► is an open-source software ► provides an easy way to develop efficient and fast NGS tools ► is based on data structure with a very low memory footprint ► allows complex genomes to be processed on desktop computers Erwan Drézen 1 , Guillaume Rizk 1 , Rayan Chikhi 2 , Charles Deltel 1 , Claire Lemaitre 1 , Pierre Peterlongo 2. GATB-TOOLS: a set of elementary NGS tools mainly built upon the GATB library (k-mer counter, contiger, scaffolder, variant detection, etc.).

3. GATB-PIPELINE: a set of NGS pipeline that links together tools from the previous layer.

License & Web Site

GATB is released under the GNU Affero General Public License.

Proprietary licencing for software editors or services providers is currently being studied.

For more details on GATB:

►

  Biological motif detectionSeveral tools based on GATB are already availableBloocooK-mer spectrum based read error corrector for large datasetsMiniaShort read assembler based on a de Bruijn graph. Results are of similar contiguity and accuracy to other de Bruijn assemblers (e.g. Velvet)

  1 and Dominique Lavenier 1 1 INRIA/IRISA/GenScale, Campus de Beaulieu, 35042 Rennes cedex 2 Department of Computer Science and Engineering, Pennsylvania State University, USA -CORE: a C++ library holding all the services needed for developing software dedicated to NGS data.

  , D. Lavenier, R. Chikhi, DSK: k-mer counting with very low memory usage, Bioinformatics, 2013 Mar 1;29(5):652-3 R. Chikhi, G. Rizk. Space-efficient and exact de Bruijn graph representation based on a Bloom filter, Algorithms for Molecular Biology 2013, 8:22 G. Collet, G. Rizk, R. Chikhi, D. Lavenier, Minia on Raspberry Pi, assembling a 100 Mbp genome on a Credit Card Sized Computer, Poster at the JOBIM conference, 2013 Jul 1-4 (Toulouse) Best poster award. K.l Salikhov, G. Sacomoto, G. Kucherov, Using Cascading Bloom Filters to Improve the Memory Usage for de Brujin Graphs, Algorithms in Bioinformatics, Lecture Notes in Computer Science, Volume 8126, 2013, pp 364-376

Tool Box for developing Tool Box for developing efficient NGS software efficient NGS software

	9th Brazilian Symposium on Bioinformatics, BSB 2014 9th Brazilian Symposium on Bioinformatics, BSB 2014

1. What is GATB ? Motivation NGS

  technologies produce terabytes of data. Efficient and fast NGS algorithms are essential to analyze them.

http://gatb.inria.fr a whole human genome sequencing reads can be handled with 5 GBytes of memory

	>read 1
	ACGACGACGTAGACGACTAGCA
	AAACTACGATCGACTAT
	>read 2
	ACTACTACGATCGATGGTCGCG
	CTGCTCGCTCTCTCGCT
	...
	>read 100.000.000
	TCTCCTAGCGCGGCGTATACGC
	TCGCTAGCTACGTAGCT
	...
	How to How to Analyze Complex Analyze Complex Genomes on a Genomes on a Simple Desktop Simple Desktop Computer ? Computer ?


Vincent Boitier
email: vincent.boitier@univ-paris1.fr.

Antoine Lepetit
email: antoine.lepetit@univ-paris1.fr.

Reduced form wage equations in the credible bargaining model *

Keywords: E2, J3, J6 search and matching models, credible bargaining, wage rigidity

 under a plausible parameter restriction. This solution is simple, micro-founded and permits a transparent analysis of the driving forces of wages. We argue that it can be used in a wide range of economic models incorporating the search and matching theory of unemployment to simplify the analysis and obtain more easily interpretable results.

Introduction

The search and matching framework has become an essential tool for the analysis of unemployment and the labor market. Because search frictions give rise to a surplus that has to be shared between firms and workers, the private efficiency of employment relationships is consistent with a broad range of wage setting mechanisms. [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF] have proposed an increasingly popular alternative to the standard Nash model of wage determination. It offers the advantage of addressing the so-called Shimer puzzle, namely the inability of the canonical search and matching model to replicate the volatility of labor market variables observed in the data. It does so by providing a micro-foundation for wage rigidity. These authors argue that the threat points of both employers and job seekers are to delay bargaining rather than terminate it. This tends to insulate wages from outside conditions in the labor market and make them endogenously rigid.

In the baseline version of this model, an analytical expression for real wages cannot be derived. As a consequence, introducing it in an otherwise standard search and matching frictions framework can substantially complexify the analysis. We show that is it possible to circumvent this problem and derive a reduced form wage equation from an alternating-offer wage bargaining game à la [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF] by imposing a plausible parameter restriction. More precisely, we impose that the probability of breakdown in bargaining is equal to the separation rate. In our specification, wages are partially connected to outside labor market conditions through the difference between the current and the expected values of unemployment. On the one hand, an increase in the current value of unemployment leads to an increase in the threat point of workers in bargaining and puts upward pressure on wages. On the other hand, an increase in the future value of unemployment leads workers to value more current employment and temper their wage claims. We provide a detailed account of how our simple wage equation could be used in a wide range of models incorporating the search and matching theory of unemployment to simplify the analysis.

The note is structured as follows. Section 2 develops a standard search and matching model of the labor market. Section 3 presents the alternating-offer bargaining game and derives the analytical solution for the wage. Section 4 analyzes the driving forces of wages and discusses how our simple expression could be used in the literature. Section 5 concludes.

Model

Consider a discrete time version of the search and matching model of [START_REF] Pissarides | Equilibrium unemployment theory[END_REF]. Firms and workers must match in the labor market in order to become productive. Matches are formed according to a constant returns to scale production function m t = µu α t v 1-α t where u is the number of job seekers, v the number of open vacancies and 0 < α < 1.

Unemployed workers find a job with probability f (θ) = mt ut and vacancies are filled at a rate q(θ) = mt vt where θ = v u is a measure of labor market tightness. At the beginning of each period, a fraction s of existing employment relationships is exogenously destroyed. Matches formed in one period become operational in the next period. The law of motion of employment n t is accordingly given by:

n t = (1 -s)n t-1 + m t-1 (1)
Workers are risk neutral and do not have access to financial markets. They can be either employed or unemployed. The values W t and U t associated with those two states are given by:

W t = w t + e -r [(1 -s)E t W t+1 + sE t U t+1 ] (2)
U t = b + e -r [f (θ t )E t W t+1 + (1 -f (θ t ))E t U t+1 ] (3)
where r is the discount rate and β = 1 1+r ≈ e -r is the discount factor. When employed, workers receive a wage w t and can expect to remain employed with probability 1 -s. When unemployed, workers receive the flow value of unemployment b and can expect to find a job with probability f (θ t ). Firms operate with a constant returns to scale production function y t = z t n t where z t , the state of technology, evolves according to an AR(1) process. They must pay a cost c to post a vacancy. The firm's values of a filled and an unfilled vacancy J t and V t are thus given by:

J t = z t -w t + e -r [(1 -s)E t J t+1 + sE t V t+1 ] (4)
V t = -c + e -r [q(θ t )E t J t+1 + (1 -q(θ t ))E t V t+1 ] (5)
Free entry in the posting of vacancies implies V t = 0. Therefore the job creation equation is:

c q(θ t ) = e -r E t J t+1 (6)
3 The alternating-offer wage bargain

Wages are determined according to a sequential bargaining game à la [START_REF] Binmore | The Nash bargaining solution in economic modelling[END_REF]. [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF] note that "many rounds of bargaining can occur within each period of search and employment". In line with this intuition, we assume that each period is divided into sub-periods during which bargaining takes place. The time interval separating one sub-period from another is τ . Firms begin the game by making an offer w to the worker. If the offer is accepted, the game ends. If the offer is rejected, the game goes on to the next sub-period when the worker makes a counter-offer w to the firm. During this time interval, the firm incurs a flow cost γτ while the worker receives flow benefits bτ . Moreover, before the worker makes his counter-offer, negotiations can breakdown with hazard δ. In this case, the worker gets U whereas the firm gets nothing. Otherwise, the game continues to the next sub-period. In this setting, it is optimal for each party to always make a just acceptable offer to the other side. Thus, the following equations govern the game:1

W w t = bτ + e -rτ (1 -e -δτ )U t + e -δτ W w t ( 7
)
J w t = -γτ + e -(r+δ)τ J w t (8)
Solving equations ( 7) and ( 8) for w (or equivalently for w ) and letting τ → 0, we obtain the following sharing rule:

2 W t - b r + δ - δU t r + δ = J t + γ r + δ ( 9
)
This equation is similar to equation (17) in [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF]. Under the assumption that the probability of breakdown during bargaining δ is equal to the separation rate s, and after using this sharing rule along with equations (2) and (4), we obtain:

w t = 1 2 z t + β(b + γ) + δ r + δ (U t -E t U t+1 ) (10)
This simple wage equation is our main result. [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF] set δ in order to match the volatility of the unemployment rate. The employer's cost of delay, γ, plays a similar role than δ in that it influences directly the volatility of unemployment. When γ is high, firms' surplus is small and changes significantly in percentage terms in response to shocks. As a result, stochastic variations in technology lead to important movements in job creation and unemployment. The converse reasoning holds when γ is low. Since knowledge about both the values of γ and δ is limited, we believe it is equivalent to fix one to a particular value and let the other adjust to match the volatility of the unemployment rate. 4 The wage equation: potential use

The steady-state equation

In steady-state, equation [START_REF] Pissarides | Equilibrium unemployment theory[END_REF] collapses to

w = 1 2 [z + β(b + γ)] (11)
The complete isolation of the wage from labor market conditions in that case has a simple intuitive explanation. On one hand, an increase in the value of unemployment U leads to an increase in the threat point of workers in bargaining and puts an upward pressure on wages. On the other hand, an increase in U leads to an increase in the value of employment W for the worker. As workers value more employment, they accept lower wages. When δ = s, those two effects cancel out. Mortensen and Nágypál (2007) obtain a similar expression within the context of an alternating-offer game with no probability of breakdown during bargaining by imposing that the separation rate s is equal to zero. We show that it is possible to find a simple analytical solution for the wage in a more realistic setup. We allow for a positive probability of breakdown during bargaining and do not impose that the separation rate is equal to zero. A similar result was also uncovered by Ljungqvist and Sargent (2014) in recent and independent work.

We believe equation ( 11) could be of great use in articles incorporating a steady-state labor market frictions model. In that type of framework, when wages are determined according to a generalized Nash bargaining game, the job creation equation becomes nonlinear in labor market tightness. One needs to solve for it numerically and this rules out the possibility of obtaining analytical results. This problem does not arise when using our simple wage solution. Because wages do not depend on labor market tightness in equation [START_REF] Shimer | The cyclical behavior of equilibrium unemployment and vacancies[END_REF], analytical expressions for all variables in the model can readily be obtained.

The dynamic case

In the more general dynamic case, the wage is not completely isolated from labor market conditions as U t and E t U t+1 may differ (see equation [START_REF] Pissarides | Equilibrium unemployment theory[END_REF]). Consider that the value of unemployment increases both today and in the future in response to a positive technology shock. In the event that U t -E t U t+1 > 0, the wage moderating effect of an increase in the value of employment will be more than offset by the effect arising from the stronger bargaining position of the worker and the improvement in labor market conditions will put upward pressure on wages. When U t -E t U t+1 < 0, the inverse reasoning holds and the improvement in labor market conditions depresses wages.

In recent years, a large literature has incorporated the search and matching theory of unemployment in dynamic stochastic general equilibrium models (DSGE) to study, among others things, the impact of fiscal and monetary policies on the labor market and the joint dynamics of inflation and unemployment. As pointed out in the introduction, when wages are Nash-bargained, these models embedding a search structure are unable to account for the volatility of labor market variables observed in U.S. data. Several fixes, including wage rigidity, have been proposed to solve this problem. Because of its micro-founded nature and its ability to generate wage rigidity endogenously, the credible bargaining model of wage-setting is becoming increasingly popular in the literature. However, in the standard setup proposed by [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF], an analytical expression for wages cannot be derived. This has an undesirable consequence; when this model of wage-setting is used, it is generally impossible to find analytical and easily interpretable results. Some authors have circumvented this problem by using simple ad-hoc wage equations which preserve the main feature of the setup, that is, the partial isolation of wages from labor market conditions. In Jung and Kuester (2011), wages are a weighted average of the technological level and the fixed outside option of workers during bargaining and are fully insulated from labor market conditions. We nest their specification when δ = s = 0 and β = 1. Hall (2014) justifies the introduction of a parameter that controls the role of labor market tightness in the Nash-bargained wage equation by invoking the logic of the alternating-offer bargaining game. Although his equation cannot be formally derived from a bargaining game, a low value for this parameter corresponds to a low value for the probability of breakdown in the credible bargaining model. We believe our wage solution could permit a wider use of the credible bargaining framework in these dynamic models. In equation [START_REF] Pissarides | Equilibrium unemployment theory[END_REF], the expression is both micro-founded and simple to use, and the driving forces of wages are transparent. We argue that since knowledge about the values of the probability of breakdown in bargaining δ and the employer's cost of delay γ is limited, fixing one of these parameters and letting the other vary to match key labor market moments is equivalent. We fix δ = s and let γ vary to obtain the advantage of the analytical solution. This strategy has an unanticipated side benefit. In the appendix, we show that when calibrating the model to standard values and matching the standard deviation of the component of unemployment driven by productivity as in [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF], we obtain a short-run elasticity of wages with respect to labor productivity of about 0.8, in line with empirical estimates reported in [START_REF] Haefke | Wage rigidity and job creation[END_REF]. 3This is because the U t -E t U t+1 term reacts in a pro-cyclical way to technology shocks. Thus, on top of its simplicity, our wage equation is consistent with important labor market facts.

Conclusion

We derive a reduced form wage equation from an alternating-offer wage bargaining game la [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF] under a plausible parameter restriction. Our simple equation connects wages to outside labor market conditions through the difference between the current and the future values of unemployment. It can easily be used in studies wishing to obtain analytical results, permits a transparent analysis of the driving forces of wages, and is consistent with key labor market facts A Derivations of ( 9), [START_REF] Pissarides | Equilibrium unemployment theory[END_REF] and [START_REF] Shimer | The cyclical behavior of equilibrium unemployment and vacancies[END_REF] The subgame perfect equilibrium of the sequential game satisfies:

W w t = bτ + e -rτ
W w t = w t + e -r [(1 -s)E t W t+1 + sE t U t+1 ] (14)
J w t = z t -w t + e -r (1 -s)E t J t+1 (15)
J w t = z t -w t + e -r (1 -s)E t J t+1 (16)
because V t = V t+1 = 0. Plugging ( 14) and ( 15) in (12) leads to:

w t + 1 -e -(r+δ)τ e -r [(1 -s)E t W t+1 + sE t U t+1 ] = bτ + e -rτ 1 -e -δτ U t + e -(r+δ)τ w t
Likewise, integrating equations ( 16) and (17) in equation ( 13) gives:

w t = γτ + 1 -e -(r+δ)τ z t + 1 -e -(r+δ)τ e -r (1 -s)E t J t+1 + e -(r+δ)τ w t
Combining the two equations above and letting τ → 0, we find:

2w t + e -r [(1 -s)E t W t+1 + sE t U t+1 ] = b + γ r + δ + δU t r + δ + z t + e -r (1 -s)E t J t+1
because, when τ → 0, e -aτ = 1-aτ with a a constant. Noting that W w t = W t and J w t = J t , we get:

W t - b r + δ - δU t r + δ = J t + γ r + δ (18)
Introducing the expressions of W t and J t in (18) leads to:

2w t + β(1 -s) [E t W t+1 -E t J t+1 ] = z t + b + γ r + δ + δU t r + δ -βsE t U t+1
since e -r ≈ β = 1 1+r . Using the sharing rule, we obtain:

E t W t+1 -E t J t+1 = δE t U t+1 r + δ + b + γ r + δ
Using the above equation and (18), we have:

2w t = z t + [1 -β(1 -s)] (b + γ) (r + δ) - δU t r + δ -βs + β(1 -s)δ r + δ E t U t+1
that is:

w t = z t 2 + (r + s)(b + γ) 2(r + δ)(1 + r) - δU t 2(r + δ) - (sr + δ)E t U t+1 2(r + δ)(1 + r) If δ = s then: w t = 1 2 z + β(b + γ) + δ (U t -E t U t+1 ) r + δ
Last, at steady state, E t U t+1 = U t = U implying that:

w = 1 2 [z + β(b + γ)]

B Calibration exercise

We calibrate the model in a conventional manner. We take one period to be a month. The discount factor is set to β = 0.99, which yields an interest rate of 4% annually. The elasticity of matches with respect to unemployment is assumed to be α = 0.5, in line with estimates in Petrongolo and Pissarides (2000). Following [START_REF] Shimer | The cyclical behavior of equilibrium unemployment and vacancies[END_REF], the separation rate is set to 0.034 and the steady-state job finding rate to 0.45. Given a steady-state labor market tightness of 0.7, matching efficiency µ is then determined through steady-state relationships. We set the flow value of unemployment to 0.71 and choose the employer's cost of delay γ to match a standard deviation of the component of unemployment driven by productivity of 0.68 percentage points, following [START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF]. Vacancy posting costs c are then determined through steady-state relationships. Finally, we use standard values for the autoregressive parameter and the standard deviation of the technology shock, ρ = 0.95 1/3 and σ z = 0.0075. Figure 1 presents the impulse response functions of selected variables to a positive technology shock. The short-run elasticity of wages with respect to labor productivity is computed in each period by using the following formula ε w,z t = w t -w w z t -z z with w and z being the steady-state values of wages and technology. It is approximately equal to 0.84 from period 1 to period 30.

  Unlike Hall and Milgrom (2008), we choose δ = s and propose to fix γ to match the volatility of the unemployment rate. This calibration strategy has the advantage of enabling us to derive a simple analytical expression for the wage. It also represents an intermediate choice in the literature.[START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF] obtain a probability of breakdown that is five times as high as the separation rate whereas Christiano et al. (2013) estimate a medium-scale dynamic stochastic general equilibrium model encompassing an alternating-offer model of wage-setting on U.S. data and find a value of the probability of breakdown that is lower than the separation rate.

  1 -e -δτ U t + e -δτ W w = w t + e -r [(1 -s)E t W t+1 + sE t U t+1 ]

	t	(12)
	and
	J w t = -γτ + e -(r+δ)τ J w t	(13)
	with
	W w t

We follow strictly[START_REF] Hall | The limited influence of unemployment on the wage bargain[END_REF] when defining the equations governing the game.

See Appendix A.

See Appendix B.


Axel Legay
email: axel.legay@inria.fr

Sean Sedwards
email: sean.sedwards@inria.fr

On Statistical Model Checking with PLASMA

Keywords: Probability, Simulation, Statistical Model Checking, Experiments

This paper surveys the main functionalities of the PLASMA statistical model checking platform developed at Inria.

I. CONTEXT

Quantitative properties of stochastic systems are usually specified in logics that allow one to compare the measure of executions satisfying certain temporal properties with thresholds. The model checking problem for stochastic systems with respect to such logics is typically solved by a numerical approach [START_REF] Baier | Model-checking algorithms for continuous-time markov chains[END_REF], [START_REF] Ciesinski | On probabilistic computation tree logic[END_REF] that iteratively computes (or approximates) the exact measure of paths satisfying relevant subformulas; the algorithms themselves depend on the class of systems being analysed as well as the logic used for specifying the properties.

Another approach to solve the model checking problem is to simulate the system for finitely many runs, and use hypothesis testing to infer whether the samples provide statistical evidence for the satisfaction or violation of the specification [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF]. This approach is known as statistical model checking (SMC) and is based on the notion that since sample runs of a stochastic system are drawn according to the distribution defined by the system, they can be used to obtain estimates of the probability measure on executions. Starting from time-bounded PCTL properties [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], the technique has been extended to handle properties with unbounded until operators [START_REF] Sen | On statistical model checking of stochastic systems[END_REF], as well as to black-box systems [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF], [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF]. Tools, based on this idea have been built [START_REF] Jegourel | A Platform for High Performance Statistical Model Checking -PLASMA[END_REF], [START_REF] Sen | Vesta: A statistical model-checker and analyzer for probabilistic systems[END_REF], [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], and have been used to analyse many systems that are intractable numerical approaches.

The SMC approach enjoys many advantages. First, the algorithms require only that the system be simulatable (or rather, sample executions be drawn according to the measure space defined by the system). Thus, it can be applied to larger class of systems than numerical model checking algorithms, including black-box systems and infinite state systems. In particular, SMC avoids the 'state explosion problem' [START_REF] Clarke | Model checking: algorithmic verification and debugging[END_REF]. Second the approach can be generalized to a larger class of properties, including Fourier transform based logics. Third, SMC requires many independent simulation runs, making it easy to parallelise and scale to industrialsized systems.

While it offers solutions to some intractable numerical model checking problems, SMC also introduces some additional problems. First, SMC only provides probabilistic guarantees about the correctness of the results. Second, the required sample size grows quadratically with respect to the required confidence of the result. This makes rare properties difficult to verify. Third, only the simulation of purely probabilistic systems is well defined. Nondeterministic systems, which are common in the field of formal verification, are especially challenging for SMC.

In this invited talk, we will overview and compare some of the existing statistical model checking algorithms. We will then present PLASMA, a modular statistical model checker being developed at Inria, which addresses the problems of rare events and nondeterminism described above. Finally, some experiments will conclude the paper.

II. ON STATISTICAL MODEL CHECKING

Consider a stochastic system S and a logical property ϕ that can be checked on finite executions of the system. Statistical Model Checking (SMC) refers to a series of simulation-based techniques that can be used to answer two questions: (1) Qualitative: Is the probability for S to satisfy ϕ greater or equal to a certain threshold? and (2) Quantitative: What is the probability for S to satisfy ϕ? In contrast to numerical approaches, the answer is given up to some correctness precision.

In the sequel, we overview two SMC techniques. Let B i be a discrete random variable with a Bernoulli distribution of parameter p. Such a variable can only take 2 values 0 and 1 with P r[B i = 1] = p and P r[B i = 0] = 1 -p. In our context, each variable B i is associated with one simulation of the system. The outcome for B i , denoted b i , is 1 if the simulation satisfies ϕ and 0 otherwise.

Qualitative Answer: The main approaches [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], [START_REF] Sen | Statistical model checking of black-box probabilistic systems[END_REF] proposed to answer the qualitative question are based on sequential hypothesis testing [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF]. Let p = P r(ϕ). To determine whether p ≥ θ, we can test H : p ≥ θ against K : p < θ. A test-based solution does not guarantee a correct result but it is possible to bound the probability of error. The strength of a test is determined by two parameters, α and β, such that the probability of accepting K (respectively, H) when H (respectively, K) holds, called a Type-I error (respectively, a Type-II error ) is less or equal to α (respectively, β). A test has ideal performance if the probability of the Type-I error (respectively, Type-II error) is exactly α (respectively, β). However, these requirements make it impossible to ensure a low probability for both types of errors simultaneously (see [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF], [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] for details). A solution is to use an indifference region [p 1 , p 0 ] (given some δ, p 1 = θ -δ and p 0 = θ +δ) and to test H 0 : p ≥ p 0 against H 1 : p ≤ p 1 . We now sketch the Sequential Probability Ratio Test (SPRT). In this algorithm, one has to choose two values A and B (A > B) that ensure that the strength of the test is respected. Let m be the number of observations that have been made so far. The test is based on the following quotient:

p 1m p 0m = m ∏ i=1 P r(B i = b i | p = p 1 ) P r(B i = b i | p = p 0 ) = p dm 1 (1 -p 1 ) m-dm p dm 0 (1 -p 0 ) m-dm
,

where d m = ∑ m i=1 b i . The idea is to accept H 0 if p1m p0m ≥ A, and H 1 if p1m p0m ≤ B.
The algorithm computes p1m p0m for successive values of m until either H 0 or H 1 is satisfied. This has the advantage of minimizing the number of simulations required to make the decision.

Quantitative Answer: In [START_REF] Hérault | Approximate probabilistic model checking[END_REF] Peyronnet et al. propose an estimation procedure to compute the probability p for S to satisfy ϕ. Given a precision δ, the Chernoff bound of [START_REF] Okamoto | Some inequalities relating to the partial sum of binomial probabilities[END_REF] is used to compute a value for p such that |p -p|≤δ with confidence 1 -α. Let B 1 . . . B m be m Bernoulli random variables with parameter p, associated to m simulations of the system considering ϕ. Let p = ∑ m i=1 b i /m, then the Chernoff bound [START_REF] Okamoto | Some inequalities relating to the partial sum of binomial probabilities[END_REF] gives P r(|p -p| ≥ δ) ≤ 2e -2mδ 2 . As a consequence, if we take m = ln(2/α)/(2δ 2 ) , then P r(|p -p|≤δ) ≥ 1 -α.

A. Rare Events

Statistical model checking avoids the exponential growth of states associated with probabilistic model checking by estimating probabilities from multiple executions of a system and by giving results within confidence bounds. Rare properties are often important but pose a particular challenge for simulation-based approaches, hence a key objective for SMC is to reduce the number and length of simulations necessary to produce a result with a given level of confidence. In the literature, one finds two techniques to cope with rare events: importance sampling and importance splitting.

In order to minimize the number of simulations, importance sampling works by estimating a probability using weighted simulations that favour the rare property, then compensating for the weights. For importance sampling to be efficient, it is thus crucial to find good importance sampling distributions without considering the entire state space. In [START_REF] Jegourel | Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking[END_REF], we presented a simple algorithm that uses the notion of cross-entropy minimisation to find an optimal importance sampling distribution. In contrast to previous work, our algorithm uses a naturally defined low dimensional vector of parameters to specify this distribution and thus avoids the intractable explicit representation of a transition matrix. We show that our parametrisation leads to a unique optimum and can produce many orders of magnitude improvement in simulation efficiency (See Section IV-D).

One of the open challenges with importance sampling is that the variance of the estimator cannot be usefully bounded with only the knowledge gained from simulation. Importance splitting achieves this objective by estimating a sequence of conditional probabilities, whose product is the required result. In [START_REF] Jegourel | Importance splitting for statistical model checking rare properties[END_REF] we motivated the use of importance splitting for statistical model checking and were the first to link this standard variance reduction technique [START_REF] Kahn | Methods of Reducing Sample Size in Monte Carlo Computations[END_REF] with temporal logical. In particular, we showed how to create score functions based on logical properties, and thus define a set of levels that delimit the conditional probabilities. In [START_REF] Jegourel | Importance splitting for statistical model checking rare properties[END_REF] we also described the necessary and desirable properties of score functions and levels, and gave two importance splitting algorithms: one that uses fixed levels and one that discovers optimal levels adaptively.

B. Nondeterminism

Markov decision processes (MDP) and other nondeterministic models interleave nondeterministic actions and probabilistic transitions, possibly with rewards or costs assigned to the actions [START_REF] Bellman | Dynamic Programming[END_REF], [START_REF] Puterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF]. These models have proved useful in many real optimisation problems (see [START_REF] White | Real applications of Markov decision processes[END_REF], [START_REF] White | Further real applications of Markov decision processes[END_REF], [START_REF] White | A survey of applications of Markov decision processes[END_REF] for a survey of applications of MDPs) and are also used in a more abstract sense to represent concurrent probabilistic systems (e.g., [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF]). Such systems comprise probabilistic subsystems whose transitions depend on the states of the other subsystems, while the order in which concurrently enabled transitions execute is nondeterministic. This order may radically affect the expected reward or the probability that a system will satisfy a given property. Numerical model checking may be used to calculate the upper and lower bounds of these quantities, but a simulation semantics is not immediate for nondeterministic systems and SMC is therefore challenging.

SMC cannot be applied to nondeterministic systems without first resolving the nondeterminism using a scheduler (alternatively a strategy or a policy). Since nondeterministic and probabilistic choices are interleaved, schedulers are typically of the same order of complexity as the system as a whole and may be infinite.

In [START_REF] Legay | Lightweight Monte Carlo verification of Markov decision processes[END_REF] we presented the basis of the first lightweight SMC algorithms for MDPs and other nondeterministic models, using an O(1) representation of history-dependent schedulers. Our solution is based on pseudo-random number generators and an efficient hash function, allowing schedulers to be sampled using Monte Carlo techniques. Previous attempts to apply SMC to nondeterministic models [START_REF] Bogdoll | Partial order methods for statistical model checking and simulation[END_REF], [START_REF] Lassaigne | Approximate planning and verification for large Markov decision processes[END_REF], [START_REF] Henriques | Statistical model checking for Markov decision processes[END_REF], [START_REF] Hartmanns | On-the-fly confluence detection for statistical model checking[END_REF] have been memory-intensive (heavyweight) and incomplete in various ways. The algorithms of [START_REF] Bogdoll | Partial order methods for statistical model checking and simulation[END_REF], [START_REF] Hartmanns | On-the-fly confluence detection for statistical model checking[END_REF] consider only systems with 'spurious' nondeterminism that does not actually affect the probability of a property. In [START_REF] Lassaigne | Approximate planning and verification for large Markov decision processes[END_REF] the authors consider only memoryless schedulers and do not consider the standard notion of optimality used in model checking (i.e., with respect to probability). The algorithm of [START_REF] Henriques | Statistical model checking for Markov decision processes[END_REF] addresses a standard qualitative probabilistic model checking problem, but is limited to memoryless schedulers that must fit into memory and does not in general converge to the optimal scheduler. III. THE PLASMA STATISTICAL MODEL CHECKER PLASMA [24] is an efficient self-contained SMC tool and software library [START_REF] Boyer | PLASMAlab: A flexible, distributable statistical model checking library[END_REF] written in Java. PLASMA features a customisable simulator class that allows SMC functionality to be added to existing domain-specific modelling platforms, such as DESYRE 1 , and allows rapid prototyping of formal verification solutions using, e.g., Scilab 2 , MATLAB and SIMULINK 3 . High performance standalone model checkers can also be constructed with PLASMA by including a suitable language parser in the simulator class. PLASMA's integrated development environment (IDE) provides the reactive modules modelling language as standard and facilitates distributed simulation. Importantly, PLASMA can work with multiple user-defined language plug-ins, which can take advantage of all the IDE's features. In contrast, other dedicated SMC tools, such as YMER 4 , VESPA, APMC 5 and COSMOS 6 each use a single modelling language. The tool MRMC 7 has both numerical and statistical functionality, but takes as input an explicit textual description of a Markov chain and maintains it in memory. This approach makes MRMC impractical as an SMC tool. Other numerical model checking tools that have added SMC functionality, such as PRISM 8 and UPPAAL 9 , are nevertheless limited to their own modelling language, albeit that these languages may encompass different semantics (e.g., [START_REF] David | Runtime verification of biological systems[END_REF], [START_REF] David | Statistical model checking for stochastic hybrid systems[END_REF]).

A. Properties

PLASMA accepts properties described in a form of bounded linear temporal logic (BLTL) extended with custom temporal operators based on concepts such as minimum, maximum and mean of a variable over time.

B. Model Checking Modes

PLASMA offers three basic modes of model checking: simple Monte Carlo, Monte Carlo using a Chernoff confidence bound and sequential hypothesis testing. There is also a simulation mode for debugging. Rare event model checking modes, such as importance sampling and importance splitting, can be implemented as part of the simulator class when the modelling semantics support them. [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF] to verify that the probability of a property is above a user-specified threshold. The user also specifies a level of indifference and parameters to control errors of Types I and II. The number of simulations is not specified a priori: simulations are performed as necessary. See [START_REF] Wald | Sequential tests of statistical hypotheses[END_REF], [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF] for details.

C. Graphical User Interface

The GUI provides an integrated development environment (IDE) to facilitate the use of PLASMA as a standalone statistical model checker with multiple 'drop-in' modelling languages. To demonstrate this, we have included a biochemical language and a language based on reactive modules. The website [24] includes other examples. The GUI implements the notion of a project file, that links the description of a model to a specific modelling language simulator and a set of associated properties and experiments. The GUI also provides 2D and 3D graphical output of results and implements a distributed algorithm that will work with any of its associated modelling languages.

D. Usage

PLASMA is usually invoked via its GUI. It may also be invoked from the command line or embedded in other software as a library. In addition to the GUI, PLASMA provides an SMC engine in the form of a pre-compiled jar file. A source template is also provided to create custom simulator classes. The minimum requirement to create a custom simulator is to implement methods that (i) initiate a new simulation and (ii) advance the simulation by one step. Dedicated language parsers are typically invoked in the constructor of the custom simulator class.

E. Distributed SMC

The administrative time needed to distribute SMC on parallel computing architectures is often a deterrent. To overcome this, the PLASMA GUI implements a simple and robust client-server architecture. The algorithm will work on dedicated clusters and grids, but can also take advantage of ad hoc networks of heterogeneous computers. The minimum requirement is that the IP address of the GUI is available to the clients. PLASMA implements the SMC distribution algorithm of [START_REF] Younes | Verification and Planning for Stochastic Processes with Asynchronous Events[END_REF], which avoids the statistical bias that might otherwise occur from load balancing. The typical "divide by number of clients" distributed performance is illustrated in Fig. 1.

The user selects the distributed mode via the GUI and publishes the IP address of the instance of PLASMA GUI that is acting as server. Clients (instances of the PLASMA service application) willing to participate respond by sending a message to the published IP address. The server sends an encapsulated version of the model and property to each of the participating clients, which then wait to be told how many simulations to perform. When sufficient clients are available, the user initiates the analysis by causing the server to broadcast the simulation requirements to each client.

IV. OVERVIEW OF RESULTS

PLASMA has state of the art performance, based on efficient simulation and optimised logic parsing. Figure 2 illustrates its performance in comparison that of a numerical approach. Checking a standard fairness property of increasing instance sizes of the probabilistic dining philosophers protocol [START_REF] Pnueli | Verification of multiprocess probabilistic protocols[END_REF], the figure illustrates how numerical model checking scales exponentially (with number of states) while PLASMA scales linearly (with length of property). While "toy" examples are often efficient with numerical model checking, "industrial scale" problems require SMC.

PLASMA has been applied to problems from, e.g., systems biology, rare events, performance, reliability, motion planning and systems of systems [24]. PLASMA is the focus of ongoing collaborations with companies Dassault, Thales, IBM, and EADS. PLASMA is also used by several European projects. In particular, sections IV-A and IV-B relate to the DALi10 and DANSE 11

A. Motion Planning

PLASMA is used by the DALi project in a novel motion planning application of SMC. DALi aims to develop an autonomous device to help those with impaired ability to negotiate complex crowded environments (e.g. shopping malls). High level constraints and the objectives of the user are expressed in temporal logic, while low level behaviour is predicted by the 'social force model' [START_REF] Helbing | Social force model for pedestrian dynamics[END_REF]. The planner first hypothesises many plausible futures for a range of possible user actions, then chooses the action which maximises the probability of success.

PLASMA was integrated with MATLAB to develop the prototype algorithm. The final version is implemented directly in C on embedded hardware and finds the optimum trajectory in a fraction of a second [START_REF] Colombo | Motion planning in crowds using statistical model checking to enhance the social model[END_REF]. PLASMA improves the social force model's ability to avoid collisions by a factor of five [START_REF] Colombo | Motion planning in crowds using statistical model checking to enhance the social model[END_REF]. Using behavioural templates [START_REF] Colombo | Behavioural templates improve robot motion planning with social force model in human environments[END_REF], the predictive power of our SMC-based motion planner can be even greater.

B. Systems of Systems

The DANSE project is concerned with the design and analysis of 'systems of systems' (SoS). SoS feature a dynamicity of configurations that introduces significant additional complexity (the state space of the model is not necessarily definable a priori). PLASMA is now an integral part of the DANSE software platform, using a custom simulator class that wraps the DESYRE 12 hybrid simulation engine to make dynamicity transparent to SMC.

C. Markov Decision Processes

We have recently developed an efficient way to represent and sample general schedulers, which thus facilitates lightweight SMC algorithms for nondeterministic systems [START_REF] Legay | Lightweight Monte Carlo verification of Markov decision processes[END_REF]. Figure 4 illustrates the results of sampling just 4000 schedulers per data point, to find the maximum probability of a second data "collision" on the shared communication channel of the WLAN protocol model of [START_REF] Kwiatkowska | Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol[END_REF]. Maximum and minimum estimated probabilities are denoted by blue and red circles, with the correct values denoted by black crosses. The shaded areas indicate the ±δ error of the estimates (using the Chernoff bound for multiple schedulers [START_REF] Legay | Lightweight Monte Carlo verification of Markov decision processes[END_REF]) and reveal that our estimates are very close to the true values.

Our ongoing focus in this cutting-edge field is the development of lightweight learning algorithms and "smart sampling" to improve scalability.

D. Parametrised Cross-Entropy Minimisation

Rare events pose a challenge for SMC because it is necessary to consider error bounds (±δ) that are relative to the estimate, such that the number of simulations required for a given confidence scales quadratically with rarity. Importance sampling is a standard technique to overcome this problem [START_REF] Kahn | Methods of Reducing Sample Size in Monte Carlo Computations[END_REF], but previous algorithms to find good importance sampling distributions do not scale, because they are parametrised at the level of individual transition probabilities [START_REF] Ridder | Importance sampling simulations of markovian reliability systems using cross-entropy[END_REF]. Our cross-entropy (C-E) minimisation algorithm achieves impressive results, but uses a natural and convenient parametrisation at the level of the syntactical description of the system.

We illustrate our algorithm with a chemically reactive system. The stochastic model is based on the following set of chemical reactions, parametrised by rates λ 1 , λ 2 and λ 3 :

A + B λ1 → C C λ2 → D D λ3 → E
With initial numbers of molecules A = B = 1000 and C = D = E = 0, the system has approximately 1.6 × 10 8 states. Figure 5 illustrates the results of 40 iterations of our C-E algorithm, considering the property P r(♦D ≥ 470). For each iteration, the blue line gives the estimated probability, while the red line gives the variance of the estimator. For rare properties, variance ≈ probability, hence the horizontal grey lines (the mean of the last ten respective data points) indicate that the overall variance reduction is ≈ 10 7 , at a total cost of only 4 × 10 5 simulations.

V. CONCLUSION

This paper briefly summarises the main functionalities of PLASMA. Our ongoing work concerns the development of (i) algorithms to estimate unbounded properties with finite traces, (ii) lightweight learning algorithms for nondeterministic systems and (iii) techniques to provide confidence bounds for rare properties.

Figure 1 .

 1 Figure 1. Scaling of PLASMA distributed algorithm applied to dining philosophers. Numbers are quantity of simulation nodes. Local simulation scaling is shown for reference.

Figure 3 .

 3 Figure 3. Control loop of DALi motion planner.

Figure 4 .

 4 Figure 4. Max. and min. probabilities of second collision in WLAN protocol of [20].

Figure 5 .

 5 Figure 5.Convergence of parametrised C-E minimisation algorithm applied to chemical system.

  Monte Carlo: the user explicitly specifies the number of simulations that PLASMA must use to estimate the probability of a property.• Chernoff: the user specifies an absolute error δ and a probability α. PLASMA calculates the number of simulations required to ensure that the resulting estimate is within ±δ of the correct value with minimum probability 1 -α.

			• Sequential: PLASMA adopts the sequential hypothesis
			ratio test of
	1 www.ales.eu.com	2 www.scilab.org	3 www.mathworks.com
	4 www.tempastic.org/ymer	5 sylvain.berbiqui.org/apmc
	6 www.lsv.ens-cachan.fr/˜barbot/cosmos/	7 www.mrmc-tool.org
	8 www.prismmodelchecker.org 9 www.uppaal.org

•

  projects, respectively.

	Overall execution time (seconds)	10 100 1000			numerical (PRISM) PLASMA
		1
		3	10		30	100	300
			Size of model (philosophers)
	Figure 2. Exponential scaling of numerical model checking vs. linear scal-
	ing of PLASMA SMC, considering a fairness property of the probabilistic
	dining philosophers protocol.
		Motion Planner Board		Sensor Board
		Social Force Model	current state	Sensor Processing
			plausible paths
			PLASMA
		SMC Engine
						Sensors
		Global Objectives	Suggested Motion	actual moon

www.ict-dali.eu

www.danse-ip.eu