J Cambon

F Guarnieri
email: franck.guarnieri@ensmp.fr

J Groeneweg
email: jop.groeneweg@fsw.leidenuniv.nl

Towards a new tool for measuring Safety Management Systems performance

This paper deals with the assessment of Safety Management Systems performance and presents a new tool developed for that purpose. It recognizes two dimensions in a SMS: a structural facet corresponding to the formal description of the system and an operational one focused on the system's influence on the working environment and practices of people. Building up the operational performance of a SMS actually strengthens the overall resilience of the organization. Authors of the paper believes that the operational performance of SMS can be measured using Tripod Delta. This method is actually designed to detect weak areas in the environment in which people are working and the level of control that the organization has on it. The method and its interesting model of organizational resilience are presented in the paper. In the framework of this paper, Tripod is used as an input to measure the SMS operational performance. Both of the tools designed to measure the structural and operational performances of Safety Management Systems are then described.

PERFORMANCE OF SAFETY MANAGEMENT SYSTEMS

Many companies are implementing a Safety Management System in order to manage health and safety in the workplace in a more coherent and more effective way. This "emerging" mode of managing safety mainly comes from the growing need for a global and structured approach of risk management. Despite the several benefits of its implementation, experience show that companies sometimes fail to implement an effective SMS. As shown by Favaro [START_REF] Favaro | Mettre en gestion la santé-sécurité. Enjeux, difficultés et pistes d'action[END_REF] and Drais [START_REF] Drais | Management de la sécurité. L'usage des référentiels. Résultats d'une étude nationale[END_REF], if special care is not taken when SMS is designed and formalized, the system can end up being quite superficial, disconnected from real work situations, be poorly dynamic and can also introduce additional constraints for workers or rigidity in the way the safety is managed in the company. In other words, the system is more likely to go against workers if the inherent prescriptive and normative tendencies of the SMS are not well managed when the system is designed and implemented.

Avoiding such shortcomings in the system inevitably includes the acknowledgement of two dimensions in the Safety Management System: a 'structural' dimension and an 'operational' dimension.

The 'structural' and 'operational' dimensions of a SMS

The 'structural' facet of the SMS can be defined as the formal description of all the efforts that are made by the company into managing health and safety at the workplace. These efforts can be categorized into several Safety Management Processes (i.e. sec-tions or chapters in safety management standards) such as the definition of an Occupational Health and Safety (OH&S) policy, an OH&S program, implementation of a communication or documentation system, hazard identification, etc. Each of these Safety Management Processes (SMPs) implies policies, rules, procedures, guidelines, working instructions, techniques or methods, etc. that the company has internally established to manage safety. These rules, procedures, techniques, etc. are the formal answers to the good practices (and legal requirements) emanating from safety management standards, from the company standards, from the branch specifications, etc. This prescribed system gives an image of how the safety management system works on "paper".

However, things can be perfectly organized on paper, but can not work in "real life". It seems then necessary to analyze how things are done in addition to how things are formalized. This aspect refers to the 'operational' facet of Safety Management Systems. Alongside their formal description, the efforts made by the company in the safety management need to be implemented and integrated throughout the company until the 'sharp end'. The way these efforts or actions are integrated within the practices of the company and its members is of concern here. This time, the scope of analysis concerns the influence of the efforts that the company has put into managing safety of peoples' activities at the workplace. It is considered that a SMS is actually 'operationally' working if the different SMPs are integrated within the practices and if they positively influence the working conditions of people. The operational facet of a SMS is of course the most important one in terms of safety. One can agree that safety practices shared by everybody in the company, well integrated within the practices and influencing positively the working environment have a higher impact on the overall safety state of a company than a well-formalized, well-structured or well-described management system.

With respect to these two dimensions, the global performance of a Safety Management System can be assessed according to its structural and an operational performance (Figure 1). Structural performance can be defined as the level of compliance of the internal processes (SMPs) as established by the company (under the forms of procedures, instructions, policies, techniques, tools, etc.) with the existing safety management standards. This performance, generally aimed at the accreditation of the SMS put into place by the company, is measured with structural indicators (e.g. has the company established a procedure regarding its training program? is the procedure updated? validated?). Operational performance can be described as the level of integration and of influence of these formal processes on the practices and the working environment of people. Examples of operational performance indicators could be: Do the personnel feel that they are correctly trained? Are trainings adapted to the level or the job of people? Are the personnel able to put in practice the theoretical courses? Are there sufficiently trained and qualified people in each team? Etc.

Operational performance is then more focused on what the management system does rather than on what it has (this matter is tackled in the structural performance) and is clearly considered as the intrinsic value of a safety management system. Building up the operational performance of a management system strengthens the overall resilience of the organization.

Main approaches currently available for measuring SMS performance and the proposed approach to measure SMS performance

Three main approaches are currently available to measure performance of safety management systems: (i) the results-based approach, (ii) the compliance-based approach and (iii) the process-based approach.

The results-based approach consists of looking at safety results obtained by the company over the past years to assess if the safety management system put into place is effective or not (accident frequency rate, injuries, incidents, near-misses, occupational diseases, etc). This approach is widely used because it is easy to implement, not too time-or cost-consuming for managers and finally because it is requested by regulation. However, it does not assess the operational nor structural aspects of the SMS whatsoever. Discussing the many other issues involved in such a safety approach falls outside the scope of this paper but examples of such limits can be found in Booth [START_REF] Booth | Monitoring Health and Safety Performance -an Overview[END_REF], [START_REF] O'brien | Business measurements for safety performance[END_REF], [START_REF] Roy | Développements d'instrument de mesure de performance en santé et sécurité des entreprises manufacturières organisées en équipes semi autonomes de travail[END_REF]; Stricoff, [START_REF] Stricoff | Safety performance measurement: identifying prospective indicators with high validity[END_REF], [START_REF] Shaw | Measuring performance in OHS: using positive performance indicators[END_REF].

The compliance-based approach is the classical way of measuring effectiveness of SMS put into place. It consists in auditing the degree of compliance of the SMS with the existing safety management standards (e.g. OHSAS 18001, ILO-OSH 2001, etc). This approach is often appealing for many managers as it can easily give a "facade" of performance as well as a "recognized" performance (e.g. OHSAS accreditation). However SMS audits focus on the "structural" side of SMS, on the formal description of all the efforts that the company has put into managing safety. Despite some visits and inspections in the different work areas, the SMS audits do not fully address the way the system influences the working environment of people and the organizational conditions of work.

The process-based approach measures the performance of each management processes (SMP) that constitutes the SMS independently (policy, communication, safety program, hazard identification, legal requirements, etc) and gives the overall level of organization's effectiveness in safety management (e.g. International Safety Rating System (ISRS)). Through interviews with management or operational staff from the company, this approach intends to assess if the safety management system put into place is actually resilient, if this system is embraced within the organizational practices. The priority of the process-based approach is the "operational" performance of the SMS while documentary compliance as required by standards is put aside. This short review emphasizes the fact that the current approaches seem quite limited to measure both the structural and operational performance of SMS in a combined way.

With regard to the limits of the current approaches, a double approach is proposed to assess the global performance of safety management systems. The prescribed system (i.e. the structural performance) is proposed to be measured according to a documentary review of the system as it is carried out in the traditional compliance-based approach via safety management audits.

Measuring the operational performance of management systems is a bit more problematic and constitutes the central idea of this paper. Authors of this paper believe that this aspect of the SMS performance can be measured using the organizational factors engineering.

Indeed, many works and models have been developed over the past decades and have helped to enrich our capacity to analyse the influence of organization on the safety in the workplace. These models have led to the formalisation of several methods aimed at assessing organizational weaknesses of sociotechnical systems. In the context of assessing the gaps in between SMS rules and their operational implementation, it seems more than relevant to refer to these methods.

TRIPOD AS A META-INSTRUMENT TO ASSESS OPERATIONAL PERFORMANCE OF SMS

In order to choose the most relevant method for measuring the operational performance of SMS, different tools identified in the literature were compared with each other. A set of 21 methods dealing with organisational factors was initially identified. The next -and more challenging -step was to assess the relevance of each method with regard to measuring operational performance of SMS.

The comparison of each method was made using different criteria such as the accuracy and coverage of the model, the model of resilience proposed, the coverage of the tool with regard to the different processes in SMS, the level of expertise required, the ability of the method to take into account the specificities of the plant, the time or costconsuming requirements, the validation of the method, etc. From this review and taking into account the different criteria chosen, Tripod Delta has emerged as being the most appropriate method for measuring operational performance [START_REF] Cambon | Bringing Tripod Delta to France for the analysis of organizational factors[END_REF].

Tripod theory

The Tripod theory and methodology was developed at Leiden and Manchester Universities. It originated from a research program investigating ways of preventing human error initiated by the Dutch Royal/Shell Group in 1986. The project resulted in an instrument that is now widely applied [START_REF] Groeneweg | Tripod: Controlling the human error components in accidents[END_REF].

Tripod is based upon the principle that the most effective way to prevent human error is to control the working environment. It aims at analyzing and controlling the environ-mental conditions, the 'latent failures' [START_REF] Reason | Human error[END_REF]) that cause human error. Latent, because they are present a long time before a specific substandard act or an accident occurs and remain hidden without a specific local trigger. According to the Tripod philosophy, these latent failures can be categorized in a limited number of ways, the Basic Risk Factors (Table 1). The BRFs are the result of brainstorming, audit report studies, accident scenario inquiries and have shown through extensive field studies to be valid for all industrial applications [START_REF] Groeneweg | Controlling the controllable. Preventing business upsets[END_REF].

All of these BRFs can contribute to accidents in subtle ways, by allowing the development of undesirable combinations of situations and acts together (psychological precursors leading to one (or more) substandard act(s) and operational disturbance in the working environment), by increasing the chance that 'sharp end' individuals will commit substandard acts and by failing to provide the means to protect from accidents already in progress. Ten of these BRFs influence the process leading to the operational disturbances ('Prevention' BRFs) and one BRF is aimed at controlling the consequences once the operational disturbance has occurred (The BRF 'Defences'). This BRF is related to all the protective barriers put in place in the system. A more complete description of the propagation of the BRFs influences through the organizational system is given in Groeneweg [START_REF] Groeneweg | Controlling the controllable. Preventing business upsets[END_REF].

The concept of organizational resilience in Tripod theory

In Tripod theory, safety is defined as an equilibrium between substandard acts and compensating factors so that unwanted operational disturbances cannot occur. The metaphore of a marble on a rough plateau illustrates this equilibrium (Figure 2). When the marble stays on the plateau the situation is safe: this situation happens when there is no operational disturbance. If the marble starts to move and gets pushed either way over the edge of the plateau, an event will happen (an accident or an incident). The chance of having an incident is much higher than having an accident, but is not part of the present discussion.

This model, first introduced by Kletz [START_REF] Kletz | An engineer's view of human error[END_REF] and further developed by Groeneweg [START_REF] Groeneweg | Controlling the controllable. Preventing business upsets[END_REF] has a few axioms, such as (i) it is impossible to predict the direction of the marble (nobody can predict if something will become an accident or an incident), (ii) external forces influence the way the marble rolls (the model recognizes that the marble rolls according to operational disturbances coming from the working environment),(iii) the surface of the plateau is rough and allows small resistance against the movement of the marble, (iv) obstacles (ie. safety barriers) can be placed on the plateau to prevent the marble from dropping off (v) however these obstacles are not effective all the time, can be sometimes too weak or even missing, etc.

