Dominique Larchey-Wendling

Bounding resource consumption with Gödel-Dummett logics

Gödel-Dummett logic LC and its finite approximations LCn are the intermediate logics complete w.r.t. linearly ordered Kripke models. In this paper, we use LCn logics as a tool to bound resource consumption in some process calculi. We introduce a non-deterministic process calculus where the consumption of a particular resource denoted • is explicit and provide an operational semantics which measures the consumption of this resource. We present a linear transformation of a process P into a formula f of LC. We show that the consumption of the resource by P can be bounded by the positive integer n if and only if the formula f admits a counter-model in LCn. Combining this result with our previous results on proof and counter-model construction for LCn, we conclude that bounding resource consumption is (linearly) equivalent to searching counter-models in LCn.

Introduction

Gödel-Dummett logic LC and its finitary versions (LC n ) n>0 are the intermediate logics (between classical logic CL and intuitionistic logic IL) characterized by linear Kripke models. LC was introduced by Gödel in [START_REF] Gödel | Zum intuitionistischen Aussagenkalkül[END_REF] and later axiomatized by Dummett in [START_REF] Dummett | A Propositional Calculus with a Denumerable matrix[END_REF]. It is now one of the most studied intermediate logics and has been recognized recently as one of the fundamental t-norm based fuzzy logics [START_REF] Hajek | Metamathematics of Fuzzy Logic[END_REF]. Proof-search in LC has benefited from the development of proof-search in intuitionistic logic IL with two important seeds: the contraction-free calculus of Dyckhoff [START_REF] Dyckhoff | Contraction-free Sequent Calculi for Intuitionistic Logic[END_REF][START_REF] Dyckhoff | A Deterministic Terminating Sequent Calculus for Gödel-Dummett logic[END_REF][START_REF] Avellone | Duplication-Free Tableau Calculi and Related Cut-Free Sequent Calculi for the Interpolable Propositional Intermediate Logics[END_REF] and the hyper-sequent calculus of Avron [START_REF] Avron | A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus[END_REF][START_REF] Metcalfe | Goal-Directed Calculi for Gödel-Dummett Logics[END_REF]. Two recent contributions propose an alternative approach based on a set of local and strongly invertible proof rules (for either sequent [START_REF] Larchey-Wendling | Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic[END_REF] or hyper-sequent [START_REF] Avron | A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus[END_REF][START_REF] Baaz | Hypersequent Calculi for Gödel Logics -A Survey[END_REF] calculus) and a semantic criterion to decide irreducible (hyper)-sequents and eventually build a counter-model.

In our previous work, we proposed a new approach to the decision problem in LC [START_REF] Larchey-Wendling | Counter-model search in Gödel-Dummett logics[END_REF]. We transform a formula (or a sequent) of LC into a conditional bi-colored graph of the same size. Then, we search counter-models of the initial formula by looking for chains of a certain kind in the graph. We call those chains alternating chains. This method constitutes a decision procedure for LC and LC n , thus we have a linear transformation of the decision problem for LC (and also LC n ) into the search for alternating chains problem in conditional graphs. Moreover, we propose a procedure based on matrix computation to solve the search of alternating chains [START_REF] Larchey-Wendling | Gödel-Dummett counter-models through matrix computation[END_REF].

In this paper, we study the reverse transformation. First, we characterize the search for alternating chains in conditional graphs as a resource use bounding problem in some particular process calculus: the processes have nondeterministic branching, conditional branching, consume some particular resource, and can be recursive. The conditions are expressed by boolean formulae. We show how to normalize process systems being thus able to view theses processes as conditional graphs. We relate resource consumption by processes to the search for alternating chains in conditional graphs.

Then we show how to encode a conditional graph into a formula of LC (of size linear w.r.t. the size of the graph). We prove the equivalence of the existence of a counter-model for this formula and the existence of an alternating chain into the conditional graph. Therefore we obtain a linear transformation of the search for alternating chains problem in conditional graphs into a decision problem for the family of logics LC n .

Moreover, this result establishes a characterization of the family of Gödel-Dummett logics LC n as resource use bounding logics for some particular process calculus. This is the main goal of this paper: to shed some new light of LC and to relate it with processes and resource consumption. In particular, the process calculus we introduce here should not be viewed as a real tool to model complex systems. However, it could be extended or integrated to other process calculi like CCS [START_REF] Milner | Communication and Concurrency[END_REF] so as to exploit the LC logic for specifying resource related properties.

Logical syntax for CL and LC

In this section we present the syntax we use for logical formulae. We either use formulae of classical propositional logic CL or formulae of propositional Gödel-Dummett logic LC. Fortunately they share the same syntax, even though their semantics differ.

The set of propositional formulae, denoted Form, is defined inductively, starting from a set of propositional variables, denoted by LVar, with an additional bottom constant ⊥ denoting absurdity and using the connectives ∧, ∨ and ⊃:

Form : f ::= ⊥ | x | f ∧ f | f ∨ f | f ⊃ f where x ∈ LVar
We use the abbreviations ¬f ≡ f ⊃ ⊥ and ⊤ ≡ ¬⊥. In conditional graphs (see sections 4 and 6), we even use the notation x ≡ ¬x but only for propositional variables. The semantics of classical formulae is as usual: given a valuation (or interpretation) of propositional variables σ : LVar → {0, 1}, the semantic value of f denoted by [[f ]] σ ∈ {0, 1} is defined inductively on the structure of f , the connectives ⊥, ⊃, ∧ and ∨ being respectively interpreted by their corresponding boolean operator. The semantics of the formulae of LC will be defined later in section 5.1.

In this section, we present a calculus for processes which consume resources. This calculus features non-determinism, choices, recursion and of course resource consumption. We only model one kind of resources in our calculus, denoted by a big dot •. The processes only consume resources, they do not produce them, neither do they transform them into another kind of resources. So the behavior of processes is characterized by how they consume resources.

Let us consider a set of process variables denoted PVar. We define the set of processes Proc as follows:

Proc : P ::= X | <f > P | • P | [P + • • • + P ] where f ∈ Form, X ∈ PVar
The process • P should be viewed as the process which consumes one resource • and then, behaves as P . The process [P + Q] should be understood as the non-deterministic sum of P and Q, i.e. the process that behaves either as P or Q. In particular, the process [ ] does nothing, i.e. does not consume any resource. Given a boolean condition f , the process <f > P is the process which behaves like P if the condition f is fulfilled, and does nothing otherwise.

Non-determinism and conditions are sufficient to represent the if-then-else construct: if

f then P else Q ≡ [<f > P + <¬f > Q].
We insist on the fact that the boolean value of the condition f does not evolve during the execution of processes: it is fixed once and for all before the execution starts. And as we are going to describe the operational semantics of processes, it should be noted that conditions (like f ) are external : even though they influence the behavior of processes, they cannot change because of that behavior.

Process systems and recursion

To represent recursion, i.e. the possibility for processes to become themselves again after having consumed some resources, we use (sets of) recursive equations: Definition 1 (Process system). A process system is a pair (E, V) where E = {X 1 = P 1 , . . . , X n = P n } is a finite set of process equations. X 1 , . . . , X n are supposed are to be n distinct process variables and V ⊆ {X 1 , . . . , X n } is a subset of relevant variables. P 1 , . . . , P n are processes. The variables occurring in E but not in V are called private variables. A sub-process of E is either one of X 1 , . . . , X n or a sub-term of one of P 1 , . . . , P n .

As an example, consider the system

V = {X} E =    X = • <a> Y Y = [<b> X + <¬a> • Z + Z] Z = [ ] [<b> X + <¬a> • Z + Z] X <b> X [ ] Y <a> Y • <a> Y Z • Z <¬a> • Z
The sub-processes are listed on the right-hand side. Intuitively, X is the process which consumes one resource and if a is true becomes Y . Y becomes either X

P -[0, σ, E] -• P [Id] Pi -[n, σ, E] -• Q [ • • • + Pi + • • • ] -[n, σ, E] -• Q [Sum] P -[n, σ, E] -• Q • P -[n + 1, σ, E] -• Q [Res] P -[n, σ, E] -• Q X = P ∈ E X -[n, σ, E] -• Q [Eq] P -[n, σ, E] -• Q [[f ]] σ = 1 <f > P -[n, σ, E] -• Q [Con]
Fig. 1. Deduction system for resource consumption if b is true, or if a is false consumes one resource and then becomes Z, or Y becomes Z. Z is the process that does nothing. This calculus should not be viewed as useful for representing real or complex systems. It has too few features for that. But it could be viewed as an abstraction calculus: either one could abstract a complex system into our simple formalism to prove resource consumption related properties for this particular system, or one could extend our calculus with further constructs to model more sophisticated systems directly.

Operational semantics for resource consumption

Given a set of process equations E and a valuation σ : LVar → {0, 1} of boolean variables, we define the ternary relation -[•, σ, E] -• ⊆ Proc × N × Proc by the set of deduction rules presented in figure 1. As the reader might notice, σ and E are not modified by the application of those rules but they occur in the side conditions of rules [Eq] and [Con], restricting the applicability of those rules. When E or σ are understood in the context, we might simplify the notation

P -[n, σ, E] -• Q into P -[n, σ] -• Q or even P -[n] -• Q. Intuitively, P -[n] -• Q
should be read as: the process P has an execution path to Q which consumes exactly n times the resource •.

Lemma 1. The [Cut] rule is admissible:

P -[m] -• Q Q -[n] -• R P -[m + n] -• R [Cut]
Proof. We prove the result by induction on the length of the deduction of

P -[m] -• Q. If P -[m] -• Q is obtained by the axiom [Id], then Q ≡ P and m = 0, thus P -[0 + n] -• R is identical to Q -[n] -• R. If P -[m] -• Q is ob-
tained by the [Res] rule then P ≡ • P ′ and we have a shorter (sub-)deduction of

