Loïg Jezequel

Didier Lime

Bastien Sérée

A lazy query scheme for reachability analysis in Petri nets

Keywords: Reachability analysis, unbounded Petri nets, inhibitor arcs, lazy algorithms

In recent works we proposed a lazy algorithm for reachability analysis in networks of automata. This algorithm is optimistic and tries to take into account as few automata as possible to perform its task. In this paper we extend the approach to the more general settings of reachability analysis in unbounded Petri nets and reachability analysis in bounded Petri nets with inhibitor arcs. We consider we are given a reachability algorithm and we organize queries to it on bigger and bigger nets in a lazy manner, trying thus to consider as few places and transitions as possible to make a decision. Our approach has been implemented in the Romeo model checker and tested on benchmarks from the model checking contest.

Introduction

In recent works [START_REF] Jezequel | Lazy reachability analysis in distributed systems[END_REF][START_REF] Jezequel | Let's be lazy, we have time -or, lazy reachability analysis for timed automata[END_REF] we proposed an algorithm for reachability analysis in networks of automata. This algorithm is called lazy as it tries to use as few automata as possible to complete its task. To that extent, it is a non-trivial instance of a general principle that has been implemented in many approaches (e.g. program slicing [START_REF] Weiser | Program slicing[END_REF]). In practice, on many benchmarks this approach proved to be efficient: the LaRA tool (which implements our approach) used only a small portion of the automata in the network to conclude about reachability. Runtime comparisons with LoLA [START_REF] Wolf | Running LoLA 2.0 in a model checking competition[END_REF] (in a non-timed setting [START_REF] Jezequel | Lazy reachability analysis in distributed systems[END_REF]) and Uppaal [START_REF] Behrmann | A tutorial on UPPAAL[END_REF] (in a timed setting [START_REF] Jezequel | Let's be lazy, we have time -or, lazy reachability analysis for timed automata[END_REF]) were also frequently in favor of LaRA.

Networks of automata are in fact a subclass of Petri nets as they can be syntactically transformed into safe Petri nets. Extending our lazy reachability algorithm to larger classes of Petri nets is thus a natural next step in our work. Moreover, it is of particular interest for us as it will allow to implement lazy reachability in the Romeo model checker [START_REF] Lime | Romeo: A parametric model-checker for Petri nets with stopwatches[END_REF], developed in our research team. In fact, Romeo works on models even more expressive than Petri nets, where reachability is not always decidable. In this paper we focus on unbounded Petri nets and bounded Petri nets with inhibitor arcs, two subclasses of these models for which reachability is decidable.

Reachability analysis in Petri nets (or equivalent models such as vector addition systems) has been widely studied. The problem is known to be decidable in general [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF][START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF][START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF]. Efficient techniques exist for performing it in the particular case of bounded nets, that is nets with a finite state space. One can notice, for example, Petri net unfolding [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits[END_REF][START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF] or variations around it [START_REF] Bonet | Directed unfolding of Petri nets[END_REF][START_REF] Chatain | Goal-driven unfolding of Petri nets[END_REF], partial order techniques [START_REF] Holzmann | An improvement in formal verification[END_REF], and decision diagram based approaches [START_REF] Couvreur | Hierarchical decision diagrams to exploit model structure[END_REF][START_REF] Miner | Meddly: Multi-terminal and edge-valued decision diagram library[END_REF].

Here we follow a different approach and do not propose a standalone reachability algorithm but rather, given such an algorithm, we propose a scheme to use its results on subnets that are built incrementally from the reachability property by adding only places and transitions that are required to make a decision. This is why we call the approach lazy. Compared to [START_REF] Jezequel | Lazy reachability analysis in distributed systems[END_REF], the main challenges we address here are (1) that the components of the system are less well-defined in a Petri net than in a network of finite automata, and (2) that the state-space is infinite in general. Note also that even if a net is bounded, its subnets might not be. We propose an algorithm for reachability in plain Petri nets, and also show how to deal with inhibitor arcs in the bounded case.

This paper is organized as follows. We start by giving some definitions and notations in Section 2. Then we present our algorithm for lazy reachability analysis in Petri nets in Section 3 and show its validity. After that, we show how this approach can be transposed to perform reachability analysis for the class of bounded Petri nets with inhibitor arcs in Section 4. Finally, in Section 5 we report on an implementation of our algorithm in the model checker Romeo and give experimental results obtained from a run of our tool on all the benchmarks from the 2020 edition of the model checking contest [START_REF] Kordon | MCC'2015 -the fifth model checking contest[END_REF][START_REF] Kordon | Complete Results for the 2020 Edition of the Model Checking Contest[END_REF].

Definitions and notations

We define Petri nets and their semantics, as well as the central notion of reachability of markings in Petri nets. Then, we define the notion of subnets and partial markings, that we use later to perform reachability analysis on a Petri net without considering it in its entirety.

Petri nets

Definition 1 (Petri net). A Petri net is a tuple N = (P, T, F, m 0 ) where P and T are disjoint finite sets of places and transitions respectively, F : P ×T ∪T ×P → N is a flow function, and m 0 : P → N is called the initial marking.

In a net N, for any x ∈ P ∪ T , we define • x = {y : F (y, x) ̸ = 0} the preset of x and x • = {y : F (x, y) ̸ = 0} the postset of x. We can extend this postset (resp preset) concept to subsets of P or T by doing the union of the postsets (resp presets) of each element of the considered subset.

In a net N, any function m : P → N is called a marking of N. A transition t ∈ T is fireable from a marking m if and only if ∀p ∈ • t, m(p) ≥ F (p, t). In this case, firing t from m leads to the new marking m ′ such that ∀p ∈ P, m ′ (p) = m(p)-F (p, t)+F (t, p). We denote it by m t -→ m ′ . Given a sequence ω = t 1 , . . . , t n of transitions, we define m

ω -→ m ′ if there exist markings m 1 , . . . m n-1 such that m t1 -→ m 1 , ∀2 ≤ i ≤ n -1, m i-1 ti -→ m i , and m n-1 tn -→ m ′ .
Definition 2 (Reachability). A marking m is said to be reachable in N if and only if there exists a sequence of transitions ω such that m 0 ω -→ m.

Definition 3 (Boundedness).

A Petri net is said to be k-bounded, for a given k, if for every reachable marking m and every place p, we have m(p) ≤ k. A Petri net is said to be bounded, if there exists a k such that it is k-bounded.

Subnets and partial markings

In the following, we will perform reachability analysis on parts of a Petri net: not all the places and transitions of the net will be considered. This is formalized through the notion of subnet.

Definition 4 (Subnet

). A Subnet N ′ of a Petri net N = (P, T, F, m 0 ) is a tuple (P ′ , T ′ , F ′ , m ′ 0 ) such that P ′ ⊆ P , T ′ ⊆ T , F ′ = F |P ′ ,T ′ , and m ′ 0 = m 0|P ′ .
Given a subnet N ′ of a net N, and for any x ∈ P ′ ∪ T ′ , we define •N x = {y : F (y, x) ̸ = 0)} and x N• = {y : F (x, y) ̸ = 0} (that is, intuitively, the preset and postset taken in N rather than in N ′ ).

We introduce two notions of completeness with respect to a net N for a subnet N ′ . They will be central in our algorithms and their proofs. The notion of P-completeness expresses that N ′ contains all the places from N that are used as preconditions for enabling transitions in N ′ .

Definition 5 (P-completeness).

A subnet N ′ of a net N is said to be Pcomplete when ∀t ∈ T ′ , •N t ⊆ P ′ .

In the other way around, the notion of T-completeness expresses that N ′ contains all the transitions from N that can add tokens on places in N ′ .

Definition 6 (T-completeness

). A subnet N ′ of a net N is said to be T- complete when ∀p ∈ P ′ , •N p ⊆ T ′ .
Partial marking will be used to express reachability objectives that do not concern all the places in a net. Definition 7 (Partial marking). For a Petri net N = (P, T, F, m 0 ), any function m p : P → N ∪ {⋆} is called a partial marking of N.

Intuitively, a partial marking is a marking which is not fully specified: when m p (p) = ⋆ for some p ∈ P it means that this value is left unspecified. For a partial marking m p of a net N, we define supp(m p ) = {p ∈ P : m p (p) ̸ = ⋆}.

A marking m such that m(p) = m p (p) for any p ∈ supp(m p ) is said to realize m p . We can notice that a every marking m of a net N is a partial marking such that supp(m) = P . For a net N with a subnet N ′ , and a (partial) marking m of N, we denote by m ′ the (partial) marking of N ′ such that m ′ = m |P ′ and call it the submarking of m in N ′ . Definition 8 (Reachability). A partial marking m p is said to be reachable in N if and only if there exists a marking m that realizes m p and is reachable in N.

Finally, a third notion of completeness, m-completeness, is defined for partial markings. It expresses the fact that, for a given marking m of N ′ , all the transitions from N that can affect this marking by reducing its value for some place are included in N ′ . Definition 9 (m-completeness). A subnet N ′ of a net N is said to be mcomplete with m a marking of N ′ when ∀p ∈ supp(m), p N• ⊆ T ′ .

Lazy reachability analysis in Petri nets

In this section we propose an algorithm which, given a Petri net N and a marking m in N, decides whether or not m is reachable in N. However, this algorithm consists in a heuristic way to perform reachability queries on smaller nets, which proves more efficient in some cases than a query on the full net. It therefore requires an algorithm to perform reachability on Petri nets, used as a blackbox. The technique works on unbounded nets, provided that the reachability black-box handles them.

We start by demonstrating the concept of our algorithm -in particular, in which way it is lazy -on two examples, then we formalize the algorithm, and finally we prove its validity.

Preliminary example

Consider the Petri net of Figure 1 -the places are represented by circles, the transitions by squares, the flow function by arrows, the initial marking by black dots. We look at two reachability questions on this net: (Q1) is it possible to reach a partial marking m 1 so that m 1 (p 2 ) = 1, and m 1 (p 3 ) = 1? (Q2) is it possible to reach a partial marking m 2 so that m 2 (p 4 ) = 3?

Let us focus on (Q1) first. To this end, consider the subnets N 1 and N 2 of Figure 2. These two subnets were built from N by considering exactly the places in the support of m 1 . If the initial marking of each of these subnets had been a submarking of m 1 , then the answer to (Q1) would immediately be a yes. This is not the case however, so we cannot conclude yet.