Fig. 2. A marble on a rough plateau

In this theory, the mechanism of a BRF is twofold: it generates substandard acts or situations (ie. it makes the marble roll) and it influences the resilience of the organization (i.e. it makes the plateau easier to drop from, the marble slides more easily). Influences of BRFs are shown in figure 3. According to Tripod theory, preventing individual substandard acts themselves, setting the right barriers at the right place are of course essential but hardly controllable. What is controllable on the other hand is the overall state of the organization, the shape of the plateau. The shape of the plateau symbolizes how resilient the organization is against operational disturbances.

Fig. 3. Influences of the Basic Risk Factors

In this model, resilient organizations are organizations able to self-recover after disturbances occur. Resilience is represented by a stable equilibrium (Figure 4a). After an operational disturbance, the marble has been put in motion but returns automatically to the initial, safe state. It does not mean that the situation is inherently absolutely safe as it is still possible for the marble to leave the plateau (in cases of extremely large external influences) as well as it is possible for 'good' companies to produce accidents. However, in this stable equilibrium, organizations can return to the initial and safe state. On the other hand, in non-resilient organizations, the initial safe state cannot be reached anymore. This equilibrium is this time unstable (Figure 4b). Here, the possibility of dropping the marble in one of the baskets is much greater after the marble was set in motion. The marble gains momentum after leaving the safe area and will not return to the initial state.

From the theory to the practice: mains principles of Tripod Delta Survey

Tripod theory and the safety equilibrium model have served as basic concepts for a methodological tool to measure the soundness of organizations in terms of safety. This tool is called the Tripod Delta Survey and is designed to detect weak areas in the environment in which people are working and the level of control that this organization has on processes. The survey uses questions to anonymously collect data relating to factual verifiable operational experiences. The questions are designed in such a way that they make it possible for the participants to establish a direct link between the question and their own knowledge or observation of the system and their actual practices within it (e.g. for BRF 'Procedures': During the past four weeks, did you have to work with procedures with conflicting information?). The questions have been gathered in a central question database (the "Delta Base") enclosing around 1,500 validated questions.

Tripod as an input for the measurement of operational performance of SMS

The capacity of Tripod to detect the consequences of Basic Risk Factors, i.e. weak areas in the working environment of people appears very relevant when measuring the operational performance of the SMS put in place by the company. As a matter of fact, the organizational weaknesses (or strengths) as observed and stressed by all the members of a company give a good picture of where the main operational weaknesses (or strengths) of its safety management system are. For instance, the Tripod question "Are the management's statements in line with their actions?" is a good indicator for measuring if the management is really involved and committed in its OH&S policy.

A tool was then designed on the basis of the assumption that the findings from a Tripod Delta Survey can be used as indicators of the operational performance of the company's SMS (Figure 5). The tool integrates 14 SMPs as the main components of the Safety Management System and interconnects them with the Tripod questions (categorized in 11 BRFs). For each of these SMPs, the Tripod questions considered as quite good, good or very good indicators were identified and selected from the Tripod Delta Base.

PRESENTATION OF THE TOOLS DEVELOPPED FOR MEASURING SAFETY MANAGEMENT SYSTEM PERFORMANCE

According to the two dimensions involved in the Safety Management System, two tools have been designed in order to measure its 'structural' and 'operational' performance.

Principles of the tools designed

The tool designed for measuring the 'structural' performance is based upon existing Safety Management standards (OHSAS 18001, ILO-OSH 2001 and MASE). It involves a checklist to help the auditor to assess through a documentary review and interviews if the structure of the SMS (procedures, policies, programs, etc) has been efficiently formalized by the company and if it complies with the standards requirements. The tool developed is based upon 230 'structural' indicators (Table 2 presents five of them). It can be used as an inventory assessment when the company is willing to build its own SMS (the tool gives an indication of what is done and what needs to be done in terms of structure) and can be used also as a diagnostic of the SMS before an audit of accreditation. This tool is currently being experimented on two French pilot plants. The tool designed for measuring the 'operational' performance uses Tripod as an input.

A Tripod Delta survey needs to be carried out in the company before its complete implementation (Figure 5). The tool assesses the influence of the SMS on the working environment and practices through the experience and observation of people. The tool developed is based upon 90 'operational' indicators. Each of these indicators refers to several Tripod questions. For example, in Table 3, the first 'operational indicator' related to the real involvement and commitment of the management in its OH&S policy can be assessed with 10 Tripod questions. This tool is currently in the experimentation stage in one French pilot plant (also pilot plant for Tripod Delta and for the implementation of the tool measuring the SMS structural performance). In practice, is the management really involved and committed into its OH&S policy? 2 Does the management give sufficient resources (financial, human and time) for the implementation and application of its OH&S policy? 3

Is this OH&S policy really known and understood by employees? …

Next stage: integrating the results

The two tools developed provide an assessment of the level of compliance of the company's SMS with the existing safety management standards as well as an assessment of its influence on the working environment and peoples' working practices. The results of these two assessments can be represented on the same graph as shown in Figure 6. The integration of results is possible as the same measurement criteria have been chosen for the two assessments (the overall SMS has been divided into 14 safety management processes (or sections)). The integration stage of the two assessments has not been reached yet as the two different tools are currently in the experimentation stage. The discontinuous line represents the structural performance of the virtual SMS put into place and the continuous line its operational performance.

The graph can be used as a support to analyze (i) the safety processes poorly formalized (e.g. processes n° 2.2 and 3.5), (ii) the safety processes with low effectiveness on people's working environment (e.g. processes n°1.1, 1.2 and 3.5) as well as (iii) the significant gaps between the system on 'paper' and the system's real influence on people's working environment (e.g. processes 5.1, 4.1, 3.4, 1.2).

Fig. 1 .

 1 Fig.1. Global performance of safety management systems

-

  Design (DE): ergonomically poor design of tools or equipment -Hardware (HW): poor quality, condition, suitability or availability of materials, tools and equipments -Maintenance (MM): no or inadequate performance of maintenance tasks and repairs, bad planning -Housekeeping (HK): no or insufficient attention given to keeping the work floor clean and tidied up -Error Enforcing Conditions (EC): unsuitable physical conditions (cold, heat, noise, darkness, etc ) or personal factors (motivation, boredom, stress, complacency, etc) influencing human functioning -Procedures (PR): insufficient quality or availability of procedures, manuals and written instructions -Training (TR): inadequate planning, ineffectiveness of trainings, insufficient competence or experience of personnel -Communication (CO): ineffective communication between sites, departments, individuals -Incompatible Goals (IG): unsuitable situations in which people must choose between optimal working methods on one hand and the pursuit of production, financial, social or individual goals on the other one -Organization (OR): shortcomings in the organizational structure, organization's philosophy, management strategies ____________________________________________________________________________________ 1 Mitigation BRF -Defences (DF): insufficient protection of people, material and environment against the consequences of operational disturbance ____________________________________________________________________________________

Fig. 5 .

 5 Fig. 5. Tripod as an input for the measurement of SMS operational performance

Fig 6 .

 6 Fig 6. Example of structural and operational performances of a Safety Management System