P ′ -[m -1] -• Q. By induction, P ′ -[m -1 + n] -• R is deducible and then, ap- plying rule [Res], we obtain • P ′ -[m -1 + n + 1] -• R, thus P -[m + n] -• R.
If the last rule is [Eq], then P ≡ X with X = P ′ ∈ E and we have a sub-deduction of P ′ -[m] -• Q. Thus, by induction, we obtain a deduction of

P ′ -[m + n] -• R.
Applying rule [Eq], we obtain a deduction of P -[m + n] -• R. The cases of rules [Sum] and [Con] are similar. ⊓ ⊔ Definition 2 (Boundable resource use). A process system (E, V) has a resource use boundable by n if there exists a valuation σ :

LVar → {0, 1} such that for any X, Y ∈ V and k ∈ N, if X -[k, σ, E] -• Y holds then k n.
This definition means that the resource use can be bounded in some context, modeled by the valuation σ. The resource use is not necessarily bounded in every context.

Normalization

We define the equivalence of process systems and a normalization procedure so that the systems appear in a shape suitable for further transformations. The process systems (E, V) and (F, V) are equivalent if for any valuation σ, the relations

-[•, σ, E] -• and -[•, σ, F] -• have identical restrictions to V × N × V.

Definition 3 (Normality). A process equation is normal if it contains no nested construct, i.e. it has one of the following forms:

X = • Y , X = <f > Y or X = [Y 1 + • • • + Y n ]
where Y and the Y i 's are process variables. A process system is normal if all its equations are normal.

Lemma 2 (Normalization). Let (E, V) be a process system of size k. There exists a normal process system (E ′ , V) of size O(k) which is equivalent to (E, V).

Proof. Let (E, V) be a process system of size k. We build the set of equations of the system E ′ . Let us introduce a new process variable X P for each strict (i.e. not a process variable) sub-process P of E. For process variables P ≡ Y occurring in E, we choose X Y ≡ Y , so there is no new process variable for atomic sub-processes. Let P be a sub-process of E.

If P ≡ • Q, we add the equation X P = • X Q to E ′ . If P ≡ <f > Q, we add X P = <f > X Q and if P ≡ [Q 1 + • • • + Q k ], we add X P = [X Q1 + • • • + X Q k ]. Finally, if Y = P is an equation of E, we add the equation Y = [X P ] to E ′ .
Obviously (E ′ , V) is a normal system and its size (number of symbols) is linear in the size of (E, V). It is a bit tedious but obvious to show that for any sub-process

P, Q ∈ E, σ : LVar → {0, 1} and n ∈ N, P -[n, σ, E] -• Q holds if and only if X P -[n, σ, E ′ ] -• X Q holds.
The proof can be done by induction on the length of deductions. Then, since for any variable Y of V we have the property

X Y ≡ Y , the relation -[•, σ, E] -• and -[•, σ, E ′ ] -• have identical restrictions to V × N × V. ⊓ ⊔
The result of the normalization procedure described previously applied to the example presented in section 3.1 is the following:

X = [K 6 ] Z = [K 5 ] K 2 = <b> X K 4 = • Z K 1 = [K 2 + K 7 + Z] Y = [K 1 ] K 6 = • K 3 K 3 = <a> Y K 5 = [ ] K 7 = <¬a> K 4
4 Conditional bi-colored graphs

In this section, we introduce the notion of conditional graphs. Then we show how to transform a normal process system into a conditional graph and the relation between the existence of some chains in those graphs and the operational semantics of the process system.

Graphs and instance graphs

A bi-colored graph is a (finite) directed graph with two kinds of arrows: green arrows denoted by → and red arrows denoted by ⇒.

Definition 4 (alternating chain).

A n-alternating chain is a chain of the form

(→ ⋆ ⇒) n .
So a chain contains a n-alternating chain if and only if it contains at least n red arrows ⇒.

Definition 5 (Conditional graph). A conditional bi-colored graph is a bicolored graph where green arrows → may be indexed with the (propositional) boolean expressions of Form.

Considering boolean expressions as representatives for boolean functions and given a valuation σ : LVar → {0, 1}, a boolean expression e is instantiated to the boolean value [[e]] σ ∈ {0, 1}. We obtain an instance graph: an arrow indexed with a boolean expression e belongs to this instance if and only if [[e]] σ = 1. The case of an unconditional (i.e. not indexed) arrow can be treated by considering that it has an implicit boolean conditional which is the tautology ⊤ (and then always evaluates to 1) and non-existing arrows have the implicit boolean condition ⊥ that always evaluates to 0. Definition 6 (Instance graph). Let G be a conditional bi-colored graph and σ be a valuation of boolean variables in {0, 1}. We define the instance graph G σ as the bi-colored graph that one obtains when one evaluates boolean expressions indexing arrows and keeping exactly those whose valuation equals 1.

From normal process systems to conditional graphs