Consider N 1 first. Our objective with this subnet is to find whether or not it is possible to reach some marking m so that m(p 2 ) = 1. As this is not the case initially, one needs to find how to increase the marking of p 2 . This can only be done by using transitions t so that p 2 ∈ t • . We thus add these transitions to our subnet, leading to N ′ 1 (which is T-complete). Now, some m so that m(p 2 ) = 1 is reachable, however, we cannot yet conclude that this is the case in the full net N because we do not have all the presets of the transitions we use. So we add the places in these presets, leading to the new subnet N ′′ 1 (which is P-complete). From this subnet, one can conclude that some m so that m(p 2 ) = 1 is reachable in N.

A similar process allows to build N ′′ 2 and prove that some m so that m(p 3 ) = 1 is reachable in N. However, having obtained these two results does not guarantee that m 1 is reachable in N because N ′′ 1 and N ′′ 2 overlap (the place p 1 appears in both), which may lead to conflicts between the transition sequences found in these two subnets. We thus merge the subnets (on common places and transitions, here only p 1 ), which leads to the subnet of Figure 3. In this subnet m 1 is reachable. Moreover -as we prove later -because this subnet is P-complete, m 1 is also reachable in N.

The place p 4 and the transition t 3 were never included in the subnets considered. This is why we call our algorithm lazy: it omits the places and transitions that are not useful for its analysis.

Let us now focus on (Q2). In this case our analysis will start from the subnet N 3 of Figure 4. For similar reasons as before, we first add the transitions that can put tokens in p 4 , leading to N ′ 3 . In this subnet, no marking m so that m(p 4 ) = 3 is reachable (because there is always an even number of tokens in p 4 ). However, markings with m(p 4 ) ≥ 3 are reachable. Hence, we add the transitions that can remove tokens from p 4 , leading to N ′′ 3 . In this subnet, such an m is reachable (for example by firing t 2 three times and then t 3 one time). As before, in order to conclude one needs to verify that (at least some of) the sequences allowing to reach such an m are fireable in the original net. For that, the places in the presets of t 2 and t 3 need to be added, leading to N ′′′ 3 . In this subnet it is not possible to fire t 2 three times. Moreover, this subnet is T-complete and so, as we prove later, if no m such that m(p 4 ) = 3 is reachable in N ′′′ 3 , no such m is reachable at all in N .

An algorithm for lazy reachability analysis in Petri nets

The formalization of the ideas presented in the above examples leads to Algorithm 1 4 . It is a lazy algorithm that, given a net N and a (partial) marking m, tells whether or not m is reachable in N . This algorithm works on subnets of N . These subnets are identified by their sets of places and transitions.

Algorithm 1 starts with subnets built from a partition of the set of places involved in m. This allows to handle each part of the objective separately as long as they do not interact. Initially, each element of the List LN ets is a pair (P, T ) representing one of these subnets. The algorithm does two main tasks: concretisation (addition of places and transitions to subnets) and merging (union of interacting subnets). At each iteration of its main loop it does at least one of those two tasks.

Concretisation. Concretisation consists in expanding one subnet. If the partial objective is not reachable one adds new transitions to add new ways to reach it. If the partial objective is reachable, one needs to add new places to ensure that Algorithm 1 Lazy algorithm checking if a marking m is reachable in a Petri net N = (P, T, F, m 0 ) the transitions used in the subnet can also be used in the original net (i.e. to ensure that their full preset is taken into account).

1: choose a partition {P1, ..., Pp} of supp(m) 2: LN ets ← [(P1, ∅), ..., (Pp, ∅)] 3: Complete ← f
More formally, the objective of the concretisation is to ensure that each subnet verifies the completeness notion of definition 10. If this is the case, then m is reachable in N (provided that there is not interaction with other subnets, which is ensured by the notion of consistency described below). If at least one subnet cannot be made complete, then it is granted that m is not reachable in N .

Definition 10. Let N = (P, T, F, m 0 ) be a Petri net and m a marking. A subnet

N ′ of N is complete (with respect to N and m) if N ′ is P -complete and the submarking m ′ is reachable in N ′ .
Remark that completeness can be effectively checked provided reachability can be checked. The rest of the conditions is syntactic.

Concretisation can be implemented as described in Algorithm 2, which alternately adds places and transitions to a subnet.

Merging. Merging consists in replacing two subnets in LN ets by a single subnet obtained by union of places and transitions sets. Merging is needed when two subnets share places, as in this case the solutions to the reachability problem Algorithm 2 Auxiliary function Concretise(LN ets, m) for Algorithm 1

1: choose k such that LN ets[k] is not complete 2: (P k , T k ) ← LN ets[k] 3: m ′ ← m |P k 4: if not Reachable(LN ets[k], m ′ ) then 5: choose T ′ k such that T k ⊂ T ′ k ⊆ supp(m ′ ) N • ∪ •N P k 6:
if not possible then choose

P ′ k such that P k ⊂ P ′ k ⊆ •N T k 13:
LN ets[k] ← (P ′ k , T k ) 14: end if 15: return true found in these subnets can interfere. For the same interference reason, merging is also needed when one of the subnets contains a transition whose postset contains a place involved in the submarking of m (the reachability objective) in another subnet. The fact that two subnets may interfere is formalised through the notion of consistency in Definition 11.

Definition 11. The list of subnets LN ets = [(P 1 , T 1 ), ...,

(P n , T n )] is consistent if 1. ∀k ̸ = ℓ, (P k ∩ P ℓ ) = ∅, and 2. ∀k ̸ = ℓ, T k N • ∩ supp(m |P ℓ ) = ∅.
Remark that the definition of consistency is completely syntactic and can therefore be checked effectively.

Proof of the algorithm

We now prove the correctness of Algorithm 1. Propositions 1 and 2 together prove the soundness of Algorithm 1, while proposition 3 proves its completeness. The proofs of these propositions are based on lemma for which proofs are presented in this part. In this case, it must not be possible to choose

T ′ such that T ⊂ T ′ ⊆ supp(m ′ ) N • ∪ •N P (line 5
). In other words, the subnet LN ets[k] considered is m ′ -complete (Definition 9) and T -complete (Definition 6). Moreover, the current marking m ′ must not be reachable in the subnet LN ets[k] (line 4) and is a submarking of m (line 3). Hence, by applying Lemma 1 below, m is not reachable in N .

⊓ ⊔

Lemma 1. Let N ′ be a subnet of a Petri net N . Assume that N ′ is T -complete. Let m ′ be a marking of N ′ , that is not reachable. If N ′ is m ′ -complete, then no marking m of N such that m ′ is the submarking of m in N ′ is reachable in N .
Proof. Let m be a reachable marking of N , with m 0 ω -→ m. Denote by n the number of transitions in ω. We prove by induction on n that m ′ is reachable in N ′ . By the contrapositive, this proves the Lemma.

Induction hypothesis for all n, if m is reachable in N and there is a sequence

ω of n transitions such that m 0 ω -→ m, then the submarking m ′ of m in N ′ is reachable in N ′ .
Initialisation when n = 0, the only possible m is m 0 (it must be reachable with 0 transitions). Thus, simply take m ′ = m ′ 0 , which is, by construction the submarking of m 0 in N ′ and is obviously reachable in N ′ . Induction Let us consider some n > 0 and assume that the induction hypothesis is verified for n -1. First, remark that ω can always be split in two parts: ω ′ of length n-1 and t n (a single transition) such that m 0 ω ′ -→ m tn -→ m in N for some marking m. From the induction hypothesis, the submarking m′ of m is reachable in N ′ . Four cases are then possible. [START_REF] Akshay | On Petri nets with hierarchical special arcs[END_REF]

t n N • ∩ P ′ = ∅ and •N t n ∩ supp(m ′ ) = ∅, in which case m′ = m ′ and so m ′ is reachable in N ′ . (2) t n N • ∩ P ′ ̸ = ∅ and •N t n ∩ supp(m ′ ) = ∅, in which case, as N ′ is T -complete, t n must be in T ′ .
Moreover, as t n is fireable in N from m, it must be fireable as well in N ′ from m′ . The effects of t n on the places of P ′ are the same in N and N ′ , so m′ tn -→ m ′ in N ′ . Hence, m ′ is reachable in N ′ . (3) t n N • ∩P ′ = ∅ and •N t n ∩supp(m ′ ) ̸ = ∅, in which case, as N ′ is m ′ -complete, t n must be in T ′ . Then, using the same arguments as in case [START_REF] Behrmann | A tutorial on UPPAAL[END_REF]

, m ′ is reachable in N ′ . (4) t n N • ∩ P ′ ̸ = ∅ and •N t n ∩ supp(m ′ ) ̸ = ∅,
in which case, as N ′ is T -complete and m ′ -complete, t n must be in T ′ . Again, using the same arguments as in case (2), m ′ is reachable in N ′ . In each case, m ′ is reachable, and so the induction hypothesis is also verified for n, which concludes the induction.

⊓

ω such that m ′ 0 ω -→ m ′ in N ′ , then m 0 ω -→ m in N .
Proof. We proceed by induction.

Induction hypothesis. For all n, if a partial marking m ′ is reachable in N ′ by a sequence ω of n transitions, then there exists a partial marking m so that supp(m) = supp(m ′ ), for all p ∈ supp(m), m(p) = m ′ (p) and m is reachable in N by the sequence ω.

Initialisation. When n = 0, any partial marking m ′ reachable by an empty sequence of transitions must realize m ′ 0 , hence the partial marking m such that ∀p ∈ P ′ , m(p) = m ′ (p) and ∀p ∈ P \P ′ , m(p) = ⋆ must also be realized by m 0 and is thus reachable. This marking m is obviously such that supp(m) = supp(m ′ ), which concludes the initialisation.

Induction. Let consider some n > 0 and assume that the induction hypothesis is verified for n-1. First remark that ω can always be split in two parts: ω ′ of length n -1 and t n (a single transition) such that m ′