Table 1 .

 1 The eleven Basic Risk Factors in Tripod theory ____________________________________________________________________________________ 10 Prevention BRFs

  All together the Tripod Delta Base includes around 1,500 questions. Approximately 70% of them (i.e. 900 Tripod questions) are assessed as good or very good indicators for measuring the SMS operational performance. Some BRFs (such as BRF Training or Com-Consultation, communication, information of employees). Most of the BRFs cover several SMPs. For instance, the BRF 'Organization' provides good indicators for the SMP 'OH&S policy and commitment of management', 'OH&S objectives and management program', 'Role and responsibilities of employees', or 'Consultation, communication, information of employees'. The SMP 'Management of safety in activities', qualified by SMS auditors as being the most time-consuming and most difficult section to evaluate, is covered by more than 300 Tripod questions.

	munication) have a direct corresponding SMP (3.1 Training, competence and specific
	trainings, 3.2
				Operational
	Operational			disturbance
	disturbance
	Accident	Incident	Accident	Safety margin	Incident
	Fig. 4a. The stable equilibrium	Fig. 4b. The unstable equilibrium
	of resilient organizations	of non-resilient organizations

Table 2 .

 2 Example of structural indicators for the OH&S policy ( §4.

	2 in OHSAS 18001, §3.1 in ILO-

Table 3 .

 3 Example of operational indicators for the OH&S policy ( §4.2 in OHSAS 18001, §3.1 in ILO-OSH2001 OH&S Policy and commitment of management 1


F Herbreteau

D Kini

B Srivathsan

I Walukiewicz

Using non-convex approximations for efficient analysis of timed automata

The reachability problem for timed automata asks if there exists a path from an initial state to a target state. The standard solution to this problem involves computing the zone graph of the automaton, which in principle could be infinite. In order to make the graph finite, zones are approximated using an extrapolation operator. For reasons of efficiency in current algorithms extrapolation of a zone is always a zone; and in particular it is convex. In this paper, we propose to solve the reachability problem without such extrapolation operators. To ensure termination, we provide an efficient algorithm to check if a zone is included in the so called region closure of another. Although theoretically better, closure cannot be used in the standard algorithm since a closure of a zone may not be convex. An additional benefit of the proposed approach is that it permits to calculate approximating parameters on-the-fly during exploration of the zone graph, as opposed to the current methods which do it by a static analysis of the automaton prior to the exploration. This allows for further improvements in the algorithm. Promising experimental results are presented.

Introduction

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] are obtained from finite automata by adding clocks that can be reset and whose values can be compared with constants. The crucial property of timed automata is that their reachability problem is decidable: one can check if a given target state is reachable from the initial state. Reachability algorithms are at the core of verification tools like Uppaal [START_REF] Behrmann | UPPAAL 4.0[END_REF] or RED [START_REF] Wang | Efficient verification of timed automata with BDD-like data structures[END_REF], and are used in industrial case studies [START_REF] Havelund | Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL[END_REF][START_REF] Bérard | Analysing the PGM protocol with UPPAAL[END_REF]. The standard solution constructs a search tree whose nodes are approximations of zones. In this paper we give an efficient algorithm for checking if a zone is included in an approximation of another zone. This enables a reachability algorithm to work with search trees whose nodes are just unapproximated zones. This has numerous advantages: one can use nonconvex approximations, and one can compute approximating parameters on the fly.

The first solution to the reachability problem has used regions, which are equivalence classes of clock valuations. Subsequent research has shown that the region abstraction is very inefficient and an other method using zones instead of regions has been proposed. This can be implemented efficiently using DBMs [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF] and is used at present in almost all timed-verification tools. The number of reachable zones can be infinite, so one needs an abstraction operator to get a finite approximation. The simplest is to approximate a zone with the set of regions it intersects, the so called closure of a zone. Unfortunately, the closure may not always be convex and no efficient representation of closures is known. For this reason implementations use another convex approximation that is also based on (refined) regions.

We propose a new algorithm for the reachability problem using closures of zones. To this effect we provide an efficient algorithm for checking whether a zone is included in a closure of another zone. In consequence we can work with non-convex approximations without a need to store them explicitly.

Thresholds for approximations are very important for efficient implementation. Good thresholds give substantial gains in time and space. The simplest approach is to take as a threshold the maximal constant appearing in a transition of the automaton. A considerable gain in efficiency can be obtained by analyzing the graph of the automaton and calculating thresholds specific for each clock and state of the automaton [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF]. An even more efficient approach is the so called LU-approximation that distinguishes between upper and lower bounds [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]. This is the method used in the current implementation of UPPAAL. We show that we can accommodate closure on top of the LU-approximation at no extra cost.

Since our algorithm never stores approximations, we can compute thresholds on-the-fly. This means that our computation of thresholds does not take into account unreachable states. In consequence in some cases we get much better LU-thresholds than those obtained by static analysis. This happens in particular in a very common context of analysis of parallel compositions of timed automata.

Related work

The topic of this paper is approximation of zones and efficient handling of them. We show that it is possible to use non-convex approximations and that it can be done efficiently. In particular, we improve on state of the art approximations [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]. Every forward algorithm needs approximations, so our work can apply to tools like RED or UPPAAL.

Recent work [START_REF] Morbé | Fully symbolic model checking for timed automata[END_REF] reports on backward analysis approach using general linear constraints. This approach does not use approximations and relies on SMT solver to simplify the constraints. Comparing forward and backward methods would require a substantial test suite, and is not the subject of this paper.

Organization of the paper

The next section presents the basic notions and recalls some of their properties. Section 3 describes the new algorithm for efficient inclusion test between a zone and a closure of another zone. The algorithm constructing the search tree and calculating approximations on-the-fly is presented in Section 4. Some results obtained with a prototype implementation are presented in the last section. All missing proofs are presented in the full version of the paper [START_REF] Herbreteau | Using non-convex approximations for efficient analysis of timed automata[END_REF].

Preliminaries

2.1 Timed automata and the reachability problem Let X be a set of clocks, i.e., variables that range over R ≥0 , the set of nonnegative real numbers. A clock constraint is a conjunction of constraints x#c for x ∈ X, # ∈ {<, ≤, =, ≥, >} and c ∈ N, e.g. (x ≤ 3 ∧ y > 0). Let Φ(X) denote the set of clock constraints over clock variables X. A clock valuation over X is a function ν : X → R ≥0 . We denote R X ≥0 the set of clock valuations over X, and 0 the valuation that associates 0 to every clock in X. We write ν φ when ν satisfies φ ∈ Φ(X), i.e. when every constraint in φ holds after replacing every x by ν(x). For δ ∈ R ≥0 , let ν + δ be the valuation that associates ν(x) + δ to every clock x. For R ⊆ X, let [R]ν be the valuation that sets x to 0 if x ∈ R, and that sets x to ν(x) otherwise.

A Timed Automaton (TA) is a tuple A = (Q, q 0 , X, T, Acc) where Q is a finite set of states, q 0 ∈ Q is the initial state, X is a finite set of clocks, Acc ⊆ Q is a set of accepting states, and T ⊆ Q × Φ(X) × 2 X × Q is a finite set of transitions (q, g, R, q ) where g is a guard, and R is the set of clocks that are reset on the transition. An example of a TA is depicted in Figure 1. The class of TA we consider is commonly known as diagonal-free TA since clock comparisons like x -y ≤ 1 are disallowed. Notice that since we are interested in state reachability, considering timed automata without state invariants does not entail any loss of generality. Indeed, state invariants can be added to guards, then removed, while preserving state reachability.

A configuration of A is a pair (q, ν) ∈ Q × R X ≥0 ; (q 0 , 0) is the initial configuration. We write (q, ν) δ,t -→ (q , ν ) if there exists δ ∈ R ≥0 and a transition t = (q, g, R, q ) in A such that ν + δ g, and ν = [R]ν. Then (q , ν ) is called a successor of (q, ν). A run of A is a finite sequence of transitions:

(q 0 , ν 0 ) δ0,t0 ---→ (q 1 , ν 1 ) δ1,t1 ---→ • • • (q n ,
ν n ) starting from (q 0 , ν 0 ) = (q 0 , 0). A run is accepting if it ends in a configuration (q n , ν n ) with q n ∈ Acc. The reachability problem is to decide whether a given automaton has an accepting run. This problem is known to be Pspace-complete [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Courcoubetis | Minimum and maximum delay problems in real-time systems[END_REF].

Symbolic semantics for timed automata

The reachability problem is solved using so-called symbolic semantics. It considers sets of (uncountably many) valuations instead of valuations separately. A zone is a set of valuations defined by a conjunction of two kinds of constraints: comparison of difference between two clocks with an integer like x-y#c, or comparison of a single clock with an integer like x#c, where # ∈ {<, ≤, =, ≥, >} and c ∈ N. For instance (x -y ≥ 1) ∧ (y < 2) is a zone. The transition relation on valuations is transferred to zones as follows. We have (q, Z)

t - → (q , Z ) if Z is the set of valuations ν such that (q, ν) δ,t
-→ (q , ν ) for some ν ∈ Z and δ ∈ R ≥0 . The node (q , Z ) is called a successor of (q, Z). It can be checked that if Z is a zone, then Z is also a zone.

The zone graph of A, denoted ZG(A), has nodes of the form (q, Z) with initial node (q 0 , {0}), and edges defined as above. Immediately from the definition of ZG(A) we infer that A has an accepting run iff there is a node (q, Z) reachable in ZG(A) with q ∈ Acc. Now, every node (q, Z) has finitely many successors: at most one successor of (q, Z) per transition in A. Still a reachability algorithm may not terminate as the number of reachable nodes in ZG(A) may not be finite [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF]. The next step is thus to define an abstract semantics of A as a finite graph. The basic idea is to define a finite partition of the set of valuations R X ≥0 . Then, instead of considering nodes (q, S) with set of valuations S (e.g. zones Z), one considers a union of the parts of R X ≥0 that intersect S. This gives the finite abstraction. Let us consider a bound function associating to each clock x of A a bound α x ∈ N. A region [START_REF] Alur | A theory of timed automata[END_REF] with respect to α is the set of valuations specified as follows:

1. for each clock x ∈ X, one constraint from the set:

{x = c | c = 0, . . . , α x } ∪ {c -1 < x < c | c = 1, . . . , α x } ∪ {x > α x } 2. for each pair of clocks x, y having interval constraints: c -1 < x < c and d -1 < y < d, it is specified if f ract(x)
is less than, equal to or greater than f ract(y).

It can be checked that the set of regions is a finite partition of R X ≥0 . The closure abstraction of a set of valuations S, denoted Closure α (S), is the union of the regions that intersect S [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF]. A simulation graph, denoted SG α (A), has nodes of the form (q, S) where q is a state of A and S ⊆ R X ≥0 is a set of valuations. The initial node of SG α (A) is (q 0 , {0}). There is an edge (q, S) t -→ (q , Closure α (S )) in SG α (A) iff S is the set of valuations ν such that (q, ν) δ,t -→ (q , ν ) for some ν ∈ S and δ ∈ R ≥0 . Notice that the reachable part of SG α (A) is finite since the number of regions is finite.

The definition of the graph SG α (A) is parametrized by a bound function α. It is well-known that if we take α A associating to each clock x the maximal integer c such that x#c appears in some guard of A then SG α (A) preserves the reachability properties.

Theorem 1. [7]

A has an accepting run iff there is a reachable node (q, S) in SG α (A) with q ∈ Acc and α A ≤ α.

For efficiency it is important to have a good bound function α. The nodes of SG α (A) are unions of regions. Hence the size of SG α (A) depends on the number of regions which is O |X|!.2 |X| . x∈X (2.α x +2) [START_REF] Alur | A theory of timed automata[END_REF]. It follows that smaller values for α yield a coarser, hence smaller, symbolic graph SG α (A). Note that current implementations do not use closure but some convex under-approximation of it that makes the graph even bigger.

It has been observed in [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF] that instead of considering a global bound function α A for all states in A, one can use different functions in each state of the automaton. Consider for instance the automaton A in Figure 1. Looking at the guards, we get that α x = 14 and α y = 10 6 . Yet, a closer look at the automaton reveals that in the state q 2 it is enough to take the bound α y (q 2 ) = 5. This observation from [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF] points out that one can often get very big gains by associating a bound function α(q) to each state q in A that is later used for the abstraction of nodes of the form (q, Closure α(q) (S)). In op. cit. an algorithm for inferring bounds based on static analysis of the structure of the automaton is proposed. In Section 4.2 we will show how to calculate these bounds on-the-fly during the exploration of the automaton's state space.

3 Efficient testing of inclusion in a closure of a zone

The tests of the form Z ⊆ Closure α (Z ) will be at the core of the new algorithm we propose. This is an important difference with respect to the standard algorithm that makes the tests of the form Z ⊆ Z . The latter tests are done in O(|X| 2 ) time, where |X| is the number of clocks. We present in this section a simple algorithm that can do the tests Z ⊆ Closure α (Z ) at the same complexity with neither the need to represent nor to compute the closure. We start by examining the question as to how one decides if a region R intersects a zone Z. The important point is that it is enough to verify that the projection on every pair of variables is nonempty. This is the cornerstone for the efficient inclusion testing algorithm that even extends to LU-approximations.

When is R ∩ Z empty

It will be very convenient to represent zones by distance graphs. Such a graph has clocks as vertices, with an additional special clock x 0 representing constant 0. For readability, we will often write 0 instead of x 0 . Between every two vertices there is an edge with a weight of the form ( , c) where c ∈ Z ∪ {∞} and is either ≤ or <. An edge x c -→ y represents a constraint y -x c: or in words, the distance from x to y is bounded by c. Let [[G]] be the set of valuations of clock variables satisfying all the constraints given by the edges of G with the restriction that the value of x 0 is 0.

An arithmetic over the weights ( , c) can be defined as follows [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF].

Equality ( 1 , c 1 ) = ( 2 , c 2 ) if c 1 = c 2 and 1 = 2 . Addition ( 1 , c 1 ) + ( 2 , c 2 ) = ( , c 1 + c 2 ) where =< iff either 1 or 2 is <. Minus -( , c) = ( , -c).
Order ( 1 , c 1 ) < ( 2 , c 2 ) if either c 1 < c 2 or (c 1 = c 2 and 1 =< and 2 =≤).

Floor (<, c) = (≤, c -1) and (≤, c) = (≤, c).

This arithmetic lets us talk about the weight of a path as a weight of the sum of its edges. A cycle in a distance graph G is said to be negative if the sum of the weights of its edges is at most (<, 0); otherwise the cycle is positive. The following useful proposition is folklore.

Proposition 1. A distance graph G has only positive cycles iff [[G]] = ∅.
A distance graph is in canonical form if the weight of the edge from x to y is the lower bound of the weights of paths from x to y. A distance graph of a region R, denoted G R , is the canonical graph representing all the constraints defining R. Similarly G Z for a zone Z.

We can now state a necessary and sufficient condition for the intersection R ∩ Z to be empty in terms of cycles in distance graphs. We denote by R xy the weight of the edge x xy cxy -----→ y in the canonical distance graph representing R. Similarly for Z.

Proposition 2. Let R be a region and let Z be a zone. The intersection R ∩ Z is empty iff there exist variables x, y such that Z yx + R xy ≤ (<, 0). A variant of this fact has been proven as an intermediate step of Proposition 2 in [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF].

Efficient inclusion testing

Our goal is to efficiently perform the test Z ⊆ Closure(Z ) for two zones Z and Z . We are aiming at O(|X| 2 ) complexity, since this is the complexity of current algorithms used for checking inclusion of two zones. Proposition 2 can be used to efficiently test the inclusion R ⊆ Closure(Z ). It remains to understand what are the regions intersecting the zone Z and then to consider all possible cases. The next lemma basically says that every consistent instantiation of an edge in G Z leads to a region intersecting Z.

v ∈ [[G]] with v(y) -v(x) = d.
Thanks to this lemma it is enough to look at edges of G Z one by one to see what regions we can get. This insight is used to get the desired efficient inclusion test Theorem 2. Let Z, Z be zones. Then, Z Closure α (Z ) iff there exist variables x, y, both different from x 0 , such that one of the following conditions hold:

1. Z 0x < Z 0x and Z 0x ≤ (≤, α x ), or 2. Z x0 < Z x0 and Z x0 ≥ (≤, -α x ), or 3. Z x0 ≥ (≤, -α x ) and Z xy < Z xy and Z xy ≤ (≤, α y ) + Z x0 .
Comparison with the algorithm for Z ⊆ Z Given two zones Z and Z , the procedure for checking Z ⊆ Z works on two graphs G Z and G Z that are in canonical form. This form reduces the inclusion test to comparing the edges of the graphs one by one. Note that our algorithm for Z ⊆ Closure α (Z ) does not do worse. It works on G Z and G Z too. The edge by edge checks are only marginally more complicated. The overall procedure is still O(|X| 2 ).

Handling LU-approximation

In [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] the authors propose to distinguish between maximal constants used in upper and lower bounds comparisons: for each clock x, L x ∈ N∪{-∞} represents the maximal constant c such that there exists a constraint x > c or x ≥ c in a guard of a transition in the automaton; dually, U x ∈ N ∪ {-∞} represents the maximal constant c such that there is a constraint x < c or x ≤ c in a guard of a transition. If such a c does not exist, then it is considered to be -∞. They have introduced an extrapolation operator Extra + LU (Z) that takes into account this information. This is probably the best presently known convex abstraction of zones.

We now explain how to extend our inclusion test to handle LU approximation, namely given Z and Z how to directly check Z ⊆ Closure α (Extra + LU (Z )) efficiently. Observe that for each x, the maximal constant α x is the maximum of L x and U x . In the sequel, this is denoted Z ⊆ Closure + LU (Z ). For this we need to understand first when a region intersecting Z intersects Extra + LU (Z ). Therefore, we study the conditions that a region R should satisfy if it intersects Extra + LU (Z) for a zone Z. We recall the definition given in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] that has originally been presented using difference bound matrices (DBM). In a DBM (c ij , ≺ i,j ) stands for x i -x j ≺ i,j c i,j .

In the language of distance graphs, this corresponds to an edge x j ≺i,j ci,j -→ x i ; hence to Z ji in our notation. Let Z + denote Extra + LU (Z) and G Z + its distance graph. We have:

Z + xy =                (<, ∞) if Zxy > (≤, Ly) (<, ∞) if -Zy0 > (≤, Ly) (<, ∞) if -Zx0 > (≤, Ux), y = 0 (<, -Ux) if -Zx0 > (≤, Ux), y = 0 Zxy otherwise. (1)
From this definition it will be important for us to note that G Z + is G Z with some weights put to (<, ∞) and some weights on the edges to x 0 put to (<, -U x ). Note that Extra + LU (Z ) is not in the canonical form. If we put Extra + LU (Z ) into the canonical form then we could just use Theorem 2. We cannot afford to do this since canonization can take cubic time [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF]. The following theorem implies that we can do the test without canonizing Extra + LU (Z ). Hence we can get a simple quadratic test also in this case. Theorem 3. Let Z, Z be zones. Let Z + denote Extra + LU (Z ) obtained from Z using Equation 1 for each edge. Note that Z + is not necessarily in canonical form. Then, we get that Z Closure α (Z + ) iff there exist variables x, y different form x 0 such that one of the following conditions hold:

1. Z + 0x < Z 0x and Z + 0x ≤ (≤, α x ), or 2. Z + x0 < Z x0 and Z x0 ≥ (≤, -α x ), or 3. Z x0 ≥ (≤, -α x ) and Z + xy < Z xy and Z + xy ≤ (≤, α y ) + Z x0 .

A New Algorithm for Reachability

Our goal is to decide if a final state of a given timed automaton is reachable. We do it by computing a finite prefix of the reachability tree of the zone graph ZG(A) that is sufficient to solve the reachability problem. Finiteness is ensured by not exploring a node (q, Z) if there exists a (q, Z ) such that Z ⊆ Closure α (Z ), for a suitable α. We will first describe a simple algorithm based on the closure and then we will address the issue of finding tighter bounds for the clock values.

The basic algorithm

Given a timed automaton A we first calculate the bound function α A as described just before Theorem 1. Each node in the tree that we compute is of the form (q, Z), where q is a state of the automaton, and Z is an unapproximated zone. The root node is (q 0 , Z 0 ), which is the initial node of ZG(A). The algorithm performs a depth first search: at a node (q, Z), a transition t = (q, g, r, q

) not yet considered for exploration is picked and the successor (q , Z ) is computed where (q, Z)

t - → (q , Z ) in ZG(A).
If q is a final state and Z is not empty then the algorithm terminates. Otherwise the search continues from (q , Z ) unless there is already a node (q , Z ) with Z ⊆ Closure α A (Z ) in the current tree.

The correctness of the algorithm is straightforward. It follows from the fact that if Z ⊆ Closure α A (Z ) then all the states reachable from (q , Z ) are reachable from (q , Z ) and hence it is not necessary to explore the tree from (q , Z ). Termination of the algorithm is ensured since there are finitely many sets of the form Closure α A (Z). Indeed, the algorithm will construct a prefix of the reachability tree of SG α (A) as described in Theorem 1.

The above algorithm does not use the classical extrapolation operator named Extra + M in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] and Extra + α hereafter, but the coarser Closure α operator [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF]. This is possible since the algorithm does not need to represent Closure α (Z), which is in general not a zone. Instead of storing Closure α (Z) the algorithm just stores Z and performs tests Z ⊆ Closure α (Z ) each time it is needed (in contrast to Algorithm 2 in [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF]). This is as efficient as testing Z ⊆ Z thanks to the algorithm presented in the previous section.

Since Closure α is a coarser abstraction, this simple algorithm already covers some of the optimizations of the standard algorithm. For example the Extra + α (Z) abstraction proposed in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] is subsumed since Extra + α (Z) ⊆ Closure α (Z) for any zone Z [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF][START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]. Other important optimizations of the standard algorithm concern finer computation of bounding functions α. We now show that the structure of the proposed algorithm allows to improve this too.