We describe how to build a conditional bi-colored graph from a normal set of process equations. Let E be a finite set of normal process equations. The equations are of one of the following forms:

X = • Y , X = <f > Y or X = [Y 1 + • • • + Y k ]
where Y and the Y i 's are process variables.

We build the graph G E (simply denoted G here). It has the process variables occurring in E as vertices. We associate to each (normal) equation of E a set of arrows:

for the equation X = • Y , we associate the arrow X ⇒ Y ;

-for X = <f > Y , we associate the arrow X → f Y ; -for X = [Y 1 + • • • + Y k ], we associate the arrows X → Y 1 , . . . , X → Y k .
Obviously, the graph G ≡ G E is a conditional bi-colored graph and its size is linear in the size of E. As an example, we display the graph associated with the example of normal process system obtained in section 3.3:

X K 2 K 1 K 7 K 4 K 6 K 3 Y K 5 Z b a a

Chains and resource consumption

In this section, we relate the consumption of the resource • by the processes of E to the alternating chains of G E . [Res] or [Con] since X is a process variable. We consider the last remaining case where the deduction ends with rule [Eq]. Then there exists an equation X = P in E. As E is normal, P is in one of the following forms:

• Z, <f > Z or [Z 1 + • • • + Z k ]
, where Z and the Z i are process variables:

-if P ≡ • Z then there is a (sub-)deduction of • Z -[n] -• Y and therefore a (sub-)deduction of Z -[n -1] -• Y . By induction on deductions, we obtain of chain Z (→ ⋆ ⇒) n-1 → ⋆ Y in G σ . Moreover, as X = • Z ∈ E, we have an arrow X ⇒ Z in G σ . Thus there exists a chain X (→ ⋆ ⇒) n → ⋆ Y in G σ ; -if P ≡ <f > Z, then we have a sub-deduction of <f > Z -[n] -• Y . It is necessary that the last rule of this sub-deduction is [Cond] and then [[f ]] σ = 1.
We have a sub-deduction of Z -[n] -• Y . By induction, there is a chain

Z (→ ⋆ ⇒) n → ⋆ Y in G σ . Since X = <f > Z ∈ E and [[f ]] σ = 1, there is an arrow X → Z in G σ . Thus there exists a chain X (→ ⋆ ⇒) n → ⋆ Y in G σ ; -if P ≡ [Z 1 +• • •+Z k ], then we have a sub-deduction of [Z 1 +• • •+Z k ] -[n] -• Y .
It is necessary that the last rule of this sub-deduction is [Sum] and thus, there exists i ∈ [1, k] and a sub-deduction of

Z i -[n] -• Y . By induction, we obtain a chain Z i (→ ⋆ ⇒) n → ⋆ Y . Since X = [Z 1 + • • • + Z k ] ∈ E, there is an arrow X → Z i in G σ ,
(→ ⋆ ⇒) n+1 Y 0 in the instance graph G σ . Then, by theorem 1, X 0 -[n + 1, σ] -• Y 0 . But X 0 , Y 0 ∈ V so we get n + 1 n, that leads to a contradiction. Conversely, let X 0 , Y 0 ∈ V and k ∈ N satisfying X 0 -[k, σ] -• Y 0 . Then, by theorem 1, there is a chain X 0 (→ ⋆ ⇒) k → ⋆ Y 0 in the instance graph G σ . If k > n then this chain contains a sub-chain of the form X 0 (→ ⋆ ⇒) n+1 Y 1 , contradiction. Consequently k n. ⊓ ⊔

From conditional graphs to normal process systems

We have proved that a normal process system can be transformed into a conditional graph of the same size. Now we present the converse transformation. We show how to recover a process system from a conditional graph.

There is only a slight problem to be addressed: the construction described in section 4.2 does not generate a configuration like for example X → Y and X ⇒ Z where these two arrows have the same source X. This can only be generated when these two arrows are green → using the [ • • • + • • • ] construct. To overcome this difficulty, we propose the following trick: every red arrows ⇒ (resp. conditional arrow → f ) is split into two arrows →⇒ (resp. →→ f ) introducing a new intermediary node for each red ⇒ and conditional → f arrow. These two splits preserve n-alternating chains.

Using such a transformation on a conditional graph G, we obtain a new conditional graph G ′ with the following property: every node which is the source of multiple arrows is the source of only unconditional green arrows → since the source of a red ⇒ (resp. conditional → f ) arrow is the intermediary node which is specifically introduced for this particular arrow.

The graph G ′ can be transformed into a normal set of process equations. Let V be a set of process variables, one X v for each vertex v of G ′ . We build E as follows. We consider each vertex as a source for some arrows and associate an equation to each vertex:

if v is the source of a red arrow v ⇒ w then v is the source of no other arrow 1and we add

X v = • X w to E;
if v is the source of a conditional green arrow v → f w then v is the source of no other arrow and we add X v = <f > X w to E; -otherwise v is the source of k (unconditional) green arrows v→w 1 , . . . , v→w k (k could be 0) and we add

