Radu Mateescu
email: radu.mateescu@inria.fr

Sylvain Rampacek
email: sylvain.rampacek@u-bourgogne.fr

Formal Modeling and Discrete-Time Analysis of BPEL Web Services

Keywords: Web services, formal specification, model checking, exhaustive simulation, process algebra

Web services are increasingly used for building enterprise information systems according to the Service Oriented Architecture (Soa) paradigm. We propose in this paper a tool-equipped methodology allowing the formal modeling and analysis of Web services described in the Bpel language. The discrete-time transition systems modeling the behavior of Bpel descriptions are obtained by an exhaustive simulation based on a formalization of Bpel semantics using the Algebra of Timed Processes (Atp). These models are then analyzed by model checking value-based temporal logic properties using the Cadp toolbox. The approach is illustrated with the design of a Web service for Gps navigation.

Introduction

Information systems present in companies and organizations are complex software artifacts involving concurrency, communication, and coordination among various applications that exchange data and participate to business processes. Service Oriented Architecture (Soa) [START_REF] Josuttis | SOA in Practice -The Art of Distributed System Design[END_REF] is a stateof-the-art methodology for developing information systems by structuring them in terms of services, which can be distributed and composed over a network infrastructure to form complex business processes. Web services are a useful basis for implementing business processes, either by wrapping existing software or by creating new functionalities as combinations of simpler ones. Bpel (Business Process Execution Language) [START_REF] Jordan | Web Services Business Process Execution Language Version 2.0 -Oasis Standard[END_REF] is a standardized language of wide industrial usage for describing abstract business processes and detailed Web services. It allows to capture both the behavioral aspects (concurrency and communication) and the timing aspects (duration of activities) of Web services.

The Bpel language allows to create Web services either from scratch, or as the composition of existing subservices, which can be invoked sequentially (one at a time) or concurrently (several ones at the same time). Each Web service described in Bpel can be used as a sub-service by other Web services (described in Bpel or not), thus en-abling a hierarchical construction of complex Web services. A Bpel business process is defined by a workflow consisting of various steps, which correspond internally to algorithmic computations (possibly with time constraints) and externally to message-passing interactions with a client. Business processes are typically built upon existing Web services (although this is not mandatory), each one being specialized for carrying out a particular task. These subservices are invoked every time a specific information is needed during a step of the workflow; therefore, a business process is not simply the set of sub-services it is built upon, but acts as an orchestrator of these sub-services in order to provide newly added functionalities.

The conjunction of concurrency and timing constraints makes business processes complex and requires a careful design in order to avoid information losses and to obtain a satisfactory quality of service. In this context, formal modeling and analysis techniques available from the domain of concurrent systems allow to improve the quality of the design process and to reduce the development costs by detecting errors as soon as possible during the business process life cycle. These techniques can operate successfully on languages equipped with a formal semantics definition, from which suitable models can be constructed and analyzed automatically.

In this paper, we propose a tool-supported approach for the formal modeling and analysis of business processes and Web services described in Bpel. Our approach consists of the following ingredients: the definition of a formal semantics of Bpel in terms of process algebraic rules, taking into account the discrete-timing aspects [START_REF] Haddad | Modelling web services interoperability[END_REF][START_REF] Haddad | A formal semantics and a client synthesis for a BPEL service[END_REF]; the automated generation of models (state/transition graphs) from the Bpel specifications using an exhaustive simulation based on the formal semantics rules, implemented in the WSMod tool; and the analysis of the resulting models by using standard verification tools for concurrent systems, such as Cadp [START_REF] Garavel | CADP 2006: A toolbox for the construction and anal-ysis of distributed processes[END_REF]. We illustrate the application of this approach to the design and discrete-time analysis of a Web service for Gps navigation.

Related work.

The modeling and analysis of Web services benefits from a considerable attention in the research community. The Wsat tool proposed in [START_REF] Fu | Analysis of interacting BPEL web services[END_REF][START_REF] Fu | WSAT: A tool for formal analysis of web services[END_REF] gives to Web service designers the possibility of verifying Ltl properties on Bpel business processes by applying the Spin model checker. Each Bpel process is transformed into a Promela model (via a pattern) and connected to other processes in the description. This work covers only the untimed aspects of Bpel.

Another approach, proposed in [START_REF] Turner | Representing and analysing composed web services using CRESS[END_REF], uses the Cress (Chisel Representation Employing Systematic Specification) notation for specifying the untimed behavior of Web services. Cress descriptions are translated into the formal description technique Lotos [START_REF] Iso/Iec | LOTOS -a formal description technique based on the temporal ordering of observational behaviour[END_REF] and analyzed with dedicated tools, such as Topo, Lola or Cadp. A direct translation from Bpel to Lotos is given in [START_REF] Ferrara | Web services: a process algebra approach[END_REF], enabling the use of the aforementioned tools for analyzing the untimed behavior of Web services. Bpel was also used as target language for producing executable Web services from Lotos specifications [START_REF] Chirichiello | Encoding abstract descriptions into executable web services: Towards a formal development[END_REF][START_REF] Salaün | Negotiation among web services using LOTOS/CADP[END_REF]; this allows to combine the advantages of the formal verification using Cadp and of the deployment and execution features of Bpel.

Compared to existing work, our approach differs in the following respects: it is based on a translation of Bpel directly into state/transition graphs, without using an intermediate language such as Promela or Lotos, thus being potentially more efficient; and it handles not only the behavioral, but also the discrete-time aspects of Bpel descriptions.

Paper outline. Section 2 presents our methodology and software platform for modeling and analyzing Bpel descriptions. Section 3 describes the Gps Web service casestudy and its analysis using the platform. Finally, Section 4 gives some concluding remarks and directions for future work.

Modeling and Analysis Approach

Web services can be seen as complex distributed systems that communicate by message-passing. Therefore, their design methodology can be naturally supported by the formal modeling and analysis techniques stemming from the domain of concurrent systems. To apply these techniques, it is necessary to represent the dynamic behavior of Web services in a formal, non-ambiguous manner.

The approach we propose for the modeling and analysis of Web services described in Bpel is illustrated in Figure 1. Our software platform consists roughly of two parts, described in the sequel: the Bpel descriptions are first translated into discrete-time Ltss using the WSMod tool, and are subsequently analyzed using the Cadp verification toolbox.

Translation from BPEL to discrete-time LTSs

The behavior of a Web service comprises not only the concurrency and communication between its various constituent activities, but also the delay of response of the service. These aspects can be modeled using dtLtss (discrete-time Labeled Transition Systems), i.e., state/transition graphs in which every transition is labeled by an action performed by the Web service. The actions are of the following kinds: emissions and receptions of messages, prefixed by ' !' and ' ?', respectively; elapsing of time, represented by the symbol χ (discrete-time tick, also noted time); the internal action τ (or tau) denoting unobservable activity of the service; and the terminating action √ (or done), which is the last internal action that a service can do. The global behavior of the Web service (and therefore, the actions it can perform) is obtained by an exhaustive simulation of the Bpel description, performed by the WSMod tool (see Figures 2,3), which is able to handle both discrete [START_REF] Haddad | Modelling web services interoperability[END_REF] and continuous [START_REF] Haddad | A formal semantics and a client synthesis for a BPEL service[END_REF] time representations. WSMod takes two different inputs (see Figure 1):

• A Web service description in Bpel [START_REF] Jordan | Web Services Business Process Execution Language Version 2.0 -Oasis Standard[END_REF], a standardized language allowing to specify the behavior of business processes. Bpel supports two different types of business processes: executable processes specify the behavior of business processes in full detail, such that they can be executed by an orchestration engine; and abstract business protocols specify the public message exchanges between the service and a client (i.e., excluding the message exchanges which take place internally, e.g., during invocations of sub-services).

• A formal representation of the Bpel semantics, based on the Algebra of Timed Processes (Atp) [START_REF] Nicollin | The algebra of timed processes ATP: Theory and application[END_REF], which specifies using operational rules how the model of the business process behavior is generated. Depending on the time representation chosen, the resulting model is either a dtLts, or a timed automaton (Ta) [START_REF] Alur | A theory of timed automata[END_REF]. The Atp rules formalizing the Bpel semantics in discretetime is shown in Table 1. For example, the process "time" can only elapse time (represented by the χ action), and the process "receive" or "reply" can send or receive a message (first rule) or elapse time too (second rule). To generate the model representing the behavior of the input Bpel description, WSMod performs an exhaustive simulation guided by the operational Atp rules. The tool is also able to synthesize automatically the model of an adapted client interacting with the Web service, whose be-havior complies with that of the service as regards emission and reception of messages, time elapsing, etc (see Figure 3). In this study, we focus only on the Web service model generation feature of WSMod in discrete time.

P ; Q a --→P ′ ; Q ∀ a, P √ ---→P ′ ∧ Q a --→Q ′ P ; Q a --→Q ′ switch switch[{P i } i∈I ] -∀ i ∈ I, switch[{P i | i ∈ I}] τ --→ P i while while[P ] τ --→ P ; while[P ] while[P ] τ --→ empty scope Let M I = {m i | i ∈ I} a set of messages and let E J = {e j | j ∈ J} a set of exceptions. scope(P, E) with E = [{(m i , P i ) | i ∈ I}, (d, Q), {(e j , R j ) | j ∈ J}] P √ ---→ scope(P,E) √ ---→0 ∀ a / ∈ {χ, √ } ∪ E X ∪ M I P a --→P ′ scope(P,E) a --→scope(P ′ ,E) d > 1, P χ --→P ′ and ∀ a∈EX ∪ {τ, √ }, ¬(P a --→) scope(P,E d ) χ --→scope(P,E d-1 ) P χ --→P ′ and ∀ a∈EX ∪ {τ, √ }, ¬(P a --→) scope(P,E 1 ) χ --→Q ∀ i ∈ I, ∀ a∈EX ∪ {τ, √ }, ¬(P a --→) scope(P,E) ?m i ----→Pi ∀ j ∈ E J , P e j ---→ scope(P,E) τ --→Rj ∀ e / ∈ E J , P e --→ scope(P,E) e --→0 pick pick[E] = scope(time, E) with E = [{(m i , P i ) | i ∈ I}, (d, Q), {(e j , R j ) | j ∈ J} flow flow[{P i } i∈I }] executes simultaneously the set of processes {P i }. ∀ a ∈ E X ∪ {τ }, ∃ j∈I, Pj a --→P ′ flow[{Pi | i∈I}] a --→flow[{Pi | i∈I\{j}}∪{P ′ }] ∀ m ∈ M, ∃ j∈I, Pj * m ----→P ′ and ∀ i =j, ∀ a∈EX ∪{τ }, ¬ ∃k∈I, (P k a --→) flow[{Pi | i∈I}] * m ----→flow[{Pi | i∈I\{j}}∪{P ′ }] ∀ i∈I, Pi √ ---→0 flow[{Pi | i∈I}] √ ---→0 ∃J =∅, J⊆I, ∀ i∈J, Pi χ --→P ′ i and ∀ i∈I\J, Pi √ ---→ flow[{Pi}i∈I ] χ --→flow[{P ′ i }i∈J ∪{Pi} i∈I\J ]