Listing 1.1. Reachability algorithm with on-the-fly bound computation and non-convex abstraction.

function main(): push((q0, Z0, α0), stack) while (stack = ∅) do (q, Z, α) := top(stack); pop(stack) explore(q, Z, α) resolve() return "empty" function explore(q, Z, α):

if (q is accepting) exit "not empty" if (∃ (q, Z , α ) nontentative and s.t. Z ⊆ Closure α (Z )) mark (q, Z, α) tentative wrt (q, Z , α ) α := α ; propagate(parent(q, Z, α)) else propagate(q, Z, α)
for each (qs, Zs, αs) in children(q, Z, α) do for each (q, Z, α) tentative wrt (q, Z , α ) do

24 if (Z ⊆ Closure α (Z )) 25 mark (q, Z, α) nontentative 26 α := -∞; propagate(parent(q, Z, α))
27 push((q, Z, α), stack) 28 29 function propagate(q, Z, α):

30 α := max (q,Z,α) g;R --→(q ,Z ,α ) maxedge(g, R, α ) 31 if (α has changed) 32
for each (qt, Zt, αt) tentative wrt (q, Z, α) do

33 αt := α; propagate(parent(qt, Zt, αt)) 34 if ((q, Z, α) = (q0, Z0, α0)) 35 propagate(parent(q, Z, α)) 36 37
function maxedge(g, R, α):

38 let α R = λx. if x ∈ R then -∞ else α(x) 39 let αg = λx. if x#c in g then c else -∞ 40 return (λx. max(α R (x), αg(x)))

Computing clock bounds on-the-fly

We can improve on the idea of Behrmann et al. [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF] of computing a bound function α q for each state q. We will compute these bounding functions on-the-fly and they will depend also on a zone and not just a state. An obvious gain is that we will never consider constraints coming from unreachable transitions. We comment more on advantages of this approach in Section 5.

Our modified algorithm is given in Figure 1.1. It computes a tree whose nodes are triples (q, Z, α) where (q, Z) is a node of ZG(A) and α is a bound function. Each node (q, Z, α) has as many child nodes (q s , Z s , α s ) as there are successors (q s , Z s ) of (q, Z) in ZG(A). Notice that this includes successors with an empty zone Z s , which are however not further unfolded. These nodes must be included for correctness of our constant propagation procedure. By default bound functions map each clock to -∞. They are later updated as explained below. Each node is further marked either tentative or nontentative. The leaf nodes (q, Z, α) of the tree are either deadlock nodes (either there is no transition out of state q or Z is empty), or tentative nodes. All the other nodes are marked nontentative.

Our algorithm starts from the root node (q 0 , Z 0 , α 0 ), consisting of the initial state, initial zone, and the function mapping each clock to -∞. It repeatedly alternates an exploration and a resolution phase as described below.

Exploration phase Before exploring a node n = (q, Z, α) the function explore checks if q is accepting and Z is not empty; if it is so then A has an accepting run. Otherwise the algorithm checks if there exists a nontentative node n = (q , Z , α ) in the current tree such that q = q and Z ⊆ Closure α (Z ). If yes, n becomes a tentative node and its exploration is temporarily stopped as each state reachable from n is also reachable from n . If none of these holds, the successors of the node are explored. The exploration terminates since Closure α has a finite range.

When the exploration algorithm gets to a new node, it propagates the bounds from this node to all its predecessors. The goal of these propagations is to maintain the following invariant. For every node n = (q, Z, α):

1. if n is nontentative, then α is the maximum of the α s from all successor nodes (q s , Z s , α s ) of n (taking into account guards and resets as made precise in the function maxedge); 2. if n is tentative with respect to (q , Z , α ), then α is equal to α .

The result of propagation is analogous to the inequalities seen in the static guard analysis [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF], however now applied to the zone graph, on-the-fly. Hence, the bounds associated to each node (q, Z, α) never exceed those that are computed by the static guard analysis.