X v = [X w1 + • • • + X w k ] to E.
E being built this way, it is obvious that it is a normal set of process equations and that G ′ appears as the conditional graph associated with E by the construction described in section 4.2, i.e. G ′ = G E .

Theorem 2. Let G be a conditional graph of size k. There exists a process system (E, V) of size O(k) with the following property: for any n ∈ N, (E, V) has a resource use boundable by n if and only if there is an instance graph G σ with no (n + 1)-alternating chain.

Proof. Obviously, the size of the graph G ′ described earlier in this section is less than 2k. The size of E is the same as the size of G ′ , so is less than 2k. Let V be the set of process variables occurring in E. The size of (E, V) is less than 3k. Then it is clear that for any σ : LVar → {0, 1}, there is a one-to-one correspondence between a (n + 1)-alternating chain of G σ and a (n + 1)-alternating chain of G ′ σ , since the splits ⇒ →⇒ and → f →→ f preserve alternating chains in every instance. As the identity G ′ = G E holds, we finish by an application of corollary 1 to E. ⊓ ⊔

From conditional graphs to LC

In this section, we introduce the algebraic semantics of the family of propositional Gödel-Dummett logics LC n . The value n belongs to the set N ⋆ = {1, 2, . . .}∪{∞} of strictly positive natural numbers with its natural order , augmented with a greatest element ∞. In the case n = ∞, the logic LC ∞ is also denoted by LC: this is the usual Gödel-Dummett logic.

After having defined the semantics of LC n , we show how to transform a conditional graph into a formula2 of LC n and we relate the existence of a countermodel for this formula to the alternating chains of the initial graph, and thus to resource consumption.

The semantics of LC n

IL denotes the set of formulae that are provable in any intuitionistic propositional calculus (see [START_REF] Dyckhoff | Contraction-free Sequent Calculi for Intuitionistic Logic[END_REF]) and CL denotes the classically valid formulae. As usual an intermediate propositional logic [START_REF] Avellone | Duplication-Free Tableau Calculi and Related Cut-Free Sequent Calculi for the Interpolable Propositional Intermediate Logics[END_REF] is a set of formulae L satisfying IL ⊆ L ⊆ CL and closed under the rule of modus ponens (if A ∈ L and A ⊃ B ∈ L then B ∈ L) and under arbitrary substitution (if A ∈ L and ρ is any substitution then A ρ ∈ L.)

We prove [[f ⋆ ]](σ) = φ [[f ]](ψ • σ) by induction on f : -if f ≡ ⊥, we obtain [[⊥ ⋆ ]] σ = [[⊥]] σ = 0 and φ([[⊥]](ψ • σ)) = 0; -if f ≡ x, then [[x ⋆ ]] σ = 0 if σ x = 0 and [[x ⋆ ]] σ = ∞ if σ x > 0. So [[x ⋆ ]] σ = φ(ψ(σ x )). On the other hand, φ([[x]](ψ • σ)) = φ(ψ • σ(x)) = φ(ψ(σ x )); -if f ≡ a ∨ b, then [[(a ∨ b) ⋆ ]] σ = [[a ⋆ ∨ b ⋆ ]] σ = max(φ([[a]](ψ • σ)), φ([[b]](ψ • σ))) = φ(max([[a]](ψ • σ), [[b]](ψ • σ))) = φ([[a ∨ b]](ψ • σ)); -the cases f ≡ a ∧ b and f ≡ a ⊃ b are similar. ⊓ ⊔

Transforming conditional graphs into formulae

Let us consider a conditional graph G. There may be some conditional formulae on green arrows like → f . We consider all these formulae and the propositional variables they contain. For each vertex v of G we introduce a new propositional variable x v , so that the propositional variables occurring in conditional formulae and the newly introduced x v do not overlap. We build a sequent S G = Γ ⊢ ∆ by adding one formula to either Γ or ∆ for each arrow of G:

-if v → w is green arrow of G, we add x v ⊃ x w to Γ ; -if v → f w is conditional green arrow of G, we add (¬¬f ) ⊃ (x v ⊃ x w ) to Γ ; -if v ⇒ w is a red arrow of G, we add x w ⊃ x v to ∆.
Theorem 3. Let G be a conditional graph, S G its associated sequent and n ∈ N.

There exists a valuation σ : LVar → {0, 1} such that the instance graph G σ does not contain a (n + 1)-alternating chain if and only if the sequent S G has a counter-model in LC n .

Proof. First, let us suppose that there exists a valuation σ : LVar → {0, 1} s.t. the instance graph G σ does not contain a chain of type (→ ⋆ ⇒) n+1 . By theorem 4 of [START_REF] Larchey-Wendling | Counter-model search in Gödel-Dummett logics[END_REF], there exists a height h s.t. for every vertices v, w of G (or G σ , they have the same vertices),