0 ω ′ -→ m′ c tn -→ m ′
c in N ′ for some marking m′ c (not a partial one) and some marking m ′ c that realizes m ′ . From the induction hypothesis the only partial marking m so that supp( m) = supp( m′ c ) is reachable in N by the sequence ω ′ , so there exists mc a marking that realizes m and is reached by ω ′ . Moreover, as N ′ is P -complete, if t n is fireable from m′ c in N ′ , then t n is fireable from mc in N (all the preconditions of t n appear in N ′ ). Firing In order to prove Proposition 3 we define a relation over the lists LN ets involved in an execution of Algorithm 1. We show that this relation is an order relation and use this fact to conclude about the termination of the algorithm. Definition 12. Let LN ets 1 and LN ets 2 be two lists involved in an execution of Algorithm 1. We write LN ets 1 < ℓ LN ets 2 if and only if:

length(LN ets 1 ) < length(LN ets 2 ) or length(LN ets 1 ) = length(LN ets 2 ) and ∃1 ≤ k ≤ length(LN ets 2 ) such that

∀1 < i < k, LN ets 1 [i] = LN ets 2 [i] and LN ets 1 [k] < n LN ets 2 [k],
where, for two subnets N 1 and N 2 of a net N, we have N 1 < n N 2 if and only if:

-P 1 ⊃ P 2 or -P 1 = P 2 and T 1 ⊃ T 2 .

If LN ets 1 < ℓ LN ets 2 or LN ets 1 = LN ets 2 we write LN ets 1 ≤ ℓ LN ets 2 .

Lemma 3. The relation ≤ ℓ of Definition 12 is an order relation.

Proof. We prove that ≤ ℓ is reflexive, antisymmetric, and transitive.

Reflexive. This is a direct consequence of the fact that equality is reflexive. We prove that the successive values of LN ets in Algorithm 1 are strictly decreasing with respect to the order relation ≤ ℓ . As there exists a minimal element (the empty list) with respect to this relation, this suffices to prove the termination.

Antisymmetric. Assume that

Assume that an iteration of the main loop (while loop at line 5) starts. This results in, at least, one call to Concretise or one call to Merge. Thus, if we show that LN ets strictly decreases with respect to ≤ ℓ after a call to either of these functions, the termination is given by the above argument.

A call to Merge strictly decreases the length of LN ets. So, by the first point of Definition 12, LN ets strictly decreases with respect to ≤ ℓ .

A call to Concretise does not modify the length of LN ets and modifies exactly one element e of LN ets (or returns false, in which case Algorithm 1 terminates). The modified element is chosen so that its set of transitions is strictly increased (line 5 of Algorithm 2) or its set of places is strictly increased (line 12 of Algorithm 2). In either case, the modified element e ′ is such that e ′ < n e. This ensures that LN ets strictly decreases with respect to ≤ ℓ and concludes the proof.

⊓ ⊔

Lazy reachability analysis with inhibitor arcs

We now transpose the previous results from Petri nets to Petri nets with inhibitor arcs. In such nets, places -when marked -can prevent transitions from being fired. The results of the previous section were correct in all Petri nets, bounded or not. In this section, this will no longer be the case as reachability is known for not being decidable in unbounded Petri nets with inhibitor arcs [START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF][START_REF] Akshay | On Petri nets with hierarchical special arcs[END_REF].

From Petri nets to Petri nets with inhibitor arcs

We start by formally defining Petri nets with inhibitor arcs.

Definition 13 (Petri net with inhibitor arcs). A Petri net with inhibitor arcs is a tuple N I = (P, T, F, I, m 0 ) where (P, T, F, m 0 ) is a Petri net and I :

P × T → N ∪ {∞} is an inhibition function.
Markings, presets and postsets are defined similarly in Petri nets with and without inhibitor arcs. In a Petri net with inhibitor arcs N I , for any t ∈ T , we define • t = {p ∈ P : I(p, t) ̸ = ∞} the inhibition set of t. We extend this notion to sets T of transitions by union of inhibition sets. A transition t ∈ T is fireable from a marking m if and only if ∀p ∈ • t, m(p) ≥ F (p, t) and ∀p ∈ • t, m(p) < I(p, t). The result of firing t is similar as for Petri nets without inhibitor arcs, only the fireability condition changes. Reachability is thus also similarly defined in these two kinds nets. Definition 14 (Subnet with inhibitor arcs). A subnet N ′ I of a Petri net with inhibitor arcs N I = (P, T, F, I, m 0 ) is a tuple (P ′ , T ′ , F ′ , I ′ , m ′ 0 ) such that (P ′ , T ′ , F ′ , m ′ 0 ) is a subnet of (P, T, F, m 0 ) and

I ′ = I |P ′ ,T ′ .
Given a subnet N ′ I of a Petri net with inhibitor arcs N I , and for any t ∈ T ′ , we define •N I t = {p ∈ P : I(p, t) ̸ = ∞)} (that is, intuitively, the inhibition set taken in N I rather than in N ′ I ). The notions of P-completeness, T-completeness, partial marking, reachability of partial markings, and m-completeness remain the same in presence of inhibitor arcs. However, we introduce two other notions of completeness with respect to a net N I for a subnet N ′ I . The notion of PI-completeness expresses that N ′ I contains all the places from N I that may inhibit transitions in N ′ I .

Definition 15 (PI-completeness

). A subnet N ′ I of a net N I is said to be PI-complete when ∀t ∈ T ′ , •N I t ⊆ P ′ .
The notion of TI-completeness expresses that N ′ I contains all the transitions from N I that may remove tokens from places that inhibit transitions in N ′ I .

Definition 16 (TI-completeness). A subnet N ′ I of a net N I is said to be TI-complete when ∀p ∈ • T ′ , p N I • ⊆ T ′ .

An algorithm for lazy reachability analysis with inhibitor arcs

The basic principles of our lazy reachability analysis algorithm for Petri nets with inhibitor arcs are the same as for the case where there are no inhibitor arcs. In fact, the main algorithm that we use is still Algorithm 1 -we simply rename N as N I to make it clear that it has inhibitor arcs -and the merging does not change. However, we use a different concretisation function (Algorithm 3) as well as the following definitions for completeness and consistency. Definition 17. Let N I = (P, T, F, I, m 0 ) be a Petri net with inhibitor arcs and m a marking. A subnet N ′ I of N I is complete with respect to N I and m if (N ′ I is P-complete, PI-complete and) the submarking m ′ is reachable in N ′ I .

Since we still need to check reachability, we must now assume that N I is bounded, though we do not need to know the bound. Even when N I is bounded, its subnets may be unbounded. In the concretisation function, we will nonetheless build our subnets so that they are bounded by construction. Definition 18. The list of subnets LN ets = [(P 1 , T 1 ), ..., (P n , T n )] is consistent if 1. ∀k ̸ = ℓ, (P k ∩ P ℓ ) = ∅, and Algorithm 3 Auxiliary function Concretise(LN ets, m) for Algorithm 1

1: choose k such that LN ets[k] is not complete 2: (P k , T k ) ← LN ets[k] 3: m ′ ← m |P k 4: choose T ′ k such that T k ⊂ T ′ k ⊆ •N I P k ∪ supp(m ′ ) N I • ∪ ( • T k ) N I • 5: if not possible then 6:
return false 7: else 8:

P ′ k ← •N I T ′ k ∪ •N I T ′ k 9: LN ets[k] ← (P ′ k , T ′ k ) 10: end if 11: return true 2. ∀k ̸ = ℓ, T k N • ∩ supp(m |P ℓ ) = ∅. 3. ∀k ̸ = ℓ, T k N • ∩ • T ℓ = ∅.
The main difference with the concretisation function that was used for Petri nets with no inhibitor arcs is that one does not distinguish between the case where transitions should be added and the case where places should be added. Indeed, if one allows for adding transitions without their preconditions, this may result in unbounded subnets. In presence of inhibitor arcs this prevents for checking reachability. One can remark, however, that if all the preconditions of all transitions of a subnet are also part of this subnet, then this subnet is necessarily bounded (if the original net was bounded). This is expressed by Proposition 4 below. Thus, in Algorithm 3, one adds transitions as before to the considered subnet but then one always adds all the preconditions of the newly added transitions.

Remark 1. This explains the parenthesis in Definition 17: all the subnets considered are always P-complete and PI-complete.

Finally, notice that transitions that may remove tokens from inhibition places are also considered when adding transitions, as they can enable new transitions firings.

Proposition 4. Let N I = (P, T, F, I, m 0 ) be a bounded Petri net with inhibitor arcs. Let

N ′ I = (P ′ , T ′ , F ′ , I ′ , m 0|P ′ ) be a subnet of N I . If P ′ ⊇ •N I T ′ k ∪ •N I T ′ k , then N ′ I is bounded.
Proof. Since N I is bounded, let k be the corresponding bound. Assume N ′ I is not k-bounded. Then there exists a transition firing sequence ω = t 1 , . . . , t n , some marking m ′ , and some place p ∈ P ′ such that in N ′ I , we have m 0 m -→ ′ and m ′ (p) > k.

We prove by induction on the length n of ω that it is also fireable in N I and that if m (resp. m ′ ) is the marking obtained in N I (resp. in N ′ I ) after firing ω, then m |P ′ = m ′ .

First suppose n = 0, then the property holds trivially. Now assume it holds for some sequence t 1 , . . . , t n , with n ≥ 0, and consider an additional transition t n+1 ∈ T ′ . Let m n (resp. m ′ n ) be the marking obtained in N I (resp. N ′ I ) after firing t 1 , . . . , t n . By the induction hypothesis m n|P = m ′ n . By construction the preset and inhibitor preset of t n+1 in N I are included in P ′ and therefore since t n+1 is fireable in N ′ I from m ′ n , it is fireable in N I from m n and the effect of those firings on the places in P ′ is the same.

Since N I is k-bounded, ω cannot be fireable in N I so we have a contradiction and N ′ I is therefore bounded. ⊓ ⊔

Proof of the algorithm

We now prove the correctness of Algorithm 1 when used with the concretisation function of Algorithm 3 on a bounded Petri net with inhibitor arcs. First, remark that completeness of the algorithm is achieved essentially for the same reasons as in the previous case. Proof. The proof of Proposition 3 also works here as the order relation of Definition 12 does not depends on the arcs of the nets but only on their places and transitions. The only difference in the proof is to remark that a call to Concretise always increases the set of transitions.

⊓ ⊔

It remains to prove to soundness of the algorithm, which is achieved by proving Propositions 6 and 7. Proposition 6. If Algorithm 1 used with the concretisation function of Algorithm 3 on a bounded Petri net N I with inhibitor arcs returns false, then m is not reachable in N I .