A delicate point about this procedure is handling of tentative nodes. When a node n is marked tentative, we have α = α . However the value of α may be updated when the tree is further explored. Thus each time we update the bounds function of a node, it is not only propagated upward in the tree but also to the nodes that are tentative with respect to n . This algorithm terminates as the bound functions in each node never decrease and are bounded. From the invariants above, we get that in every node, α is a solution to the equations in [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF] applied on ZG(A).

It could seem that the algorithm will be forced to do a high number of propagations of bounds. The experiments reported in Section 5 show that the present very simple approach to bound propagation is good enough. Since we propagate the bounds as soon as they are modified, most of the time, the value of α does not change in line 30 of function propagate. In general, bounds are only propagated on very short distances in the tree, mostly along one single edge. For this reason we do not concentrate on optimizing the function propagate.

In the implementation we use the presented function augmented with a minor "optimization" that avoids calculating maximum over all successors in line 30 when it is not needed.

Resolution phase Finally, as the bounds may have changed since n has been marked tentative, the function resolve checks for the consistency of tentative nodes. If Z ⊆ Closure α (Z ) is not true anymore, n needs to be explored. Hence it is viewed as a new node: the bounds are set to -∞ and n is pushed on the stack for further consideration in the function main. Setting α to -∞ is safe as α will be computed and propagated when n is explored. We perform also a small optimization and propagate this bound upward, thereby making some bounds decrease.

The resolution phase may provide new nodes to be explored. The algorithm terminates when this is not the case, that is when all tentative nodes remain tentative. We can then conclude that no accepting state is reachable. Theorem 4. An accepting state is reachable in ZG(A) iff the algorithm reaches a node with an accepting state and a non-empty zone.

Handling LU approximations

Recall that Extra + LU (Z) approximation used two bounds: L x and U x for each clock x. In our algorithm we can easily propagate LU bounds instead of just maximal bounds. We can also replace the test

Z ⊆ Closure α (Z ) by Z ⊆ Closure α (Extra + L U (Z ))
, where L and U are the bounds calculated for (q , Z ) and α x = max(L x , U x ) for every clock x. As discussed in Section 3.3, this test can be done efficiently too. The proof of correctness of the resulting algorithm is only slightly more complicated.

Experimental results

We have implemented the algorithm from Figure 1.1, and have tested it on classical benchmarks. The results are presented in Table 1, along with a comparison to UPPAAL and our implementation of UPPAAL's core algorithm that uses the Extra +

LU extrapolation [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] and computes bounds by static analysis [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF]. Since we have not considered symmetry reduction [START_REF] Hendriks | Adding symmetry reduction to UPPAAL[END_REF] in our tool, we have not used it in UPPAAL either.

The comparison to UPPAAL is not meaningful for the CSMA/CD and the FDDI protocols. Indeed, UPPAAL runs out of time even if we significantly increase the time allowed; switching to breadth-first search has not helped either. We suspect that this is due to the order in which UPPAAL takes the transitions in the automaton. For this reason in columns 4 and 5, we provide results from our own implementation of UPPAAL's algorithm that takes transitions in the same order as the implementation of our algorithm. Although RED also uses approximations, it is even more difficult to draw a meaningful comparison with it, since it uses symbolic state representation unlike UPPAAL or our tool. Since this paper is about approximation methods, and not tool comparison, we leave more extensive comparisons as further work.

The results show that our algorithm provides important gains. Analyzing the results more closely we could see that both the use of closure, and on-the-fly computation of bounds are important. In Fischer's protocol our algorithm visits much less nodes. In the FDDI protocol with n processes, the DBMs are rather big square matrices of order 3n + 2. Nevertheless our inclusion test based on Closure is significantly better in the running time. The CSMA/CD case shows that the cost of bounds propagation does not always counterbalance the gains. However the overhead is not very high either. We comment further on the results below.

The first improvement comes from the computation of the maximal bounds used for the abstraction as demonstrated by the examples A 2 (Figure 2), Fischer and CSMA/CD that correspond to three different situations. In the A 2 example, the transition that yields the big bound 10 4 on y in q 0 is not reachable from any (q 0 , Z), hence we just get the lower bound 20 on y in (q 0 , Z), and a subsequent gain in performance.

The automaton A 1 in Figure 2 illustrates the gain on the CSMA/CD protocol. The transition from q 0 to q 1 is disabled as it must synchronize on letter a!. The static analysis algorithm [START_REF] Behrmann | Static guard analysis in timed automata verification[END_REF] ignores this fact, hence it associates bound 10 4 to y in q 0 . Since our algorithm computes the bounds on-the-fly, y is associated the bound 10 in every node (q 0 , Z). We observe that UPPAAL's algorithm visits 10003 nodes on ZG(A 1 ) whereas our algorithm only visits 2 nodes. The same situation occurs in the CSMA/CD example. However despite the improvement in the number of nodes (roughly 10%) the cost of computing the bounds impacts the running time negatively.

The gains that we observe in the analysis of the Fischer's protocol are explained by the automaton A 3 in Figure 2. A 3 has a bounded integer variable n that is initialized to 0. Hence, the transitions from q 0 to q 2 , and from q 1 to q 2 , that check if n is equal to 10 are disabled. This is ignored by the static analysis algorithm that associates the bound 10 4 to clock y in q 0 . Our algorithm however associates the bound 10 to y in every node (q 0 , Z). We observe that UPPAAL's algorithm visits 10004 nodes whereas our algorithm only visits 3 nodes. A similar situation occurs in the Fischer's protocol. We include the last row to underline that our implementation is not as mature as UPPAAL. We strongly think that UPPAAL could benefit from methods presented here.

The second kind of improvement comes from the Closure α abstraction that particularly improves the analysis of the Fischer's and the FDDI protocols. The situation observed on the FDDI protocol is explained in Figure 2. For the zone Z in the figure, by definition Extra + LU (Z) = Z, and in consequence Z ⊆ Z. However, Z ⊆ Closure α (Z). On FDDI and Fischer's protocols, our algorithm performs better due to the non-convex approximation.

Conclusions

We have proposed a new algorithm for checking reachability properties of timed automata. The algorithm has two sources of improvement that are quite independent: the use of the Closure α operator, and the computation of bound functions on-the-fly.

Apart from immediate gains presented in Table 1, we think that our approach opens some new perspectives on analysis of timed systems. We show that the use of non-convex approximations can be efficient. We have used very simple approximations, but it may be well the case that there are more sophisticated approximations to be discovered. The structure of our algorithm permits to calculate bounding constants on the fly. One should note that standard benchmarks are very well understood and very well modeled. In particular they have no "superfluous" constraints or clocks. However in not-so-clean models coming from systems in practice one can expect the on-the-fly approach to be even more beneficial.

There are numerous directions for further research. One of them is to find other approximation operators. Methods for constraint propagation also deserve a closer look. We believe that our approximations methods are compatible with partial order reductions [START_REF] Hendriks | Adding symmetry reduction to UPPAAL[END_REF][START_REF] Malinowski | SAT based bounded model checking with partial order semantics for timed automata[END_REF]. We hope that the two techniques can benefit from each other.

A Proofs from Section 3

We provide all the proofs from the section presenting the efficient inclusion testing algorithm. For convenience, we recall the statements of the facts that are proven together with their original numbering. They are preceded with black arrow for readability. Otherwise there is a variable, say y, that is not fixed in G. We will show how to fix it. Let us multiply all the constraints in G by 2. This means that we change each arrow

x 1 c -→ x 2 to x 1 2c -→ x 2 . Let us call the resulting graph H. Clearly H is in canonical form since G is. Moreover [[H]] is not empty iff [[G]
] is not empty. The gain of this transformation is that for our chosen variable y we have in H edges 0 c0y -→ y and y cy0 -→ 0 with c y0 + c 0y ≥ 2. This means that there is a natural number d such that (≤, d) ≤ ( c 0y ) and (≤, -d) ≤ ( c y0 ). Let H d be H with edges to and from y changed to 0 ≤d -→ y and y ≤-d -→ 0, respectively. This is a distance graph where y is fixed. We need to show that there is no negative cycle in this graph.

Suppose that there is a negative cycle in H d . Clearly it has to pass through 0 and y since there was no negative cycle in H. Suppose that it uses the edge 0 ≤d -→ y, and suppose that the next used edge is y cyx -→ x. The cycle cannot come back to y before ending in 0 since then we could construct a smaller negative cycle. Hence all the other edges in the cycle come from H. Since H is in the canonical form, a path from x to 0 can be replaced by the edge from x to 0, and the value of the path will not increase. This means that our hypothetical negative cycle has the form 0 Summarizing, starting from G that has no negative cycles we have constructed a graph H d that has no negative cycles, and has one more variable fixed. We also know that if [[H d ]] is not empty then [[G]] is not empty. Repeatedly applying this construction we get a graph where all the variables are fixed and no cycle is negative. As we have seen above the semantics of such a graph is not empty.

Proposition 2. Let R be a region and let Z be a zone. The intersection R ∩Z is empty iff there exist variables x, y such that Z yx + R xy ≤ (<, 0). Before proving the above proposition, we will start with some notions. Let R be a region wrt. a bound function α : X → N. A variable x is bounded in R if a constraint x ≤ c holds in R for some constant c; otherwise the variable is called unbounded in R. Observe that if x 1 , x 2 are bounded then we have

x 1 -x 2 = c or c -1 < x 1 -x 2 < c in R.
If y is unbounded then we have y > α y in R.

For two distance graphs G 1 , G 2 which are not necessarily in canonical form, we denote by min(G 1 , G 2 ) the distance graph where each edge has the weight equal to the minimum of the corresponding weights in G 1 and G 2 . Even though this graph may be not in canonical form, it should be clear that it represents intersection of the two arguments, that is,

[[min(G 1 , G 2 )]] = [[G 1 ]] ∩ [[G 2 ]
]; in other words, the valuations satisfying the constraints given by min(G 1 , G 2 ) are exactly those satisfying all the constraints from G 1 as well as G 2 .

We are now ready to examine the conditions when R ∩ Z is empty. We start with the following simple lemma.

Lemma 2. Let G R be the distance graph of a region and let x 1 , x 2 be two variables bounded in R. For every distance graph G:

if in min(G R , G) the weight of the edge x 1 -→ x 2 comes from G then x 1 -→ x 2 -→ x 1 is a negative cycle in min(G R , G).
Proof. Suppose that the edge x 1 c -→ x 2 is as required by the assumption of the lemma. In R we can have either

x 2 -x 1 = d or d -1 < x 2 -x 1 < d.
In the first case we have edges

x 1 ≤d -→ x 2 and x 2 ≤-d -→ x 1 in G R . Since the edge x 1 c -→ x 2 comes from G we have c < d or c = d and is the strict inequality. We get a negative cycle x 1 c -→ x 2 ≤-d -→ x 1 .
In the second case we have edges x 2

<-d+1 -→ x 1 and x 1 <d -→ x 2 in R. Hence c < d and x 1 c -→ x 2 <-d+1 -→ x 1 gives a negative cycle.
Proof of Proposition 2 Let G R , G Z be the canonical distance graphs representing the region R and the zone Z respectively. One direction is immediate: If min(G R , G Z ) has a negative cycle then R ∩ Z is empty by Proposition 1.