BPEL Process to ATP

This section describes shortly each algebra rule presented in Table 1. In fact, each process described here corresponds to a process in Bpel language. For readability, we do not follow the (verbose) Xml syntax of a Bpel process.

The empty process can only terminate (the notation 0 is the null process).

The time process can only elapse time (represented by the χ action).

The throw process can raise an exception. Generally, in a correct specification, the exception must the catched in some scope process.

The receive or reply process can send (!o[m]) or receive (?o[m]) a message (first rule) or elapse time too (second rule). They correspond to input/output Wsdl operations.

The sequence P ; Q process executes the process P followed by the process Q. Since the operator ";" is associative, we safely restrict the number of operands to two processes. The sequence process acts as its first subprocess while this process does not indicate its termination. In the latter case, the sequence process acts as the second process can do.

The switch[{P i } i∈I ] process chooses to execute one of P i process. In Bpel, the choice is done internally by the Web service: the client doesn't know the result of the condition evaluation. So, we translate this choice by the internal action (τ ).

The while[P ] process executes the process P as long as an internal condition is evaluated at true. Again, the client does not know the result of the condition evaluation.

The scope(P, E) process executes the process P according to some events and guards (timing and exception) defined by the Web services and represented here by the ex-

pression E = [{(m i , P i ) | i ∈ I}, (d, Q), {(e j , R j ) | j ∈ J}],
where:

• m i are the events and P i the associated processes triggered;

• d the maximum execution time unit for process P (otherwise, the process Q is executed);

• e j the exceptions that can be catched and R j the associated processes triggered.

The pick process is a particular case of scope in which there is no main process (and more precisely, only one that consist to elapse time).

The flow[{P i } i∈I }] process executes simultaneously the set of processes P i , according to the rules concerning time, exceptions, etc. In Bpel, there is a mechanism that enables the Web service to do some synchronization dependencies (links) that is not present in the rules, but taken into account in the WSMod tool.

Transition system synthesis

Transition system synthesis begins from the algebra rules (describe in Table 1) and the intermediate language (see Figure 3). This intermediate language is based on a syntactical tree. We can remark that the root of the syntactical tree is the global business process, which denotes the global behavior of the Web service. By analysing its root according to the algebra rules, we can infer a set of actions that can be executed: these actions will be represented by transitions in the dtLts. Due to the structure of the global expression representing the business process, it can be useful to repeat the analysis recursively to refine the set of actions. For example, we can take the process "?a; !b" corresponding to the reception of an "a" message, followed sequentially by the reply of a "b" message. The set of actions that a process sequence can do, depends on the first process in it. So, we must analyze, first, the process "?a". This process can do two actions: (i) the time elapsing or (ii) receiving the message "a" (see Figure 4(a)). Next, we must verify the compatibility of the process "?a" actions with each guard of sequence process, and then, determine the action set that this one can realize. Here, the two sets are identical.

The "empty; !b" process has been created during the previous step. We can simplify this process, according to the sequence algebra rules, for two reasons: (i) the "empty" process can only terminate ( √ action), and (ii) if the first sub-process of a sequence can terminate, then the sequence process executes the second sub-process. So, "empty; !b" process can become (or is equivalent to) "!b" process. The analysis of "empty; !b" and empty processes are explained respectively in Figure 4(c) and Figure 4(d).

Each step enables us to determine the global dtLts of "?a; !b" process (see details in Figure 4). The initial state is "?a; !b" and the final state is "0". Of course, each analysis step is not hard-coded, but the tool analyses the algebra rules to determine each derivate action to be executed by a given process.

Analysis of discrete-time LTSs

Once the dtLts model of the Bpel specification under design has been obtained, it can be analyzed by using standard tool environments available for concurrent systems. For our purpose, we use the Cadp (Construction and Analysis of Distributed Processes) toolbox [START_REF] Garavel | CADP 2006: A toolbox for the construction and anal-ysis of distributed processes[END_REF] dedicated to the formal specification and verification of concurrent asynchronous systems. Cadp accepts as input specifications written in process algebraic languages, such as Lotos [START_REF] Iso/Iec | LOTOS -a formal description technique based on the temporal ordering of observational behaviour[END_REF], Fsp [START_REF] Magee | Concurrency: State Models and Java Programs[END_REF][START_REF] Salaün | Translating FSP into LOTOS and networks of automata[END_REF] or Chp [START_REF] Martin | Compiling communicating processes into delay-insensitive VLSI circuits[END_REF][START_REF] Salaün | Translating hardware process algebras into standard process algebras -illustration with CHP and LOTOS[END_REF], as well as networks of communicating automata given in the Exp language [START_REF] Lang | EXP.OPEN 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods[END_REF]. These formal specifications are translated by specialized compilers into labeled transition systems (Ltss), i.e., state spaces modeling exhaustively the dynamic behavior of the specified systems. Ltss are the for-mal model underlying the analysis functionalities offered by Cadp, which aim at assisting the user throughout the whole design process: code generation and rapid prototyping, random execution, interactive and guided simulation, model checking and equivalence checking, test case generation, and performance evaluation.

An Lts can be represented within Cadp in two complementary ways: either explicitly, by its list of states and transitions encoded as a file in the Bcg (Binary Coded Graphs) format equipped with specialized compression algorithms, or implicitly, by its successor function given as a C program complying to the interface defined by the Open/Caesar [START_REF] Garavel | OPEN/CAESAR: An open software architecture for verification, simulation, and testing[END_REF] environment for graph manipulation. The explicit representation is suitable for global verification algorithms, which explore transitions forward and backward, whereas the implicit representation is suitable for local (or on-the-fly) verification algorithms, which explore transitions forward, thus enabling an incremental construction of the Lts during verification. To deal with large systems, Cadp provides several advanced analysis techniques: on-the-fly verification, partial order reductions, compositional verification, and massively parallel verification using clusters of machines.

Cadp contains currently over 40 tools and libraries for Lts manipulation, which can be invoked either in interactive mode via the Eucalyptus graphical interface, or in batch mode via the Svl [START_REF] Garavel | SVL: a scripting language for compositional verification[END_REF] scripting language dedicated to the description of complex verification scenarios. The toolbox was used for the validation of more than 100 industrial case-studies 1 .

A fragment of the MCL language

Since we focus on model checking discrete-time properties on dtLtss, we could apply in principle existing tools operating on Ltss, such as the Evaluator 3.5 [START_REF] Mateescu | Efficient onthe-fly model-checking for regular alternation-free mu-calculus[END_REF] on-the-fly model checker of Cadp, which takes as input temporal formulas expressed in regular alternation-free µ-calculus, an extension of alternation-free µ-calculus [START_REF] Emerson | Efficient Model Checking for Fragments of the Propositional Mu-Calculus[END_REF] with regular expressions over transition sequences. However, the evaluation of discrete-time properties requires the counting of time actions in the dtLts; this can be encoded in standard modal µ-calculus [START_REF] Stirling | Modal and Temporal Properties of Processes[END_REF] using fixed point operators (one operator for each counter value), but may lead to prohibitively large temporal formulas, as noticed in the framework of temporal Ccs [START_REF] Morley | Safety-level communication in railway interlockings[END_REF]. Discrete-time properties can be succinctly and naturally formulated using data-handling extensions of the modal µ-calculus, such as the Mcl language underlying the Evaluator 4.0 tool recently integrated into Cadp.

Mcl (Model Checking Language) [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] is an extension of the alternation-free µ-calculus [START_REF] Emerson | Efficient Model Checking for Fragments of the Propositional Mu-Calculus[END_REF] with regular expressions and data-handling operators. We describe below the syntax and semantics of an Mcl fragment containing modal operators equipped with extended regular expressions over 1 See the online catalog at http://www.inrialpes.fr/vasy/cadp/case-studies transition sequences, a more detailed description of the language being available in [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF]. The Mcl fragment considered consists of action formulas (noted α), regular formulas (noted ρ), and state formulas (noted φ), which characterize actions, transition sequences, and states of the dtLts, respectively. Action formulas have the following syntax:

α ::= a | true | false | ¬α | α 1 ∨ α 2 | α 1 ∧ α 2
An action formula α denotes a set of action names (transition labels) of the dtLts. The action name a denotes the singleton set containing the action a. The boolean connectors have their usual interpretation: true and false denote the set of all actions of the dtLts and the empty set; ¬α denotes the complement of the action set denoted by α; α 1 ∨ α 2 and α 1 ∧ α 2 denote the union and the intersection of the action sets denoted by α 1 and α 2 . Action formulas provide a simple, yet useful means of characterizing subsets of actions. This kind of formulas were originally introduced in action-based logics such as Actl (Action-based Computation Tree Logic) [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF]. Regular formulas have the following syntax:

ρ ::= α | nil | ρ 1 .ρ 2 | ρ 1 |ρ 2 | ρ * | ρ + | ρ{m} | ρ{m...n} | ρ{m...}
A regular formula ρ denotes a binary relation containing the couples of states which are source and target of a transition sequence in the dtLts such that the word obtained by concatenating all actions labeling the transitions of the sequence belongs to the regular language defined by ρ. The regular formula α denotes all one-step sequences consisting of a single transition labeled by an action satisfying the action formula α. The nil operator denotes the empty sequence, containing zero transitions. The concatenation ρ 1 .ρ 2 denotes the sequences containing two adjacent subsequences satisfying ρ 1 and ρ 2 , respectively. The choice ρ 1 |ρ 2 denotes the sequences satisfying either ρ 1 , or ρ 2 . The transitive reflexive closure ρ * (resp. the transitive closure ρ + ) denotes the sequences consisting of the concatenation of zero or more (resp. one or more) subsequences satisfying ρ. The bounded iterations ρ{m}, ρ{m...n}, and ρ{m...} denote the sequences consisting of the concatenation of exactly m, between m and n, and at least m subsequences satisfying ρ, respectively. These extended regular operators are similar to the operators implemented by string searching tools such as the egrep utility available on Unix systems; in practice they turn out to be as useful for describing transition sequences in dtLtss as their egrep counterparts are for describing character strings. State formulas have the following syntax:

φ ::= true | false | ¬φ | φ 1 ∨ φ 2 | φ 1 ∧ φ 2 | ρ φ | [ρ]φ | X | µX.φ | νX.φ
A state formula φ denotes a set of states of the dtLts.

The boolean connectors have the usual interpretation over the set of dtLts states. The possibility modality ρ φ denotes the states from which there is (at least) an outgoing transition sequence satisfying ρ and leading to a state satisfying φ. The necessity modality [ρ]φ denotes the states from which all outgoing transition sequences satisfying ρ must lead to states satisfying φ. The minimal fixed point operator µX.φ (resp. the maximal fixed point operator νX.φ) denote the minimal (resp. maximal) solution of the equation X = φ interpreted over the powerset lattice of the state set. Propositional variables X denote sets of states; they are bound by the fixed point operators in a way similar to quantifiers in first-order logic. The state formulas of the Mcl fragment above are similar to those of the modal µ-calculus, except for the two modalities containing regular formulas, which are inspired from dynamic logics such as Pdl (Propositional Dynamic Logic) [START_REF] Harel | Dynamic Logic[END_REF]. The usage of this Mcl fragment for specifying discretetime properties of Bpel descriptions will be illustrated in Section 3.3.

Case Study: A Web Service for GPS Navigation

We illustrate in this section the application of our approach to the modeling and analysis of a Web service dedicated to Gps navigation. Given the relative complexity of this Web service, we do not detail here its textual Bpel and Wsdl descriptions, but present its workflow graphically using the Bpmn [12] notation.

System description

The purpose of the Gps Web service is to compute itineraries from a position to a destination fixed by a user (client of the service). In addition to the requested itinerary, the user can also obtain: pictures of the travel (taken from the air), the global map of the itinerary, and various kinds of information (about traffic, radar stations, point of interest (Poi), etc). At last, the user can configure the subscription to the various kinds of information, as well as some parameters of the travel (e.g., to take motorway or not, to deviate toward a Poi, etc.). The relationships between these functionalities are represented in Figure 5. The behavior of the Gps Web service consists of two main phases, described in the sequel: the initialization phase (login, setting of the initial position and destination) and the main loop phase (management of the itinerary, modification of the parameters, etc.).

Initialization phase

The initialization phase comprises three activities: login, position and destination.

Login activity. The access to the Web service is restricted to authenticated users only. To identify itself, the user must send a couple login/password, to which the service responds by a message "Ok" or "NOk" depending whether the couple is valid or not.

Position activity. After authentication, in order to use the main functionalities of the Web service, the user must indicate where the start location of the travel is. This is done by sending a message with information about the street, city, and country where the navigation session must be started; the message must be resent until the start location is accepted by the service (message "Ok").

Destination activity. Finally, before the service may attempt to calculate an itinerary, the user must enter a destination. This is similar to the position activity above: the user must retry until the end location is accepted by the service.

Main loop phase

After the initialization phase, the service can compute an itinerary, send information about traffic, Poi, etc. To maintain the connection with the user, the service requires that the time elapsed between certain consecutive user actions does not exceed a given timeout value (a kind of "ping alive"). In Section 3.2 we will consider for analysis configurations of the system with a timeout value ranging from 1 to 60 seconds.

From the Web service point of view (see Figure 5), this timeout is managed by a "scope" process: when the timeout is reached, this process generates an exception that will be caught by another process. The main activity of this "scope" process is a "pick" process. This kind of choice enables the user to select a desired action; if we used the "switch" Bpel construct instead, the choice would be made by the Web service and not by the user. Furthermore, the "scope" is encapsulated into a "while", enabling the user to do more than one operation during the session (notice that the first action carried out by the service when entering the "while" is the emission of a ready message to the user). Finally, the "while" is the main activity of a second "scope", that catches the first exception thrown when the timeout is reached.

The activities executed by the main loop are partitioned in two modes, described in the sequel: the navigation mode (obtaining the itinerary, modifying the current position or destination, getting a picture or a roadmap), and the configuration mode (subscribing to a Poi, getting information on radars or traffic, setting of parameters).

Navigation mode. In navigation mode, the user can change the current position and the destination (using the same procedure as for the initialization phase). Next, the user can ask for the itinerary, a picture, the roadmap, or enter in configuration mode. There are two types of answer for itinerary requests: either a complete itinerary leading from the current position to the destination, with various information (about street, radar, Poi, etc.) depending on the user subscriptions, or simply a destination message indicating that the current position is (near) to the destination. The requests for picture and roadmap allow the user to obtain an air-picture of the area (in Png format) or a veritable roadmap (in Svg format).

Configuration mode. In configuration mode, the user can subscribe or cancel his subscription to information about Poi, radar or traffic. This information is added to the itinerary if necessary. Additionally, the user can set various parameters, such as the kind of the itinerary (on motorway or not), etc.

Discrete-time LTS synthesis

Starting from the Bpel description of the Gps Web service, we apply the WSMod tool in order to obtain a dtLts on which the verification tools of Cadp will operate. We show below the dtLts model obtained for a timeout of 1 second, then we study its variation in size as the timeout value increases, and finally we discuss the behavior of the Web service w.r.t. the ambiguity detection feature implemented in WSMod.

Discrete-timed labeled transition system. dtLts models represent the observable behavior of Web services. The actions labeling the dtLts transitions denote the messages exchanged (emissions and receptions are prefixed by ' !' and ' ?', respectively), the elapse of a discrete-time unit χ (or time), the internal action τ (or tau), and the termination action √ (or done). The global behavior of the Web service is obtained by an exhaustive simulation of the Bpel description driven by the Atp rules given in Table 1. The dtLts obtained in this manner for the Gps Web service with a timeout value of 1 second is shown in Figure 6.

Variation of DTLTS size with the timeout value.

The size of the dtLts (number of states and transitions) depends on several aspects of the Bpel description: the number of Bpel processes, their complexity and nesting, the amount of communications, and the values of the timeouts. For the sake of readability, we have shown in Figure 6 the dtLtss for a timeout of 1 second (corresponding to one χ in discrete-time), but we carried out verification also for larger values of the timeout. The figure above shows the variation of the dtLts size for timeout values ranging from 1 to 60. We observe a linear increase of both the number of states and transitions; this is a consequence of the fact that the Bpel description contains a single timeout (according to the Atp rules). In the presence of multiple, overlapped timeouts, the size of the dtLts may increase much more quickly.

Non ambiguous Web service. In this study, we focus on the verification of the Web service behavior. However, the WSMod tool can also synthesize automatically a dtLts modeling the behavior of an adapted client interacting with the Web service, provided that the model of the service respects certain properties (concerning non ambiguity in message exchanges, time elapsed, etc.) detailed in [START_REF] Haddad | Modelling web services interoperability[END_REF]. Here, the Gps Web service is identified as non ambiguous by WSMod, meaning that the tool can synthesize an adapted client that can know, on each message exchange, the exact choice made on the service side, and therefore the client and the service can evolve without any deadlocks or mismatches.

Verification of discrete-time properties

We analyze below the behavior of the Gps Web service (considering a timeout of 50 seconds) by means of discretetime model checking using the Evaluator 4.0 [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] tool of Cadp. Table 2 illustrates the formulation in Mcl of several safety and liveness properties, of both untimed and timed nature. The colored parts of the formulas indicate discrete-time properties, which involve the counting of time actions. All properties were successfully verified on the corresponding dtLts of the system, which has 535 states and 1473 transitions.

Safety properties: they specify informally that "something bad never happens" during the execution of the system. In the Mcl language, these properties can be expressed in a concise manner by identifying the undesirable execution sequences, characterizing them using extended regular expressions, and forbidding their existence in the dtLts model using necessity modalities.

Properties S 1 and S 2 concern the ordering of actions during the initialization phase: S 1 specifies that the user cannot set the position or the destination before logging in successfully, and S 2 states that after requesting the position or the destination, the Web service cannot begin the main loop before receiving an appropriate answer from the user. Properties S 3 and S 4 deal with the main loop phase: S 3 forbids the user to make another request before the current one (here, an itinerary demand) has been handled by the service, and S 4 states that a demand cannot be fulfilled anymore by the service after the timeout has expired.

Liveness properties: they specify informally that "something good eventually happens" during the execution of the system. In Mcl, these properties contain diamond modalities and minimal fixed point operators for encoding the existence of certain desirable execution sequences (potentiality) or trees (inevitability) in the dtLts.

Properties L 1 and L 2 concern the initialization phase: L 1 specifies that after the user has logged in, the Web service will eventually ask for the position, the destination, or end the initialization, and L 2 states that after the initialization was finished the service will end up in the main loop or decide to terminate the session. Properties L 3 and L 4 deal with the main loop phase: L 3 indicates that as long as the timeout has not expired, the service can still prompt for a user request, and L 4 states that an expiration of the timeout eventually interrupts the connection. The AF p operator of Ctl [START_REF] Clarke | Model Checking[END_REF] expressing the inevitable reachability of a state p is defined in µ-calculus as µX.p ∨ ( true true ∧ [true]X).

Conclusion and Future Work

The design of complex business processes according to the Soa approach requires to carefully take into account the presence of concurrency, communication, and timing constraints induced by the interaction of Web services. To facilitate the design process, we propose here a toolequipped methodology for modeling and analyzing Web services described in Bpel. We focus on the behavioral and discrete-time aspects of Web services, and rely upon the model-based verification technologies stemming from the concurrency domain. The state/transition models of Bpel Web services are produced automatically by the WSMod tool, which implements an exhaustive simulation algorithm based on a formalization of Bpel semantics by means of process algebraic rules. The tool is able to handle both discrete and continuous time constraints; for the moment we handle only discrete-time models, which can be analyzed using the Evaluator 4.0 model checker [START_REF] Mateescu | A model checking language for concurrent value-passing systems[END_REF] of the Cadp toolbox [START_REF] Garavel | CADP 2006: A toolbox for the construction and anal-ysis of distributed processes[END_REF]. Discrete-time safety and liveness properties can be concisely expressed using the datahandling facilities of the Mcl language accepted as input by Evaluator 4.0, and particularly the extended regular expressions over transition sequences, which allow to count tick actions occurring in the model. We illustrated the verification of discrete-time properties on the example of a Gps Web service; however, most of them can be easily adapted for other business processes described in Bpel. Our methodology enables the Web service designers to carry out formal analysis on complex Web services before publishing them, and thus to improve the quality of the design process.

