Fabrizio Biondi
email: fabrizio.biondi@inria.fr

Axel Legay
email: axel.legay@inria.fr

Bo Friis Nielsen

Pasquale Malacaria
email: p.malacaria@qmul.ac.uk

Andrzej W Ąsowski
email: wasowski@itu.dk

Bo Friis Nielsen

Andrzej W Ąsowski;

Information Leakage of Non-Terminating Processes *

Keywords: 1998 ACM Subject Classification D.4.6 Security and Protection, G.3 Stochastic Processes, H.1.1 Systems and Information Theory Quantitative information flow, Markov chain, information leakage, infinite execution Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

In recent years, quantitative security techniques have been providing effective measures of the security of a system against an attacker. Such techniques usually assume that the system produces a finite amount of observations based on a finite amount of secret bits and terminates, and the attack is based on these observations. By modeling systems with Markov chains, we are able to measure the effectiveness of attacks on non-terminating systems. Such systems do not necessarily produce a finite amount of output and are not necessarily based on a finite amount of secret bits. We provide characterizations and algorithms to define meaningful measures of security for non-terminating systems, and to compute them when possible. We also study the bounded versions of the problems, and show examples of non-terminating programs and how their effectiveness in protecting their secret can be measured.

Introduction

Information-theoretical quantitative security techniques evaluate the effectiveness of a system in protecting a secret it depends on. Given a known finite size of a secret in bits, they quantify how many bits of the secret can be inferred by an attacker able to observe the system's output. This value is referred to as information leakage, or just leakage. Leakage quantification techniques have been successfully applied to security problems, including proving the effectiveness of bug fixes to the Linux kernel [START_REF] Heusser | Quantifying information leaks in software[END_REF], quantifying anonymity [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF], and analyzing side channel attacks to the cache of a processor [START_REF] Köpf | Automatic quantification of cache side-channels[END_REF].

The theory behind these techniques commonly assumes that the program under analysis terminates at some point, and the computed leakage corresponds to the amount of information that the attacker gains at program termination time. When the secret does not change during computation, a program can be modeled as a channel matrix, assigning the conditional probability of each possible output for each possible input. The size of the channel matrix is usually exponential in both secret and output size. We have previously proposed the use of Markovian models instead to overcome this problem [START_REF] Biondi | Quantifying information leakage of randomized protocols[END_REF].

Markovian models can also be conveniently used to model non-terminating processes, something finite-size channel matrices cannot do. This allows us to study leakage properties of systems like webservices, server modules and operating system daemons.

In this paper we provide techniques and algorithms to quantify the Shannon leakage and leakage rate of non-terminating processes. Shannon leakage has a clear operational significance related to the number of attempts that an attacker has to try to guess a secret [START_REF] Massey | Guessing and entropy[END_REF]. Other measures exist, modeling different security properties (e.g. [START_REF] Smith | On the foundations of quantitative information flow[END_REF]). Our contributions are:

We characterize program-attacker scenarios according to the finiteness of the system's secret and the finiteness of the attacker's observation. We show how this characterization influences the finiteness of the information leakage in the scenario. We provide a method to compute information leakage of a scenario with either an infinite secret or an infinite observation. Such scenarios cannot even be modeled with a finite size channel matrix.

We demonstrate this method with an example. We provide a method to compute the rate of information leakage per time unit, when the leakage itself is infinite. This is the case when a scenario has an infinite secret and an infinite observation, as is common e.g. in webservices. We demonstrate this method using a mix node as an example.

We provide an algorithm to compute how much information is leaked from a given time to another given time.

We show that determining the exact time in which a given amount of information is leaked is hard, by reduction to the knowingly hard to decide Skolem's problem. We distinguish four possible scenarios, according to whether the observation by the attacker is finite or infinite and whether the secret itself is finite or infinite. The cases are summarized in Fig. 1. The case with finite observation over a program depending on a finite secret is the terminating case we considered previously [START_REF] Biondi | Quantifying information leakage of randomized protocols[END_REF], while the others will be considered in this paper. When only one of observation or secret is finite the leakage is finite but cannot be computed using the method we introduced previously [START_REF] Biondi | Quantifying information leakage of randomized protocols[END_REF], thus we provide a new technique in Section 3. When both observation and secret are infinite, the leakage is potentially infinite. In this case we compute the rate of leakage, i.e. the amount of information leaked for each time unit. Intuitively, this quantifies the average amount of information the attacker infers for each time unit over an infinite time. This is presented in Section 4. In Section 5 we analyze how much information is leaked in a given time frame and how much time it takes to leak a given amount of information. Section 6 concludes the paper and discusses related work.

Background

We refer to literature [START_REF] Cover | Elements of Information Theory[END_REF] for the definitions of sample space S, probability of event P (E) and so on. X is a discrete stochastic process if it is an indexed infinite sequence of discrete random variables

(X 0 , X 1 , X 2 , ...). A discrete stochastic process is a Markov chain C = (C 0 , C 1 , C 2 , ...) iff ∀k ∈ N. P (C k |C k-1 , C k-2 , ..., C 1 , C 0 ) = P (C k |C k-1
). A Markov chain on a sample space S can also be defined as follows:

◮ Definition 1. A tuple C = (S, s 0 , P ) is a Markov Chain (MC), if S is a finite set of states, s 0 ∈ S is the initial state and P is a single |S| × |S| probability transition matrix, so ∀s, t ∈ S. P s,t ≥ 0 and ∀s ∈ S. t∈S P s,t = 1.

The probability of transitioning from any state s to a state t in k steps can be found as the entry of index (s, t) in P k [START_REF] Cover | Elements of Information Theory[END_REF]. We write π (k) for the probability distribution vector over S at time k and π (k) s the probability of visiting the state s at time k; note that π (k) = π 0 P k , where π (0) s is 1 if s = s 0 and 0 otherwise. A probability distribution π over the states of the chain is stationary if π = πP . Given an initial distribution π (0) we compute the unique stationary limit distribution µ as µ = lim k→∞ π (0) P k . We write ξ s for the expected residence time of state s ∈ S: ξ s = ∞ k=0 P k s0,s . A state s ∈ S is absorbing if P s,s = 1. In the figures we do not draw the looping transition of the absorbing states, to reduce clutter.

We will enrich our Markovian models with a finite set V of natural-valued variables, and for simplicity we assume that there is a very large finite bit-size M such that a variable is at most M bit long. We define an assignment function A : S → [0, 2 M -1] |V| assigning to each state the values of the variables in that state. We write v(s) to denote the value of the variable v ∈ V in the state s ∈ S. Consider a stochastic process representing the value of a variable v over time, derived fro the behavior of a Markov chain labeled with valuations of this variable. We will call this process the marginal process, or just marginal, C |v on v, formally: ◮ Definition 2. Let C = (S, s 0 , P ) be a Markov chain and v ∈ V a variable. Then we define the marginal process C |v of C on v as a stochastic process (v 1 , v 2 , ...) where ∀n.

P (v k = n) = {s|v(s)=n} π (k) s
We will use v to denote the marginal process when it is clear from the context that we refer to it. Note that C |v is not necessarily a Markov chain. When it is, it can be drawn like in Fig. 3bcd. In the paper we will allow assignments of sets of values to variables and marginals on sets of variables; such extensions are straightforward, since multiple variables can be seen as a single variable on their product space. Assume that the system modeled by C has a single secret variable h and a single observable variable o. Then the distributions over the marginal processes C |h and C |o model the behavior of the secret and observable variable respectively at each time step, and their correlation quantifies the amount of information about the secret that can be inferred by observing the observable variable.

Entropy is a measure of the uncertainty of a probability distribution. The following definitions are standard:

◮ Definition 3 ([8]). Let X and Y be two random variables with probability mass functions p(x) and p(y) respectively and joint probability mass function p(x, y). Then we define the following non-negative real-valued functions:

Entropy

H(X) = -x∈X p(x) log 2 p(x) Joint entropy H(X, Y ) = -x∈X y∈Y p(x, y) log 2 p(x, y) Conditional entropy H(X|Y ) = -x∈X y∈Y p(x, y) log 2 p(x|y) = = y∈Y p(y)H(X|Y = y) = -y∈Y p(y) x∈X p(x|y) log 2 p(x|y) = = H(X, Y ) -H(Y ) (chain rule) Mutual information I(X; Y ) = x∈X y∈Y p(x, y) log 2 p(x,y) p(x)p(y) = = H(X) + H(Y ) -H(X, Y ) ≤ min(H(X), H(Y ))
Mutual information can be generalized to two vectors of random variables X, Ȳ as

I( X; Ȳ ) = x∈ X ȳ∈ Ȳ p(x, ȳ) log 2 p(x,ȳ) p(x)p(ȳ) .
◮ Definition 4. [START_REF] Cover | Elements of Information Theory[END_REF] Let X = (X 1 , X 2 , ...) and Y = (Y 1 , Y 2 , ...) be two stochastic processes. Then we define the following non-negative real-valued functions:

Entropy

H(X ) = lim k→∞ H(X 1 , X 2 , ..., X k ) Entropy rate H(X ) = lim k→∞ 1 k H(X 1 , X 2 , ..., X k ) when the limit exists Mutual information I(X ; Y) = lim k→∞ I(X 1 , X 2 , ..., X k ; Y 1 , Y 2 , ..., Y k ) Mutual information rate Ī(X ; Y) = lim k→∞ 1 k I(X 1 , X 2 , ..., X k ; Y 1 , Y 2 , .
.., Y k ) when the limit exists Entropy and mutual information of stochastic processes always exist, as shown in Section 3. Entropy rate and mutual information rate may not exist in general, but exist when the stochastic processes are Markov chains [START_REF] Cover | Elements of Information Theory[END_REF]; we discuss them in Section 4.

Since every state s in a MC C = (S, s 0 , P ) has a discrete probability distribution over the successor states we can calculate the entropy of this distribution, the local entropy: ◮ Definition 5. Let C = (S, s 0 , P ) be a Markov chain. Then for each state s ∈ S we define the local entropy of s as L(s) = -t∈S P s,t log 2 P s,t Note that L(s) ≤ log 2 (|S|) [START_REF] Biondi | Maximizing entropy over Markov processes[END_REF]. If a stochastic process is a Markov chain C, its entropy H(C) can be computed by considering the local entropy L(s) as the expected reward of a state s and then computing the expected total reward of the chain [START_REF] Biondi | Maximizing entropy over Markov processes[END_REF]: H(C) = s∈S L(s)ξ s . It is also known that the entropy rate can be computed similarly by summing the local entropies of each state weighted by the state's probability in the limiting distribution [START_REF] Cover | Elements of Information Theory[END_REF]:

H(C) = s∈S L(s)µ s .
In this paper we use information theory to compute the amount of bits of a secret variable h that can be inferred by an attacker able to observe the value of an observable variable o at any moment in time. We call this amount Shannon leakage or just leakage, and it corresponds to the mutual information I(C |o , C |h ) between the marginal on the secret and the marginal on the observable variable.

Operationally, Shannon leakage is related to the number of attempts that an attacker has to do to guess the value of the secret. Other leakage measures exist, but Shannon leakage is the only one for which the chain rule of Definition 3 holds; since the chain rule is used in many results in this work, we do not expect such results to extend to other leakage measures. The modeling of a process as a Markov chain in our context starts by dividing the variables in private and public variables. Private variables, including the secret variable h, are the ones whose value is not defined at compilation time. In each state of the Markov chain a set of allowed values is assigned to each private variable. Public variables, including the observable variable o and the program counter pc, are variables whose value is known to the analyst. On each state a given value is assigned to each public variable.

Given the source code and a prior distribution over the private variables, we have enough information to build a Markov chain representing the semantics, since for each state we can determine its successor states and the corresponding transition probabilities. We show a simple example, and refer to [START_REF] Biondi | Quantifying information leakage of randomized protocols[END_REF] for the complete semantics. The source code for the example is shown in Fig. 2 and the corresponding Markov chain semantics in Fig. 3a.

Let h be a secret bit, o an observable bit and r a random bit being assigned the value 0 with probability 0.75 and 1 otherwise. We assign to o the result of the exclusive OR between h and r and terminate. We want to quantify the amount of information about h that can be inferred by knowing the value of o.

To compute the leakage we need to compute three marginals from the Markov chain semantics: Joint marginal The joint marginal process C |(o,h) models the joint behavior of the secret and observable variables. It is shown in Fig. 3b.

Figure 3 Bit XOR example: a) Markov chain semantics C. b) Joint marginal C |(o,h) . c) Secret's marginal C |h . d) Observer's marginal C |o .
Secret's marginal The secret's marginal process C |h models the behavior of the secret variable. It is shown in Fig. 3c. Observer's marginal The observer's marginal process C |o models the behavior of the observable variable. It is shown in Fig. 3d. Finally we compute the mutual information between the secret and observable variable using the formula

I(X; Y ) = H(X) + H(Y ) -H(X, Y ), obtaining I(o; h) = I(C |o ; C |h ) = H(C |o ) + H(C |h )) -H(C |(o,h) )) = 1 + 1 -1.8112... ≈ 0.
1887 bits, proving that the program leaks ≈ 0.1887 bits, or 18.87% of the secret.

Non-terminating Processes with Finite Leakage

The Markov chain semantics of the system describes the joint behavior of all variables. To compute information leakage we are only interested in the secret and the observable variables, so we can restrict to them only for simplicity. We assume that the system has a single secret variable h with uniform prior distribution and a single observable variable o, but the procedure does not change for multiple secret or observable variables. We remark that, even though the attacker can perform multiple observations, we do not model the case in which the attacker actually interacts with the system. In such case directed information would have to be used as the leakage metric instead of mutual information. We refer to Alvim et al. [START_REF] Alvim | Quantitative information flow in interactive systems[END_REF] for the details.

The behavior of the secret variable h is modeled by the marginal C |h , and similarly the behavior of o is modeled by C |o and the joint behavior of the two variables by C |o,h . The following lemma shows the existence of the entropy values of such marginals and a sufficient condition for the finiteness of their mutual information: ◮ Theorem 6. Let C = (S, s 0 , P ) be a Markov chain with secrets and observations and C |o and C |h its marginals on the observable and secret variables, respectively. Then:

H(C |o ), H(C |h ) and I(C |o ; C |h ) exist; H(C |o ) < ∞ ∨ H(C |h ) < ∞ ⇒ I(C |o , C |h ) < ∞ Intuitively, if H(C |o ) < ∞ and H(C |h ) = ∞
then there is an infinite number of secret bits but only a finite amount of observations we can analyze. In the opposite case where H(C |o ) = ∞ and H(C |h ) < ∞ we can analyze an infinite number of observations, but there is only a finite amount of secret bits to be discovered.

If either H(C |o ) = ∞ or H(C |h ) = ∞ then H(C |o,h ) = ∞, since H(X, Y ) ≥ max(H(X), H(Y )).
It follows that if either the observation or the secret are infinite but not both, the formula

I(C |o , C |h ) = H(C |o ) + H(C |h ) -H(C |o,h
) will produce an indeterminate form ∞ -∞ and thus cannot be directly used to compute the leakage. Nonetheless, in both cases leakage has a finite value by Theorem 6.

If any marginal is a Markov chain, it is possible to compute its entropy in polynomial time in the size of the chain [START_REF] Biondi | Maximizing entropy over Markov processes[END_REF]. Otherwise, consider that the entropies of the marginals are limit computations, since H(C |v ) = lim k→∞ H(v 1 , ..., v k ). This allows us to compute mutual information using the limit of the entropies of the marginal processes:

I(C |o ; C |h ) = lim k→∞ I(o 1 , ..., o k ; h 1 , ..., h k ) = lim k→∞ (H(o 1 , ..., o k ) + H(h 1 , ..., h k ) -H((o, h) 1 , ..., (o, h) k ))
The limit above computes information leakage in any case, but is not always the most efficient option available. When it is known that the secret (resp. observation) is finite, it is more efficient to use the formula

I(C |o ; C |h ) = H(C |h ) -H(C |h |C |o ) (resp. I(C |o ; C |h ) = H(C |o ) -H(C |o |C |h )).
Remember that when both secret and observation are finite the process terminates, so the procedure we proposed in [START_REF] Biondi | Quantifying information leakage of randomized protocols[END_REF] can be used with some additional assumptions.

Example: A Non-terminating Program on a Finite Secret

We now solve a case in which the secret is finite and Markovian and the observation infinite. Consider a program (Figure 4) with a secret bit h. If h is 0 the program produces an infinite string of zeroes and ones with the same probability 0.5, starting with a zero. If h is 1 the program also produces a string of zeroes and ones starting with a zero, but the probability that it will produce a zero is 0.75. Note that this program cannot be encoded as a finite channel matrix, as it has an infinite amount of possible outputs.

An attacker may be able to observe this infinite string and infer information about the secret by studying the frequencies of zeroes and ones. The attacker starts with no knowledge of the secret, which is encoded as an initial uniform distribution over the secret bit h. Reasonably, an attacker observing the output for an infinite time would be able to decide whether the frequency of zeroes is 0.5 or 0.75 and infer the value of h consequently. The Markov chain semantics for it is shown in Fig. 4a on the right.

Since h 1 = h 2 = h 3 = ... we will just call it h. The behavior of h is modeled by the Markov chain in Fig. 4b on the right, and its entropy is

H(h) = 1 bit. H(C |h |C |o ) corresponds to lim k→∞ H(h|o 1 , ..., o k ).
We compute H(h|o 1 , ..., o k ) for k → ∞. Note that at time 1 o is always 0, then it changes randomly depending on the value of h. We will write down the joint distribution of h and o as a function of k and use it to compute the marginal over o and finally the conditional entropy.

The joint distribution of h and o is shown in the Appendix due to space constraints. Now let w k ∈ {0, 1} k be a sequence of k bits. Consider the formula for conditional entropy:

H(h|o 1 , ..., o k ) = w k ∈{0,1} k P (o 1 , ..., o k = w k )H(h|o 1 , ..., o k = w k ) (1)
In our case it holds that

H(h|o) = lim k→∞ H(h|o 1 , ..., o k ) = 0 thus I(o; h) = H(h)-H(h|o) = 1 -0 = 1 bit.
The leakage of the program in Fig. 4 is 1 bit, proving that an attacker able to analyze the bit streams produced by the system will eventually learn the value of the secret h with an arbitrary confidence. Note that this considers an attacker able to observe the system for an infinite time.

More importantly, note that the marginal process of o is not a Markov chain. This depends on the fact that the joint distribution depends also on the information that the attacker has about h, so while the attacker gathers information about o and h the joint distribution changes and thus the marginal distribution of o changes also. Nonetheless, the marginal process can be represented in a closed form like the one in Fig. 6d.

Leakage Rate of a Markov Chain

In the case in which H(C |o ) = ∞ and H(C |h ) = ∞, i.e. when the secret is an infinite number of bits and the observer can observe it for an infinite time, then the leakage I(o, h) can be infinite. In this case it is more interesting to compute how much information the process leaks for each time step. This quantity is known as leakage rate, and corresponds to the mutual information rate of the secret and observable.

Note that the computation of leakage as a rate over time assumes that the attacker is able to keep track of the discrete time, so in this section we will assume that every constant-time operation takes 1 time step. This can be equivalently stated as saying that all transitions between states of the Markov chain semantics represent observable steps.

To compute leakage rate, we encode the process-attacker scenario with a Markov chain as shown in Section 2 and compute the joint, secret and attacker's marginal, which may not be Markovian. Then we can use the marginals to compute leakage rate by applying the following definition: ◮ Definition 7. Let C = (S, s 0 , P ) be a Markov chain and C |o,h , C |o and C h its marginals on (o,h), o and h respectively. Then the leakage rate Ī is defined as

Ī(C |o ; C h ) = H(C |o ) + H(C |h ) -H(C |o,h ).
Leakage rate can also be computed as a limit, since

Ī(C |o ; C |h ) = lim k→∞ I(o 1 , ..., o k ; h 1 , ..., h k ) k = lim k→∞ (H(o 1 , ..., o k ) + H(h 1 , ..., h k ) -H((o, h) 1 , ..., (o, h) k )) k
when the limit exists.

Generally both entropy and leakage rate could be infinite, for instance for a program that leaks 1 bit at time 1, 2 bits at time 2, and so on, the leakage rate would be infinite. Since we postulated that there exists a very large but finite maximum size M for the variables declared in the system, Data: A Markov Chain C = (S, s 0 , P ) and its initial probability distribution π (0) . Result: The limit probability distribution µ of the chain.

1 foreach transient state t do 2 µ t ← 0; 3 foreach u ∈ S \ {t} do 4 π (0) u ← π (0) u + π (0) t Pt,u 1-Pt,
Ri = r∈Ri π (0)
s and E i be a system of linear equations;

13 foreach r ∈ R i do Add to E i the equation µ r = r ′ ∈Ri µ r ′ P r ′ ,r ; 14 Solve the system E' under the condition r∈Ri µ r = π (∞)
Ri to obtain µ r for each r ∈ R i ; 15 end Algorithm 1: Compute the limit distribution of a Markov chain.