For the other direction suppose that R ∩ Z is empty. Again, by Proposition 1 the graph min(G R , G Z ) has a negative cycle. An immediate case is when in this graph an edge between two variables bound in R comes from G Z . From Lemma 2 we obtain a negative cycle on these two variables. So in what follows we suppose that in min(G R , G Z ) all the edges between variables bounded in R come from G R . Hence every negative cycle should contain an unbounded variable.

Let y be a variable unbounded in R that is a part of the negative cycle. Consider y with its successor and its predecessor on the cycle: x -→ y -→ x . We will show that we can assume that x is x 0 . Observe that in G R every edge to y has value ∞. So the weight of the edge x -→ y is from G Z . If the weight of the outgoing edge is also from G Z then we could have eliminated y from the cycle by choosing x -→ x from G Z . Hence the weight of y -→ x comes from G R . Since y is unbounded in R, the weight of this edge is d-α y , where d is the value on the edge 0 d -→ x in G R . This is because we can rewrite inequation x -y < d -α y as y -x > α y -d, and we know that α y is the smallest possible value for y, while d is the supremum on the possible values of x . But then instead of the edge y -→ x we can take y -→ x 0 -→ x in min(G R , G Z ) which has smaller value since we have y

<-αy -→ x 0 in G R .
If x is x 0 then we get a cycle of a required form since it contains only x 0 and y. Otherwise, let us more closely examine the whole negative cycle:

x 0 -→ x i1 -→ . . . -→ x i k -→ x -→ y -→ x 0 .
By the reasoning from the previous paragraph, all of x i1 , . . . , x i k can be assumed to be bounded in R. Otherwise we could get a cycle visiting x 0 twice and we could remove a part of it with one unbounded variable and still have a negative cycle. By our assumption, all the edges from and to these variables come from R. This means that the path from x 0 to x can be replaced by an edge x 0 -→ x from R. So finally, the negative cycle has the required form x 0 -→ x -→ y -→ x 0 with the edges x 0 -→ x and y -→ x 0 coming from G R and the edge x -→ y coming from G Z . Since G R is canonical, we can reduce this cycle to x -→ y -→ x with x -→ y coming from G Z and y -→ x coming from G R .

A.1 Efficient inclusion testing

Given two zones Z and Z and a bound function α, we would like to know if Z ⊆ Closure α (Z ): that is, does there exist a region R that intersects Z but does not intersect Z ? From Proposition 2 this reduces to asking if there exists a region R that intersects Z and two variables x, y such that Z yx + R xy < (≤, 0). This brings us to look for the least value of R xy from among the regions R intersecting Z. We begin with the observation that every consistent instantiation of an edge in a canonical distance graph G gives a valuation satisfying the constraints of G.

Lemma 1. Let G be a distance graph in canonical form, with all cycles positive. Let x, y be two variables such that x -→ x for variables x and y and the rest of the edges come from G. We show that all cycles in G d are positive. For contradiction, suppose there is a negative cycle N in G d . Clearly, since G does not have negative cycle, N should contain the variables x and y. The value of the shortest path from x to y in G was given by ( xy , c xy ). Therefore, the shortest path value from x to y in G d is given by d and the shortest path value from y to x is -d. Hence the sum of the weights in N is negative would imply that the value of the cycle x → y → x is negative. However since, this is 0, such a negative cycle N cannot exist. The lemma follows from Proposition 1.

Recall that for a zone Z, we denote by Z xy the weight of the edge x For a weight ( , c) we define -( , c) as ( , -c). We now define a ceiling function • for weights.

Definition 1. For a real c, let c denote the smallest integer that is greater than or equal to c. We define the ceiling function ( , c) for a weight ( , c) depending on whether equals ≤ or <, as follows:

(≤, c) = (≤, c) if c is an integer (<, c ) otherwise (<, c) = (<, c + 1) if c is an integer (<, c ) otherwise Lemma 3.
Let Z be a non-empty zone and let x be a variable different from x 0 . Then, from among the regions R that intersect Z:

the least value of R 0x is given by

(<, ∞) if Z x0 < (≤, -α x ) -Z x0 otherwise -the least value of R x0 is given by max{ -Z 0x , (<, -α x )}. Proof. Let Z 0x = ( 0x , c 0x ) and Z x0 = ( x0 , c x0 ).
For the least value of R 0x , first note that if Z x0 < (≤, -α x ) then all valuations v ∈ Z have v x > α x and by definition [v] 0x = (<, ∞) for such valuations. If not, we know that for all valuations -v x x0 c x0 , that is, v x x0 -c x0 . If x0 is ≤, then from Lemma 1 there exists a valuation with v x = -c x0 and this is the minimum value that can be attained. When x0 is <, then we can find a positive < 1 such that c x0 -x0 c x0 and -c x0 + 0x c 0x . From Lemma 1, there exists a valuation with v x = -c x0 + for which [v] 0x = (<, -c x0 + 1). Since x0 is a strict <, this is the minimum value for R 0x . This gives that the minimum value is -Z x0 .

Now we look at the minimum value for R x0 . If ( 0x , c 0x ) ≤ (≤, α x ), then all valuations v have v x ≤ α x and by an argument similar to above, the minimum value of R x0 would be given by -Z 0x . Since ( 0x , c 0x ) ≤ (≤, α x ), we have

( 0x , -c 0x ) ≥ (≤, -α x ) > (<, -α x ). If ( 0x , c 0x ) > (≤, α x )
, then from Lemma 1, there are valuations in Z with v x > α x and for these valuations, [v] x0 = (< , -α x ). In this case the minimum value is given by (<, -α x ). Since ( 0x , c 0x ) > (≤, α x ), we have ( 0x , -c 0x ) < (<, -α x ) and so -Z 0x ≤ (<, -α x ). In each case, observe that we get max{ -Z 0x , (<, -α x )} as the minimum value. Lemma 4. Let Z be a non-empty zone and let x, y be variables none of them equal to x 0 . Then, from among the regions R that intersect Z, the least value of R xy is given by

(<, ∞) if Z y0 < (≤, -α y ) max{ -Z yx , -Z y0 -(≤, α x )} otherwise
Proof. Let G be the canonical distance graph representing the zone Z. We denote the weight of an edge i -→ j in G by ( ij , c ij ). Recall that this means Z ij = ( ij , c ij ). For clarity, for a valuation v, we write v x for v(x).

We are interested in computing the smallest value of the y-x constraint defining a region belonging to Closure α (Z), that is, we need to find min{ [v] xy | v ∈ Z}. Call this β. By definition of regions, we have for a valuation v:

[v] xy =      (<, ∞) if v y > α y (≤, v y -v x ) if v y ≤ α y and v x ≤ α x (<, v y -α x ) if v y ≤ α y and v x > α x (2)
We now consider the first of the two cases from the statement of the lemma. Namely, Z y0 < (≤, -α y ). This means that 0 -v y y0 c y0 and c y0 ≤ -α y ; moreover y0 is the strict inequality if c y0 = -α y . In consequence, all valuations v ∈ Z, satisfy v y > α y . Whence β = (<, ∞).

We now consider the case when Z y0 ≥ (≤, -α y ). Let G be the graph in which the edge 0 -→ y has weight min{(≤, α y ), ( 0y , c 0y )} and the rest of the edges are the same as that of G. This graph G represents the valuations of Z that have v y ≤ α y : [[G ]] = {v ∈ Z | v y ≤ α y }. We show that this set is not empty. For this we check that G does not have negative cycles. Since G does not have negative cycles, every negative cycle in G should include the newly modified edge 0 -→ y. Note that the shortest path value from y to 0 does not change due to this modified edge. So the only possible negative cycle in G is 0 -→ y -→ 0. But then we are considering the case when Z y0 ≥ (≤, -α y ), and so Z y0 +(≤, α y ) ≥ (≤, 0). Hence this cycle cannot be negative either. In consequence all the cycles in G are positive and [[G ]] is not empty.

To find β, it is sufficient to consider only the valuations in [[G ]]. As seen from Equation 2, among the valuations in [[G ]], we need to differentiate between those with v x ≤ α x and the ones with v x > α x . We proceed as follows. We first compute min{ [v]

xy | v ∈ [[G ]] and v x ≤ α x }. Call this β 1 . Next, we compute min{[v] xy | v ∈ [[G ]
] and v x > α x } and set this as β 2 . Our required value β would then equal min{β 1 , β 2 }.

To compute β 1 , consider the following distance graph G 1 which is obtained from G by just changing the edge 0 -→ x to min{(≤, α x ), ( 0x , c 0x )} and keeping the remaining edges the same as in G . The set of valuations [v] xy is given by (≤, v y -v x ) . Let ( 1 , w 1 ) be the shortest path from y to x in the graph G 1 . Then, we have for all

[[G 1 ]] equals {v ∈ [[G ]] | v x ≤ α x }. If [[G 1 ]] = ∅, we set β 1 to (<, ∞) and proceed to calculate β 2 . If not, we see that from Equation 2, for every v ∈ [[G 1 ]],
v ∈ [[G 1 ]], v x -v y 1 w 1 , that is, v y -v x 1 -w 1 . If 1 is
≤, then the least value of [v] xy would be (≤, -w 1 ) and if 1 is <, one can see that the least value of [v] xy is (<, -w 1 + 1). This shows that β 1 = ( 1 , -w 1 ) . It now remains to calculate ( 1 , w 1 ).

Recall that G 1 has the same edges as in G except possibly different edges 0 -→ x and 0 -→ y. If the shortest path from y to x has changed in G 1 , then clearly it should be due to one of the above two edges. However note that the edge 0 -→ y cannot belong to the shortest path from y to x since it would contain a cycle y -→ . . . 0 -→ y -→ . . . x that can be removed to give shorter path. Therefore, only the edge 0 -→ x can potentially yield a shorter path: y -→ . . . -→ 0 -→ x. However, the shortest path from y to 0 in G 1 cannot change due to the added edges since that would form a cycle with 0 and we know that all cycles in G 1 are positive. Therefore the shortest path from y to 0 is the direct edge y -→ 0, and the shortest path from y to x is the minimum of the direct edge y -→ x and the path y -→ 0 -→ x. We get: ( 1 , w 1 ) = min{( yx , c yx ), ( y0 , c y0 ) + (≤, α x )} which equals min{Z yx , Z y0 + (≤, α x )}. Finally, from the argument in the above two paragraphs, we get:

β 1 =      (<, ∞) if [[G 1 ]] = ∅ -Z yx if [[G 1 ]] = ∅ and Z yx ≤ Z y0 + (≤, α x ) -Z y0 + (≤, -α x ) if [[G 1 ]] = ∅ and Z yx > Z y0 + (≤, α x ) (3)
We now proceed to compute

β 2 = min{[v] xy | v ∈ [[G ]] and v x > α x }. Let G 2 be
the graph which is obtained from G by modifying the edge x -→ 0 to min{Z x0 , (<, -α x )} and keeping the rest of the edges the same as in