We plan to continue our work along several directions. Firstly, we can improve the connection between WSMod and Cadp by producing implicit dtLtss according to the interface defined by Open/Caesar [START_REF] Garavel | OPEN/CAESAR: An open software architecture for verification, simulation, and testing[END_REF]. This would enable on-the-fly verification, which allows to detect errors in large systems without constructing the complete dtLts model beforehand but exploring it in a demand-driven way. Secondly, using discrete-time models allows to directly reuse the tools available for data-based temporal logics, such as Evaluator 4.0; however, this may lead to state explosion in the presence of numerous timeouts. An alternative solution would be to use continuous time models; this can be achieved by connecting the time automata produced by WSMod with the Uppaal [START_REF] Larsen | Uppaal in a Nutshell[END_REF] tool dedicated to the verification of continuous time models. Finally, we will extend the methodology to handle compositions of multiple Web services, following our previous work on automated client synthesis [START_REF] Melliti | Verifying correctness of web services choreography[END_REF], but focusing on the verification of composition. For this purpose, the compositional verification techniques available in tools such as Exp.Open [START_REF] Lang | EXP.OPEN 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods[END_REF] will be certainly useful.

Figure 1 :Figure 2 :Figure 3 :

 123 Figure 1: Platform for Web service modeling and analysis

Figure 4 :

 4 Figure 4: Actions set synthesis example for the process ?a; !b, in discrete time.

Figure 5 :

 5 Figure 5: Functionality workflow of the Gps Web service

Figure 6 :

 6 Figure6: dtLts model of the Gps Web service, with zoom on the initialization phase. The action !GoodJourney makes the link between the initialization phase and the main loop phase.

S 2 [ 3 [ 4 [ 4 [

 2344 (true * . ((!getP osition.(¬?setP osition) * ) | (!getDestination.(¬?setDestination) * )) . !GoodJourney) ] false S true * .?getItinerary.(¬(!Itinerary ∨ !Destination)) * . (?getP icture ∨ ?getRoadM ap ∨ ?conf igM ode ∨ ?setP osition ∨ ?setDestination ∨ ?getItinerary) ] false S true * .?getItinerary.(¬(!Itinerary ∨ !Destination)) * . (time.(¬(!Itinerary ∨ !Destination)) * ){51} . (!Itinerary ∨ !Destination) ] false L 1 [ true * .!LoginOk ] AF !getP osition ∨ !getDestination ∨ !GoodJourney true L 2 [ true * .!GoodJourney.(τ ∨ time) * ] (τ ∨ time) * . !Ready ∨ !bye true) L 3 [ true * .!Ready. time{ 0 ... 50 } ] true * .!P icture ∨ !RoadM ap ∨ !Itinerary ∨ !Destination true L true * .!Ready. ((¬(!Itinerary ∨ !Destination ∨ !P icture ∨ !RoadM ap)) * .time){51} ] AF !ConnectionError true

Table 1 :

 1 The process algebra formalizing BPEL, in discrete-time

	BPEL empty time throw	ATP empty √ ---→ 0 time χ --→ time ∀ e ∈ E X , throw[e] --→ 0 e with E X set of exceptions that can be thrown.
	receive / reply sequence ( ; )	* o[m] ∀ a = * m ----→ empty with * ∈ {?, !} * o[m] χ --→ * o[m] √ , P a --→P ′

Table 2 :

 2 Safety and liveness properties of the Gps Web service (timeout of 50 sec.)

	Prop.	Mcl formula
	S 1	[ (¬!LoginOk)

* .?setP osition ∨ ?setDestination ] false


Marlène Rippe

Talitha F Stefanello

Vanessa Kaplum

Elizandra A Britta

Francielle P Garcia

Mychelle Robin Poirot

V P Companhoni

Celso V Nakamura

Anna Szarpak-Jankowska

Rachel Auzély-Velty

Mychelle V P Companhoni

Heparosan as a potential alternative to hyaluronic acid for the design of biopolymer-based nanovectors for anticancer therapy

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

Introduction 1

Self-assembled nanogels, nanometer-sized hydrogels obtained 2 by physical self-assembly of interactive hydrophilic polymers, have 3 attracted growing interest for drug delivery as these systems 4 combine the advantages of hydrogels with nanoscale formulations. 1- 5 5 These soft nanoparticles (NPs) can be designed to facilitate the 6 encapsulation of diverse classes of bioactive compounds, and their 7 hydrophilic shell can be exploited to control their biological behavior 8 and targeting ability. In this regard, nanogels made of amphiphilic 9 polysaccharides hold promise as versatile nanocarriers due to the presence of various functional groups on shell-forming polysaccharides in addition to their unique physicochemical properties, including biocompatibility and biodegradability. 1,6 Among polysaccharides, glycosaminoglycans such as hyaluronic acid and chondroitin sulfate (CS) are being used increasingly to design self-assembled nanoparticles for tumor-targeted drug delivery. [7][8][9][10][11][12][13][14][15][16] These two GAGs can indeed be specifically recognized by cell surface CD44 receptors that are over-expressed by several cancer cells [17][18][19][20] .

Yet, these polysaccharides also bind to other receptors in the human body, such HA receptor for endocytosis (HARE) that facilitates efficient receptor-mediated endocytosis 21,22 . Moreover, CD44 and 21 other variants are also expressed on a wide variety of normal cell 22 types, including epithelial cells and haematopoietic cells. [23][24][25][26] In this HA-CD44 interactions to selectively deliver cytotoxic drugs to cancer 25 cells, 27 observing the uptake of their HA-derived nanoparticles into 26 CD44-expressing tumors and in other organs, i.e. liver and spleen 28, 27 29 . Based on this, they rationally modified HA through its N-28 deacetylation and selective sulfation to investigate the potential to 29 minimize interaction of HA with CD44, with the aim of achieving 30 maximum tumor accumulation. 27

31

In this study, we explored the possibility of using heparosan as a 32 potential alternative to HA for designing nanogels as drug carriers for 33 tumor-targeted drug delivery. This was motivated by the "stealthty" 34 properties of this GAG, [30][31][32][33] although its chemical structure is very 35 similar to HA. Indeed, Hep has a repeating disaccharide unit of D-36 glucuronic acid (GlcA) and N-acetyl-D-glucosamine (GlcNAc) residues 37 such as HA, but the α-1,4 bond between the GlcA and the GlcNAc 38 units replaces the β-1,3 bond found in HA (Scheme 1). Moreover, 39 since Hep is the natural precursor to the heparin/heparan sulfate 40 biosynthesis, it is biocompatible. This non-sulfated GAG appears to 41 be biologically inert in the extracellular spaces; indeed, it is not 42 known to participate in biological binding interactions. 31 Please do not adjust margins Please do not adjust margins cell, which avoids accumulation in the body. 31 The peculiar features They were prepared in a very straightforward way using thiol-ene was kindly provided by Ciba Speciality Chemicals (Basel, Switzerland).

13

Sulfo-Cyanine7 amine (Cy7-amine) was purchased from Lumiprobe.

44

The critical aggregation temperature (CAT) of the HA-and Hep-

Please do not adjust margins

Please do not adjust margins

Self-assembly into well-defined nanostructures is also reflected in

23 regard,

 23 Bhattacharya et al. recently raised the question of exploiting

24

 24

1 of

 1 Hep have recently attracted interest for its use as a potential 2 alternative to poly(ethylene glycol) (PEG) in the design of 3 nanocarriers for passive tumor targeting in anticancer therapy.4 Indeed, though the modification of nanoparticles with PEG is a widely 5 adopted approach to extend blood circulation time and improve drug 6 efficacy, several papers from the past decade have suggested that 7 PEG can elicit antibody formation against PEG (anti-PEG) and can also 8 trigger complement activation. 34-37 Therefore, to propose alternative 9 stealth nanoparticles, some research teams developed NPs by the 10 self-assembly of Hep modified with deoxycholic acid, cholesterol or 11 the anticancer drug doxorubicin (DOX). 30, 32, 33, 38 These authors 12 showed potential of these systems for intracellular delivery of DOX 13 in vitro. Furthermore, incubation of heparosan-based drug delivery 14 systems with different cancer cells revealed that these nanocarriers 15 have different uptake and subcellular distribution behavior in tumor 16 cells. 32 However, the in vivo behaviour of the nanocarriers was not 17 investigated. Besides these self-assembled NPs, Hep-coated 18 liposomes were also prepared by post-insertion of Hep-lipid 19 conjugates. 39 Interestingly, these liposomes loaded with DOX were 20 shown to impair tumor growth in a mouse breast cancer model 21 similar to PEG-coated DOX-liposomes, supporting the idea of using 22 Hep as a shell-forming polysaccharide of nanocarriers for anti-cancer 23 therapy. 24 In this work, we designed Hep-and HA-based nanogels possessing 25 similar properties in terms of chemical composition (except the 26 hydrophilic shell), size and morphology to best assess the effect of 27 the outer shell-forming GAG on their in vivo biodistribution and 28 tumor-targeting efficiency after intravenous administration in 29 Ehrlich solid tumor-bearing mice. The nanogels were prepared by 30 temperature-induced self-assembly of Hep and HA suitably modified 31 with a thermoresponsive ethylene glycol-based copolymer (Scheme 32 1). Such temperature-triggered approach allows spontaneous 33 nanogel formation due to the dehydration of the grafted copolymer 34 chains when heated above the cloud point temperature (Tcp). Herein, 35 we synthesized a copolymer of di(ethylene glycol) methacrylate and 36 butylmethacrylate (poly(DEGMA-co-BMA)) exhibiting a Tcp well 37 below the room temperature by judiciously adjusting the 38 comonomer ratio. This allowed obtaining stable nanogels at room 39 temperature as required for good handling and biological 40 application. Shell-crosslinked (SCL) nanogels were also designed to 41 increase their colloidal stability (Scheme 1).

Scheme 1 .

 1 Scheme 1. Strategy for the synthesis of un-crosslinked and shell-crosslinked nanogels based on heparosan and hyaluronic acid modified with poly(DEGMA-co-BMA) (Heppoly(DEGMA-co-BMA) and HA-poly(DEGMA-co-BMA)). A) Grafting of the thermoresponsive copolymer on Hep and HA using radical thiol-ene chemistry; B) formation of nanogels by temperature-triggered self-assembly of modified Hep and HA, and C) shell-crosslinking using radical thiol-ene chemistry.

1 chemistry

 1 40, 41 allowing i) the coupling of the thiol-end functionalized 2 copolymer with the polysaccharide modified with alkene groups and, 3 ii) the subsequent crosslinking of the shell-forming polysaccharide by 4 reaction of a bi-functional thiol reagent with the remaining alkene 5 groups. The Hep and HA nanogels were then carefully characterized 6 in terms of size, morphology and cytotoxicity. Finally, their in vivo 7 biodistribution was evaluated by near-infrared fluorescence imaging 8 to shed some light on the role of GAGs on the in vivo fate of the 9 nanogels. To our knowledge, this study provides the first comparison 10 of the in vivo behavior of HA and Hep-based nanoparticles that differ 11 only in the hydrophilic outer shell.