Proof. As before, the only way for Algorithm 1 to return false is at line 11. It implies that the previous call to the Concretise function (Algorithm 3) returned false. This can only occur at line 6 of Algorithm 3.

In this case, it must not be possible to choose Proof. Let m be a reachable marking of N I , with m 0 ω -→ m. Denote by n the number of transitions in ω. We can prove by induction on n that m ′ is reachable in N ′ I . By the contrapositive, this proves the Lemma. The induction is in fact similar to the one used for proving Lemma 1. The only difference is in the induction step where -in cases (2), (3), and (4) -one could imagine that t n would be fireable in N I but not in N ′ I , due to inhibitor arcs. However, the fact N ′ I is TI-complete prevents this: any place p that could inhibit t n must have its full postset in N ′ I and so, if, at some point in ω, p is marked, and later it is unmarked by some transition t, then t must be a transition ). As a consequence, the concatenation of all the ω k allows to reach the objective marking m in N . ⊓ ⊔ Lemma 5. Let N ′ I be a P -complete and PI-complete subnet of a bounded Petri net with inhibitor arcs N I . Let m ′ be a partial marking of N ′ I and let m be a partial marking of N I so that supp(m) = supp(m ′ ) and for all p ∈ supp(m), m(p) = m ′ (p). If there exists a sequence of transitions ω such that m

T ′ k such that T k ⊂ T ′ k ⊆ •N I P k ∪ supp(m ′ ) N I • ∪ ( • T k ) N I • (line 4
′ 0 ω -→ m ′ in N ′ I , then m 0 ω -→ m in N I .
Proof. The only difference with Lemma 2 is that some places in N I may inhibit a transition of ω. This is prevented by the fact that N ′ I is PI-complete: all these place must also exist in N ′ I as well. A similar induction proof can thus be performed.

⊓ ⊔

Experimental evaluation

We have implemented the algorithms in the tool Romeo [16]5 .

Note that since Romeo deals with a very expressive formalism, encompassing inhibitor arcs, we have only implemented the concretisation function described in Section 4, even if it is less efficient than the one in Section 3 for the nets used in the experiments, which do not contain inhibitor arcs.

We implement line 4 in Algorithm 3 by always choosing the biggest possible T ′ k . Actually to account for the added expressiveness of Romeo, where transitions can modify the marking in an arbitrarily complex way, we add even a bit more: every transition that may modify the marking in P k , i. e.,

•N I P k ∪ P k N I • .
For reachability, we perform a simple explicit state exploration with no particular optimization.

Romeo has then been run in a setting as close as we could of the Reachabil-ityCardinality category of the 2020 edition of the model checking contest [START_REF] Kordon | Complete Results for the 2020 Edition of the Model Checking Contest[END_REF], and we compare it with the results of the other tools, which we do not recall here for the sake of space but which are fully available in [START_REF] Kordon | Complete Results for the 2020 Edition of the Model Checking Contest[END_REF]. For each model of the contest, we gave Romeo one hour to solve the same 16 formulas that the contestant had to solve during the contest. The machine we used is not as powerful as the machines used for running the contest (it has four Intel Xeon E5-2620 processors and 128GB of memory), but we did not run Romeo on a virtual machine (during the MCC it would have been the case).

On a factual point of view, Romeo, using only the algorithm presented here, has thus been faced to 1016 different models, among which it fully solved 120 (that is, it solved the 16 formulas corresponding to the model within one hour) and partially solved 288 (that is, solved at least 1 of the formulas within one hour but not the 16 of them). In total, Romeo solved 2654 formulas among 16256. We have also run our algorithm on the 2018 version of the contest, thus on a subset of the models but with different formulas, with similar overall results.

While this overall result is not outstanding, the details are a lot more interesting. First, each result that Romeo returned was the same as the result obtained by the majority of the tools during the actual contest, and hence we can assume with some confidence that all those results are correct.

Second, there is also a lot of room left to improve the algorithm itself, by choosing more cleverly which places to add, which transitions, how much of each partial net to compute, etc. And actually, since we require nothing in terms of exploration order, the technique we propose here should easily be combinable with, e.g., stubborn sets [START_REF] Lehmann | Stubborn sets for simple linear time properties[END_REF] for much better results.

Finally, and most significantly, Romeo managed to completely solve (all 16 formulas) one model (GPPP-PT-C0010N1000000000) that no other tool could handle (they solved at most the first formula). We have had the same results for the 2018 formulas and at that time the other tools had solved none of them. This is very relevant because most of the best performing tools actually have a portfolio approach, in which several techniques are tried in parallel. It thus seems that this model is particularly difficult for current state-of-the-art tools, none of the currently implemented approaches is efficient to handle it, and hardly any progress has been made on it for the last four years (the model was introduced in the 2016 edition).

In contrast, the algorithm we have proposed here performs very well on that model and is thus likely to be a worthy addition to the portfolio approach.

Conclusion

In this paper, we have presented an algorithm for reachability analysis in possibly unbounded Petri nets and in bounded Petri Nets with inhibitor arcs. This algorithm heuristically performs reachability queries on subnets of the original net, in a lazy manner: it works on subnets of increasing size, trying to answer as soon as possible. We have proven that, in each case (unbounded Petri nets, bounded Petri nets with inhibitor arcs), the algorithm terminates, always answers, and always gives correct answers.

We have implemented the approach in the tool Romeo and performed a large scale experimental evaluation based on the models from the 2018 edition of the model-checking contest, showing that on all the models we indeed answered correctly. Moreover, it revealed that our implementation can solve problems that state-of-the-art model-checking tools cannot handle. While for many other problems, those tools outperform our implementation, we believe our algorithm is still a good candidate for inclusion in a portfolio approach.

Future work consists in incorporating the rest of the features of Roméo in the lazy framework: timing parameters, cost optimization, properties beyond reachability, control, etc.

2 Fig. 2 .

 22 Fig. 1. A Petri net N.

Fig. 3 . 3 Fig. 4 .

 334 Fig. 3. Merging of N ′′ 1 and N ′′ 2 .

Proposition 1 .

 1 If Algorithm 1 returns false, then m is not reachable in N . Proof. The only way for Algorithm 1 to return false is at line 11. It implies that the previous call to the Concretise function (Algorithm 2) returned false. This can only occur at line 7 of Algorithm 2.

Proposition 3 .

 3 t n in N leads to a marking m c so that ∀p ∈ P ′ , m c (p) = m ′ c (p), by definition of a subnet. Hence, taking for m the partial marking such that ∀p ∈ supp(m ′ ), m(p) = m c (p) = m ′ c (p) = m ′ (p) and ∀p ∈ P \supp(m ′ ), m(p) = ⋆ concludes the induction. ⊓ ⊔ Algorithm 1 always terminates and returns true or false.

Proposition 5 .

 5 Algorithm 1 always terminates and returns true or false when used with the concretisation function of Algorithm 3 on a bounded Petri net with inhibitor arcs.

Lemma 4 .

 4 ). In other words, the subnet LN ets[k] considered is m ′ -complete (Definition 9), T -complete (Definition 6), and TIcomplete (Definition 16). Moreover, the current marking m ′ must not be reachable in the subnet LN ets[k] due to Remark 1 and is a submarking of m. Hence, by applying Lemma 4 below, m is not reachable in N I .⊓ ⊔ Let N ′ I be a subnet of a bounded Petri net with inhibitor arcs N I . Assume that N ′ I is T -complete and TI-complete. Let m ′ be a marking of N ′ I , that is not reachable. If N ′ I is m ′ -complete, then no marking m of N I such that m ′ is the submarking of m in N ′ I is reachable in N I .

  alse 4: Consistent ← true 5: while not Complete or not Consistent do

	6:	Complete ← ∀k, LN ets[k] is complete
	7:	if not Complete then
	8:	optional unless Consistent
	9:	mayHaveSol ← Concretise(LN ets, m)
	10:	if not mayHaveSol then
	11:	return false
	12:	end if
	13:	end option
	14:	end if
	15:	Consistent ← LN ets is consistent
	16:	if not Consistent then
	17:	optional unless Complete
	18:	M erge(LN ets)
	19:	end option
	20:	end if

21: end while 22: return true

⊔

  Proposition 2. If Algorithm 1 returns true, then m is reachable in N . Proof. The only way for Algorithm 1 to return true is at line 22. This implies that it goes out of the while loop. It means that both Complete and Consistent are true (line 5). So, each element of the list LN ets is complete according to Definition 10 (line 6). Hence, for any k, LN ets[k] is P -complete and the submarking m k of m in LN ets[k] is reachable in LN ets[k]. By Lemma 2, the partial marking of N whose support is exactly the same as the support of m k is reachable in N , using the same sequence of transitions ω k as in LN ets[k]. Moreover, the list LN ets is consistent according to Definition 11 (line 15). Hence, for any k, ℓ the sets of places of LN ets[k] and LN ets[ℓ] are disjoint (part 1. of Definition 11), as LN ets[k] is P -complete, this implies that no transition from LN ets[k] can reduce the marking of a place from LN ets[ℓ]. Moreover, no transition from LN ets[k] can increase the marking of a place from the support of m ℓ (part 2. of Definition 11). As a consequence, the concatenation of all the ω k allows to reach the objective marking m in N . ⊓ ⊔ Lemma 2. Let N ′ be a P -complete subnet of a Petri net N . Let m ′ be a partial marking of N ′ and let m be a partial marking of N so that supp(m) = supp(m ′ ) and for all p ∈ supp(m), m(p) = m ′ (p). If there exists a sequence of transitions

  LN ets 1 ≤ ℓ LN ets 2 and LN ets 2 ≤ ℓ LN ets 1 . Suppose that LN ets 1 < Assume that LN ets 1 ≤ ℓ LN ets 2 and LN ets 2 ≤ ℓ LN ets 3 . We show that LN ets 1 ≤ ℓ LN ets 3 . If LN ets 1 = LN ets 2 or LN ets 2 = LN ets 3 , this is clearly true. Thus, assume LN ets 1 < ℓ LN ets 2 and LN ets 2 < ℓ LN ets 3 . If length(LN ets 1 ) < length(LN ets 2 ), then, as length(LN ets 2 ) ≤ length(LN ets 3 ), one gets length(LN ets 1 ) < length(LN ets 3 ), thus LN ets 1 ≤ ℓ LN ets 3 . In the case where length(LN ets 1 ) = length(LN ets 2 ), two cases are possible : (1) length(LN ets 2 ) < length(LN ets 3 ), then length(LN ets 1 ) < length(LN ets 3 ) is clearly true, and so LN ets 1 ≤ ℓ LN ets 3 , (2) length(LN ets 2 ) = length(LN ets 3 ). In this second case, there exists k such that LN ets1 [k] < n LN ets 2 [k] with ∀i < k, LN ets 1 [i] = LN ets 2 [i] and k ′ such that LN ets 2 [k ′ ] < n LN ets 3 [k ′ ] with ∀i < k ′ , LN ets 2 [i] = LN ets 3 [i].We need to distinguish three cases: (a) k < k', (b) k = k', and (c) k > k'. In case (a), one gets LN ets 1 [k] < n LN ets 3 [k] and ∀i < k, LN ets 1 [i] = LN ets 3 [i], thus LN ets 1 ≤ ℓ LN ets 3 . In case (b), one gets ∀i < k, LN ets 1 [i] = LN ets 3 [i] and LN ets 1 [k] < n LN ets 2 [k] < n LN ets 3 [k]. The transitivity of < n (immediately obtained by transitivity of ⊂) is sufficient to conclude that LN ets 1 [k] < n LN ets 3 [k], and thus LN ets 1 ≤ ℓ LN ets 3 . In case (c), one gets LN ets 1 [k ′ ] < n LN ets 3 [k ′ ] and ∀i < k ′ , LN ets 1 [i] = LN ets 3 [i], thus LN ets 1 ≤ ℓ LN ets 3 . ⊓ ⊔ Proof (of Proposition 3). The only return statements in Algorithm 1 are at line 22 and line 11. At line 22 the algorithm returns true and at line 11 it returns false. This implies that the only possible return values are true and false. It remains to prove that the algorithm terminates.