G . Clearly [[G 2 ]] = min{v ∈ [[G ]] | v x > α x }. Again, if [[G 2 ]
] is empty, we set β 2 to (<, ∞). Otherwise, from Equation 2, for each valuation v ∈ [[G 2 ]], the value of [v] xy is given by (<, v y -α x ). For the minimum value, we need the least value of v y from v ∈ [[G 2 ]]. Let ( 2 , w 2 ) be the shortest path from y to 0 in G 2 . Then, since -v y 2 w 2 , the least value of v y would be -w 2 if 2 =≤ and equal to -w 2 if 2 =< and β 2 would respectively be (<, -w 2 -α x ) or (<, -w 2 + 1 -α x ). It now remains to calculate ( 2 , w 2 ).

Recall that G 2 is G with 0 -→ y and x -→ 0 modified. The shortest path from y to 0 cannot include the edge 0 -→ y since it would need to contain a cycle, for the same reasons as in the β 1 case. So we get ( 2 , w 2 ) = min{Z y0 , Z yx + (<, -α x )}. If Z y0 ≤ Z yx + (<, -α x ), then we take ( 2 , w 2 ) as Z y0 , otherwise we take it to be Z yx + (<, -α x ). So, we get β 2 as the following:

β 2 =      (<, ∞) if [[G 2 ]] = ∅ -Z yx + (<, 1) if [[G 2 ]] = ∅ and Z y0 ≥ Z yx + (<, -α x ) -Z y0 + (<, -α x ) if [[G 2 ]] = ∅ and Z y0 < Z yx + (<, -α x ) (4)
However, we would like to write β 2 in terms of the cases used for β 1 in Equation 3 so that we can write β, which equals min{β 1 , β 2 }, conveniently.

Let ψ 1 be the inequation: Z yx ≤ Z y0 +(≤, α x ). From Equation 3, note that β 1 has been classified according to ψ 1 and ¬ψ 1 when [[G 1 ]] is not empty. Similarly, If the constant c yx < c y0 + α x , then -c yx > -c y0 -α x and we clearly get that -Z yx ≥ -Z y0 + (<, -α x ). If the constant c yx = c y0 + α x and if y0 =≤, then the required inequation is trivially true; if y0 =<, it implies that yx =< too and clearly (<, -c yx ) equals (<, -c y0 ) + (<, -α x ).

Theorem 2. Let Z, Z be zones. Then, Z Closure α (Z ) iff there exist variables x, y such that one of the following conditions hold:

1. Z 0x < Z 0x and Z 0x ≤ (α x , ≤), or 2. Z x0 < Z x0 and Z x0 ≥ (-α x , ≤), or 3. Z x0 ≥ (-α x , ≤) and Z xy < Z xy and Z xy ≤ (α y , ≤) + Z x0
Proof. By definition of the Closure abstraction, Z Closure α (Z ) iff there exists a region R that intersects Z but does not intersect Z . Therefore, from Proposition 2, we need an R that intersects Z and satisfies Z yx + R xy < (≤, 0) for some variables x, y. This is equivalent to saying that for the least value of R xy that can be obtained from the zone Z, we have Z yx + R xy < (0, ≤). Depending on if x is x 0 or y is x 0 or both x and y are not x 0 we get the following three conditions that correspond to the three conditions given in the theorem.

Case 1: Z 0x + R x0 < (≤, 0)
From Lemma 3, the minimum value of R x0 from among the regions intersecting Z is given by max{ -Z 0x , (<, -α x )}. So we have:

Z 0x + max{ -Z 0x , (<, -α x )} < (≤, 0) ⇒ Z 0x + -Z 0x < (≤, 0) and Z 0x + (<, -α x ) < (≤, 0) ⇒ Z 0x < Z 0x and Z 0x ≤ (≤, α x )
This gives Condition 1 of the theorem. Case 2:

Z x0 + R 0x < (≤, 0) From Lemma 3, the minimum value of R 0x is (<, ∞) if -Z x0 > (≤, α x )
and hence it cannot be part of a negative cycle. The edge R 0x can yield a negative cycle only when -Z x0 ≤ (≤, α x ), in which case the least value of R 0x is given by -Z x0 . So we have Z x0 + -Z x0 < (≤, 0) which translates to Z x0 < Z x0 . Therefore, this case is equivalent to saying Z x0 ≥ (≤, -α x ) and Z x0 < Z x0 which gives Condition 2 of the theorem. Case 3: Z yx + R xy < (≤, 0) From Lemma 4, we get that the minimum value of the edge R xy is (<, ∞) if -Z y0 > (≤, α y ). Similar to the case above, R xy cannot be part of a negative cycle if -Z y0 > (≤, α y ). So we need to first check if -Z y0 ≤ (≤, α y ), that is, if Z y0 ≥ (≤, -α y ). Now, from Lemma 4, the minimum value of R xy is given by the max{ -Z yx , -Z y0 -(≤, α x )}. We get:

Z yx + max{ -Z yx , -Z y0 -(≤, α x )} < (≤, 0) ⇒ Z yx + -Z yx < (≤, 0) and Z yx + -Z y0 -(≤, α x ) < (≤, 0) ⇒ Z yx < Z yx and Z yx + -Z y0 -(≤, -α x ) < (≤, 0)
Let us look at the second inequality: Z yx + -Z y0 -(≤, -α x ) < (≤, 0). If Z y0 is of the form (≤, c) with c an integer, then -Z y0 = (≤, -c) and -Z y0 is the same: (≤, -c). So we get:

Z yx + (≤, -c) + (<, -α x ) < (≤, 0) ⇔ Z yx + (<, -c -α x ) < (≤, 0) ⇔ Z yx ≤ (≤, c + α x )
When Z y0 = (<, c), then -Z y0 = (<, -c + 1) and we get:

Z yx + (<, -c + 1) + (<, -α x ) < (≤, 0) ⇔ Z yx + (<, -c + 1 -α x ) < (≤, 0) ⇔ Z yx ≤ (≤, c -1 + α x )
This gives Condition 3 of the Theorem (symmetric in x and y).

A.2 Handling LU-approximation

Recall that for a zone Z, we denote by Z + the zone Extra + LU (Z). Also note that Z + is not necessarily in canonical form. Proposition 3. Let R be a region and Z be a zone. Then, R ∪ Z + is empty iff there exist variables x, y such that Z + yx + R xy < (≤, 0).

Proof. Let G R be the canonical graph representing R and let G Z be the canonical distance graph representing Z. Let G Z + be the graph that representing Z + . By definition, G Z + is obtained from G Z by changing some edges to (<, ∞) and some edges incident on x 0 to (<, -U (x)). Also, note that G Z + is not necessarily in canonical form.

From Proposition 1, R ∪ Z + is empty iff min(G R , G Z + ) has a negative cycle. An easy case is when in min(G R , G Z + ) a weight of an edge between two variables bound in R comes from G Z + . Using Lemma 2 we get a negative cycle of the required form on these two variables.

It remains to consider the opposite case. We need then to have an unbounded variable on the cycle. Let y be a variable unbounded in R that is part of the negative cycle. Consider y with its successor and its predecessor on the cycle: x -→ y -→ x . Observe that in R every edge to y has value ∞. So the weight of the edge x -→ y is from Z + . By definition of Z + , it is also from Z. If also the weight of the outgoing edge were from Z then we could have obtained a shorter negative cycle by choosing x -→ x from Z. Hence the weight of y -→ x comes from an edge modified in Z + or from R. In the first case it is y <-U (y) -→ 0, in the second it is y <-αy -→ 0. However, note that since U (y) ≤ α y , we have -α y ≤ -U (y) and therefore, in min(G R , G Z + ) we could consider the edge to come from R, that is y <-αy -→ 0. The same analysis as in the proof of Proposition 2 we get that the shortest cycle of this kind should be of the form 0 -→ y -→ 0 or 0 -→ x -→ y -→ 0; where y is an unbound variable and x is a bound variable. This cycle has the required form.

Efficient inclusion testing for LU approximations Let Z, Z be two zones and let G Z , G Z be the respective distance graphs in canonical form. By extrapolating G Z with respect to the Extra + LU operator gives a zone Z + and a corresponding distance graph G Z + , which is not necessarily in canonical form. However, from Proposition 3, the check Z ⊆ Closure + LU (Z ) can be reduced to an edge by edge comparison with every region intersecting Z. Lemmas 3 and 4 give the least value of the edge R xy for a region intersecting Z. Hence, similar to the case of Z ⊆ Closure α (Z ), it is enough to look at edges of G Z one by one to look at what regions we can possibly get. As a result we get an analogue of Theorem 2 with Z replaced by Z + . Theorem 5. Let Z, Z be zones. Writing Z + for Extra + LU (Z ) we get that Z Closure α (Z + ) iff there exist variables x, y such that one of the following conditions hold: Here we show the proof of Theorem 4 An accepting state is reachable in ZG(A) iff the algorithm reaches a node with an accepting state and a non-empty zone.

The right-to-left direction follows by a straightforward induction on the length of the path. The left-to-right direction is shown using the following lemmas.

Let P ost(S, t) stand for the set of all valuations of clocks reachable by t from valuations in S. We will need the following observation. Lemma 5 ([7]). For every zone Z, transition t and a bound function α: P ost(Closure α (Z), t) ⊆ Closure α (P ost(Z, t)). Lemma 6. Suppose that algorithm concludes that the final state is not reachable. Consider the tree it has constructed. For every (q, Z) reachable from (q 0 , Z 0 ) in ZG(A), there is a non tentative node (q, Z , α ) in the tree, such that Z ⊆ Closure α (Z ).

Proof. The hypothesis is vacuously true for (q 0 , Z 0 ). Assume that the hypothesis is true for a node (q, Z) ∈ ZG(A). We now prove that the lemma is true for every successor of (q, Z).

From hypothesis, there exists a non tentative node (q, Z L , α) in the constructed tree such that Z ⊆ Closure α (Z L ). Let t = (q, g, r, q ) be a transition of A and let (q, Z) t -→ (q , Z ) ∈ ZG(A). The transition t is enabled from (q, Z L , α) because Z ⊆ Closure α (Z L ), and, due to constraint propagation, for every clock x, α x is greater than the maximum constant it is compared to in the guard g. So we have (q, Z L , α) t -→ (q , Z L , α ) in the constructed tree.

Since Z ⊆ Closure α (Z L ), we have P ost(Z, t) ⊆ P ost(Closure α (Z L ), t), that is Z ⊆ P ost(Closure α (Z L ), t). From Lemma 5, Z ⊆ Closure α (P ost(Z L , t)), that is Z ⊆ Closure α (Z L ). We now need to check if we can replace α with α . But Closure α (Z L ) ⊆ Closure α (Z L ) since by definition of constant propagation α x ≥ α (x) for all clocks x not reset by t, and for clocks x that are reset, Z L entails x = 0, therefore irrespective of α or α the regions that intersect with Z L should satisfy x = 0.

If n = (q , Z L , α ) is non tentative, we are done and n is the node in the constructed tree corresponding to (q , Z ). If n is tentative then by definition we know that there exists a non tentative node (q , Z L , α ) such that α = α and Z L ⊆ Closure α (Z L ). Thus Z ⊆ Closure α (Z L ). In this case (q , Z L , α ) is the node corresponding to (q , Z ).

B.2 Correctness of the algorithm with LU approximation