it is impossible to declare an unbounded amount of secret or observable bits on each step of the program execution. We do not think that this restriction limits significantly the programs that can be analyzed, while guaranteeing that the entropy and leakage rate do not diverge to positive infinity is a significantly useful result. entropy rate and leakage rate may still oscillate, even though since they are defined in terms of Cesàro limits this happens only in pathological cases. We do not expect these cases to be common in normal secret-dependent systems, and leave finding a meaningful measure of leakage for these cases an open problem. This reflects similar issues in related definitions of leakage rate [START_REF] Chothia | Probabilistic point-to-point information leakage[END_REF][START_REF] Malacaria | Assessing security threats of looping constructs[END_REF].

A case in which both entropy and leakage rate exist is when the marginal processes modeling the behavior of the observable and secret variables are both Markovian. Intuitively, this happens when the secret gets periodically replaced with a new one, and thus the information the attacker has on it is reset to the prior information. We will show this with an example in Section 4.1.

When any of the marginals is a Markov chain it is possible to compute its entropy rate efficiently as H(C) = s∈S L(s)µ s , where µ is the limit distribution of the chain. The entropy rate of a Markov chain with a given initial probability distribution π (0) exists and is unique [START_REF] Cover | Elements of Information Theory[END_REF].

Computing the limit distribution can be accomplished on irreducible Markov chains by solving a system of linear equations, but the Markov chains we consider are usually reducible, so a new algorithm is required. Algorithm 1 computes the limit distribution of any Markov Chain C = (S, s 0 , P ). The algorithm uses the well-established concept of end components of a MC; each end component R i behaves as an irreducible MC, so it is sufficient to compute the probability π (∞)

Ri of eventually visiting R i and redistribute π (∞)

Ri among the states of R i by solving a system of linear equations.

◮ Theorem 8. Algorithm 1 terminates in polynomial time in |S| and when it does it returns the limit distribution µ.

Due to space constraints we refer to the Appendix for the proof of this theorem and a full explanation of the steps of Algorithm 1. 2) is trivial, the formula H(C) = s∈S L(s)µ s can be used to compute entropy rate of a Markov chain in polynomial time. Note that this is a particular case of the computation of an expected infinite-horizon reward rate of a reward function defined on the transitions of a Markov chain.

Since computing the local entropy of each state in time O(|S|

Having computed the entropy rates of the joint, secret and attacker's marginals we can apply Definition 7 to obtain the leakage rate of the system.

Example: Leaking Mix Node Implementation

We show an example of a program leaking an infinite amount of information and we compute its leakage rate using the method described above. A mix node [START_REF] Danezis | Mixminion: Design of a type iii anonymous remailer protocol[END_REF] is a program meant to scramble the order in which packages are routed through a network, to increase the anonymity of the sender. Even if the packages are encrypted, some information about the sender could be inferred by observing the order in which they are forwarded. A mix node changes this order to a random one, thus making it harder for an attacker to connect each package to its sender.

A mix node waits until it has accumulated a fixed amount of packages, and then forwards them in a random order. If the exit order of the packages is independent from the entrance order, then no information about the latter can be inferred by observing the former. We will present an implementation of a mix node where the entrance and exit order are not independent and compute the rate of the information leakage.

The implementation of the mix node is shown in Fig. 5. This particular node waits until it has accumulated 3 packages and then sends them in a random order. Naming the packages A, B and C there are 6 possible entrance orders: ABC, ACB, BAC, BCA, CAB, and CBA. We will number them from 0 to 5.

In line 5 of the code a random number from 0 to 5 is assigned to the secret variable inorder, modeling the secret entrance order. Then in line 6 a random value uniformly distributed from 0 to 5 is assigned to the variable rand. Finally, in line 7 the bitwise exclusive OR modulo 6 of the variables inorder and rand is assigned to the observable variable outorder, which represents the order in which the packages exit from the mix node and is observable to the attacker. After producing an exit order the mix node receives three more packages in a new entrance order, scrambles them the same way and forwards them, and so on forever.

Assume that the prior distribution over the input order is uniform. The resulting probability distribution on the exit order is P (outorder) = {0 → 5 /18, 1 → 5 /18, 2 → 2 /18, 3 → 2 /18, 4 → 2 /18, 5 → 2 /18}. This depends on the fact that bitwise OR and modulo operations do not preserve distribution uniformity.

The Markov chain semantics of the system has more than 300 states. It can be computed and analyzed automatically in less than a second. Assuming that each line of code is executed in one time step, the entropy rates of the marginals are H(inorder) = 0.86165... bits, H(outorder) = 0.82766... and H(inorder, outorder) = 1.59367..., giving a leakage rate of Ī(inorder; outorder) = H(inorder)+ H(outorder)-H(inorder, outorder) = 0.86165...+0.82766...-1.59367... ≈ 0.09564 bits.

The leakage rate for each time unit is ≈ 0.09564 bits. Since the entropy rate of the secret is ≈ 0.86165 bits, we can conclude that this implementation of a mix node has a rate of leakage Data: A Markov Chain C = (S, s 0 , P ) with the variables o and h, two integers t 1 and t 2 satisfying t 1 ≤ t 2 . Result: The leakage from time t 1 to time t 2 I (t1,t2) (o, h)

1 for x ∈ {o, h, (o, h)} do 2
Compute the marginal C |x , and let π (t1) |x be the probability distribution over its states at time t 1 and

H (t1) (C |x ) = H(π (t1) |x ); 3 end 4 Compute I (t1,t1) = H (t1) (C |o ) + H (t1) (C |h ) -H (t1) (C |o,h ); 5 for i = t 1 + 1 to t 2 do 6 for x ∈ {o, h, (o, h)} do 7 H (i) (C |x ) ← H (i-1) (C |x ) + s∈S |x π (i-1) |x (s)L |x (s); 8 π (i) |x ← π (i-1) |x P (i-1,i) |x ; 9 end 10 I (t1,i) ← H (i) (C |o ) + H (i) (C |h ) -H (i) (C |o,h );
11 end 12 return I (t1,t2) ; Algorithm 2: Compute the leakage of a MC from a time t 1 to a time t 2 . 0.09564/0.86165 ≈ 11.1% of each of its infinite secrets.

Note that in this simple case the loop always takes 3 time units to complete, so it would have been possible to just compute the leakage of one loop and divide it by 3, but in general loops do not compute for a fixed number of time units, e.g. if they contain multiple return statements.

Bounded Time/Leakage Analysis

We consider two similar bounded approaches to the leakage problem: computing the leakage of a Markov chain within a given time frame, or computing how long it takes for the Markov chain to leak a given amount of information.

Bounded Time

We want to compute the leakage for an attacker that is able to observe the behavior of the program for t < ∞ time units. We abstract time by considering each time unit as a step in the evolution of the Markov chain modeling the system. The definition of mutual information from a time t 1 to a time t 2 > t 1 is as follows: ◮ Definition 9. Let X and Y be two stochastic processes. Then the mutual information between X i and

Y i from time t 1 to time t 2 is I(X t1 , ..., X t2 ; Y t1 , ..., Y t2 ) = H(X t1 , ..., X t2 ) + H(Y t1 , ..., Y t2 ) - H(X t1 , ..., X t2 , Y t1 , ..., Y t2 )
We will refer to it as I (t1,t2) (X ; Y) for simplicity. Consider as usual the Markov chain semantics C = (S, s o , P ) modeling the behavior of the system. We present an iterative algorithm to compute I (t1,t2) (o, h) in time O(t 2 |S| 2 ): the algorithm first computes the distribution at time t 1 and then computes the behavior of the chain until time t 2 while keeping track of the amount of leakage accumulated. In the algorithm let S |x be the state space of the marginal, π

(i)
|x the distribution on the marginal at time i, and P (i,j) |x the probability of transitioning from i to j in the marginal. ◮ Theorem 10. Algorithm 2 terminates in time O(t 2 |S| 2 ) and when it does it outputs I (t1,t2) (o, h).

Note that Algorithm 2 is pseudopolynomial, as it depends not only on the size of the chain but also on the parameter t 2 . Also note that due to the Markov property it holds that I (t1,t2) = I

(t ′ 1 ,t ′ 2 )
whenever π

(t1) |o,h = π (t ′ 1 )
|o,h and t 2 -

t 1 = t ′ 2 -t ′ 1 .

Bounded Leakage

We want to determine how many time units it takes for the system to leak a given amount c of bits of information. The problem is more complex than the one analyzed in the previous section, since leakage is a complex function of the behavior of the system in time and finding a way to bound or reverse it is not obvious. We start by considering the qualitative version of the problem: does there exist a time t such that I t (C O , C h ) ≥ c? To answer we note that the the sequence of leakages is monotonic non-decreasing over time, so if the answer is yes then the leakage will remain greater than c for each time t ′ ≥ t. This allows us to answer the qualitative question by computing the leakage on the infinite time horizon as shown in Section 3; let it be l ∞ . If l ∞ < c then there is no time t such that the leakage is c, while if l ∞ > c then such time exists. If l ∞ = c then the system leaks c bits on the infinite time horizon but we have no guarantee that this amount will be reached in finite time.

In the case in which l ∞ ≥ c we can ask the quantitative question, i.e. at what time t the system will have leaked at least c bits. If l ∞ > c we know that such time t exists, while if l ∞ = c it may not. We will define the bounded leakage problem as follows: given a Markov chain C = (S, s 0 , P ) labeled with secrets and observations and a positive real number c, determine if there exists a finite time t such that the information leakage of the chain at time t is exactly c.

The problem is harder than it seems. For deterministic programs, it has been shown by Terauchi that it is not a k-safety property for any k [START_REF] Yasuoka | On bounding problems of quantitative information flow[END_REF]. The problem has also been addressed computationally by Heusser and Malacaria [START_REF] Heusser | Quantifying information leaks in software[END_REF]. For randomized programs, we will show that the problem can be reduced from Skolem's problem [START_REF] Ouaknine | Decision problems for linear recurrence sequences[END_REF]. While smaller instances have been shown to be decidable, the full decidability of Skolem's problem is still an open question [START_REF] Ouaknine | Positivity problems for low-order linear recurrence sequences[END_REF]. Akshay et al. [START_REF] Akshay | Reachability problems for Markov chains[END_REF] show that Skolem's problem is equivalent to the following: given a Markov chain C = (S, s 0 , P ), a state s and a probability r determine whether there is a time t such that π (t) s = r. We will call this Skolem's Markov chain reachability problem. Intuitively, information leakage is a harder problem than reachability, as formally stated by the following theorem: ◮ Theorem 11. Let A be an algorithm deciding the bounded leakage problem. Then A decides Skolem's Markov chain reachability problem.

Conclusions and Related Work

We have shown how to provide meaningful measures of the effectiveness of a secret-dependent non-terminating program in protecting its secret, by computing Shannon leakage when its value is finite and Shannon leakage rate otherwise. Operationally, Shannon leakage is related to the expected number of guesses it will take for the attacker to find out the secret's value, so leakage and leakage rate can be used to understand the amount of time that the attacker will require to infer the system's secret [START_REF] Massey | Guessing and entropy[END_REF]. To the same aim, we provided an algorithm that computes the amount of leakage from a program in a given time frame. Finally, we have shown that a precise quantification of the time required to leak a given amount is a hard problem, proving the complexity of the problem.

The quantification of leakage for an infinite observation and a finite or infinite secret has been recently considered by Chothia et al. [START_REF] Chothia | Probabilistic point-to-point information leakage[END_REF]. Their framework is different from ours as they study probabilistic "point to point" leakage; also they provide no algorithms to compute leakage. The authors do not consider the case in which the observation is finite and the secret infinite. Also, in the infinite secret and observation case they explicitly do not consider the leakage rate per time unit, preferring to compute the leakage for each occurrence of the secret command in their framework.

Alvim et al [START_REF] Alvim | Quantitative information flow in interactive systems[END_REF] study the setting of interactive systems, where secrets and observables can alternate during the computation and influence each other. They show that in this case mutual information is only an upper bound on leakage and "direct information" is a more precise leakage measure. This work is related to ours in that it investigates multi-stage processes but it presents significant differences as it doesn't investigate infinite leakage nor Markovian processes.

Recently Backes et al. also present a method for leakage rate computation based on stationary distribution of Markov chains, which they compute using PageRank [START_REF] Backes | Preventing side-channel leaks in web traffic: A formal approach[END_REF]. We expect that Algorithm 1 would be a useful addition to their approach.

Data: A Markov Chain C = (S, s 0 , P ) and its initial probability distribution π (0) . Result: The limit probability distribution µ of the chain.

(∞) Ri = r∈Ri π (0)
s and E i be a system of linear equations; If the chain has transient states, the loop in lines 1-10 of the algorithm trickles down the initial probability of the transient states appropriately to the end components. The transient states are removed one by one from the chain and the transition and initial probabilities of the other states updates accordingly. Let t be a transient state to be removed. For each other state u ∈ S \ {t}, the probability that the behavior of the chain will move to u after looping an arbitrary number of times on t is Pt,u 1-Pt,t . This means that whenever a path starts or passes by t, the next state it will visit after t will be u with probability Pt,u 1-Pt,t ; for this reason, by redistributing the initial probability π (0) t of t to each of its successor states u weighted by Pt,u 1-Pt,t we do not change the long-term probability of visiting each end components of the chain. Note that this only holds because t is transient. This modification of the chain does decrease the convergence time, but we are not concerned by it in this algorithm.

Similarly, for each predecessor s and successor u of t we increase the probability of transitioning from s to u by P s,t Pt,u 1-Pt,t to account for the probability of the paths that pass by t. Finally we isolate t by setting P s,t to zero for each of its predecessors, effectively removing it from the chain.

The loop in lines 1-10 repeats this operation for each transient state in the chain, effectively removing them without changing the limit probabilities of visiting each end components. This parti of the algorithm is inspired by Algorithm 1 in [START_REF] Biondi | Quantifying information leakage of randomized protocols[END_REF]. Having redistributed the initial probability of the transient states to the end components, we can just compute the final probability π (∞) Ri of end component R i as the sum of the initial probabilities of the states in R i ; this is done for each end component in line 12.

Since each R i is irreducible we can compute the limiting distribution of each of them independ-ently under the condition that r∈Ri µ r = π (∞)

Ri by solving the system of equations ∀r ∈ R i . µ r = r ′ ∈Ri µ r ′ P r ′ ,r Solving such system of equation provides the limit probability of each state in an end component, and doing it for each end component provides the limit probability of each state in the chain.

For the time complexity, the loop in lines 1-10 runs in time O(|S| 3 ). For the system of equations in lines 11-15 we have to solve O(|S|) systems of O(|S|) equations. The Coppersmith-Winograd complexity for solving systems of n linear equations is ∼ O(n 2.3 ), thus the final complexity is ∼ O(|S| 3.3 ).

◭

Proof of Theorem 10. The algorithm uses a chain rule for mutual information. Let X and Y be two time-indexed Markovian stochastic processes. Then

I (t1,t2) (X ; Y) = t2 i=t1 H(X i |X t1 , ..., X i-1 ) + H(Y i |Y t1 , ..., Y i-1 ) - -H(X i , Y i |X t1 , Y t1 , ..., X i-1 , Y i-1 )
This can be proved as follows: The algorithm starts by computing the mutual information at time t 1 , then updates it step by step until time t 2 . The correctness of an update step comes from considering that due to the Markov property it holds that H(X i |X 0 , ..., X i-1 ) = H(X i |X i-1 ) = s∈S π (i-1) s

I (t1,t2) (X ; Y) = H (t1,t2) (X i ) + H (t1,t2) (Y i ) -H (t1,t2) (X i , Y i ) = = t2 i=t1

L(s)

The algorithm clearly terminates for a finite t 2 and |S|. The computation of the marginals can be solved in O(|S| 2 ), while the probability distributions at time t 1 require time O(t 1 |S| 2 ), dominating the cost of the other operations before the for cycle. Inside the cycle the operations have cost O(|S| 2 ) and the cycle gets repeated t 2 -t 1 times, bringing the total cost to O(t 2 |S| 2 ) ◭

1Figure 2

 2 Figure 2 Bit XOR example: source code.

1 3 observableFigure 4

 34 Figure 4 Non-terminating leaking program example. On the left: program code. On the right: Markov chain semantics a) joint marginal C |o,h b) secret's marginal C |h