ℓ LN ets 2 . If length(LN ets 1 ) < length(LN ets 2 ), then length(LN ets 1 ) ̸ = length(LN ets 2 ) and length(LN ets 2 ) < length(LN ets 1 ) cannot be true, so neither LN ets 2 < ℓ LN ets 1 nor LN ets 2 = LN ets 1 can be true, so LN ets 2 ≤ ℓ LN ets 1 cannot be true. If length(LN ets 1 ) = length(LN ets 2 ) and

LN ets 1 [k] < LN ets 2 [k] for some k with LN ets 1 [i] = LN ets 2 [i]

for any i < k, then either (1) P 1 ⊂ P 2 or (2) P 1 = P 2 and T 1 ⊂ T 2 . In case (1), then P 2 ̸ = P 1 and P 2 ⊂ P 1 cannot be true, moreover length(LN ets 2 ) < length(LN ets 1 ) cannot be true. So LN ets 2 < ℓ LN ets 1 nor LN ets 2 = LN ets 1 can be true, so LN ets 2 ≤ ℓ LN ets 1 cannot be true. In case (2), then P 2 = P 1 but T 2 ̸ = T 1 and T 2 ⊂ T 1 cannot be true, moreover length(LN ets 2 ) < length(LN ets 1 ) cannot be true. So LN ets 2 < ℓ LN ets 1 nor LN ets 2 = LN ets 1 can be true, so LN ets 2 ≤ ℓ LN ets 1 cannot be true. In all cases if LN ets 1 < ℓ LN ets 2 then LN ets 2 ≤ ℓ LN ets 1 cannot be true. Thus, as LN ets 1 ≤ ℓ LN ets 2 , one necessarily gets LN ets 1 = LN ets 2 . This proves that ≤ ℓ is antisymmetric.

Transitive.

  If Algorithm 1 used with the concretisation function of Algorithm 3 on a bounded Petri net N I with inhibitor arcs returns true, then m is reachable in N I . Proof. The only way for Algorithm 1 to return true is at line 22. This implies that it goes out of the while loop. It means that both Complete and Consistent are true (line 5). So, each element of the list LN ets is complete according to Definition 17 (line 6). Hence, for any k, LN ets[k] is P -complete, PI-complete, and the submarking m k of m in LN ets[k] is reachable in LN ets[k]. By Lemma 5, the partial marking of N I whose support is exactly the same as the support of m

	from N ′ I .	⊓ ⊔
	Proposition 7.

k is reachable in N I , using the same sequence of transitions ω k as in LN ets[k]. Moreover, the list LN ets is consistent according to Definition 18 (line 15). Hence, for any k, ℓ the sets of places of LN ets[k] and LN ets[ℓ] are disjoint (part 1. of Definition 18), as LN ets[k] is P -complete, this implies that no transition from LN ets[k] can reduce the marking of a place from LN ets[ℓ]. Moreover, no transition from LN ets[k] can increase the marking of a place from the support of m ℓ (part 2. of Definition 18) or the marking of a place that inhibits a transition of LN ets[ℓ] (part 3. of Definition 18

It uses the classical list data structure. The length of a list L is given by length(L). The k th element of L is L[k].

64bits Linux binaries for Romeo and converters from pnml (MCC) to cts (Romeo), and full results are at http://lara.rts-software.org/


Steven J Portugal

Jonathan A Green

Lewis G Halsey
email: l.halsey@roehampton.ac.uk

Walter Arnold

Vincent Careau

Peter Dann

Peter B Frappell

David Grémillet

Yves Handrich

Graham R Martin

Thomas Ruf

Magella M Guillemette

Patrick J Butler

Percy Fitzpatrick

Associations between Resting, Activity, and Daily Metabolic Rate in Free-Living Endotherms: No Universal Rule in Birds and Mammals

Keywords: energy management model; energy expenditure, heart rate, intra-specific, oxygen consumption Running

published or not. The documents may come   L'archive ouverte pluridisciplinaire

INTRODUCTION

Knowledge of energy budgets underlies our understanding of processes operating at every level of biological organisation from the sub-cellular to entire communities. At the whole organism level, energy use is typically quantified in terms of daily energy expenditure (DEE, a proxy for the mean daily energy expenditure of a free-living animal), or basal metabolic rate (BMR, the metabolic rate of an inactive adult non-reproductive post-absorptive endotherm in its thermoneutral zone). Data for rates of energy expenditure, including DEE and BMR, are now available for over 1000 species of birds and mammals [START_REF] Mcnab | An analysis of the factors that influence the level and scaling of mammalian BMR[END_REF][START_REF] Mcnab | Ecological factors affect the level and scaling of avian BMR[END_REF][START_REF] Speakman | Maximal heat dissipation capacity and hyperthermia risk: neglected key factors in the ecology of endotherms[END_REF]. At the intra-specific (interindividual) level, these rates of energy expenditure have been related to other measures such as behaviour, reproductive output, fitness and survival [START_REF] Artacho | Natural selection reduces energy metabolism in the garden snail, Helix aspersa (Cornu aspersum)[END_REF][START_REF] Blackmer | Exploring individual quality: basal metabolic rate and reproductive performance in stormpetrels[END_REF][START_REF] Bochdansky | Experimental evidence for selection against fish larvae with high metabolic rates in a food limited environment[END_REF][START_REF] Boratyński | Sex-specific selection on energy metabolismselection coefficients for winter survival[END_REF][START_REF] Jackson | Associations between energetics and overwinter survival in the short-tailed field vole Microtus agrestis[END_REF][START_REF] Larivée | Associations between over-winter survival and resting metabolic rate in juvenile North American red squirrels[END_REF]).