12

 12

14 26 Analytical techniques 27 1H 7 for 5 23 solution ( 4 ´ 25 (porosity 4 ), the solution was dialyzed against deionized water 26 ( 62 Scanning electron microscopy and transmission electron 63 microscopy 64 For

 262775234254266264 Dulbecco's Modified Eagle's Medium (DMEM), L-glutamine and 15 fetal bovine serum (FBS) were provided by Gibco. All chemicals, 16 except DEGMA and BMA which were purified by running them 17 through a column packed with aluminum oxide, were used without 18 any further purification. The positively charged resin, 19 diethylaminoethyl cellulose (DEAE Sepharose CL-6B) was purchased 20 from GE Healthcare Life Science. Spectra/Por 1 (MWCO 6-8000 21 g/mol) membrane used for dialysis was obtained from Fisher 22 Scientific (Rancho Domingez, CA). The water used in all experiments 23 was purified by a Elga Purelab purification system, with a resistivity 24 of 18.2 MΩ cm. Deuterium oxide (D2O) and deuterated 25 dichloromethane (CDCl3) were obtained from SDS (Vitry, France). NMR spectra were recorded at 5, 25 or 80 °C using a Bruker 28 AVANCE III HD spectrometer operating at 400 MHz. All spectra were 29 recorded by applying a 45° tip angle for the excitation pulse, and a 30 10 s recycle delay. Chemical shifts (δ in ppm) are given relative to 31 external tetramethylsilane (TMS = 0 ppm) and calibration was 32 performed using the signal of the residual protons of the solvent as 33 a secondary reference. Fourier transform infrared spectroscopy 34 (FTIR) measurements were performed on a RX1 spectrometer 35 (Perkin Elmer, UK) with horizontal ATR accessory. For each sample, 36 32 scans were recorded between 4000 and 400 cm -1 with a resolution 37 of 2 cm -1 using the Spectrum software V 5.0.0. The spectra was then equipped with a HeNe laser at 173° and a temperature controller. A 59 solution of HA-poly(DEGMA-co-BMA) or Hep-poly(DEGMA-co-BMA) 60 in PBS at a concentration of 0.5 mg/mL was filtered through a 0.45 61 µm polycarbonate filter and heated from 10 to 40 °C using a 5 °C 62 interval. The CAT was considered to be the temperature at the 63 intersection between the lower horizontal portion of the plotted 64 curve (average scattered intensity versus temperature dependence) 65 and the tangent line of the curve. The size and size distribution of 66 nanogels were simultaneously measured with the CAT by dynamic 67 light scattering (DLS) using a Zetasizer NanoZS Malvern Instruments 68 apparatus operating with a HeNe laser at 173°. The hydrodynamic 69 diameters were calculated from diffusion coefficients using the 70 Stokes-Einstein equation. All correlogram analyses were performed 71 with software supplied by the manufacturer. All the measurements 72 were performed in PBS (pH 7.4, [NaCl] = 0.15 M). 73 Synthesis of poly(DEGMA-co-BMA) 74 DEGMA (10 g, 50 mmol) and BMA (0.398 g, 2.79 mmol), the RAFT 75 agent 2-Cyano-2-propyl benzodithioate (0.082 g, 0.372 mmol) and 76 AIBN (3 mg, 0.0186 mmol) in anhydrous toluene (25 mL) were placed 77 in a round bottom Schlenk flask and oxygen was removed via 78 bubbling the mixture under nitrogen atmosphere for 30 min. Then, 79 the flask was sealed and placed in a thermostatic oil bath pre-heated 80 at 80 °C. The reaction was quenched by cooling and exposure to 81 oxygen. The resulting copolymer was precipitated in cyclohexane. 82 The precipitate was dissolved in dichloromethane and the copolymer 83 was precipitated again in cyclohexane. The resulting precipitate was 84 finally dried under high vacuum to give 6 g of pure poly(DEGMA-co-85 BMA). Samples taken before and during the polymerization were 86 analyzed by 1 H NMR to determine monomers conversion. The Mn, 87 Mw and Đ values of the copolymer were determined by size exclusion 88 chromatography in DMF. 89 Synthesis of HA-poly(DEGMA-co-BMA) and Hep-poly(DEGMA-co-90 BMA) 91The pentenoate modified HA20 (Mw = 20 kg/mol) and Hep30 (Mw = 92 30 kg/mol) derivatives with a degree of substitution of 0.5 were 93 synthesized as previously described.41 The poly(DEGMA-co-BMA) 94 copolymer was subjected to aminolysis using n-butylamine, to 95 convert the RAFT end-group to a thiol. Briefly, the copolymer (600 96 mg, 0.375 mmol) was solubilized in dichloromethane (9 mL) and n-97 butylamine (6.5 mL, 66 mmol) was added. After 5 min under stirring 98 at room temperature, the reaction mixture was concentrated under 99 reduced pressure, resulting in a waxy liquid that was solubilized in 100 dichloromethane. The copolymer was recovered by precipitation in 101 cyclohexane and dried under vacuum at 45 °C during 4 hours to 102 remove residual solvent. Next, the thiol-end-functionalized 103 copolymer (550 mg, 0.0312 mmol) was solubilized in 14 mL of pure 104 water and TCEP (10 mg, 0.0350 mmol) was added. After 30 min of Please do not adjust margins Please do not adjust margins stirring at 4 °C under nitrogen atmosphere, the copolymer solution 1 was added to an aqueous solution of pentenoate modified HA or 2 pentenoate modified Hep (50 mg, 0.116 mmol) in pure water (4 mL), 3 followed by a solution of Irgacure 2959 (2 mL) in water (10 g/L) in 4 order to obtain a final photoiniator concentration of 0.1 % (w/v) in 5 the reaction media. The reaction mixture cooled in a ice bath, was 6 exposed to UV light (λ = 365 nm) with an intensity of 20 mW/cm 2 min under stirring and nitrogen atmosphere. The resulting HA-8 poly(DEGMA-co-BMA) and Hep-poly(DEGMA-co-BMA) derivatives 9 were purified via a batch ion exchange process using DEAE Sepharose 10 CL-6B as a weak-anion exchanger. Briefly, DEAE resin (20 mL), stored 11 in a solution of ethanol 30 %, was washed three times with ultrapure 12 water at 4 °C (3 ´ 20 mL, contact times of 10 min). Excess liquid was 13 removed by centrifugation (10000 rpm, 10 min) at 4° C. Then, the 14 resin was activated by successive washes with a 0.5 M NaCl aqueous 15 solution (20 mL), a 1 M NaCl aqueous solution (20 mL) and finally, 16 four times with ultrapure water (4 ´ 20 mL). The HA-poly(DEGMA-17 co-BMA) or Hep-poly(DEGMA-co-BMA) derivative was then added to 18 the resin in a conical tube and allowed to interact with the resin overnight at 4°C under stirring with an orbital shaker. Then, the HA 20 or Hep derivative bound to the resin was subjected to seven washes 21 with ultrapure water (7´ 20 mL) to remove un-grafted copolymer.22Finally, the HA or Hep derivative was eluted with a 1 M NaCl aqueous 10 mL). After filtration of the solutions of the HA or Hep 24 derivative through a Buchner funnel with a porous glass filter plate membrane with cut-off 6-8 Da MW, 72 h). The product was 27 recovered by freeze-drying as a white powder. 28 Synthesis of crosslinked nanogels 29 To a solution of HA-poly(DEGMA-co-BMA) or Hep-poly(DEGMA-co-30 BMA) (0.015 g, 0.022 mmol) with a DS of 0.03 at a concentration of 31 0.5 g/L in PBS (pH 7.4) at 4°C under nitrogen atmosphere in an ice 32 bath, 564 µL (1.41 mg, 0.009 mmol) of a solution of DTT in PBS (2.5 33 g/L) was added under stirring. Next, the temperature of the solution 34 was increased to 40°C (above the CAT). After stirring at 40°C for 45 35 min, 3.3 mL of an aqueous solution of Irgacure 2959 (10 mg/mL) was 36 then added to the nanogels suspension to obtain a final photoiniator 37 concentration of 10 % (w/v). The mixture was exposed to UV light ( and its absorbance was determined by spectrophotometry at 530 58 nm. The polysaccharide concentration was calculated from a 59 calibration curve (0.050 to 0.200 g/L), which allowed the indirect 60 determination of copolymer amount in the HA-and Hep-61 poly(DEGMA-co-BMA) samples. SEM analysis, drops of un-crosslinked and crosslinked nanogels 65 solutions (0.5 mg/mL) in ultrapure water at both 5 and 40 °C were 66 deposited onto mica-coated copper stubs (also precooled/heated at 67 5 or 40 °C, respectively) and allowed to air drying at 5 or 40 °C. The 68 samples were then coated by approximately 2 nm of sputtered Au-69 Pd and observed in secondary electron imaging mode with a ZEISS 70 Ultra 55 FEG-SEM (Grenoble INP -CMTC). Images were acquired at 71 low voltage of 3 kV using an in-lens detector. For TEM analysis, all 72 samples were dispersed in ultrapure water, stained with 5 % uranyl 73 acetate and observed with a JEOL JEM 1400 (Jeol, USA) transmission 74 electron microscope operating at 120 kV acceleration voltage. 75 Labeling of nanogels based on HA-poly(DEGMA-co-BMA) and Hep-76 poly(DEGMA-co-BMA) with sulfo-cyanine7 77 Fluorescent nanogels were prepared by grafting the dye Cy7-amine 78 on un-crosslinked and crosslinked nanogels based on HA-79 poly(DEGMA-co-BMA) and Hep-poly(DEGMA-co-BMA) by an amine-80 acid coupling reaction using DMTMM as a coupling agent 42 . To this 81 end, crosslinked nanogels (0.008g, 0.0135 mmol) were solubilized in 82 water/DMF (1:1 v/v; 4 mL) and DMTMM (3.7 mg, 0.0135 mmol) was 83 added to the solution, followed by adjusting the pH to 6.5. After 30 84 min of stirring, Cy7-amine (0.5 mg, 0.000676 mmol) solubilized in 85 water/DMF (1:1 v/v) at a concentration of 5 g/L was

20 mice.39

 20 After tumor grown period (≈10 days), animals were 21 anesthetized with isoflurane 2% in an air/O2 mixture, and 100 µL of 22 suspensions of Cy7-labeled uncrosslinked and crosslinked HA and 23 Hep NGs (3 g/L in PBS) were administered in the tail vein. For 24 comparison, Cy7-labeled HA (Mw = 20 and 40 kg/mol) and Hep (Mw = 25 30, 3 g/L in PBS) were also injected. Immediately after injection, mice 26 were evaluated using an In-vivo MS FX PRO (Carestream Molecular 27 Imaging, Carestream Health, United States). Fluorescent images (λ 28 exc = 750 nm; λem = 790 nm) were obtained with a CCD camera 29 (Kodak Image Station) at 0, 1, 3 and 24 h post-injection. Mice were 30 then sacrificed and the main organs (liver, spleen, lung, kidney, heart, 31 bladder and tumor) were removed for ex-vivo imaging. Images 32 acquisition and semi-quantification of relative fluorescence intensity 33 in regions of interest (ROI) were performed using Carestream 34 Molecular Imaging 5.0 software (Carestream Molecular Imaging, The copolymer poly(DEGMA-co-BMA) was prepared via the 40 reversible addition-fragmentation chain transfer (RAFT) process ) monomers using 2,2-azobis(2-43 methylpropionitrile) (AIBN) as an initiator and 2-cyano-2-propyl 44 benzodithioate (CPB) as a chain transfer agent (CTA) (Scheme 2A). A 45 DEGMA/BMA ratio of 95:5 was selected to obtain a copolymer 46 exhibiting a Tcp well below the room temperature and thereby, 47 allowing formation of nanogels at room temperature (i.e. ~ 25 °C). 1 H 48 NMR analysis was conducted to monitor the copolymerization 49 kinetics. The kinetic plots proved that, in these reaction conditions, 50 CPB allowed a good control over the RAFT copolymerization of 51 DEGMA and BMA (Figure S1).

Scheme 2 . 57 1 9 (

 2579 Scheme 2. Synthetic pathway to Hep-and HA-poly(DEGMA-co-BMA). A) Synthesis of poly(DEGMA-co-BMA) via the RAFT process; B) Grafting of the thermoresponsive copolymer