The proof of the correctness of the algorithm using Z ⊆ Closure + LU (Z ) test is similar to that using Z ⊆ Closure α (Z ) test. We call it LU-algorithm for short. Since Extra + LU is difficult to handle, we do a small detour through another approximation a LU (Z) introduced in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF]. We recall its definition here.

Definition 2 (LU-preorder). Fix integers L and U . Let ν and ν be two valuations. Then, we say ν LU ν if for each clock x:

either ν (x) = ν(x), or L(x) < ν (x) < ν(x), or U (x) < ν(x) < ν (x). This LU-preorder can be extended to define abstractions of sets of valuations.

Lemma 10. For every (q, Z) reachable in ZG(A), there exists a non tentative node (q, Z 1 , L 1 U 1 ) in the tree constructed by the LU-algorithm, such that Z ⊆ a L 1 U 1 (Z 1 ).

Proof. The hypothesis is vacuously true for (q 0 , Z 0 ). Assume that the hypothesis is true for a node (q, Z) ∈ ZG(A). We prove that the lemma is true for every successor of (q, Z).

From hypothesis, there exists a node (q, Z 1 , L 1 , U 1 ) in the tree constructed by the LU-algorithm such that Z ⊆ a L 1 U 1 (Z 1 ). Let t = (q, g, r, q ) be a transition of A and let (q, Z) t -→ (q , Z ) ∈ ZG(A). There are two cases.

(q, Z 1 ) is not tentative Since Z ⊆ a L 1 U 1 (Z 1 ), the transition t is enabled from a L 1 U 1 (Z 1 ). From Lemma 7, t is enabled from Z 1 too. Since Z ⊆ a L 1 U 1 (Z 1 ), we have P ost(Z, t) ⊆ P ost(a L 1 U 1 (Z 1 ), t), that is Z ⊆ P ost(a L 1 U 1 (Z 1 ), t). From Lemma 9, Z ⊆ a L 1 U 1 (P ost(Z 1 , t)). We can take Z 1 as P ost(Z 1 , t) and then let (q , Z 1 , L 1 U 1 ) be the successor node in the tree computed by LU-algorithm. It remains to show that Z ⊆ a L 1 U 1 (Z 1 ) is the node corresponding to (q , Z ). This follows because by definition L 1 (x) ≥ L 1 (x), U 1 (x) ≥ U 1 (x) for all clocks x that are not reset by the transition t and for the clocks reset by t, Z 1 entails x = 0.

(q, Z 1 ) is tentative If it is a tentative node, we know that there exists a nontentative node (q, Z 2 , L 2 U 2 ) in the tree constructed by the LU-algorithm such that Z 1 ⊆ Closure L2U2 (Z 2 ), that is, Z 1 ⊆ a L2U2 (Z 2 ). The rest of the argument is the same as in the previous case with (q, Z 2 , L 2 U 2 ) instead of (q, Z 1 , L 1 U 1 ).

5 yy ≥ 10 6 Fig. 1 .

 561 Fig. 1. Timed automaton A.

Lemma 1 .

 1 Let G be a distance graph in canonical form, with all cycles positive. Let x, y be two variables, and let x xy cxy -→ y and y yxcyx -→ x be edges in G. For every d ∈ R such that d xy c xy and -d yx c yx there exists a valuation

  19 if (Zs = ∅) 20 explore(qs, Zs, αs) 21 22 function resolve():23

Fig. 2 .

 2 Fig. 2. Examples explaining gains obtained with the algorithm.

Proposition 1 .

 1 A distance graph G has only positive cycles iff [[G]] = ∅. Proof. If there is a valuation v ∈ [[G]] then we replace every edge x c -→ y by x ≤d -→ y where d = v(y) -v(x). We have d xy c xy . Since every cycle in the new graph has value 0, every cycle in G is positive. For the other direction suppose that every cycle in G is positive. Let G be the canonical form of G. Clearly [[G]] = [[G]], i.e., the constraints defined by G and by G are equivalent. It is also evident that all the cycles in G are positive. We say that a variable x is fixed in G if in this graph we have edges 0 ≤cx -→ x and x ≤-cx -→ 0 for some constant c x . These edges mean that every valuation in [[G]] should assign c x to x. If all the variables in G are fixed then the value of every cycle in G is 0, and the valuation assigning c x to x for every variable x is the unique valuation in [[G]]. Hence, [[G]], and in consequence [[G]] are not empty.

  By canonicity of H we have ( yx , c yx ) + ( x0 , c x0 ) ≥ ( y0 , c y0 ). Putting these two facts together we get (≤, 0) > (≤, d) + ( yx , c yx ) + ( x0 , c x0 ) ≥ (≤, d) + ( y0 , c y0 ) but this contradicts the choice of d which supposed that (≤, d) + ( y0 , c y0 ) is positive. The proof when the hypothetical negative cycle passes through the edge y ≤-d -→ 0 is analogous.

  xy cxy -→ y and y yxcyx -→ x are edges in G. Let d ∈ R such that d xy c xy and -d yx c yx . Then, there exists a valuation v ∈ [[G]] such that v(y) -v(x) = d. Proof. Take d as in the assumption of the lemma. Let G d be the distance graph where we have the edges x ≤d -→ y, and y ≤-d

  xy cxy -----→ y in the canonical distance graph representing Z. We denote by[v] the region to which v belongs to;[v] xy denotes the value ( xy , r xy ) of the constraint y -x xy r xy defining the region [v]. This is precisely the value of the edge x xy rxy -----→ y in the canonical distance graph representing the region [v]. We are interested in finding the least value of [v] xy from among the valuations v ∈ Z. Lemmas 3 and 4 describe this least value of [v] xy for different combinations of x and y.

B Proofs from Section 4 B. 1

 41 1. Z + 0x < Z 0x and Z + 0x ≤ (α x , ≤), or 2. Z + x0 < Z x0 and Z x0 ≥ (-α x , ≤), or 3. Z x0 ≥ (-α x , ≤) and Z + xy < Z xy and Z + xy ≤ (α y , ≤) + Z x0 Correctness of the algorithm with Closure approximation

Table 1 .

 1 Experimental results: number of visited nodes and running time with a timeout (T.O.) of 60 seconds. Experiments done on a MacBook with 2.4GHz Intel Core Duo processor and 2GB of memory running MacOS X 10.6.7.

	Model	Our algorithm UPPAAL's algorithm UPPAAL 4.1.3 (-n4 -C -o1)
		nodes	s. nodes	s.	nodes	s.
	A1	2	0.00 10003	0.07	10003	0.07
	A2	7	0.00	3999	0.60	2003	0.01
	A3	3	0.00 10004	0.37	10004	0.32
	CSMA/CD7 5031	0.32	5923	0.27	-	T.O.
	CSMA/CD8 16588	1.36 19017	1.08	-	T.O.
	CSMA/CD9 54439	6.01 60783	4.19	-	T.O.
	FDDI10	459	0.02	525	0.06	12049	2.43
	FDDI20	1719	0.29	2045	0.78	-	T.O.
	FDDI30	3779	1.29	4565	4.50	-	T.O.
	Fischer7	7737	0.42 20021	0.53	18374	0.35
	Fischer8	25080	1.55 91506	2.48	85438	1.53
	Fischer9	81035	5.90 420627	12.54 398685	8.95
	Fischer10	-	T.O.	-	T.O. 1827009	53.44

let ψ 2 be the inequation: Z y0 ≥ Z yx + (<, -α x ). From Equation 4we see that β 2 has been classified in terms of ψ 2 and ¬ψ 2 when [[G 2 ]] is not empty. Notice the subtle difference between ψ 1 and ψ 2 in the weight component involving α x : in the former the inequality associated with α x is ≤ and in the latter it is <. This necessitates a bit more of analysis before we can write β 2 in terms of ψ 1 and ¬ψ 1 .

Suppose ψ 1 is true. So we have ( yx , c yx ) ≤ ( y0 , c y0 + α x ). This implies:

For the case when c y0 = c yx -α x , note that in ψ 2 the right hand side is always of the form (<, c yx -α x ), irrespective of the inequality in Z yx and so yet again, ψ 2 is true. We have thus shown that ψ 1 implies ψ 2 .

Suppose ¬ψ 1 is true. We have ( yx , c yx ) > ( y0 , c y0 + α x ). If c yx > c y0 + α x , then clearly c y0 < c yx -α x implying that ¬ψ 2 holds. If c yx = c y0 + α x , then we need to have yx =≤ and y0 =<. Although ¬ψ 2 does not hold now, we can safely take β 2 to be -Z y0 + (<, -α x ) as its value is in fact equal to -Z yx + (<, 1) in this case. Summarizing the above two paragraphs, we can rewrite β 2 as follows:

We are now in a position to determine β as min{β 1 , β 2 }. Recall that we are in the case where Z y0 ≤ (≤, -α y ) and we have established that

] by construction, both of them cannot be simultaneously empty. Hence from Equations 3 and 5, we get β, the min{β 1 , β 2 } as:

There remains one last reasoning. To prove the lemma, we need to show that β = max{ -Z yx , -Z y0 + (<, -α x )}. For this it is enough to show the following two implications:

We prove only the first implication. The second follows in a similar fashion. Let us consider the notation ( yx , c yx ) and ( y0 , c y0 ) for Z yx and Z y0 respectively. So we have:

Definition 3 (a LU , abstraction w.r.t LU ). Let W be a set of valuations. Then,

It is shown in [START_REF] Behrmann | Lower and upper bounds in zone-based abstractions of timed automata[END_REF] that this is a sound, complete and finite abstraction, coarser than Closure. The soundness of this abstraction follows from the lemma given below.

Lemma 7. Let q be a state of A and t = (q, g, R, q 1 ) a transition. Assume that for a clock x: L(x) ≥ c for all c such that x ≥ c or x > c occurs in g; and U (x) ≥ d for all d such that x ≤ d or x < d occurs in g. Let ν and ν be valuations such that ν LU ν. Then, (q, ν) δ,t -→ (q 1 , ν 1 ) implies that there exists a delay δ and a valuation ν 1 such that (q, ν )

The relation between a LU (Z) and Extra + LU (Z) is summarized by the following.

Lemma 8. For all zones Z,

We are now in a position to prove the correctness of LU-algorithm.

Theorem 6. An accepting state is reachable in ZG(A) iff the LU-algorithm reaches a node with an accepting state and a non-empty zone.

The right to left direction is straightforward, so we concentrate on the opposite direction. Lemma 9. For every zone Z, and transition t: P ost(a LU (Z), t) ⊆ a LU (P ost(Z, t))

Proof. Pick ν 1 ∈ P ost(a LU (Z), t). There exists a valuation ν ∈ a LU (Z) such that ν t -→ ν 1 . By definition of a LU , there exists a valuation ν ∈ Z such that ν LU ν. From Lemma 7, ν

The left to right implication of the theorem follows from the next lemma and from the following invariant on the nodes of the tree that is computed. For every node n = (q, Z, L, U ):

1. if n is nottentative, then L, U are respectively the maximum of the L s , U s from all successor nodes (q s , Z s , L s , U s ) of n (taking into account guards and clock resets, even if Z s is empty); 2. if n is tentative with respect to (q , Z , L , U ), then L and U are equal to L and U respectively.