Meanwhile at the inter-specific level, variation in these rates have been hypothesised to underlie a range of ecological patterns [START_REF] Allen | Global biodiversity, biochemical kinetics, and the energetic-equivalence rule[END_REF][START_REF] Brown | Toward a metabolic theory of ecology[END_REF][START_REF] Buckley | Thermal and energetic constraints on ectotherm abundance: a global test using lizards[END_REF][START_REF] Meehan | Energy use and animal abundance in litter and soil communities[END_REF][START_REF] Meehan | Energetic determinants of abundance in winter landbird communities[END_REF][START_REF] Munch | Latitudinal variation in lifespan within species is explained by the metabolic theory of ecology[END_REF]. As such there has been considerable interest in the effect of broad-scale environmental characteristics on both DEE and BMR (e.g. [START_REF] Anderson | The broad-scale ecology of energy expenditure of endotherms[END_REF][START_REF] Humphries | Expenditure freeze: the metabolic response of small mammals to cold environments[END_REF][START_REF] Jetz | Environment, migratory tendency, phylogeny and basal metabolic rate in birds[END_REF][START_REF] Lovegrove | The influence of climate on the basal metabolic rate of small mammals: a slow-fast metabolic continuum[END_REF][START_REF] Mcnab | Body temperature and metabolism in subspecies of Peromyscus from arid and mesic environments[END_REF][START_REF] Mueller | Metabolic rate and environmental productivity: Wellprovisioned animals evolved to run and idle fast[END_REF][START_REF] Speakman | Maximal heat dissipation capacity and hyperthermia risk: neglected key factors in the ecology of endotherms[END_REF][START_REF] White | Basal metabolic rate of birds is associated with habitat temperature and precipitation, not primary productivity[END_REF]. For example, these inter-specific comparative studies have revealed that both BMR and DEE are negatively associated with mean habitat temperature.

There is also interest in the relationship between DEE and BMR [START_REF] Daan | Avian basal metabolic rates: their association with body composition and energy expenditure in nature[END_REF][START_REF] Koteja | On the relation between basal and field metabolic rates in birds and mammals[END_REF][START_REF] Ricklefs | The relationship between basal metabolic rate and daily energy expenditure in birds and mammals[END_REF][START_REF] White | Does BMR contain a useful signal? Mammalian BMR allometry and correlations with a selection of physiological, ecological and life-history variables[END_REF]. Once the effect of body mass is accounted for, BMR and DEE are positively correlated across eutherian mammals but not significantly correlated across birds or across marsupials [START_REF] Koteja | On the relation between basal and field metabolic rates in birds and mammals[END_REF][START_REF] Ricklefs | The relationship between basal metabolic rate and daily energy expenditure in birds and mammals[END_REF][START_REF] White | Does BMR contain a useful signal? Mammalian BMR allometry and correlations with a selection of physiological, ecological and life-history variables[END_REF]. Intra-specific studies of the relationship between DEE and BMR are less common because both of these quantities have only been measured on the same individuals for a small number of species. Collectively, these investigations yielded equivocal results regarding the relationship between DEE and BMR. While some studies reported a significant correlation between DEE and BMR [START_REF] Nilsson | Metabolic consequences of hard work[END_REF][START_REF] Rezende | Running Behavior and Its Energy Cost in Mice Selectively Bred for High Voluntary Locomotor Activity[END_REF][START_REF] Tieleman | Effects of experimentally increased costs of activity during reproduction on parental investment and selfmaintenance in tropical house wrens[END_REF], other studies reported a nonsignificant correlation after correcting for various intrinsic and extrinsic factors [START_REF] Fyhn | Individual Variation in Field Metabolic Rate of Kittiwakes (Rissa tridactyla) during the Chick-Rearing Period[END_REF][START_REF] Meerlo | Basal metabolic rate in relation to body composition and daily energy expenditure in the field vole, Microtus agrestis[END_REF][START_REF] Peterson | Intrapopulation Variation in Ecological Energetics of the Garter Sanke Thamnophis sirtalis, with Analysis of the Precision of Doubly Labeled Water Measurements[END_REF][START_REF] Speakman | Resting and daily energy expenditures of free-living field voles are positively correlated but reflect extrinsic rather than intrinsic effects[END_REF]. Moreover, some studies found that the association between DEE and BMR can change from one context to another. For example, DEE and RMR were positively correlated in free-living chipmunks during the reproductive season, but this correlation did not persist during other periods of the year [START_REF] Careau | Contextdependent correlation between resting metabolic rate and daily energy expenditure in wild chipmunks[END_REF]. The opposite was found in captive zebra finches, where DEE and RMR were positively correlated at the nonbreeding stage, but not correlated during reproduction (at the one-egg stage, the relationship is dependent on the context under which it is examined, i.e., reproductive season: [START_REF] Careau | Contextdependent correlation between resting metabolic rate and daily energy expenditure in wild chipmunks[END_REF]Vezina et al. 2006).

Our understanding of how animals manage their energy budget assuming they have energetic constraints is intimately linked to the way in which DEE and RMR relate to each other at the intraspecific level. Yet significant insight may be gained by not only looking at BMR (or RMR) and DEE of an animal, but also the energy spent specifically on energetically costly activities [START_REF] Ricklefs | The relationship between basal metabolic rate and daily energy expenditure in birds and mammals[END_REF]. This quantity can be described as AEE (Activity Energy Expenditure; AEE = DEE -RMR; [START_REF] White | Metabolic rate throughout the annual cycle reveals the demands of an Arctic existence in great cormorants[END_REF]. Considering RMR, DEE, and AEE allows us to distinguish among three different conceptual models of energy budgets:

 The 'performance model' [START_REF] Careau | Energy metabolism and animal personality[END_REF]. (Also referred to as the increased-intake hypothesis ;[START_REF] Nilsson | Metabolic consequences of hard work[END_REF]. This model assumes that the capacity to expend energy at a high rate during activity requires greater maintenance costs (i.e., AEE and RMR should be positively correlated). In this case, higher RMR is predicted to be positively related to DEE with a slope >1 [START_REF] Mathot | Energetics and behavior: unrequited needs and new directions[END_REF].

 The 'allocation model' [START_REF] Careau | Energy metabolism and animal personality[END_REF]) sets DEE as a fixed amount and thus it does not vary with RMR, while AEE decreases with increasing RMR. In this case, the slope of the DEE-RMR relationship is predicted to be zero [START_REF] Mathot | Energetics and behavior: unrequited needs and new directions[END_REF].

 Finally, the 'independent model' [START_REF] Careau | Performance, Personality, and Energetics: Correlation, Causation, and Mechanism[END_REF]) describes RMR and AEE as independent of each other such that, for example, increases in RMR do not result in changes to energy spent on other processes. Increases in RMR are nonetheless predicted to have a positive relation with DEE since the former is a component of the latter, but with a slope no greater than unity since there is no relationship between RMR and AEE [START_REF] Mathot | Energetics and behavior: unrequited needs and new directions[END_REF].

An example of the application of such analysis is demonstrated in a study of Australasian gannets Morus serrator by [START_REF] Green | An increase in minimum metabolic rate and not activity explains field metabolic rate changes in a breeding seabird[END_REF], using heart rate (fH) as a calibrated proxy for metabolic rate. The positive correlation between RMR and DEE in this species reflects variation in the magnitude of RMR, but there is no variation in AEE with RMR, suggesting the independent model of energy management. These findings for gannets contrast with the only comparable inter-specific study, in which [START_REF] Ricklefs | The relationship between basal metabolic rate and daily energy expenditure in birds and mammals[END_REF] found that birds showed no significant correlation between BMR and DEE as well as no significant correlation between BMR and AEE, whereas mammals showed a positive correlation between BMR and both DEE and AEE. However, whether the findings of inter-specific studies are comparable to those of intra-specific studies is questionable. Certainly, if we wish to study the consistency/variability of relationships across species, comparisons must be made of multiple intra-specific analyses.

In the present study, we expand on the limited intra-specific data previously analysed and examine the generality of the relationships among RMR, AEE, and DEE using long-term data sets for seven species of bird and four species of mammal. We investigate whether the strategy of energy management differs within or between these two taxa. Each of these data sets uses heart rate (fH) as a proxy for metabolic rate, since heart rate and rate of oxygen consumption ( 2 O V  ) have been shown to be positively correlated in every endothermic species examined so far [START_REF] Green | The heart rate method for estimating metabolic rate: Review and recommendations[END_REF], in accordance with Fick's principle (Fick 1870). For birds we use a quantitative approach (see Green 2011) since qualitative approach for comparative purposes. For mammals we used a qualitative approach (see [START_REF] Green | The heart rate method for estimating metabolic rate: Review and recommendations[END_REF] where directional trends in fH are used to infer directional trends in 2 O V  .

METHODS

Heart rate was measured continuously using surgically implanted heart rate data loggers or transmitters, or by ruminal devices administered orally [START_REF] Signer | A versatile telemetry system for continuous measurement of heart rate, body temperature and locomotor activity in freeranging ruminants[END_REF], employed primarily to investigate other research questions. In total, data sets from seven bird and four mammal species were available for analysis (Table 1). Information and details regarding the devices used, implantation and removal procedures, and data collection protocols are available from the following sources; great cormorants Phalacrocorax carbo [START_REF] Grémillet | Year-round recordings of behavioural and physiological parameters reveal the survival strategy of a poorly insulated diving endotherm during the Arctic winter[END_REF], barnacle geese Branta leucopsis [START_REF] Portugal | Predicting the rate of oxygen consumption from heart rate in barnacle geese Branta leucopsis: effects of captivity and annual changes in body condition[END_REF]), Australasian gannets [START_REF] Green | An increase in minimum metabolic rate and not activity explains field metabolic rate changes in a breeding seabird[END_REF], little penguins Eudyptula minor (J.A. Green, L.R. Horne, P. Dann, P.J. Butler & P.B. Frappell, unpublished data), king penguins Aptenodytes patagonicus [START_REF] Halsey | Changes in the foraging dive behaviour and energetics of king penguins through summer and autumn: a month by month analysis[END_REF], macaroni penguins Eudyptes chrysolophus [START_REF] Green | Evaluating the prudence of parents: daily energy expenditure throughout the annual cycle of a free-ranging bird[END_REF], eider ducks Somateria mollissima [START_REF] Guillemette | Flightlessness and the energetic cost of wing molt in a large sea duck[END_REF]), Przewalski horses Equus ferus przewalksii [START_REF] Arnold | Seasonal adjustment of energy budget in a large wild mammal, the Przewalski horse (Equus ferus przewalskii) II. Energy expenditure[END_REF], alpine ibex Capra ibex [START_REF] Signer | Hypometabolism and basking: the strategies of Alpine ibex to endure harsh over-wintering conditions[END_REF], red deer Cervus elaphus [START_REF] Turbill | Regulation of heart rate and rumen temperature in red deer: effects of season and food intake[END_REF]) and roe deer Capreolus capreolus (W. Arnold, F. Schober, unpublished data). For alpine ibex and red deer, heart rate was determined from an accelerometer located in the reticulum, which accurately recorded heart rate when the instrumented animal was stationary and during relatively gentle activity. At higher levels of activity, however, heart rate was not discernible in the recorded acceleration data, and thus heart rate at high levels of activity is not included in the data sets for these two species.

For all individuals of each species, mean daily heart rate was calculated for each day (i.e., for each 24 h period), while minimum daily heart rate was determined by calculating mean fH for consecutive short time intervals (5-15 min depending on study) throughout the day and selecting the lowest of these values for each day. Activity daily fH was then calculated as the difference between mean daily fH and minimum daily fH. A grand mean of all individuals was then calculated for each day of each study for all three variables. As the data are mean measures of heart rate from successive days, the degree of serial autocorrelation in the data was assessed prior to all statistical tests. The autocorrelation function in Minitab (Mintab Inc.) indicated, for each species, the number of data points between values of mean daily fH, minimum daily fH and activity daily fH required to produce non-significant levels of autocorrelation, i.e. the minimum interval necessary for time series data to be independent. We then calculated means of each of the three variables for time periods equal to the largest of these three intervals for each species (see Table 1) to give the following three variables: mean fH, min fH and activity fH. For birds, mean fH and min fH were converted into estimates of mean V  from fH during flight in the geese at least [START_REF] Ward | Heart rate and the rate of oxygen consumption of flying and walking barnacle geese (Branta leucopsis) and bar-headed geese (Anser indicus)[END_REF]. There is thus an argument to analyse fH data for birds instead. To investigate this we repeated the 2 O V  -based analysis for birds on the underlying heart rate data (Appendix 1).

RESULTS