h v ∈ [0, n], if v→w ∈ G σ then h v h w and if v⇒w ∈ G σ then h v < h w . We define h ′ v = n v, i.e. h ′ v = h v if h v < n and h ′ v = ∞ if h v = n. We define a valuation σ ′ : LVar → [0, n). If x ≡ x v is a variable corresponding to one of the vertices of G then σ ′ xv = h ′ v .
Otherwise we define σ ′ x = φ(σ x ). We recall that the x v do not overlap with the variables occurring in the conditional formulae of G. We prove that σ ′ is a counter-model of S G ≡ Γ ⊢ ∆: Proof. Let G be the conditional graph associated to E (see corollary 1), S be the sequent associated to G (see theorem 3). Then f E is a formula logically equivalent to S, see proposition 1.

-consider the formula x v ⊃ x w occurring in Γ . Then [[x v ⊃ x w ]] σ ′ = [[x v ]] σ ′ [[x w ]] σ ′ = σ ′ (x v ) σ ′ (x w ) = h ′ v h ′ w = ∞ because h ′ v h ′ w since v → w occurs in G σ . Thus [[x v ⊃ x w ]] σ ′ = ∞; -consider the formula (¬¬f ) ⊃ (x v ⊃ x w ) occurring in Γ . Then [[(¬¬f ) ⊃ (x v ⊃ x w )]] σ ′ = [[¬¬f ]] σ ′ [[x v ⊃ x w ]] σ ′ . [[¬¬f ]] σ ′ = φ([[f ]](ψ • σ ′ )) = φ([[f ]](ψ • φ • σ)) = φ([[f ]] σ ). If [[f ]] σ = 0 and in this case [[¬¬f ]] σ ′ [[x v ⊃ x w ]] σ ′ = 0 [[x v ⊃ x w ]] σ ′ = ∞. On the other hand, if [[f ]] σ = 1, then v → w occurs in G σ , and thus h ′ v h ′ w . So [[¬¬f ]] σ ′ [[x v ⊃ x w ]] σ ′ = ∞ [[x v ⊃ x w ]] σ ′ = [[x v ⊃ x w ]] σ ′ = h ′ v h ′ w = ∞. In either case, [[(¬¬f ) ⊃ (x v ⊃ x w )]] σ ′ = ∞; -consider the formula x w ⊃ x v occurring in ∆. Then v ⇒ w occurs in G σ . [[x w ⊃ x v ]] σ ′ = h ′ w h ′ v = h ′ v since h ′ v < h ′ w . Moreover, as h ′ v < h ′ w , we deduce h ′ v < ∞ and then [[x w ⊃ x v ]] σ ′ < ∞. Then ⌈⌈∆⌉⌉ σ ′ < ∞ and that ⌊⌊Γ ⌋⌋ σ ′ = ∞. So σ ′ is a counter-model of S G . Conversely, consider σ : LVar → [0, n) a counter-model of S G . We define σ ′ = ψ • σ. Let us consider a conditional arrow v → f w of G. We compute [[¬¬f ]] σ = φ([[f ]] σ ′ ). [[f ]] σ ′ = 1 if and only if there is an arrow v →w in G σ ′ . If [[f ]] σ ′ = 1 then φ([[f ]] σ ′ ) = ∞ and [[(¬¬f )⊃(x v ⊃x w )]] σ = ∞ [[x v ⊃x w ]] σ = [[x v ⊃x w ]] σ . On the other hand, if [[f ]] σ ′ = 0, then [[(¬¬f )⊃(x v ⊃x w )]] σ = 0 [[x v ⊃x w ]] σ = ∞.
⊓ ⊔

6 Counter-models of LC n and resource consumption

In this section, we briefly recall some of our previous results which provide the proof of the converse of corollary 2. Given a formula f of LC, we explain how to build a conditional graph G f of size linear w.r.t. the size of f which represents the proof-search process on f and on which it is possible to either prove f or extract counter-models of f . For an explanation of the construction in full details, the reader is invited to consult [START_REF] Larchey-Wendling | Gödel-Dummett counter-models through matrix computation[END_REF]. Let f be a formula of LC. We build a conditional graph G f based on the decomposition tree of f , i.e. the set of sub-formula occurrences of f . An occurrence of a sub-formula r can be identified with the root node of the sub-tree corresponding to r. Each node is polarized starting with polarity -for the root f - and propagated the following way: the connectives ∨ and ∧ preserve the polarity while the connective ⊃ preserves the polarity on the right hand side and inverses it on the left-hand side.

f - ♦ v + v - v ⊥ + ⊥ - x x ∧ - a - b - ∨ - a - b - x x ⊃ - a + b - ♦ k ∧ + a + b + x x ∨ + a + b + x x ⊃ + a - b + Fig. 2.
Counter-model search system for LC

We add a supplementary node for each propositional variable v occurring in f . This is one node per variable, not per occurrence: two occurrences of the same variable only produce one supplementary node. These added nodes are not polarized. Two more nodes are added: ♦ and . Intuitively, ♦ represents the semantic value ∞ whereas represents the semantic value 0.