1 7 assign outorder := 8 (Figure 5 A

 785 Figure 5 A leaking implementation of a mix node.

  13foreach r ∈ R i do Add to E i the equation µ r = r ′ ∈Ri µ r ′ P r ′ ,r ; 14Solve the system E' under the conditionr∈Ri µ r = π (∞)Ri to obtain µ r for each r ∈ R i ; 15 end µ is 0 on each transient state: the behavior of the chain will eventually visit the end components and stay there forever.If a chain has no transient states, the final probability π (∞)Ri of ending in end component R i just corresponds to the sum of the initial probabilities of the states in R i , since by definition of end component the behavior of the chain never exits from each end component. Note that for the same reason π (∞) Ri = r∈Ri µ r .

  H(Xi |X t1 , ..., X i-1 ) + |Y t1 , ..., Y i-1 )-|X t1 , ..., X i-1 , Y t1 , ..., Y i-1 ) + H(Y i |X t1 , ..., X i , Y t2 , ..., Y i-1 ) |X t2 , ..., X i-1 ) + |Y t2 , ..., Y i-1 )-, Y i |X t1 , Y t1 , ..., X i-1 , Y i-1 ) |X t1 , ..., X i-1 ) + H(Y i |Y t1 , ..., Y i-1 )--H(X i , Y i |X t1 , Y t1 , ..., X i-1 , Y i-1 )

	t2
	i=t1 H(Y i -t2 i=t1 H(X i = t2 i=t1 H(X i t2 i=t1 t2 H(Y i -i=t1 t2 H(X = H(X i
	i=t1

i

The research presented in this paper has been partially supported by the MEALS project and by the MSR-INRIA project "Privacy-Friendly Services and Apps".

Appendix

Fig. 6 depicts the joint distribution of variables o and h for the Markov chain semantics in Fig. 4 . For compactness we do not represent the cases with probability 0 in Fig. 6cd,i.e. all the cases in which o 1 = 1. Proof of Theorem 6. For any variable v∈V,

is also a convergent monotonic non-decreasing non-negative sequence on k. Since ∀k ∈ N.

then the sequence

Proof of Theorem 8. Let C = {S, s 0 , P } be a Markov chain and π (0) its initial distribution. We want to compute its limiting distribution µ.

We call a state t reachable from a state s if ∃k.P k s,t > 0. We write s ↔ t if s is reachable from t and vice versa. A subset of states R ⊆ S is a end component if for each pair of states s, t ∈ R it holds that s ↔ t and no state in the component has transitions with nonzero probability to states not in the component, i.e. r∈R P r,t = 0 for t / ∈ R. We call a state s recurrent if ξ s = ∞, transient otherwise. It is known that the states in the end components are all and only the recurrent states of the chain. Thus, the limit probability distribution

Information Leakage of Non-Terminating Processes

Proof of Theorem 11. We show a reduction to the bounded leakage problem from Skolem's Markov chain reachability problem.

Consider an instance of Skolem's Markov chain reachability problem, i.e. a Markov chain C = (S, s 0 , P ), a state s and a probability r. Label state s with the information h = 0, o = 0 and all other states with the information h = [0, 1], o = 1, for a secret variable h and an observable variable o. Then being in state s gives us exactly 1 bit of information over h, while no other state gives any information.

Let I(o; h) k be the mutual information between o and h at time k ∈ N. Let p k be a path in C of length k, p k (s) a path in C of length k ending in state s, and p k (¬s) a path in C of length k not ending in state s. Then it holds that

proving that the leakage at time k is equivalent to the reachability probability of state s at time k. Thus if we had a way to determine whether the leakage of the system at some time t is r bits we would conclude that π (t) s = r, deciding Skolem's Markov chain reachability problem. Thus we conclude that determining whether there is a time t such that the leakage of the system is a given value is at least as hard as deciding Skolem's problem. ◭


Franc ¸ois Pasteau

Vishnu K Narayanan

Marie Babel
email: marie.babel@irisa.fr

A visual servoing approach for autonomous corridor following and doorway passing in a wheelchair

Keywords: Visual servoing, Wheelchair navigation, Assistive robotics, Vision-based robotics

Navigating within an unknown indoor environment using an electric wheelchair is a challenging task, especially if the user suffers from severe disabilities. In order to reduce fatigability and increase autonomy, control architectures have to be designed that would assist users in wheelchair navigation. We present a framework for vision-based autonomous indoor navigation in an electric wheelchair capable of following corridors, and passing through open doorways using a single doorpost. Visual features extracted from cameras on board the wheelchair are used as inputs for image based controllers built-in the wheelchair. It has to be noted that no a-priori information is utilised except for the assumption that the wheelchair moves in a typical indoor environment while the system is coarsely calibrated. The designed control schemes have been implemented onto a robotized wheelchair and experimental results show the robust behaviour of the designed system.

Introduction

Independent mobility for wheelchair users is a necessary part of the social and physical well being. While mobility increases social opportunity and reduces dependence, numerous studies have shown that a decrease in mobility can lead to social disorders like depression, anxiety and a fear of abandonment [START_REF] Finlayson | Experiencing the loss of mobility: perspectives of older adults with ms[END_REF] [START_REF] Iezzoni | Mobility difficulties are not only a problem of old age[END_REF]. However utilizing an electric wheelchair, especially in constrained environments, can be a challenging task for disabled individuals. In the case of severe disability, it is almost impossible for a user to effectively navigate without the help of another person. The issue of security is also an important one in these cases where for example, a person with neuromuscular disabilities finds it difficult to steer a wheelchair, particularly in limited space environments, without the risk of collision [START_REF] Murarka | Towards a safe, low-cost, intelligent wheelchair[END_REF]. In addition, it was reported that accessibility was the main problem encountered by wheelchair users [START_REF] Kaye | Mobility device use in the united states[END_REF] when more than four fifths of mobility device users in the United States identified themselves as living in a house with all the rooms on the same level.

Recent advances in robotics have paved way for a variety of opportunities facilitating the design of smart assistive technologies in order to help improve the lives of disabled people [START_REF] Yanco | Integrating robotic research: A survey of robotic wheelchair development[END_REF]. Keeping pace these advances in robotics, an ordinary powered wheelchair can be enhanced into an "Intelligent wheelchair" using sensors that perceive the surroundings and control architectures that affect the motion of the wheelchair.

Extensive works have previously been reported in this area, mainly focussing on the issue of increasing the safety levels of the wheelchair (and thereby decreasing the amount of human intervention). In all these systems, the human controls the higher level intelligence whereas the wheelchair is responsible for the lower level tasks. For example one can mention the TAO Project [START_REF] Gomi | Developing intelligent wheelchairs for the handicapped[END_REF], NavChair [START_REF] Levine | The navchair assistive wheelchair navigation system[END_REF], European FP7 Radhar project [START_REF] Demeester | Wheelchair navigation assistance in the fp7 project radhar: Objectives and current state[END_REF] and the recent SYSIASS project [START_REF] Kokosy | SYSIASS An Intelligent Powered Wheelchair[END_REF] all of which are designed to provide assistance in tasks like navigating through indoor environments like corridors, basic obstacle detection/avoidance and also, in some cases, autonomous passage through narrow doorways.

We observe that such behaviour-based design approaches have been proven to lead to robust systems. However, it has to be noted that the majority of the previous works in this area use a multi-sensor system with a distributed architecture. The motivation of our work comes partly from the fact that low cost sensors such as vision sensors could be employed in designing such systems. This can ensure widespread usage taking into account the fact that reimbursement from government/healthcare companies typically only covers the wheelchair, and not its technological adaptations. But relevant control systems have to be designed around a vision-based paradigm which still remains a highly challenging task. Thus, in this work, we aim to develop a solution for autonomous wheelchair navigation in an indoor environment using a set of monocular cameras with each one being devoted to a particular task.

That being said, the aim of the work is to serve as a first step in designing assistive systems (particularly lowcost vision-based systems) that may have a human in the control loop. Such semi-autonomous wheelchair systems would be helpful in conditions where motor impairments may hinder secure and effective navigation, by providing safe assistance in performing fundamental tasks while giving high level control to the user. As such, we have tackled two important low-level tasks related to indoor navigation: autonomously keeping a stable position along corridors in a secure way and detecting and passing through doorways. We will see that this second task can also be used directly for turning from a corridor to another one. These tasks represent the fundamental capability of a wheelchair performing indoor navigation.

While specifically considering corridor following using a wheeled robot, in [START_REF] Winters | Omni-directional vision for robot navigation[END_REF] a vision-based approach was designed using an omni-directional camera along with a visual memory framework. Whereas in [START_REF] Carelli | Corridor navigation and wall-following stable control for sonar-based mobile robots[END_REF] a stable control system was designed for corridor following and wall-following for sonar-based mobile robots (which may be extended to a wheelchair platform). Furthermore, in [START_REF] Carelli | Stable agv corridor navigation with fused vision-based control signals[END_REF] two vision-based control algorithms for corridor navigation were presented that exploited the geometry of a typical corridor. The first one uses the optical flow measured from the corridor's lateral walls to generate an angular velocity command for the mobile robot. The second scheme finds the perspective lines of the walls meeting the floor to generate the angular velocity command for the robot. Therefore, the geometry of a corridor in an image is a viable solution to employ while designing vision-based algorithms around it for realising the task of corridor following.

Several results have also been reported in the area of doorway passing with mobile/wheeled robots. A multi-sensor based algorithm for guiding a non-holonomic platform through a doorway was presented in [START_REF] Patel | Sensor based door navigation for a nonholonomic vehicle[END_REF]. The controller uses information from a camera system and a laser range finder for navigation. In the case of the previously mentioned SYSIASS project, a laser range finder with a PID controller is employed for doorway passing with a mobile robot. Another solution for secure navigation of a mobile robot in particular for doorway passing was proposed by [START_REF] Chung | Safe navigation of a mobile robot considering visibility of environment[END_REF]. The framework exploited a laser-based hybrid control scheme with dynamic obstacle avoidance and path planning. It has to be noted that a purely vision-based solution for doorway passing has not been proposed in literature and is therefore one of our major contributions.

Another important constraint arises when considering that the wheelchair must be able to perform in an indoor environment without any a-priori knowledge of the environment. Consequently, a solution where the geometry of the environment and the metrical data are not known is expected. Therefore we apply an Image-based Visual Servoing (IBVS) scheme which controls the relevant degrees of freedom (dof) of the wheelchair based on visual features directly extracted from a camera on board the wheelchair [START_REF] Chaumette | Visual servo control, part i: Basic approaches[END_REF].

The initial objective in any visual servoing scheme is to select features that represent visual data which can be effectively exploited to perform the task at hand. With respect to the task of autonomously following a corridor, features like the vanishing point and the straight lines that represent the edges of the corridors are relevant [START_REF] Hadj-Abdelkader | Catadioptric visual servoing from 3-d straight lines[END_REF] [START_REF] Faragasso | Vision-based corridor navigation for humanoid robots[END_REF]. There are several studies which indicate the robustness of the aforementioned features [START_REF] Toibero | Switching visual servoing approach for stable corridor navigation[END_REF]. Consequently to design a stable control law that achieves the objective robustly, we have developed a system that employs the measure of the vanishing point and the position of the vanishing line that corresponds to the median line of the corridor.

When dealing with the task of passing through doorways, the features available are mostly line features that represent the position of the doorposts in the image. This is a highly challenging task while employing a monocular vision sensor especially in the case where a single doorpost is visible. Thus, we have developed a novel and robust control scheme which only uses the position of the line feature corresponding to the nearest doorpost in the image to achieve the goal. This approach is utilized since global asymptotic stability [START_REF] Blazic | A novel trajectory-tracking control law for wheeled mobile robots[END_REF] of the system can be demonstrated as will be shown in Section 4.3.2. Moreover, higher level constraints like the status of the door (open/closed), the decision making process of passing through the door (i.e. which door to choose from), etc, make the task non-trivial. We here focus on low level control without the help of a global planning framework. The high level attributes are left for the user/home automation system to set as they are not the objective of this work.

The developed schemes do not require any initialization step owing to the fact that a dedicated line detection framework was designed to detect and track the relevant line features in real time. Thus, bottleneck stage that still remains in most of the servoing schemes is avoided. In addition, as mentioned before, no a-priori environment data is required or utilized in the servoing process. The paper is organized as follows. Section 2 deals with the geometric modelling of the robotized wheelchair. Section 3 details the task of corridor following with the definition of the visual features used and the control law formulation. Section 4 explains the task of doorway passing and proposes a new Lyapunov-based controller. Finally Section 5 exposes the experiments done and the results obtained while implementing the designed framework on a robotized wheelchair.

Modelling

The wheelchair is modelled as a six wheeled robot moving on a horizontal/inclined plane. Two differentially actuated wheels located in the middle of the wheelchair provide motion along with four passive caster wheels with two each located in the front and back. The wheelchair can then be though of as a simple unicycle robot [START_REF] Park | A smooth control law for graceful motion of differential wheeled mobile robots in 2d environment[END_REF], thus matching non-holonomous constraints.

Owing to the actuated wheels, two variables can be controlled, namely the translational velocity v and the rotational velocity ω. In this study, the control variable is restricted to the rotational velocity ω while a constant forward velocity v * is maintained for motion exigency. Three cameras located at different positions on the wheelchair are employed in order to realise the two different tasks. A front facing camera denoted as camera 1 which is located on the left handle at a height h 1 from the floor is employed for the task of corridor following. The second and third cameras denoted as camera 2 and camera 3 are respectively located on the right and left handle at heights h 2 and h 3 from the floor. These cameras are used for realising doorway passing: the right one to pass doors located on the right wall and the left one for doors on the left wall. These cameras are oriented in order to ensure that the doorpost stays in the camera field of view during the servoing process. In this paper, we refrain the study to the camera located on the right side of the wheelchair as the solution for the left camera is straightforward and symmetric. Now, according to Figure 1, the robot frame is defined as F r (P O , x r , y r , z r ). The origin of the frame F r is chosen as the mid-point of the line segment joining the two centres of the differential wheels. The camera frames are defined namely as, F c i (C i , x c i , y c i , z c i ), i = 1, 3 where C i denotes the optical center of each camera. We finally denote the orientation of cameras i with respect to frame F r as θ i . Consequently, the rotation matrices relative to the robot frame F r and the camera frames F c i are given by

c i R r =           sin θ i -cos θ i 0 0 0 -1 cos θ i sin θ i 0           . ( 1
)
By

denoting f v = (υ, ω) = f v x , f v y , f v z , f ω x , f ω y , f ω z the velocity of a frame F f expressed in F f
, where the first three components υ represent the translational velocities and the last three components ω the rotational velocities, we have r v = (v, 0, 0, 0, 0, ω) .

(

) 2
The translation r t c i between the robot frame and camera frames is given by (l i , w i , 0). Note that for camera 1 on the left, we have θ 1 = 0, l 1 > 0 and w 1 > 0 while for camera 2 on the right, θ 2 < 0, l 2 > 0 and w 2 < 0.

By applying the well known formula

c i v = c i R r [ c i t r ] × c i R r 0 c i R r . r v (3)
we obtain using (1)

c i v = c i v x , 0, c i v z , 0, c i ω y , 0 (4)
where

           c i v x = v sin θ i -ω(l i cos θ i + w i sin θ i ) c i v z = v cos θ i + ω(l i sin θ i -w i cos θ i ) c i ω y = -ω (5)

Autonomous Corridor Following

As stated earlier, the task of autonomously following a corridor is modelled as an IBVS problem. The objective is to devise a control law which minimises the error between a set of observed visual features and the set of their desired values. A discriminative representation of the relevant features of a corridor is given in Figure 2 from which some of the visual features can be observed which could be exploited for realising the task. The desired system should perform the task of following a corridor without collision with the walls, that is to say the system should position the optical axis of camera parallel to the wall and at the middle of the corridor. To design such a task, two visual features are selected.

Visual Features -Definition and Extraction

The x-coordinate x f of the vanishing point f t = (x f , y f ) at instant t (shown in Figure 3) is chosen as the first feature. When the robot is positioned parallel to the wall, looking forward, this feature goes to zero. As the second feature, the angle θ m made by the z-axis of the camera with the median line of the corridor is chosen (see Figure 3). When the position of the camera is in the middle of the corridor, this feature is equal to zero.

Since the median line is not visible in the image, this feature is computed from the orientations θ l and θ r of the straight lines in the image related to the intersection of the walls and the floor of the corridor. The median of the corridor is projected onto the image as a straight line parametrized by (ρ m , θ m ) where

ρ m = x f cos θ m + y f sin θ m . (6)
Geometrically, in the 3D world, the lines related to the wall and the median of the corridor are parallel and coplanar. As a consequence, the corresponding lines in the image intersect at the vanishing point while respecting

θ m = arctan tan θ l + tan θ r 2 . (7)
Also, the lateral distance between the camera and the median of the corridor is given by y = h 1 tan(θ m ), where h 1 is the distance between the camera 1 optical centre and the floor (see Figure 1). Therefore, we get y = 0 when θ m = 0.

. Estimation of x f

Estimating the vanishing point robustly and in real time is still an open area of research in computer vision. In the case of navigating through a corridor, the vanishing point corresponds to the point where a significant number of straight lines may intersect. We use the classical Gaussian sphere projection framework [START_REF] Rother | A new approach for vanishing point detection in architectural environments[END_REF] [START_REF] Boulanger | ATIP: A Tool for 3D Navigation inside a Single Image with Automatic Camera Calibration[END_REF] to estimate the vanishing point. The idea is to project onto this sphere the set of detected non-vertical lines in the image. Then the vanishing point is chosen as the point which has accumulated the maximum number of votes.

For extracting the straight lines in the image, the Line Segment Detection (LSD) algorithm is used [START_REF] Grompone Von Gioi | LSD: a Line Segment Detector, Image Processing On Line[END_REF]. It is based on local gradient orientations in the image, from which major segments are detected. The detected segments are then classified into vertical lines and non-vertical lines. The latter is used for estimating the vanishing point.

However, the main issue of the LSD algorithm is the cutting off of one line when the direction of the observed gradient changes. Thus, to increase the robustness, a dedicated merging process is applied to a group of segments that can be considered as a single straight line. For two segments, this process is done by taking into account the slope and extremities, and if they are close enough, they are merged to form a unique line. More details are given in [START_REF] Sekkal | Simple Monocular door detection and tracking[END_REF].

Since the vanishing point f t is estimated at each frame during a sequence, a factor α ∈ ]0, 1[ is introduced for temporal filtering as

f t = α f t-1 + (1 -α) f t
in order to ensure a smooth variation of the resulting estimated vanishing point in the current frame. The value of α is empirically tuned and has been chosen for the experiments at α = 0.1.

Estimation of θ m

The angles θ l and θ r can be easily calculated if we have an accurate estimate of the wall/floor boundaries. A variety of techniques have been proposed in the area of wall/floor boundary detection. For example, wall/floor features are defined by the corners corresponding to the intersection of a vertical line and the floor plane in [START_REF] Ok | Vistas and wall-floor intersection features -enabling autonomous flight in man-made environments[END_REF]. Whereas in [START_REF] Delage | A dynamic bayesian network model for autonomous 3d reconstruction from a single indoor image[END_REF], floor boundary is estimated by a dynamical Bayesian network model which is applied on each column of the image.

In our proposed scheme, a set of non-vertical lines are searched for along the image that correspond to the wall/floor boundary. The search is conducted based on two criteria: the first one being that they contribute to the vanishing point and, the second one being that they cross the bottom extremities of most number of vertical lines. In order to minimize false positives, a maximal distance between the vertical line extremity and the vanishing line is defined.

Then, from the angles θ l and θ r , the value of θ m is directly obtained using equation 7.

Image-based visual servoing scheme

Visual servoing is a classical approach to control robot motion from visual data [START_REF] Chaumette | Visual servo control, part i: Basic approaches[END_REF]. The design of the kinematics controller is based on modelling the variation ṡ of the visual features s with respect to the camera velocity v c . More precisely, when the observed environment is static, we have

ṡ = L s v c (8)
where L s is named the interaction matrix. In our case when s = (x f , θ m ), the analytical form of L s is given in [START_REF] Espiau | A new approach to visual servoing in robotics[END_REF] and [START_REF] Azinheira | Image-based visual servoing for vanishing features and ground lines tracking: Application to a uav automatic landing[END_REF] as

L s = 0 0 0 x f y f -1 -x 2 f y f λ θ m λ θ m sin θ m -λ θ m ρ m -ρ m cos θ m -ρ m sin θ m -1 , (9)
where λ θ m = (A sin θ m -B cos θ m )/D wherein AX + BY + CZ + D = 0 defines a plane to which the median line belongs.

In the present case, this line belongs to the floor plane which is defined by Y = h 1 . Therefore A = C = 0 and we obtain

λ θ m = cos θ m /h 1 . (10)
Using 4 in 8, we obtain the variation of the task function e = ss * (where s * = (0, 0)) as

ė = ṡ = J ω ω + J v v
where

J ω = 1 + x f 2 cos θ m h 1 (cos θ 1 (w 1 ρ m -l 1 ) -sin θ 1 (w 1 + l 1 ρ m )) + ρ m sin θ m (11)
and

J v = 0 cos θ m h 1 (sin θ 1 -ρ m cos θ 1 )
.

Following the same strategy as in [START_REF] Cherubini | Visual servoing for path reaching with nonholonomic robots[END_REF], designing a locally asymptotically stable control scheme that tries to exponentially regulates e to 0 (i.e. such that ė = -λe where λ > 0) leads to

ω = -J + ω (λe + J v v * ) ( 13
)
where J + ω is the pseudo-inverse of J ω and v * the constant forward velocity. From the control law given in 13, one can observe that J ω is always of full rank, but for two singular degenerate configurations. They occur when the vanishing point lies at either side of the image plane (i.e if the wheelchair is perpendicular to the corridor wall), wherein x f = ±∞ and the first row of J ω tends to ±∞. In such a case the robot cannot decide by itself where to move (i.e. the human should make the decision). Moreover, if x f = ∞, the vanishing point will not be detected by the feature extraction process. Another important caveat to consider is that the control law aims to center the camera in the middle of the corridor. Therefore, in order to center the wheelchair in the middle of the corridor, a non-zero value should be tuned for the desired value of θ m as soon as w 1 0.

Simulation Results

We report two simulated cases meant to illustrate the convergence of the control law and validate it as a suitable system for the task of corridor following. The two initial conditions assessed were as follows.

• Case I represents a case where initially x f = 0.15 meters and θ m = 0.55 rad which represents a situation where the robot is closer to the right corridor wall while facing the right corridor wall. The extrinsic parameters l 1 , w 1 were set to zero in order to asses the control law in an ideal case.

• Case II for which initially x f = -1 meter and θ m = -0.85 rad which represents a case where the robot is closer to the left corridor wall and facing the left side. The extrinsic parameters were set at l 1 = 0.5m and w 1 = 0.5m. The desired value of θ m was tuned to -0.3 rad so that the wheelchair is centered within the corridor. The performance of this case was compared to the performance when there exists some calibration errors with l 1 having an error of 0.15m, w 1 an error of -0.15m and h 1 an error of +0.2m. The translational velocity v * was set as 0.2 ms -1 while the height h 1 as 0.5m. The results of the simulation can be observed in Figures 4 and5 where the evolution of the visual features x f , θ m , ω and also the distance of the camera from the center of the corridor are shown.

We can observe that the rotational velocity ω decreases in a pure exponential way and that the visual features converge to their desired values x * f = 0 m and θ * m = 0/0.3 rad in both the cases. The convergence of x f is not completely exponential owing to the fact that two visual features are controlled with 1 DOF only. We can see that x f tends to a value > 0 or < 0 which in turn allows θ m to converge. This data is corroborated by the fact that the wheelchair distance from the center of the corridor moves to zero as θ m converges to θ * m . Moreover the inclusion of calibration errors in the camera extrinsic parameters does not affect the convergence of the system as seen in Figure 5. The only effect such errors in modelling have is an offset in the position of the wheelchair in the corridor corresponding to the modelling error: the wheelchair naturally overshoots the center of the corridor by 0.15m due to the error in w 1 .

Based on the above results, it can be concluded that the proposed formulation for corridor following in a wheelchair is a viable solution for implementation in a real-time system. Experimental results will be shown in Section 5.

Autonomous Doorway Passing

The task of autonomously passing through a doorway once it is detected is a non-trivial task owing to the fact that there are a lot of high level constraints to be taken care of. For example, whether the door is open or closed, and/or, is the width of the door sufficient enough to let the wheelchair through, etc remain unknown. However, these attributes either can be left for the user to set (i.e. human in the control loop), or left to a home automation system (which works directly with the wheelchair) that manages these high level parameters. Therefore, the aim here is to design a robust low-level controller that achieves an adequate wheelchair motion given a detected doorway.

Based on the above criteria, a novel Lyapunov-based control scheme is designed which exploits the position of the line feature representing the initial doorpost of the door in the image (i.e. the doorpost closer to the robot) as the visual feature.

Door recognition and tracking

There are several methods for detecting and representing doors in an indoor navigation construct [30] [31]. But, in the present case, the representations have to be simple enough so that effective features can be extracted for visual servoing. Also, detections have to be robust as well as fast enough to process frames in real time at a reasonable speed.

Consequently, we use a door detection and tracking framework specifically developed for indoor navigation tasks [START_REF] Sekkal | Simple Monocular door detection and tracking[END_REF]. This framework uses a set of information including the vanishing point to estimate a 3-D geometrical structure of the corridor. This structure then defines a search space in which trapezoidal shapes representing doors are extracted. To this aim we consider that the doorposts are nearly vertical in the image. Furthermore, for tracking the detected doorposts, a 2-D edge tracker inspired from the Moving Edges (ME) algorithm [START_REF] Bouthemy | A maximum likelihood framework for determining moving edges[END_REF] [33] is applied on the doorposts. The implementation of this framework on a generic corridor is shown in Figure 6. It has to be noted that the doorpost at the far end of the door will not be present in the field of view of the camera as the wheelchair tries to position itself in front of the door. Consequently we have to design a solution which uses the position of a single (i.e. the initial) doorpost as the input to the system.

Visual Feature -Definition and Extraction

Considering If the point D projects in the image at point P = (x P , y P ), then owing to a calibrated camera, the perspective projection equations reduce to

x P = x d z d and y P = h 2 z d .
To perform a successful doorway passing, the wheelchair needs to avoid the closest doorpost with a predefined margin m. To do so we formally define the visual feature as the angle φ d , since it can be easily estimated from the measure of the position of the doorpost . Indeed from x P coordinate, we immediately obtain using 14b.

φ d = arctan(x P ).
Similarly from y P coordinate of D, the distance r between the camera and the doorpost is given by

r = h 2 y P . cos(φ d ) , (15)
since we get z d = r cos(φ d ) from Figure 7b.

Lyapunov-based controller

The visual feature φ d must evolve in a certain way so that the wheelchair takes up a trajectory that realises the task. To assign a desired value φ * d which must be achieved by φ d for task completion, we have to first assess this trajectory.

Desired trajectory

We specify the desired trajectory that the wheelchair should follow for a successful doorway passage as presented in Figure 8. This trajectory has been chosen since the wheelchair must be able to position itself in front of the doorpost with a tolerance of m no matter what its starting position and orientation is. Consequently, the wheelchair must ideally take a tangential path towards an imaginary circle centred at the doorpost (with radius m) and when the camera distance to the doorpost r is equal to m, it must take up a smooth circular trajectory about the doorpost. Note that this trajectory implicitely allows avoiding collision with the walls of both sides of the corridor. The trajectory can be decomposed into two parts with the first one containing the tangential motion towards the circle (when r > m) and the second containing the circular motion about the doorpost (when r ≤ m). The characteristic of the tangential motion toward the circle is that ideally the value of θφ d (see Figure 8) should be equal to arcsin( m r ). Since the angle θ and θ 2 are defined in the frames F c 2 and F r respectively, and since θ corresponds to the same angle as θ 2 geometrically, we have θ = -θ 2 . Therefore

φ * d = θ 2 + arcsin( m r ) if r > m. (16)
As r gets closer to m, the wheelchair must switch to the circular motion about the doorpost. For such case it is clear from Figure 8 that the desired value of the visual feature φ * d must be equal to π 2 -θ. Therefore, we can state that

φ * d = θ 2 + π 2 if r ≤ m. ( 17
)

Control law formulation

To design a globally asymptotically stable system, we select as Lyapunov candidate function

V = 1 2 (φ d -φ * d ) 2 . ( 18
)
Of course we have V = 0 when φ d = φ * d . Then, we have to design a control scheme so that V < 0. We have

V = (φ d -φ * d )( φd -φ * d ). ( 19
)
First by deriving 14b we obtain φd = z d ẋd -

x d żd x 2 d + z 2 d , (20)
which can be re-written as (see Appendix),

φd = ω + 1 r sin(φ d -θ 2 )v + (l 2 cos(φ d -θ 2 ) -w 2 sin(φ d -θ 2 ))ω . ( 21
)
Then from 16 we obtain when r > m

φ * d = d dt arcsin m r = -ṙm r √ r 2 -m 2 (22)
which can be re-written as (see Appendix)

φ * d = sin(φ * d -θ 2 ) cos(φ d -θ 2 )v -(l 2 sin(φ d -θ 2 ) + w 2 cos(φ d -θ 2 ))ω r cos(φ * d -θ 2 ) (23)
Finally from 17 we have when r ≤ m φ *

d = 0. ( 24
)
By substituting the expressions for φd and φ * d in 19, we obtain a form for the derivative of V as (see Appendix)

V = φ d -φ * d (vA(r, φ d ) + ω(1 + B(r, φ d ))) ( 25
)
where, when

r > m                  A(r, φ d ) = sin(φ d -φ * d ) r cos(φ * d -θ 2 ) B(r, φ d ) = l 2 cos(φ d -φ * d ) -w 2 sin(φ d -φ * d ) r cos(φ * d -θ 2 ) . . ( 26
)
and when r ≤ m in which case we recall that φ * d = 0,

             A(r, φ d ) = sin(φ d -θ 2 ) r B(r, φ d ) = l 2 cos(φ d -θ 2 ) -w 2 sin(φ d -θ 2 ) r . . (27)
Thus in both cases, if we choose ω such that

ω = -k(φ d -φ * d ) -A(r, φ d )v * 1 + B(r, φ d ) , ( 28
)
where k is a positive gain factor, then V < 0. This ensures that the system is globally asymptotically stable and the visual feature φ d will converge asymptotically to the desired value φ * d . Furthermore, when r > m, it can also be shown that ω = 0 when φ d = φ * d thus providing a straight tangential motion towards the circle. Finally, as soon as 27) we have A = 1 r and B = -w 2 r from which we deduce ω = -v * r-w 2 . This naturally corresponds to a circular motion when r = m whose radius is equal to mw 2 . Note also that the switching has to be performed just before r = m so that A and B in [START_REF] Delage | A dynamic bayesian network model for autonomous 3d reconstruction from a single indoor image[END_REF] does not reach a very high value.

φ d = φ * d = θ 2 + π 2 (when r ≤ m) from (

Simulation Results

To validate the framework formulated above, the results of two simulated cases are presented. The aim of the simulations were to assess the trajectory taken by the wheelchair during the doorway passage, particularly the control law switch which happens as r ∼ m which facilitates the wheelchair to take up a circular trajectory about the doorpost. For both cases the doorpost was fixed at the origin of a Cartesian door frame say F d with the wheelchair starting at a relative position (x door , y door ) with respect to F d with x door = -1.5m and y door = -1.5m. The camera was initially aligned parallel to the corridor wall. The margin m was set at 0.2m, the height h 2 to 0.5m and v * was set to 0.1 ms -1 . Finally the gain k was set to 2.

• Case I represents an ideal case where the factors l 2 , w 2 and θ 2 representing the extrinsic parameters were set to 0.

• Case II represents a real world situation where the extrinsic parameters were set to non-zero so that l 2 = 0.5m, w 2 = -0.5m and the angle θ 2 = -0.8rad. Moreover, this case was compared using calibration errors. Indeed, errors of 0.2m, -0.2m and -0.15m were respectively added to l 2 , w 2 and h 2 respectively. Also an error of +0.2 rad was added on θ 2 . The trajectories taken by the wheelchair are shown in Figure 9. It can be observed that in both cases, the wheelchair takes up a straight line and tangential motion towards a circle centered at the doorpost and as r ≈ m, the control law switch allows the robot to take up a circular trajectory around the doorpost. We can observe the evolution of r, φ * d , the feature error φ d -φ * d and ω in Figures 10 and11. As for case I, the visual feature φ d converges to φ * d in a few iterations as shown by the evolution of the feature error. As the the control law switches at r ≈ 0.2m, the error increases due to the change in behaviour of φ * d but again moves to zero exponentially. Furthermore, it is clear that the distance from the camera to the doorpost r decreases constantly and stays near to the margin m = 0.2m. During the task, the rotational velocity ω is initially high but converges rapidly to 0. It then reacts to the control law switch and converges to the expected value for realizing the circular trajectory. In practice, in order to avoid a sudden increase in ω at the start, a method ensuring the continuity of the control law, such as the one proposed in [START_REF] Mansard | Task sequencing for high-level sensor-based control[END_REF] could be used.

The addition of the real world dimensions does not affect the system dynamics at all. As shown in Figure 9 the trajectory taken up by the wheelchair respects the dimensions of the wheelchair in the case with perfect calibration. Moreover, errors in calibration do not have an impact on the convergence of the control law as can be seen from the evolution of the feature error in Figure 11. But since there is an error in the angle θ 2 , this affects the value of φ * d . Also, the error in w 2 naturally affects the trajectory of the wheelchair corresponding to the error since the radius of the circular motion is equal to mw 2 according to the designed control law. We can however note that the feature error φ d -φ * d remains small, demonstrating the robustness of the control scheme with respect to large calibration errors.

Experiments and Results

The wheelchair robot used in this work is an off-the-shelf Penny and Giles wheelchair adapted to robotic use using ROS middleware [START_REF] Quigley | Ros: an open-source robot operating system[END_REF]. The wheelchair is equipped with two Raspberry PI [START_REF] Fundation | Raspberry Pi An ARM GNU/Linux box for $25. Take a byte![END_REF] camera modules with 100 • field of view. The video stream from the camera runs at 15 frames per second and correspond to a frame width of 808 pixels and a frame height of 480 pixels. The camera 1 was coarsely calibrated at l 1 = 0.38m, w 1 = 0.32m and h 1 = 0.64m while camera 2 at l 2 = 0.0m, w 2 = -0.32m and h 2 = 0.5m with respect to F r . Camera 2 was aligned at an angle of θ 2 = -50 • ∼ -0.88rad with respect to the robot frame. Finally, the margin for doorway passing m was set at 0.2m. Also, prior to the feature extraction, images are rectified against the distortions due to the camera lens. Extraction of the visual features as well as the computation of the control laws were performed using the ViSP software [START_REF] Marchand | ViSP for visual servoing: a generic software platform with a wide class of robot control skills[END_REF]. Computation is performed on a Core i7 laptop connected to the wheelchair using Ethernet network. The results presented here pertain to the one realised in one of the corridors of the Inria building 12C in Rennes, France. Human intervention is needed only for turning the visual servoing process on/off and to select a doorway to pass through. [START_REF] Finlayson | Experiencing the loss of mobility: perspectives of older adults with ms[END_REF] The wheelchair starts at an unknown position in the corridor and the servoing process is activated in order to follow the corridor.

2 As soon as a turn arrives, the user interacts with the system to select the end of the corridor to turn about using the doorway passing control scheme.

3 After the wheelchair has turned about the corridor, the servoing process for following the new corridor switches on automatically when both φ * d = π 2 + θ 2 and a vanishing point is detected. 4 While the wheelchair is still following the corridor the user interacts again, this time to select a doorway to pass through.

5 The servoing process is switched off once the wheelchair manages to pass through the specific doorway. Figure 12 shows the trajectory taken by camera 1, camera 2 and the wheelchair during the experiment process. It is reproduced in a global frame with the wheelchair starting position taken as the origin. Odometry has been used to reconstruct the trajectory on a map of the environment for visualization. It has to be noted that neither odometry nor the environment map is employed in the servoing process.

The trajectory is decomposed into four parts. During part A, the wheelchair performs corridor following in order to position itself in the middle of the corridor while controlling the two visual features x f and θ m . It can be noted that the wheelchair starts relatively in a central position and the correction is done as soon as the servoing starts. As the wheelchair moves to the end of the corridor, the user selects the wall partition to turn right. Consequently, part B is activated where the wheelchair manages to judge the wall partition as a doorpost and turn about it. Thus we can observe that the framework for doorway passing can be employed for turning within corridors.

After the wheelchair successfully turns, the corridor following task (part C) is automatically activated once φ d = π 2 + θ 2 and a vanishing point is detected. Again the control scheme acts to position the wheelchair in the middle of the corridor. Finally, the user selects a doorway to pass through to start (part D) while the wheelchair manages to turn about the doorpost for a successful doorway passage. The servoing process is stopped as soon as the wheelchair is positioned in front of the doorway. At critical points of the servoing process, the camera view can be seen in Figures 13 and14 for camera 1 and camera 2 respectively. Figures 13a and14a represent the start of the servoing process. The user selects the wall partition in the frames shown in Figures 13b and14b which marks the transition from A to B. A new vanishing point is obtained in frame 241 (Figures 13c and14c) with the visual feature φ d ∼ π 2 + θ 2 . Then frame 392 (Figures 13d and14d) marks the start of doorway passing and a transition onto part D. Finally, frame 590 (Figures 13e and14e) shows the frames at the end of the navigation. Figure 15 shows the behaviour of visual features x f and θ m during the servoing process. Since the front facing camera 1 is located at w = 0.32m from the centre of the wheelchair reference frame, the desired value of θ m was set at -0.3rad. This was done in order to facilitate the wheelchair in the middle of the corridor rather than the camera. During part A, we can observe the convergence of the features to their desired values x f = 0 and θ m = -0.3 rad as the wheelchair centres itself in the corridor. The features evolve till the vanishing point is not detected anymore during the corridor turning part B. As part C starts, the features are detected again and we can observe the exponential decrease of x f to zero. Also, θ m converges gradually to -0.3rad as observed in simulation. Again, the features are correctly extracted during part D owing to the fact that the vanishing point is detected until the wheelchair makes a complete turn. Thus, the behaviour of x f and θ m during parts A and C validates the control scheme for autonomous corridor following for use in a real time system. The perturbations in φ d can be attributed to the low dynamics of the wheelchair and to visual tracking errors. But we can observe that the control scheme manages to servo the feature to its desired value. A similar behaviour of φ d can be reported while in part D. The visual feature manages to follow the desired value during the servoing process. There is a small discrepancy at the end which is again due to some tracking errors even though φ d converges to φ * d at the end. The final desired value of 0.69 rad is not reached since the servoing is stopped as soon as the wheelchair is positioned in front of the doorway.

When considering r, we can observe an almost constant decrease to the margin m = 0.2m. Then the value of r = m remains almost constant till the task switch occurs. This behaviour is critical for the purpose of doorpost collision avoidance and for the requirement that the wheelchair is able to position in front of the doorway no matter what its initial position.

A final important point to mention is that the cameras are coarsely calibrated with respect to the intrinsic parameters as well as their position with respect to the wheelchair. The robust performance of the controller in such a case demonstrates that the impact of modelling errors is minimal on the system.

Conclusion

In this work we have proposed a visual servoing approach for autonomously following a corridor as well as pass though doorways and turn about corridors in an electric wheelchair. The task of corridor following is realised by exploiting two visual features, namely the vanishing point and the angle obtained from the projection of the median line of the corridor onto the image. A control law was designed to servo the features onto their desired values by taking into account the kinematics of the wheelchair. The doorway passing (and corridor turning) task employs the position of a single doorpost in the image as an input to a Lyapunov-based control scheme which allows the wheelchair to take up a desired trajectory about the doorpost. This trajectory avoids collision with the wall and guarantees that the wheelchair positions itself in front of the doorway regardless of its initial position.

Results in simulation demonstrate the convergence and robustness of both control schemes. Experiments conducted on a robotic platform indicate the validity of applying the proposed low-level control system on an assitive wheelchair. Future works aim at enhancing the system to account for the human-in-the-loop condition where the wheelchair user would have considerable presence in the control loop thus modifying the system into a semiautonomous assitive system. from which we deduce the form for V given in 25.

Figure 1 :

 1 Figure 1: Robot and camera frame definitions (a) Top view with relative position of robot and camera 1 frames. (b) Top view with camera 2 and camera 3 frames. (c) Simplified side view of the camera frames. (d) Robotic platform.

Figure 2 :

 2 Figure 2: Corridor geometrical structure with floor and wall planes

Figure 3 :

 3 Figure 3: x f and θ m visual features

Figure 4 :Figure 5 :

 45 Figure 4: Evolution of x f , θ m , ω and camera distance to the corridor center -Case I

Figure 6 :

 6 Figure 6: Door detection framework

Figure 7 ,Figure 7 :

 77 Figure 7: Geometrical constraints while considering doorway passing(top view (a), front view(b)

Figure 8 :

 8 Figure 8: The desired camera trajectory shown in green. (a) when r > m and (b) when r < m.

Figure 9 :

 9 Figure 9: The trajectories: Case I (left) and Case II -without error in blue and with error in red (right)

Figure 10 :

 10 Figure 10: Evolution of r, φ * d , φ d -φ * d and ω -Case I

  /s) -Without calibration error ω (rad/s) -With calibration error

Figure 11 :

 11 Figure 11: Evolution of r, φ * d , φ d -φ * d and ω -Case II

Figure 12 :

 12 Figure 12: Trajectory taken by the wheelchair with respect to a frame fixed at the initial position

Figure 13 :

 13 Figure 13: The camera 1 frame at points A,B,C,D at the end of the navigation respectively.

Figure 14 :

 14 Figure 14: The camera 2 frame at points A,B,C,D and at the end of the navigation respectively.

Figure 15 :

 15 Figure 15: The evolution of the corridor visual features x f and θ m

Figure 16 :Figure 17 :

 1617 Figure 16: The evolution of the visual feature φ d Figures 16 and 17 present the evolution of the visual feature φ d as well as the distance r from the camera to the doorpost/wall partition during the experiment. The values are naturally zero in part A and C as no servoing occurs for doorway passing. It is activated as soon as the user selects the wall partition to turn about. We can observe that

From 2 , 2 d + z 2 d. ( 35 )√ r 2 -m 2 ( 39 )

 222352239 the well known kinematics equation ẋ = -υ -[ω] × x, we deduce ẋd and żd as     ẋd = -c 2 v xz c 2 d ω y żd = -c 2 v z + x c 2d ω y[START_REF] Anguelov | Detecting and modeling doors with mobile robots[END_REF] which using equation (5) leads to ẋd =sin θ 2 v + ω(l 2 cos θ 2 + w 2 sin θ 2 )+ z d ω, (31a) żd =cos θ 2 v -ω(l 2 sin θ 2w 2 cos θ 2 )x d ω.(31b)Sincex d = r sin φ d and z d = r cos φ d , we obtain φd = r cos φ d [-sin θ 2 v + ω(l 2 cos θ 2 + w 2 sin θ 2 ) + r cos φ d ω]r sin φ d [-cos θ 2 v -ω(l 2 sin θ 2w 2 cos θ 2 )r sin φ d ω] r(32)which can be re-written asφd = 1 r (v(-cos φ d sin θ 2 + sin φ d cos(θ 2 )) + 1 r ω(l 2 (cos φ d cos θ 2 + sin φ d sin θ 2 ) + w 2 (cos φ d sin θ 2sin φ d cos θ 2 )) + rω) . (33)Using trigonometric relations we finally get,φd = ω + 1 r sin(φ d -θ 2 )v + (l 2 cos(φ d -θ 2 )w 2 sin(φ d -θ 2 ))ω .(34)Similarly to obtain ṙ, in order to derive φ * d (in equation 22), we deduce from 14a ṙ = x d ẋd + z d żdx Therefore using 31a and 31b, we can writeṙ = r sin φ d [-sin θ 2 v + ω(l 2 cos θ 2 + w 2 sin θ 2 ) + r cos φ d ω] + r cos φ d [-cos θ 2 v -ω(l 2 sin θ 2w 2 cos θ 2 )r sin φ d ω] r . (36) This gives, ṙ = -v(sin φ d sin θ 2 + cos φ d cos θ 2 ) + ω[l 2 (sin φ d cos θ 2cos φ d sin θ 2 ) + w 2 (sin φ d sin θ 2 + cos φ d cos θ 2 )](37)and using trigonometric formulae we finally have,ṙ =cos(φ d -θ 2 )v + (l 2 sin(φ d -θ 2 ) + w 2 cos(φ d -θ 2 ))ω. (38)Therefore φ * d can be written as (from 22)φ * d = m cos(φ d -θ 2 )v -(l 2 sin(φ d -θ 2 ) + w 2 cos(φ d -θ 2 ))ω rFrom 16 and basic trigonometric relations, if we substitute m r = sin(φ * d -θ 2 ) and√ r 2 -m 2 r = cos(φ * d -θ 2 ), we obtain φ * d = sin(φ * d -θ 2 ) cos(φ d -θ 2 )v -(l 2 sin(φ d -θ 2 ) + w 2 cos(φ d -θ 2 ))ω r cos(φ * d -θ 2 )(40)Finally we derive the details to obtain 25. From 21 and 40 we can write φdφ * d asφdφ * d = ω + 1 r sin(φ d -θ 2 )v + (l 2 cos(φ d -θ 2 )w 2 sin(φ d -θ 2 ))ω sin(φ * d -θ 2 ) cos(φ d -θ 2 )v -(l 2 sin(φ d -θ 2 ) + w 2 cos(φ d -θ 2 ))ω r cos(φ * d -θ 2 ).(41)We can rearrange the above equation as,φdφ * d = v r sin(φ d -θ 2 ) -sin(φ * d -θ 2 ) cos(φ d -θ 2 ) cos(φ * d -θ 2 ) + ω 1 + l 2 r cos(φ d -θ 2 ) + sin(φ d -θ 2 ) sin(φ * d -θ 2 ) cos(φ * d -θ 2 ) -w 2 r sin(φ d -θ 2 ) -sin(φ * d -θ 2 ) cos(φ d -θ 2 ) cos(φ * d -θ 2 ).(42) and finally we can re-write the equation as φdφ * d = v sin(φ d -φ * d ) r cos(φ * d -θ 2 ) + ω 1 + l 2 cos(φ d -φ * d )w 2 sin(φ d -φ * d ) r cos(φ * d -θ 2 ) (43)

Acknowledgement

This work is supported by the Inria large-scale initiative action Personally Assisted Living (PAL). The authors would like to thank Daniel Guillard and Luc Le Pape from Ergovie and Eric Bazin from INSA Rennes.

Appendix

We recall that (see 20