Table 1 provides full details on the results of statistical analyses undertaken in this study. The duration of data collection varied between species from a few weeks to over two years. Conducting the statistical analysis on data for each species reduced to the size of the smallest data set did not change the overall findings of the study and thus the statistical analyses reported here are based on the full data set available for each species. For all 7 bird species, there was strong evidence that mean 2 O V  was positively related to min 2 O V  (Figure 1a), while in all 4 mammal species there was strong evidence that mean fH was positively related to min fH (Figure 1c). Only the data for macaroni penguins indicated strong evidence for a relationship between activity 2 O V  and min 2 O V  , while there was some evidence for such a relationship in the little penguin data (Figure 1b). For all other bird species there was no evidence of such a relationship. Analysing the fH data for birds, i.e. using the qualitative approach, yielded broadly similar results with only one exception (Appendix 1). All four mammal data sets provided strong evidence of a positive relationship between activity fH and min fH (Figure 1d).

DISCUSSION

The present study shows that qualitative (fH) and quantitative ( 2 O V  ) proxies of resting metabolic rate (RMR) and daily energy expenditure (DEE) are positively related at the intra-specific level in all species of bird and mammal for which data are available (Table 1; Figure 1a andc). This provides evidence that a relationship between RMR and DEE is a consistent feature of endothermic species. The present study also shows that there is a positive intra-specific relationship between qualitative proxies of RMR and activity energy expenditure (AEE) in all examined mammals (Table 1; Figure 1d). In contrast, for five of the seven species of bird examined in the present study there was no evidence for a relationship between estimated RMR and AEE (Table 1; Figure 1b).

Examination of the relationships between RMR, AEE and DEE offers insight into the energy management strategies employed by each species. The key to this analysis is to partition DEE into RMR and AEE in order to test for evidence supporting each of the three theorised models (independent, allocation, performance).For five species of bird analysed, the data suggest they tend to employ the independent model of energy management, however for the macaroni and little penguins, there is evidence of energy management based on the performance model.

Evidence of the energy management strategy employed by each of the mammal species represented in this study can also be obtained through the analysis of the fH data. A relationship with a slope greater than 1 between activity fH and min fH supports the performance model; this was the case for all four species of mammal. Some variety in the energy utilisation model apparently employed between bird species, in contrast to the consistency found within mammals, may at least in part be due to the broader taxonomic range of bird species analysed, though there was a greater range of body masses in the mammals (roe deer: 25 kg; Przewalski horse: 300 kg) than in the birds (eider ducks: 2 kg; king penguins: 10 kg). DEE and RMR were strongly correlated in all 11 species examined here. This is in stark contrast with many previous intra-specific studies, which report non-significant results [START_REF] Fyhn | Individual Variation in Field Metabolic Rate of Kittiwakes (Rissa tridactyla) during the Chick-Rearing Period[END_REF][START_REF] Meerlo | Basal metabolic rate in relation to body composition and daily energy expenditure in the field vole, Microtus agrestis[END_REF][START_REF] Peterson | Intrapopulation Variation in Ecological Energetics of the Garter Sanke Thamnophis sirtalis, with Analysis of the Precision of Doubly Labeled Water Measurements[END_REF][START_REF] Speakman | Resting and daily energy expenditures of free-living field voles are positively correlated but reflect extrinsic rather than intrinsic effects[END_REF]. Aside from one study, based on a low sample size (n=6, r2=0.70 in [START_REF] Nilsson | Metabolic consequences of hard work[END_REF], the r 2 of all of the previously reported statistically significant correlations fall below the range observed in the present study: r 2 =0.20 in [START_REF] Tieleman | Effects of experimentally increased costs of activity during reproduction on parental investment and selfmaintenance in tropical house wrens[END_REF], r 2 =0.23 in [START_REF] Careau | Contextdependent correlation between resting metabolic rate and daily energy expenditure in wild chipmunks[END_REF], r 2 =0.35 in [START_REF] Vézina | Individually variable energy management strategies in relation to energetic costs of egg production[END_REF] and r 2 =0.50 in [START_REF] Rezende | Running Behavior and Its Energy Cost in Mice Selectively Bred for High Voluntary Locomotor Activity[END_REF]. One noticeable difference is that our results are based on heart rate telemetry, whereas all of the studies listed above used doubly labelled water and respirometry techniques to estimate DEE and BMR. Moreover, most of the previous studies reported correlations on a massresidual basis [START_REF] Careau | Contextdependent correlation between resting metabolic rate and daily energy expenditure in wild chipmunks[END_REF] also reported statistically significant correlations on a whole-animal basis), whereas our results are not adjusted for body mass differences between individuals. Previous studies investigated correlations across individuals, whereas in the present study each data point is comprised of the same set of animals. Variation in body mass within individuals over time may well at least in part drive the relationships seen in the present study between RMR, DEE and AEE [START_REF] Portugal | Predicting the rate of oxygen consumption from heart rate in barnacle geese Branta leucopsis: effects of captivity and annual changes in body condition[END_REF].

RMR often shows substantial plasticity, and can be higher in cold-acclimated animals than warm-acclimated ones [START_REF] Mcdevitt | Central limits to sustainable metabolic rate have no role in cold acclimation of the short-tailed field vole (Microtus agrestis)[END_REF][START_REF] Mckechnie | Phenotypic flexibility in basal metabolic rate and the changing view of avian physiological diversity: a review[END_REF][START_REF] Mckechnie | Phenotypic flexibility in the basal metabolic rate of laughing doves: responses to short-term thermal acclimation[END_REF][START_REF] Nespolo | When nonshivering thermogenesis equals maximum metabolic rate: Thermal acclimation and phenotypic plasticity of fossorial Spalacopus cyanus (Rodentia)[END_REF][START_REF] Smit | Avian seasonal metabolic variation in a subtropical desert: basal metabolic rates are lower in winter than in summer[END_REF][START_REF] West | Seasonal differences in resting metabolic rate of Alaskan ptarmigan[END_REF]. Similarly, DEE is negatively related to ambient temperature in some studies (e.g. [START_REF] Speakman | The cost of living: Field metabolic rates of small mammals[END_REF][START_REF] Tinbergen | Parental energy expenditure during brood rearing in the Great Tit (Parus major) in relation to body mass, temperature, food availability and clutch size[END_REF][START_REF] Weathers | Field metabolic rate and water flux of nectarivorous honeyeaters[END_REF], though not in others (e.g. [START_REF] Humphries | Expenditure freeze: the metabolic response of small mammals to cold environments[END_REF]. Where both DEE and RMR are negatively associated with temperature, variation in temperature during the long periods over which heart rate measurements can be made (e.g. 24 -441 d in the present study; Table 1) will manifest as a positive association between DEE and RMR, which might spuriously indicate use of the independent model of energy management. Indeed in macaroni penguins, which spend many months of their annual cycle continuously at sea, RMR will be higher during this period as the animals are in water rather than air which brings a substantial thermoregulatory challenge [START_REF] Green | Cardiovascular adjustments during locomotion in penguins[END_REF]. These days are likely to also be associated with high activity as birds are continually active diving and foraging.

Thus both RMR and AEE are elevated due to covarying environmental circumstances rather than physiological coupling. This may also be the case to a lesser extent for little penguins, which during their winter intersperse intermittent periods of several weeks at sea with periods of several days ashore [START_REF] Ritchie | Do implanted data-loggers affect the time spent at sea by Little Penguins (Eudyptula minor) during winter?[END_REF]. Alternatively, temperature-dependent changes in behaviour may act to buffer or eliminate the effect of ambient temperature on DEE [START_REF] Humphries | Expenditure freeze: the metabolic response of small mammals to cold environments[END_REF][START_REF] Speakman | The cost of living: Field metabolic rates of small mammals[END_REF], and these changes may act in opposition to extrinsically caused changes in RMR. In addition, substitution of the heat required for thermoregulation by the heat produced by activity introduces another potential route for compensation within AEE [START_REF] Humphries | Heat for Nothing or Activity for Free? Evidence and Implications of Activity-Thermoregulatory Heat Substitution[END_REF]; see also 'substitution model' [START_REF] Careau | Performance, Personality, and Energetics: Correlation, Causation, and Mechanism[END_REF]. Therefore, intraspecific associations among RMR, AEE and DEE could be context dependent, as has also been suggested for the consequences of intraspecific variation in RMR [START_REF] Burton | What causes intraspecific variation in resting metabolic rate and what are its ecological consequences?[END_REF]).

Thus it is not clear if the differences observed within the birds, and between birds and mammals in the present study, result from differences among species in their (a) metabolic pathways contributing to RMR and DEE, (b) responses to environmental factors that act as extrinsic drivers of RMR and DEE, or (c) perhaps even locomotion types (all four mammals are terrestrial quadrupeds while the species of bird are either predominantly flyers or swimmers).

Complex interactions among components of energy budgets can obfuscate associations

among RMR, AEE, and DEE. Moreover, even if the performance model is strongly supported at the among-individual level (i.e., slope of the DEE-RMR relationship is >1), this does not rule out the possibility that some form of allocation is occurring within individuals (see Fig. IB in Careau and Garland Jr 2015). Furthermore, AEE is often a broad category encompassing a number of behaviours including feeding, preening, fighting and various types of locomotion that can differ greatly in terms of energy expenditure, and thus further understanding of an animal's energy management strategy may be obtained by investigating the heart rate of various activity sub categories. Finally, it may be the case that some animals alter their energy management strategy during different periods of their breeding or life cycles. For example, during moulting the energy costs of feather production may increase the RMR of birds without affecting their AEE (as shown in eider ducks; [START_REF] Guillemette | Flightlessness and the energetic cost of wing molt in a large sea duck[END_REF]) (the independent model) while during hyperphagia before migration, as their muscles and organs grow they could in theory exhibit both an increase in RMR and a correlated increase in AEE (the performance model) (cf Guillemette and Butler 2012). Future within-species research involving 1) environmentally-controlled scenarios, 2) repeated measures of DEE and RMR on multiple individuals and during different seasons, and perhaps 3) the analysis of metabolic rate for different activity types, will be necessary to uncover any intrinsically driven physiological processes contributing to variation in these traits among and within individuals. V  or fH) in eleven species of free-ranging birds and mammals. Correlations indicating some degree of evidence of a relationship are indicated in bold. Also shown are the number of animals from which data were analysed (N), the length of the data set in days (duration), the autocorrelation, and the resultant number of data points used in the analysis for each species (n). Values in square brackets are bias corrected accelerated 95% confidence intervals (CI) based on 10 000 bootstrapped iterations. *The relationships for king penguins were analysed after a log10 transformation because the data clearly fit a power relationship rather than a linear 500 relationship. The way the exponent is interpreted is the same as for the linear relationships exhibited by all the other species. Some data points are obscured behind others. The y axis of panel C does not include 0. In each panel, the slope of unity is presented as a dashed line. See Table 1 for species name abbreviations.

Species Mean 2 O V  ~ min 2 O V  Activity 2 O V  ~ min 2 O V  Model supported N

APPENDIX -QUALITATIVE ANALYSIS OF METABOLIC RATES IN BIRDS

We repeated the analysis between RMR, AEE and DEE using heart rate (min fH, activity fH and mean fH, respectively) for the seven bird species under consideration. For most correlations for the seven species of bird, the conclusion does not change whether interpreting the data quantitatively ( 2 O V  data) or qualitatively (fH data); Table A1. However, the relationship between activity fH and min fH for Australasian gannets is significantly negative. This is a product of the curvilinear relationship between 2 O V  and fH [START_REF] Green | An increase in minimum metabolic rate and not activity explains field metabolic rate changes in a breeding seabird[END_REF]) and the greater proportion of the day spent in flight by this species (25-35%; Green et al 2013) compared to the other volant bird species included in the present study (usually <5%; [START_REF] Grémillet | Year-round recordings of behavioural and physiological parameters reveal the survival strategy of a poorly insulated diving endotherm during the Arctic winter[END_REF]Pelletier et al. 2008;Portugal et al. 2012). For any species, a curvilinear relationship results in the difference in heart rate between min fH and mean fH equating to a greater difference in 2 O V  at higher heart rates than at lower heart rates. However for the geese, eider and cormorants there is no difference in interpretation between the qualitative and quantitative analyses since on a typical day, high heart rates associated with flight are rarely recorded. In contrast, for the gannets the high heart rates associated with flight are often recorded and these have a disproportionately large effect on DEE. Thus the lack of a relationship between AEE and RMR in Australasian gannets presents as a negative relationship between activity fH and min fH. Overall this then supports the use of the quantitative approach where possible, since it incorporates the maximum amount of information that we have about the respiratory and cardiovascular physiology of these birds. While 2 O V  -fH calibrations were not available for the four mammal species in this study, calibrations for other terrestrial mammals have been reported as linear relationships [START_REF] Green | The heart rate method for estimating metabolic rate: Review and recommendations[END_REF]. Assuming this holds for the mammal species presently under consideration, we would expect the conclusions formed from the fH relationships to hold for those data when converted to 2 O V  . Table 1A. Results of simple linear regressions between qualitative proxies of resting metabolic rate (min fH), daily metabolic rate (mean fH), and activity metabolic rate (activity fH) in seven species of free-ranging birds. Correlations indicating some degree of evidence of a relationship are indicated in bold. Also shown are the number of animals from which data were analysed (N), the length of the data set in days (duration), the autocorrelation, and the resultant number of data points used in the analysis for each species (n)