24 25Figure 1 . 1 H29

 2411 Figure 1. 1 H NMR spectra (400 MHz, 6 mg/mL in D2O) of Hep-poly(DEGMA-co-26 BMA) (A) and HA-poly(DEGMA-co-BMA) (B) at 5°C.27

Figure 2 .

 2 Figure 2. Temperature responsiveness of Hep-and HA-poly(DEGMA-co-BMA). A) 41 Dynamic light scattering analysis of Hep and HA-poly(DEGMA-co-BMA) solutions 42 in PBS (Cp = 0.5 g/L) at 37 °C. B) TEM image of Hep NGs in water at 40 °C (Cp = 0.5 43 g/L).

1 6

 6 the sharp decrease of the polydispersity index (PdI) above the CAT as 2 well as in the values of mean diameter in different distributions 3 (intensity and number distribution) and of Z-average size, which are 4 similar. In contrast, strong discrepancies between the mean size 5 values are observed below the CAT. Synthesis and characterization of shell-crosslinked nanogels Please do not adjust margins Please do not adjust margins In vitro cytotoxicity, in vivo biodistribution and tumor targeting of 1 crosslinked and uncrosslinked Hep-NGs and HA-NGs 2 The in vitro cytotoxicity of un-crosslinked and shell-crosslinked Hep 3 NGs and HA NGs, as well as of native HA and Hep, was evaluated in 4 Vero cells after 72 h of incubation by MTT assay. For all the samples, 5 the toxic concentration for 50 % of the cells was higher than 1000 6 μg/mL, the maximum assessed concentration, demonstrating the 7 very low cytotoxicity and biocompatibility of our HA and Hep 8 derivatives (Figure S6).

9 19 ( 20 (

 1920 The in vivo biodistribution and tumor targeting of Hep-and HA-based 10 nanogels were then evaluated in Ehrlich solid tumor (EST)-bearing 11 mice 45 by a non-invasive fluorescence imaging system. The main 12 characteristics of the nanogels in terms of mean size and PdI near 13 body temperature are summarized in Table 1. Importantly, the 14 similar size of both HA-and Hep-based un-crosslinked nanogels as 15 well as of both crosslinked ones together with their similar chemical 16 composition, except the hydrophilic shell structure, allowed a proper 17 comparison of the biodistribution of HA-and Hep NGs. The nanogels 18 and the native polysaccharides, HA (Mw = 20 and 40 kg/mol) and Hep Mw = 30 kg/mol), were labeled with the NIR dye Sulfo-Cyanine7 Cy7) to visualize their biodistribution. Briefly, the samples were 21 chemically modified with Cy7-amine using 4-(4,6-dimethoxy-1,3,5-22 triazin-2-yl)-4-methylmorpholinium chloride as an amine-acid 23 coupling agent. 46 The content of Cy7 molecules in the polysaccharide 24 derivatives (DS) was 0.002, as determined by UV/Vis spectroscopy at 25 680 nm. After Cy7 labeling, the nanogels maintained their size as 26 shown by nanoparticle tracking analysis (NTA), 47 which enables the Particle size distribution obtained by NTA ranged from 60 to 250 with 29 an average of 150 ± 40 nm and from 60 to 300 with an average of 30 190 ± 43 nm for the SCL NGs based on HA and Hep, respectively 31 (Figure S7).

  32

4 5Figure 7 . 6 Fluorescence 8 Fluorescence 11 * 16 ( 7 ) 21 crosslinked Hep-NG. 22 Conclusion 23 In

 476811167212223 Figure 7. In vivo biodistribution of Hep-and HA-NGs in Ehrlich solid tumor-bearing mice.6

  Moreover,

	a. Univ. Grenoble Alpes, Centre de Recherches sur les Macromolécules Végétales (CERMAV-CNRS), 601, rue de la Chimie, BP 53, 38041 Grenoble Cedex 9 (France)	43
		it has no known extracellular degradation pathway and thus, it is
		47

44

stable in the bloodstream contrary to HA and heparin/heparan 45 sulfate which are degraded by enzymes in the blood. On the other 46 hand, Hep is degraded by lysosomal enzymes following entry into the * E-mail: rachel.auzely@cermav.cnrs.fr b. Laboratory of technological innovation in the development of pharmaceuticals and cosmetics, State University of Maringa, Colombo Avenue, 5790, 87020-900, Maringa, Brazil Electronic Supplementary Information (ESI) available: [details of any supplementary information available should be included here]. See DOI: 10.1039/x0xx00000x

Table 1 .

 1 Size and polydispersity of nanogels based on Hep-poly(DEGMA-co-BMA) and

	33
	34	HA-poly(DEGMA-co-BMA) determined by dynamic light scattering at 40 °C (0.5 g/L in
	35	PBS).
			Nanogels	Z-Average size (nm)	PdI
		HA	Un-crosslinked nanogels	108 ± 1	0.174 ± 0.03
			Crosslinked nanogels (1 eq DTT)	151 ± 2	0.176 ± 0.01	86
		Hep	Un-crosslinked nanogels	119 ± 1	0.095 ± 0.006	87	organism as it is the biosynthetic precursor of heparin and heparan
			Crosslinked nanogels (1 eq DTT)	146 ± 2	0.095 ± 0.013	88	sulfate. Therefore, as Hep is biologically inert in the extracellular
	36					89	environment, it can circulate in the bloodstream for a prolonged
	37		Time-dependent biodistribution of Cy7-labeled native Hep, HA	90	period of time. In this regard, it was previously reported that its half-
	38	and nanogels on EST-bearing mice was observed after intravenous	91	life can vary from 15 h to 2 days depending on its molar mass (60 or
	39	administration. Ex vivo fluorescence images of excised organs and	92	100 kg/mol). 60 As a result, the prolonged circulation of Hep in the
	40	tumors showed a higher accumulation of Hep NGs in the tumor than	93	bloodstream may increase its probability of reaching the tumor
		HA NGs. As shown in Figure 7A, the intensity ratio of tumor-to-liver	94	tissue after systemic administration in vivo as well as that of Hep
	42	between 1 h and 24 h was in the order un-crosslinked Hep NGs >	95	NGs.
		crosslinked Hep NGs > un-crosslinked HA NGs » crosslinked HA NG,	96	Finally, comparison of un-crosslinked and crosslinked NGs did not
		suggesting lower liver uptake and higher tumor accumulation for the		show significant differences in their in vivo fate, despite the slightly

44

nanogels based on Hep. These results were consistent with those the major site of circulating HA uptake and degradation in contrast 81 to Hep which does not bind to HARE 21 . Actually, Hep stands out 82 among other GAGs (HA, CS, heparin, dermatan sulfate) that 83 selectively interact with HARE, resulting in their clearance from 84 circulating lymph and blood. 21 This unique feature of Hep may be 85 related to the fact this GAG is only temporarily present in the 97 higher size and presumably decreased deformability of the 98 crosslinked nanogels (Figure 7C, 7F). All together, these results 99 demonstrate that the HA and Hep NGs exhibit the same in vivo Please do not adjust margins Please do not adjust margins 3 promising as nanocarriers for cancer diagnosis and treatment.

visualization and recording of nanoparticles in solution (FigureS7).

uncrosslinked and crosslinked HA-as well as Hep-NGs and native polysaccharides (HA

and Hep) (n = 3). The results were expressed as mean ± SD. One-way ANOVA followed

poly(DEGMA-co-BMA) conjugates was determined by measuring the In order to avoid a fast destabilization of the nanogels structure after in the blood or by the interaction with blood components, the polysaccharide shell of Hep and HA NGs was crosslinked using thiolene chemistry by reaction of the remaining pentenoate groups with dithiothreitol (DTT) as a bis-thiol crosslinker (Figure 4A). This crosslinking step was performed under relatively dilute conditions (Cp = 0.5 g/L) to avoid inter-nanogel coupling, and by varying the [SH]/[=] ratio from 1 to 2 to ensure that all nanogels were sufficiently crosslinked to be stable at low temperature. Comparison of 1 H NMR spectra before and after the thiol-ene reaction with DTT provided evidence of successful shell-crosslinking (Figure 4B). Indeed, the addition of thiols to alkenes during the crosslinking step leads to the formation of thioether bonds and concomitantly, to the disappearance of the double bonds of the pentenoate groups.

Consequently, the intensity of the alkene protons at 5.9 and 5. Successful crosslinking was further confirmed by FT-IR spectroscopy (Figure S4). In the IR spectra of the crosslinked nanogels, additional bands at 839 cm -1 and 911 cm -1 are observed after reaction with DTT, which can be attributed to C-S bend, C-S stretching and H-C-S bend, respectively. The new band observed at 1253 cm -1 (CH2 vibrations) also suggests incorporation of DTT. [19][20] Temperature responsiveness of crosslinked nanogels obtained from native polysaccharides (Figure 7B). Indeed, as can be 46 seen from Figure 7B, the intensity ratio of tumor-to-liver is much