Before we describe how we build the arrows of G f , we precise that we will sometimes introduce new conditional variables denoted x and use either x or its negation x ≡ ¬x as a condition indexing some green arrows like → x or → x . Now we describe how we build the arrows of G f :

for the root f -, we add a red arrows f ⇒ ♦; -for every added node v corresponding to a propositional variable occurring in f , we add a green arrow → v; -for a positive occurrence v + of a variable in f , we add a green arrow v + → v; -for a negative occurrence v -of a variable in f , we add a green arrow v → v -; -for a positive occurrence of ⊥ + in f , we add a green arrow ⊥ + → ; -for a negative occurrence of ⊥ -in f , we add a green arrow → ⊥ -. All these rules correspond to the left part of figure 2. Now we describe what we do with internal nodes, which corresponds to the right part of figure 2: for each negative occurrence of a sub-formula r -≡ a -∧ b -, we introduce a new conditional variable x and we add the two conditional green arrows a -→ x r -and b -→ x r -; -for each positive occurrence of a sub-formula r + ≡ a + ∧ b + , we add the two green arrows r + → a + and r + → b + ; -for r -≡ a -∨ b -, we add the two green arrows a -→ r -and b -→ r -; -for r + ≡ a + ∨ b + , we introduce a new variable x and add the two arrows r + → x a + and r + → x b + ; -for r -≡ a + ⊃ b -, we introduce a new variable x and a new node k and the five arrows b -→ x k, k ⇒ a + , k → r -, k ⇒ ♦ and ♦ → x r -; -for r + ≡ a -⊃ b + , we introduce a variable new x and add the two arrows r + → x b + and a -→ x b + .

The construction of G f is finished after each internal node has been processed. The order in which they are processed is indifferent. We recall the main result4 of [START_REF] Larchey-Wendling | Counter-model search in Gödel-Dummett logics[END_REF], which relates conditional graphs and LC n : Theorem 4. Let f be a formula of LC, G ≡ G f be the conditional graph associated to f by the construction described in this section and n ∈ N. Then f has a counter-model in LC n if and only if there exists a valuation σ such that the instance graph G σ has no (n + 1)-alternating chain.

Corollary 3. Let f be a formula of LC of size k. There exists a process system (E, V) of size O(k) such that for any n ∈ N, (E, V) has resource use boundable by n if and only if f has a counter-model in LC n .

Proof. Let f be a formula of LC. We apply theorem 4 and obtain a conditional graph G f . The size of G f is linear w.r.t. the size of f . Then we apply theorem 2 and obtain a process system (E, V). The size of (E, V) is linear w.r.t. the size of G f , thus also w.r.t. the size of f . (E, V) has resource use boundable by n if and only if G f has no (n + 1)-alternating chains if and only if f has a counter-model in LC n . ⊓ ⊔

Conclusion

We have defined a process calculus and an operational semantics that measures resource consumption. We establish a correspondence between normal process systems and conditional bi-colored graphs: a process system has resource use boundable by an integer n if and only if the corresponding graph has no (n + 1)alternating chain. Then we show how the absence of (n + 1)-alternating chain in a graph can be expressed by the refutability of a formula of LC n . Combining the two results, we get a linear transformation of a resource bounding problem in a process calculus into a decision problem in LC n . We recall our previous result on counter-model search in LC [START_REF] Larchey-Wendling | Counter-model search in Gödel-Dummett logics[END_REF] and relate it to the process formalism we introduced. Thus, we have a linear transformation of a decision problem in LC n into a resource bounding problem in a process calculus. This establishes the linear equivalence of the two problems. So LC could be viewed as a logic for specifying some resource related properties. This sheds some new lights on LC.

In further studies, we want to use the process calculus defined in this paper as an abstraction of more complex calculi: by keeping only the basic constructs present in our calculus and abstracting the other constructs. Counter-model search in LC could be used as a tool to bound resource consumption in some specified complex systems.