V

  calibration equations from the following sources: great cormorants[START_REF] White | Metabolic rate throughout the annual cycle reveals the demands of an Arctic existence in great cormorants[END_REF], barnacle geese[START_REF] Portugal | Predicting the rate of oxygen consumption from heart rate in barnacle geese Branta leucopsis: effects of captivity and annual changes in body condition[END_REF]), Australasian gannets[START_REF] Green | An increase in minimum metabolic rate and not activity explains field metabolic rate changes in a breeding seabird[END_REF], little penguins[START_REF] Green | Predicting rate of oxygen consumption from heart rate while little penguins work, rest and play[END_REF], king penguins[START_REF] Halsey | How accurately can we estimate energetic costs in a marine top predator, the king penguin?[END_REF]), macaroni penguins(Green et al. 2000), common eiders (Hawkins et al. 2000) and, where necessary, animal masses reported therein were quantitative proxies for DEE, RMR and AEE, respectively, while for mammals, mean fH, min fH and activity fH were qualitative proxies for DEE, RMR and AEE, respectively. Simple linear regressions conducted in SPSS v.21 (IBM Inc.) examined the relationships between min fH and mean fH, between min fH and activity fH, between min 2 The P value associated with these tests is interpreted as a continuous variable indicating the strength of evidence against the null hypothesis[START_REF] Fisher | Statistical Methods and Scientific Inference[END_REF][START_REF] Halsey | The fickle P value generates irreproducible results[END_REF][START_REF] Lew | Bad statistical practice in pharmacology (and other basic biomedical disciplines): you probably don't know P[END_REF]).These analyses have taken advantage of the2 O V  -fH calibration equations available for all species of bird in the present study. For two of the bird species (great cormorants and Australasian gannets) these calibrations account for the curvilinear relationships in fH and 2 O V observed in flying birds[START_REF] White | Metabolic rate throughout the annual cycle reveals the demands of an Arctic existence in great cormorants[END_REF][START_REF] Green | An increase in minimum metabolic rate and not activity explains field metabolic rate changes in a breeding seabird[END_REF]. However it has not yet been possible to account for this in the calibration equations available for barnacle geese or eider, despite knowing that calibrations based on walking may not accurately estimate 2 O

Figure 1 .

 1 Figure 1. Relationships between qualitative and quantitative proxies of metabolic rate (A and B) in seven species of birds and between measures of heart rate (C and D) in four species of mammal. Explanations for each measure are provided in the main text. Evidence for correlations are indicated by the presence of best fit lines (all data points in panels A, C and D have best fit lines; the line for little penguins in panel B has been extended for clarity).

Figure A1 .

 A1 Figure A1. Relationships between qualitative proxies of metabolic rate in seven species of birds. Evidence for correlations are indicated by the presence of best fit lines (all data points in panel A have best fit lines). Some data points are obscured behind others. In each panel, the slope of unity is presented as a dashed line. See TableA1for species name abbreviations.

Table 1 .

 1 Results of simple linear regressions between qualitative and quantitative proxies of resting metabolic rate (min

	2 V  or fH), daily metabolic rate O

33 [1.08,1.75] 0.88 <0.001 0.33 [0.09,0.76] 0.31 0.03

	Roe Deer	RO	1.2 [1.05,1.34]	0.83 <0.001	0.19 [0.04,0.32]	0.11	0.03	Performance	14	1254	30	45
												Auto-
			slope [95% CI]	r 2	P	slope [95% CI]	r 2	P			Duration	correlation	n
	Great Cormorant	G	1.12 [0.55,1.64]	0.66	0.001	0.12 [-0.50,0.63]	0.02	0.63	Independent	7	172	14
	Barnacle Goose	B	1.12 [0.88,1.32]	0.91 <0.001	0.15 [-0.07,0.34]	0.17	0.12	Independent	6	361	23
	Australasian
	Gannet	A	1.25 [1.01,1.38]	0.82 <0.001	0.26 [-0.02,0.41]	0.16	0.11	Independent	6	237	14
	Little Penguin	L	1.22 [0.89,1.39]	0.86 <0.001	0.21 [-0.17,0.41]	0.15	0.08	Independent/Performance	5	208	10
	King Penguin	K *0.58 [0.14,0.66]	0.83	0.01	*0.38 [-2.15,0.89]	0.08	0.32	Independent	6	30	2
	Macaroni Penguin	M	1.Performance	63	730	49
	Eider Duck	E	1.06 [0.82,1.49]	0.74 <0.001	0.12 [-0.14,0.53]	0.03	0.52	Independent	13	220	13
			Mean fH ~ min fH		Activity fH ~ min fH
			slope [95% CI]	r 2	P	Slope [95% CI]	r 2	P
	Przewalski Horse	P	1.17 [1.08,1.49]	0.97 <0.001	0.17 [0.11,0.35]	0.41	0.01	Performance	7	371	24
	Alpine Ibex	A	1.13 [1.04,1.31]	0.98 <0.001	0.14 [0.06,0.25]	0.40	0.01	Performance	20	348	48
	Red Deer	R	1.07 [1.04,1.09]	1.00 <0.001	0.08 [0.05,0.11]	0.56 <0.001	Performance	15	771	24

33 [1.06,1.79] 0.87 <0.001 0.33 [0.08,0.76] 0.31 0.03

  . Values in square brackets are bias corrected accelerated 95% confidence intervals (CI) based on 10 000 bootstrapped iterations. 545

			Mean fH ~ min fH		Activity fH ~ min fH
												Auto-
	Species		slope [95% CI]	r 2	P	slope [95% CI]	r 2	P	Model supported	N Duration	correlation	n
	Great Cormorant	G	0.83 [0.47,1.14]	0.70 <0.001	-0.17 [-0.54,0.15]	0.08	0.34	Independent	7	172	14
	Barnacle Goose	B	1.13 [0.91,1.31]	0.92 <0.001	0.13 [-0.09,0.32]	0.13	0.17	Independent	6	361	23
	Australasian
	Gannet	A	0.66 [0.53,0.75]	0.79 <0.001	-0.33 [-0.46,-0.25]	0.49	<0.01		6	237	14
	Little Penguin	L	1.21 [0.90,1.40]	0.86 <0.001	0.23 [-0.10,0.41]	0.18	0.06	Independent/Performance	5	208	10
	King Penguin	K	1.04 [0.27,1.36]	0.67 <0.001	0.04 [-0.75,0.36]	0.00	0.85	Independent	6	30	2
	Macaroni Penguin	M	1.Performance	63	730	49
	Eider Duck	E	1.08 [0.79,1.50]	0.68 <0.001	0.05 [-0.28,0.59]	0.00	0.81	Independent	13	220	13

OV  -fH calibrations were available for each species, and also report the output resulting from the

ACKNOWLEDGEMENTS

We are particularly thankful for the input to this manuscript by Craig White. We are grateful to Tony Woakes and Maarten Loonen for assistance with the barnacle geese data, to Frank Shober for help with roe deer data collection, and to Grégoire Kuntz and Caroline Gilbert for help with collection of the great cormorant data. For funding and ethical approvals for each species, please refer to the relevant studies.

AUTHOR CONTRIBUTIONS

LH conducted all the statistical analyses, produced all the figures, interpreted the results and fronted the writing of the manuscript in its current format; JG conducted some preliminary analyses, interpreted the results and had considerable input to the writing of the manuscript; SP and PB also supported writing the manuscript; all coauthors provided data and commented on manuscript drafts.