Hugo Herbelin
email: hugo.herbelin@inria.fr

Gyesik Lee
email: gslee@ropas.snu.ac.kr

Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus

Keywords: Intuitionistic Gentzen-style sequent calculus, Kripke semantics, completeness, cut-elimination

We give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-free intuitionistic sequent calculus as formal system and by combining soundness with completeness, we obtain an executable cut-elimination procedure. The proof, which has been formalised in the Coq proof assistant, easily extends to the case of the absurdity connective using Kripke models with exploding nodes.

Introduction

The intuitionistic completeness proofs for intuitionistic full first-order predicate logic given by Veldman [START_REF] Veldman | An intuitionistic completeness theorem for intuitionistic predicate logic[END_REF] and Friedman [START_REF] Troelstra | Constructivism in Mathematics: An Introduction I and II[END_REF]Chapter 13] use nonstandard Kripke model and Beth model, respectively (the false formula may be forced at some nodes). Both the proof of Veldman and that of Friedman work by building a model made of infinite contexts. Especially, they had to deal with language extensions and work with spreads in order to meet some closure conditions for disjunction and existential quantification:

-Γ ⊢ A ∨ B implies Γ ⊢ A or Γ ⊢ B. -Γ ⊢ ∃x A(x) implies Γ ⊢ A(c) for some constant c.
Note however that this is not only the case for intuitionistic proofs, but also the case for a classical, Henkin-type proof given in Troelstra and van Dalen [2, Chapter 2].

On the other hand, C. Coquand [START_REF] Coquand | From Semantics to Rules: A Machine Assisted Analysis[END_REF] shows that an intuitionistic proof for intuitionistic propositional logic with implication as a sole logical symbol can be obtained in a much simpler way by building a universal model made of finite contexts of formulae. She gave a mechanised proof of the completeness proof and even got a cut-elimination proof by using some interpreter and inversion functions, a method called "normalisation by evaluation" in general, cf. [START_REF] Berger | Normalisation by Evaluation[END_REF]. They correspond to the soundness and the completeness, respectively, of the propositional logic with implication as sole connective w.r.t. Kripke semantics. The completeness result there is strong in two ways: in the traditional sense that it holds in arbitrary contexts (see [START_REF] Troelstra | Constructivism in Mathematics: An Introduction I and II[END_REF]) and in a sense (due to Okada [START_REF] Okada | A uniform semantic proof for cut-elimination and completeness of various first and higher order logics[END_REF]) that it builds normal proofs. In this paper, we extend C. Coquand's idea to the intuitionistic first-order predicate logic with implication and universal quantification as logical symbols.

The predicate system used here is a Gentzen-style sequent calculus. The advantage is that the notion of normal proofs is easy to define: one just has to remove the cut rule. More precisely, the calculus we consider is the intuitionistic restriction LJT of a sequent calculus named LKT that Danos et al [START_REF] Danos | LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of the classical implication[END_REF] derived from an analytical decomposition of Gentzen's LK within Girard's Linear Logic [START_REF] Girard | Linear logic[END_REF]. LKT is a constrained variant of LK. Its main property is the bijective correspondence between its set of cut-free proofs and the set of normal forms3 of classical natural deduction [START_REF] Parigot | Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction[END_REF]. LJT itself is a constrained variant of LJ and its main property is the bijective correspondence between its set of cut-free proofs and the set of normal forms of natural deduction [START_REF] Herbelin | A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure[END_REF][START_REF] Herbelin | Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de λ-termes et comme calcul de stratégies gagnantes[END_REF]. By choosing LJT and its cut-free variant as our reference calculus, we emphasise that our completeness theorem builds not any arbitrary proofs but cut-free ones in a subset of LJ which bijectively maps to normal natural deduction proofs (and hence to normal λ-terms).

We show that the strong completeness holds both for the system with or without (⊥ i ). In case of with (⊥ i ), we adopt Veldman's modified Kripke semantics. Both proofs are intuitionistic and almost the same. Therefore, we can get a very simple cut-elimination proofs as a by-product at the end. A main difference compared with Veldman's or Friedman's proof is that we deal with contexts made of formulae, not just of sentences, therefore we need to handle substitutions.

The Kripke models we are considering are Kripke models with constant domain, i.e. with the domain function D being the same for every world:

D = D(w) for all w.
As a consequence, in the case of universal quantification, considering of all possible future worlds is not necessary and the following simpler definition

w ∀x A(x) iff, for all d ∈ D, w A(d).
gets equivalent, by monotonicity of forcing and invariance of the domain, to the standard definition: w ∀x A(x) iff, for all w ′ ≥ w and for all d ∈ D, w ′ A(d).

This paper is organised as follows. We first prove the soundness of the Kripke semantics with respect to cut-free LJT. Then give a intuitionistic strong completeness proof which results in the intuitionistic completeness proof. Finally, an intuitionistic cut-elimination process is described.

The sequent calculus LJT

Let L = L(C, F, P) be a first-order language with an infinite set C of individual constants, among them a distinguished constant c 0 , a non-empty set F of functions, and a non-empty set P of predicates. The logical symbols are the implication → and the universal quantification ∀. We assume furthermore that there are countably many free variables. Terms, formulae and sentences are defined in the usual way. We follow the convention that A(x) denotes the formula A where the variable x might appear. Any two formulae are considered identical when they are different only in names for bound variables. A variable or a constant is called fresh in a formula A or a context Γ when it does not occur free or at all, respectively. Definition 1 (Simultaneous substitutions). Let ρ be a function from finite set of variables to the set of terms.

1. Given a term t, t[.\ρ] is inductively defined:

-x[.\ρ] = ρ(x) if x ∈ dom(ρ), x otherwise. -c[.\ρ] = c for any c ∈ C. -(f t 1 • • • t n )[.\ρ] = f (t 1 [.\ρ]) • • • (t n [.\ρ]).

Given a formula A, A[.\ρ] is inductively defined:

-