Theorem 1 .

 1 Let E be a normal set of process equations and G = G E be its associated conditional graph. Let σ : LVar → {0, 1} be a valuation. Then for any process variables X, Y ∈ E and anyn ∈ N, X -[n, σ] -• Y holds if and only if there exists a chain X (→ ⋆ ⇒) n → ⋆ Y in the instance graph G σ .Proof. Let us fix E and σ : LVar → {0, 1}. We consider the conditional graphG E and its instance G σ . Let X ⇒ Y be an arrow of G σ . By construction of G E , there is an equation X = • Y in E. Thus, X -[1] -• Y holds. Now let us consider an arrow X → Y of G σ : either there exists an equation X = <f > Y in E s.t. [[f ]] σ =1 or there exists an equation X = [ • • • + Y + • • • ] in E. In either case, X -[0] -• Y holds. Then by using the derived [Cut] rule of lemma 1, from a chain X (→ ⋆ ⇒) n → ⋆ Y containing exactly n red arrows ⇒, we can deduce that X -[n] -• Y holds. Conversely, let us show how to transform a deduction of X -[n] -• Y into a chain of the form X (→ ⋆ ⇒) n → ⋆ Y in G σ , by induction on the length of the deduction. Suppose it ends with the [Id] rule. Then Y ≡ X and n = 0. Thus X → 0 Y is a zero length chain. Considering other rules, we remark that a deduction of X -[n] -• Y cannot end with rules [Sum],

  Let use denote Γ ′ the multiset where we have replaced the formula (¬¬f ) ⊃ (x v ⊃ x w ) byx v ⊃ x w when [[f ]] σ ′ = 1 and by nothing (i.e. we simply erase it) when [[f ]] σ ′ = 0. It is clear that ⌊⌊Γ ′ ⌋⌋ σ = ⌊ ⌊Γ ⌋ ⌋ σ . So σ is also a counter-model in LC n of the implicational sequent Γ ′ ⊢ ∆ corresponding to the instance graph G σ ′ .According to theorem 6 of[START_REF] Larchey-Wendling | Counter-model search in Gödel-Dummett logics[END_REF], since the implicational sequent Γ ′ ⊢ ∆ has a counter-model in LC n , its instance graph G σ ′ does not contain a chain of type (→ ⋆ ⇒) n+1 . ⊓ ⊔ It is obvious that the size of S G is linear in the size of G (of course, the size of G should account for the size of conditional formulae). So there exists a linear transformation of the problem of resource consumption bounding into the decision problem in LC n .Corollary 2. Let E be a normal set of process equations of size k and V the set of variables of E. There exists a formula f E of LC of size O(k) such that for any n ∈ N, (E, V) has a resource use boundable by n if and only if f E has a counter-model in LC n .

  and there exists a chainX (→ ⋆ ⇒) n → ⋆ Y in G σ . ⊓ ⊔ Corollary 1.Let E be a normal set of process equations, V the set of variables of E, G its associated conditional graph and n ∈ N. The process system (E, V) has a resource use boundable by n if and only if there is an instance graph G σ with no (n + 1)-alternating chain.

Proof. If (E, V) has a resource use boundable by n, there exists a valuation σ :

LVar → {0, 1} s.t. for any X, Y ∈ V and k ∈ N, if X -[k, σ] -• Y holds then k n.

Suppose there exists a (n + 1)-alternating chain X 0

v is new and has been introduced in G ′ specifically for this purpose.

In fact, into a sequent which can straightforwardly be transformed into an equivalent formula, see proposition 1.

[[⊥ ⋆ ]] σ = [[⊥]] σ [[(a ∨ b) ⋆ ]] σ = max([[a ⋆ ]] σ , [[b ⋆ ]] σ ) [[(a ⊃ b) ⋆ ]] σ = [[a ⋆ ]] σ [[b ⋆ ]] σ [[(a ∧ b) ⋆ ]] σ = min([[a ⋆ ]] σ , [[b ⋆ ]] σ )3 With the convention [0, ∞) = N ∪ {∞}. With our particular representation, the algebraic models [0, n) form a strictly increasing sequence of subsets of N.

To be precise, the construction of G f we present here, and the associated theorem 4 are a slight but obvious modification of the cited result, to integrate the case of the ⊥ logical constant and to avoid generating conditional red arrows like ⇒x or ⇒x.

For any n ∈ N ⋆ , the Gödel-Dummett logic LC n is an intermediate logic. On the semantic side, it is characterized by the linear Kripke models of size n, see [START_REF] Dummett | A Propositional Calculus with a Denumerable matrix[END_REF].

The following strictly increasing sequence holds:

In the particular case of LC, the logic has a simple Hilbert axiomatic system: (X ⊃ Y ) ∨ (Y ⊃ X) added to the axioms of IL.

In this paper, we will use the algebraic semantic characterization of LC n [7] rather than the Kripke semantics. Let us fix a particular n ∈ N

⋆ . The algebraic model is the set [0, n) = [0, . . . , n[∪{∞} composed of n+1 elements. 3 A valuation (or interpretation) on propositional variables σ : LVar → [0, n) is inductively extended to formulae:

where the operator is defined by

A sequent is a pair Γ ⊢ ∆ where Γ and ∆ are multisets of formulae. Γ, ∆ denotes the sum of the two multisets and if Γ is the empty multiset, we write ⊢ ∆.

The proof of this proposition is trivial. Let f be a propositional formula. It can either be viewed as a boolean formula, or a formula of LC n . We relate the two semantic interpretations using the double negation. We define the mappings φ : {0, 1} → [0, n) and ψ : [0, n) → {0, 1} by φ 0 = 0, φ 1 = ∞, ψ 0 = 0 and ψ x = ∞ for x > 0.

Proposition 2. Let f be a propositional formula and σ : LVar → [0, n) be an interpretation of variables. The identity

Proof. Let us denote ¬¬f by f ⋆ . We remark that φ commutes with the interpretation of the connectives ∧, ∨ and ⊃; for instance max(φ x , φ y ) = φ(x ∨ y). Then, the following logical identities hold in LC n :