(P t 1 • • • t n )[.\ρ] = P (t 1 [.\ρ]) • • • (t n [.\ρ]). -(A → B)[.\ρ] = (A[.\ρ] → (B[.\ρ]). -(∀x A)[.\ρ] = ∀x (A[.\ρ -x ]
). Here ρ -x denotes the function obtained from ρ with dom(ρ -x ) = dom(ρ)\{x}, i.e., if y ∈ dom(ρ) and x = y, then ρ -x (y) = ρ(y) and undefined otherwise. We also take care of variable capture by changing bound variables when necessary.

Given a formula

A(x), we use A x (t) or A[x\t] for A[.\ρ] where ρ = {(x, t)}.
We also consider substitution of a term t for a constant c in a similar way and use the notation A c (t).

The Gentzen-style sequence calculus LJT is obtained from the intuitionistic sequent calculus LJ by restricting the use of the left introduction rules of the implication and the universal quantification. See Table 1 for the cut-free fragment.

In that way, one can get a one-to-one correspondence between cut-free proofs in LJT and normal terms in λ-style calculus.

In LJT, a sequent has one of the forms Γ ; A ⊢ C or Γ ⊢ C, where Γ is a list of formulae. That is, the location of a formula occurring multiple times is important. The right side of ";" in the antecedence is called stoup . Γ, Γ ′ , ∆, ... Proof. By a simple simultaneous induction on deduction.

Γ ; Ax(t) ⊢ C Γ ; ∀x A(x) ⊢ C (∀ ℓ ) Γ ⊢ A(x) x fresh in Γ Γ ⊢ ∀x A (∀r)
⊑ Γ ′ . 1. Γ ⊢ C implies Γ ′ ⊢ C. 2. Γ ; A ⊢ C implies Γ ′ ; A ⊢ C.

⊓ ⊔

The following lemma says that a fresh constant is as good as a fresh variable and will play an important role in the proof of the strong completeness.

Lemma 4. Given a context Γ , a formula A(x), and a constant c fresh in Γ and A(x), Γ ⊢ A x (c) implies Γ ⊢ A x (y) for any variable y which is not bound in Γ, A.

Proof. It follows directly from the lemma just before.

⊓ ⊔

Kripke semantics

Kripke semantics was created in the late 1950s and early 1960s by Saul Kripke [START_REF] Kripke | A Completeness Theorem in Modal Logic[END_REF][START_REF] Kripke | Semantical considerations on modal and intuitionistic logic[END_REF]. It was first made for modal logic, and later adapted to intuitionistic logic and other non-classical systems. In this section we discuss Kripke models for the first-order predicate logic with implication and universal quantification as sole logical symbols and their connection with intuitionistic validity.

Definition 5. A Kripke model is a quadruple K = (W, ≤, , D, V ), W inhab- ited, such that 1. (W, ≤) is a partially ordered set.
2. D is an inhabited set, called the domain of K.

3. Let the language be extended with constant symbols for each element of D.

Then is a relation between W and the set of prime sentences in the extended language such that

(w ≤ w ′ ∧ w P d 1 • • • d n ) ⇒ w ′ P d 1 • • • d n
where w, w ′ ∈ W, P ∈ P, d 1 , ..., d n ∈ D, and n = arity(P ).

4. V is a function such that -V (c) ∈ D for all c ∈ C. -V (f ) : D arity(f ) → D for all f ∈ F.
An association ρ based on K is a function from a finite set of variables to D.

Given an association ρ, each term has an interpretation in D:

-

x [ρ] = ρ(x) if x ∈ dom(ρ), V (c 0 ) otherwise. -c [ρ] = V (c) for any c ∈ C. -(f t 1 • • • t ℓ ) [ρ] = V (f )(t 1 [ρ]) • • • (t ℓ [ρ]).
The forcing relation is then inductively extended by the forthcoming clauses to all L-formulae.

-

w (P t 1 • • • t n )[ρ] iff w P (t 1 [ρ]) • • • (t n [ρ]). -w (A → B)[ρ] iff, for all w ′ ≥ w, if w ′ A [ρ], then w ′ B [ρ]. -w (∀x A)[ρ] iff, for all d ∈ D, w A [ρ(x → d)].
Here ρ(x → d) denotes the association ρ ′ such that ρ ′ (y) = ρ(y) if y = x and ρ ′ (x) = d. The definition of forcing is extended to contexts as follows:

w Γ [ρ] iff w A [ρ] for all A ∈ Γ , Remark 6. There are two points to be mentioned.

1. The forcing relation is upward monotone, i.e., if w ≤ w ′ and w A [ρ], then

w ′ A [ρ]. 2.
As mentioned in the introduction, the forcing definition at the universal quantification case is much simpler than the usual definition, where the domain depends on worlds:

w (∀x A(x))[ρ] iff, for all w ′ ≥ w and d ∈ D(w), w ′ A [ρ(x → d)].
Indeed, they are "functionally equivalent" in the sense that soundness and completeness hold in both cases.

We consider a formulation of Kripke semantics for sequent calculus built on two kinds of judgements Γ ⊢ C and Γ ; A ⊢ C. Theorem 7 (Soundness). We have the following soundness. Proof. By a simultaneous induction on the deduction.

⊓ ⊔

Completeness

In this section we present a constructive completeness proof by constructing a simple universal model. First we construct a universal model for which a strong completeness holds.

Definition 8 (Universal Kripke model). The universal Kripke model U = (W u , ⊑, u , D u , V u ) is defined as follows:

-W u is the set of all contexts.

-⊑ denotes the sub-context relation, i.e., Γ ⊑ Γ ′ holds when, for all

A ∈ Γ , A ∈ Γ ′ . -D u consists of all closed terms. -V u (c) = c for all c ∈ C, and V u (f )(t 1 , ..., t ℓ ) = f t 1 • • • t ℓ for all f ∈ F and t 1 , ..., t ℓ ∈ D arity(f ) u -Γ P t 1 • • • t ℓ if Γ ⊢ P t 1 • • • t ℓ . It is obvious that Γ ⊑ Γ ′ and Γ ⊢ P t 1 • • • t ℓ imply Γ ′ ⊢ t 1 • • • t ℓ .
Theorem 9 (Strong Completeness). Let Γ be a context of sentences, A a formula, and ρ an association based on K u such that F V (A) ⊆ dom(ρ). Then

1. If Γ A [ρ] then Γ ⊢ A[.\ρ]. 2. If, for all formula C and context Γ ′ such that Γ ⊑ Γ ′ , Γ ′ ; A[.\ρ] ⊢ C implies Γ ′ ⊢ C, then it holds that Γ A [ρ].
Proof. Given the assumptions we prove both claims by a simultaneous induction on the complexity of A. Note first that t [ρ] = t[.\ρ] for any term t occurring in A since F V (A) ⊆ dom(ρ).

case:

A is a prime formula. Then the first claim is obvious. For the second claim take just Γ ′ := Γ and C := A[.\ρ].

case:

A = A 1 → A 2 . -Assume Γ (A 1 → A 2 ) [ρ]. To show Γ ⊢ A 1 [.\ρ] → A 2 [.\ρ], it suffices to prove that A 1 [.\ρ], Γ ⊢ A 2 [.\ρ]. Note that the i.h. on A 1 for the second claim implies that A 1 [.\ρ], Γ A 2 [ρ]
. Indeed, the premise of the second claim holds trivially for any Γ ′ such that A 1 [.\ρ], Γ ⊑ Γ ′ . This in turn implies that A 1 [.\ρ], Γ A 2 [ρ] by the assumption. Then the i.h. on A 2 for the first claim leads to the goal.

-Assume for all formula C and context

Γ ′ such that Γ ⊑ Γ ′ , Γ ′ ; A 1 [.\ρ] → A 2 [.\ρ] ⊢ C implies Γ ′ ⊢ C. Assume furthermore that Γ ⊑ ∆ and ∆ A 1 [ρ].
Then it remains to show ∆ A 2 [ρ]. For that we apply the i.h. on A 2 for the second claim. Let C be a formula and

∆ ′ a context such that ∆ ⊑ ∆ ′ , assume ∆ ′ ; A 2 [.\ρ] ⊢ C. Note that ∆ ⊢ A 1 [.\ρ] by i.h. on A 1 for the first claim, hence ∆ ′ ⊢ A 1 [.\ρ] by the Weakening Lemma 2. By applying (→ ℓ ) we get ∆ ′ ;(A 1 → A 2 )[.\ρ] ⊢ C, so ∆ ′ ⊢ C
holds by the assumption.

case:

A = ∀x B(x). -Assume Γ (∀x B) [ρ], i.e., for all closed term t, Γ B [ρ(x → t)]. To show Γ ⊢ ∀x (B[.\ρ -x ]), we need to prove that Γ ⊢ (B[.\ρ -x ])[x\y] for some variable y fresh in Γ and B[.\ρ -x ]. For this we show Γ ⊢ (B[.\ρ -x ])[x\c]
for some constant c and apply Lemma 4. Let c be a constant fresh in Γ and

B[.\ρ -x ]. Note first that (B[.\ρ -x ])[x\c] = B[.\ρ -x (x → c)] = B[.\ρ(x → c)]
since the values of ρ are closed terms. However, Γ ⊢ B[.\ρ(x → c)] follows from the i.h. on B for the first claim. 4-Assume for all formula C and context Γ ′ such that Γ ⊑ Γ ′ , it holds that In the intuitionistic predicate logic with implication and universal quantification as sole connectives, the Kripke semantics with constant domain is functionally equivalent to the usual Kripke semantics where the domain depends on worlds in the sense that soundness and completeness hold in both cases.

Γ ′ ; ∀x (B[.\ρ -x ]) ⊢ C implies Γ ′ ⊢ C.
Proof. The exactly same proofs for soundness and completeness hold with the usual Kripke models. ⊓ ⊔ Remark 13. We furthermore believe that, in the first-order predicate language with →, ∧ and ∀ as sole connectives, the usual Kripke semantics is equivalent to the Kripke semantics with constant domain in the sense that each usual Kripke model can be transformed into an equivalent Kripke model with a constant domain.

Remark 14. The completeness above easily extends to the case of the absurdity connective

Γ ⊢ ⊥ Γ ⊢ C (⊥ i )
using modified Kripke models with exploding nodes à la Veldman. A modified Kripke model K = (W, ≤, , D, V ) is defined as the (unmodified) Kripke model, but with one change:

-

w (P t 1 • • • t n )[ρ] iff (w P (t 1 [ρ]) • • • (t n [ρ]) or w ⊥).
The universal Kripke model is defined in the same way as before, but with the following additional clause:

-Γ ⊥ iff Γ ⊢ ⊥.
Then nothing new is involved in the proof of completeness, the construction proceeds as before. Note only that Γ ⊢ ⊥ implies Γ ⊢ A for any formula A.

On the other hand, if we include the absurdity rule and want to stick to the (unmodified) Kripke semantics, we have to give up constructiveness in the proof above. This is because we have to deal only with consistent context Γ , i.e., Γ ⊥. However, it is in general undecidable to check if a context is consistent or not. In the implication case of the strong completeness, we had to make case distinction between A 1 [.\ρ], Γ ⊢ ⊥ or not. This maybe is not so surprising because, in the full first-order predicate logic, an intuitionistic completeness proof entails Markov's Principle, a non-intuitionistic principle, see Kreisel [START_REF] Kreisel | On Weak Completeness of Intuitionistic Predicate Logic[END_REF].

Cut admissibility

In this section we consider only sentences and contexts of sentences. Then the cut-rule is admissible with/without (⊥ i ).

Theorem 15 (Cut admissibility). Γ ⊢ A and Γ ; A ⊢ B imply Γ ⊢ B.

Proof. By the Strong Completeness it suffices to show Γ B. But this follows from the Soundness applied on the two assumptions. Note also that ⊢ denotes a cut-free system.

⊓ ⊔

Conclusion

We extended C. Coquand's proof of soundness and completeness for implicative natural deduction w.r.t. Kripke semantics [START_REF] Coquand | From Semantics to Rules: A Machine Assisted Analysis[END_REF] to the case of predicate logic with implication and universal quantification. We could show that omitting disjunction and existential quantification from the intuitionistic first-order predicate logic results, as it was the case for C. Coquand, in a significantly simple, intuitionistic completeness proof with respect to (also simplified) Kripke semantics.

The fact that all of the proofs given in this paper are intuitionistic has been verified in the proof assistant Coq, cf. [START_REF] Bertot | Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions)[END_REF]. Indeed, the whole work is formalised, so that we can get a mechanical process producing cut-free proofs. The formalisation is performed using cofinite quantification for fresh variables and a locally named approach with two kinds of names for variables, one for free variables and the other for binders. The formalisation is publicly available from the web page of the first author, directory code/kripke.

Proof.Lemma 3 .

 3 One can easily prove both claims by a simultaneous induction on the deduction. ⊓ ⊔ Let Γ be a context, A, C formulae, and c a constant. 1. Γ ⊢ C implies Γ c (y) ⊢ C c (y) for any variable y which is not bound in Γ, A. 2. Γ ; A ⊢ C implies Γ c (y) ; A c (y) ⊢ C c (y) for any variable y which is not bound in Γ, A, C.

1 .

 1 if Γ ⊢ C then, for all w and ρ, w Γ [ρ] implies w C [ρ]. 2. if Γ ; A ⊢ C then, for all w and ρ, (w Γ [ρ] and w A [ρ]) implies w C [ρ].

Corollary 10 .

 10 Given a closed term t, we have to show that Γ B [ρ(x → t)]. In order to apply the i.h. on B for the second claim assume furthermore that a formula C and a context Γ ′ are given such that Γ ⊑ Γ ′ and Γ ′ ; B[.\ρ(x → t)] ⊢ C. Note that B[.\ρ(x → t)] = B[.\ρ -x ][x\t] since only closed terms are substituted. Therefore, it holds that Γ ′ ; ∀x (B[.\ρ -x ]) ⊢ C. Then by the main assumption, Γ ′ ⊢ C. The i.h. implies Γ B [ρ(x → t)]. ⊓ ⊔ For any context Γ of sentences, Γ Γ . Proof. The second claim of the strong completeness and the rule (Contr) implies that Γ A for any A ∈ Γ . ⊓ ⊔ Theorem 11 (Completeness). Let Γ be a context of sentences and A a sentence. If for all Kripke model K and a world w in K, w Γ implies w A, then Γ ⊢ A. Proof. It follows from the Strong Completeness and the fact that Γ Γ , i.e., Γ ⊢ A iff Γ A. ⊓ ⊔ Corollary 12.

Table 1 .

 1 Cut-free LJT

vary over lists of formulae. We write A ∈ Γ when A occurs in Γ . Γ ⊑ ∆ denotes that, for all A, A ∈ Γ implies A ∈ ∆. Γ c (t) is obtained from Γ by replacing each formula A with A c (t).

Lemma 2 (Weakening and Exchange). Let A, C be formulae and Γ, Γ ′ two contexts such that Γ

To be precise: normal forms along a call-by-name reduction semantics.

Γ ; A ⊢ A (Ax) Γ ; A ⊢ C A ∈ Γ Γ ⊢ C (Contr) Γ ⊢ A Γ ; B ⊢ C Γ ; A → B ⊢ C (→ ℓ ) A, Γ ⊢ B Γ ⊢ A → B (→r)

One can see here that we don't need any quantification in the definition of w ∀x A(x).