Browse ORBi by ORBi project

- Background
- Content
- Benefits and challenges
- Legal aspects
- Functions and services
- Team
- Help and tutorials

A model for ternary projective relations between regions Billen, Roland ; in Lecture Notes in Computer Science (2004) Detailed reference viewed: 22 (3 ULg)A dynamic neighbourhood discovery protocol for active overlay networks Martin, Sylvain ; Leduc, Guy in Lecture Notes in Computer Science (2004), 2982 d-RADAR(1) is a neighbourhood discovery protocol for overlay network environments designed for (but not limited to) active network overlays. The core of the algorithm is an expanding ring-search based on ... [more ▼] d-RADAR(1) is a neighbourhood discovery protocol for overlay network environments designed for (but not limited to) active network overlays. The core of the algorithm is an expanding ring-search based on the IP routing table content augmented with traffic-based and dynamic refreshing techniques that allows it to react to virtual topology changes (nodes joining/leaving the overlay) as well as IP topology changes (broken and repaired link, route changes and moving nodes). This paper presents how the protocol detects overlay candidate nodes using probing capsules and the algorithms needed to select neighbours among the candidates. We also show how d-RADAR keeps the neighbouring table up to date and learns topology changes while keeping a low discovery and refresh overhead. A short summary of simulations carried out with our active network simulator illustrates how these algorithms actually behave. [less ▲] Detailed reference viewed: 53 (18 ULg)Invisible Sketch Interface in Architectural Engineering, in Graphics Recognition, Recent Advanced and Perspectives Leclercq, Pierre in Lecture Notes in Computer Science (2004), 3088 Detailed reference viewed: 27 (8 ULg)Omega-regular model checking Boigelot, Bernard ; ; Wolper, Pierre in Lecture Notes in Computer Science (2004), 2988 "Regular model checking" is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words or trees, sets of states by finite automata on these objects ... [more ▼] "Regular model checking" is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words or trees, sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. In this context, the central problem is then to compute the iterative closure of a finite-state transducer. This paper addresses the use of regular model-checking like techniques for systems whose states are represented by infinite (omega) words. Its main motivation is to show the feasibility and usefulness of this approach through a combination of the necessary theoretical developments, implementation, and experimentation. The iteration technique that is used is adapted from recent work of the authors on the iteration of finite-word transducers. It proceeds by comparing successive elements of a sequence of approximations of the iteration, detecting an "increment" that is added to move from one approximation to the next, and extrapolating the sequence by allowing arbitrary repetitions of this increment. By restricting oneself to weak deterministic Buchi automata, and using a number of implementation optimizations, examples of significant size can be handled. The proposed transducer iteration technique can just as well be exploited to compute the closure of a given set of states by the transducer iteration, which has proven to be a very effective way of using the technique. Examples such as a leaking gas burner in which time is modeled by real variables have been handled completely within the automata-theoretic setting. [less ▲] Detailed reference viewed: 59 (10 ULg)Hybrid Acceleration using Real Vector Automata Boigelot, Bernard ; ; Jodogne, Sébastien in Lecture Notes in Computer Science (2003, July), 2725 This paper addresses the problem of computing an exact and effective representation of the set of reachable configurations of a linear hybrid automaton. Our solution is based on accelerating the state ... [more ▼] This paper addresses the problem of computing an exact and effective representation of the set of reachable configurations of a linear hybrid automaton. Our solution is based on accelerating the state-space exploration by computing symbolically the repeated effect of control cycles. The computed sets of configurations are represented by Real Vector Automata (RVA), the expressive power of which is beyond that of the first-order additive theory of reals and integers. This approach makes it possible to compute in finite time sets of configurations that cannot be expressed as finite unions of convex sets. The main technical contributions of the paper consist in a powerful sufficient criterion for checking whether a hybrid transformation (i.e., with both discrete and continuous features) can be accelerated, as well as an algorithm for applying such an accelerated transformation on RVA. Our results have been implemented and successfully applied to several case studies, including the well-known leaking gas burner, and a simple communication protocol with timers. [less ▲] Detailed reference viewed: 24 (4 ULg)Iterating transducers in the large Boigelot, Bernard ; ; Wolper, Pierre in Lecture Notes in Computer Science (2003), 2725 Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system ... [more ▼] Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, e.g. a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this paper, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performance. [less ▲] Detailed reference viewed: 39 (7 ULg)Decidability of invariant validation for paramaterized systems ; Gribomont, Pascal in Lecture Notes in Computer Science (2003), 2619 Detailed reference viewed: 20 (4 ULg)Smoothing the TCP rate by learning the delay versus window size dependency ; Leduc, Guy in Lecture Notes in Computer Science (2003), 2899 We propose TCP-L, an improved version of TCP, equipped with a learning algorithm whose purpose is to avoid probing for additional bandwidth when the network conditions are known to be unfavourable. TCP-L ... [more ▼] We propose TCP-L, an improved version of TCP, equipped with a learning algorithm whose purpose is to avoid probing for additional bandwidth when the network conditions are known to be unfavourable. TCP-L learns the relationship between its current (average) one-trip delay and its current window size when congestion occurs, leading to packet loss. After the learning phase, TCP-L will only probe for bandwidth by increasing its window if, under the current network conditions (measured by the one-trip delay), this inflated window has not previously created congestion. Simulations show that after the learning phase, TCP-L reaches a much more stable throughput, while remaining TCP-friendly, which makes it usable for a larger class of applications, including some multimedia applications that will benefit from that stability. TCP-L is a simple backward compatible extension of TCP which can thus be deployed progressively. We show that there is a benefit for the Internet to deploy TCP-L, because the overall traffic becomes smoother when the proportion of TCP-L flows increases. Finally, our learning component can also be easily embedded in other unicast or multicast transport protocols. [less ▲] Detailed reference viewed: 37 (4 ULg)RADAR: Ring-based adaptive discovery of active neighbour routers Martin, Sylvain ; Leduc, Guy in Lecture Notes in Computer Science (2002, December), 2546 The RADAR protocol and its underlying neighbourhood discovery framework extend the ANTS toolkit by giving active nodes the ability to discover dynamically other active nodes close to them without relying ... [more ▼] The RADAR protocol and its underlying neighbourhood discovery framework extend the ANTS toolkit by giving active nodes the ability to discover dynamically other active nodes close to them without relying on any configuration file. Such an automatic discovery is the key to administration of large or sparse active networks and the first step towards an efficient active routing. Active nodes will use their local IP routing table to run an extended ring search in their domain. An Additive Increase Multiplicative Decrease control allows RADAR to discover several neighbours per physical interface without searching too far away or fixing a maximum distance a priori. The protocol is complemented by a traffic-driven discovery that can grab capsules coming from unknown nodes (mainly outside the local domain) and trigger targetted probing of those addresses. [less ▲] Detailed reference viewed: 52 (4 ULg)Representing arithmetic constraints with finite automata: An overview Boigelot, Bernard ; Wolper, Pierre in Lecture Notes in Computer Science (2002, July), 2401 Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of ... [more ▼] Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of techniques based on finite automata that lead to decision procedures and other useful algorithms, as well as to a normal form, for the first-order linear theory of the integers, of the reals, and of the integers and reals combined. This approach has led to an implemented tool, which has the so far unique capability of handling the linear. first-order theory of the integers and reals combined. [less ▲] Detailed reference viewed: 35 (7 ULg)Characterizing simpler recognizable sets of integers Rigo, Michel in Lecture Notes in Computer Science (2002), 2420 For the k-ary numeration system, we characterize the sets of integers such that the corresponding representations make up a star-free regular language. This result can be transposed to some linear ... [more ▼] For the k-ary numeration system, we characterize the sets of integers such that the corresponding representations make up a star-free regular language. This result can be transposed to some linear numeration systems built upon a Pisot number like the Fibonacci system and also to k-adic numeration systems. Moreover we study the problem of the base dependence of this property and obtain results which are related to Cobham's Theorem. [less ▲] Detailed reference viewed: 11 (5 ULg)A Stable and Flexible TCP-friendly congestion control protocol for layered multicast transmission ; Leduc, Guy in Lecture Notes in Computer Science (2001, September 04), 2158 We propose an improvement of our RLS (Receiver-driven Layered multicast with Synchronization points) protocol, called CIFL for “Coding-Independent Fair Layered mulaticast”, along two axes. In CIFL, each ... [more ▼] We propose an improvement of our RLS (Receiver-driven Layered multicast with Synchronization points) protocol, called CIFL for “Coding-Independent Fair Layered mulaticast”, along two axes. In CIFL, each receiver of a layered multicast transmission will try and find the adequate number of layers to subscribe to, so that the associated throughput is fair towards TCP and stable in steady-state. The first improvement is that CIFL is not specific to any coding scheme. It can work as well with an exponentially distributed set of layers (where the throughput of each layer i equals the sum of the throughputs of all layers below i), or with layers of equal throughputs, or any other scheme. The second improvement is the excellent stability of the protocol which avoids useless join attempts by learning from its unsuccessful previous attempts in the same (or better) network conditions. Moreover, the protocol tries and reaches its ideal TCP-friendly as soon as possible by computing its target throughput in a clever way when an incipient congestion is confirmed. [less ▲] Detailed reference viewed: 20 (1 ULg)Counting the Solutions of Presburger Equations without Enumerating Them Boigelot, Bernard ; in Lecture Notes in Computer Science (2001), 2494 The Number Decision Diagram (NDD) has recently been proposed as a powerful representation system for sets of integer vectors. In particular, NDDs can be used for representing the sets of solutions of ... [more ▼] The Number Decision Diagram (NDD) has recently been proposed as a powerful representation system for sets of integer vectors. In particular, NDDs can be used for representing the sets of solutions of arbitrary Presburger formulas, or the set of reachable states of some systems using unbounded integer variables. In this paper, we address the problem of counting the number of distinct elements in a set of vectors represented as an NDD. We give an algorithm that is able to perform an exact count without enumerating explicitly the vectors, which makes it capable of handling very large sets. As an auxiliary result, we also develop an efficient projection method that allows to construct efficiently NDDs from quantified formulas, and thus makes it possible to apply our counting technique to sets specified by formulas. Our algorithms have been implemented in the verification tool LASH, and applied successfully to various counting problems. [less ▲] Detailed reference viewed: 10 (1 ULg)Constructing Automata from Temporal Logic Formulas: A Tutorial Wolper, Pierre in Lecture Notes in Computer Science (2001), 2090 This paper presents a tutorial introduction to the construction of finite-automata on infinite words from linear-time temporal logic formulas. After defining the source and target formalisms, it describes ... [more ▼] This paper presents a tutorial introduction to the construction of finite-automata on infinite words from linear-time temporal logic formulas. After defining the source and target formalisms, it describes a first construction whose correctness is quite direct to establish, but whose behavior is always equal to the worst-case upper bound. It then turns to the techniques that can be used to improve this algorithm in order to obtain the quite effective algorithms that are now in use. [less ▲] Detailed reference viewed: 63 (10 ULg)On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables Boigelot, Bernard ; Jodogne, Sébastien ; Wolper, Pierre in Lecture Notes in Computer Science (2001), 2083 This paper considers finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite ... [more ▼] This paper considers finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on in finite words, but this involves some difficult and delicate to implement algorithms. The contribution of this paper is to show, using topological arguments, that only a restricted class of automata on in finite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms and opens the path to the implementation of a usable system for handling this combined theory. [less ▲] Detailed reference viewed: 35 (6 ULg)Constitutive equations and numerical modelling of time effects in soft porous rocks ; Charlier, Robert ; Collin, Frédéric in Lecture Notes in Computer Science (2001), 1988 A constitutive model is developed within the framework of Perzyna's viscoplasticity for predicting the stress-strain-time behaviour of soft porous rocks. The model is based on the hyperelasticity and ... [more ▼] A constitutive model is developed within the framework of Perzyna's viscoplasticity for predicting the stress-strain-time behaviour of soft porous rocks. The model is based on the hyperelasticity and multisurface viscoplasticity with hardening. A time-stepping algorithm is presented for integrating the creep sensitive law. An example of application to one-dimensional consolidation is presented. The objectives are to: 1. present a soft rock model which is capable of taking into account the rate sensitivity, time effects and creep rupture; 2. to discuss the use of an incremental procedure for time stepping using large time increments and 3. to extend the finite element code Lagamine (MSM-ULg) for viscoplastic problems in geomechanics. [less ▲] Detailed reference viewed: 58 (31 ULg)An Active Layered Multicast Adaptation Protocol ; Leduc, Guy in Lecture Notes in Computer Science (2000, October 16), 1942 We describe an active application in the field of multicast congestion control for real-time traffic. Our Active Layered Multicast Adaptation Protocol is a layered multicast congestion control scheme ... [more ▼] We describe an active application in the field of multicast congestion control for real-time traffic. Our Active Layered Multicast Adaptation Protocol is a layered multicast congestion control scheme built on top of an Active Network infrastructure. It benefits from router support in order to obtain information about resources available and to perform the adaptation tasks at the places where shortage of resources occur. It supports heterogeneous receivers through the combination of layered multicast transmission with selective filtering and pruning of layers within the active nodes. Market-based resource management ideas are applied to achieve a resource utilisation level that represents an equilibrium between the user goals and the node operator goals. Our simulation results show that the protocol is feasible and provides adequate reactions to short term and persistent congestion, while keeping the amount of state and processing in the active nodes limited. [less ▲] Detailed reference viewed: 23 (1 ULg)An agent-inspired active network resource trading model applied to congestion control ; Leduc, Guy in Lecture Notes in Computer Science (2000, September), 1931 In order to accommodate fluctuations in network conditions, adaptive applications need to obtain information about resource availability, Using active networks, new models for adaptive applications can be ... [more ▼] In order to accommodate fluctuations in network conditions, adaptive applications need to obtain information about resource availability, Using active networks, new models for adaptive applications can be envisaged, which can benefit from the possibility to send mobile code to the network nodes. We describe a model for trading resources inside an active net-work node, based on the interaction between capsules as reactive user agents, and resource manager agents which reside in the network nodes. We apply the model to the case of a many-to-one audio application with congestion control, which trades off link resources against memory when there is congestion at the outgoing interface towards the destination. Our simulation results indicate that the application makes effective use of the available resources, and it also allows resources to be shared according to user preferences. [less ▲] Detailed reference viewed: 20 (1 ULg)On the construction of automata from linear arithmetic constraints Wolper, Pierre ; Boigelot, Bernard in Lecture Notes in Computer Science (2000, March), 1785 This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed ... [more ▼] This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed allows a linear-time determinization procedure to be used. Furthermore, it shows through theoretical analysis and experiments that the special structure of the constructed automata does, in quite a general way, render the usual upper bounds on automata operations vastly overpessimistic. [less ▲] Detailed reference viewed: 37 (6 ULg)On the Expressiveness of Real and Integer Arithmetic Automata Boigelot, Bernard ; ; Wolper, Pierre in Lecture Notes in Computer Science (1998), 1443 If read digit by digit, a n-dimensional vector of integers represented in base r can be viewed as a word over the alphabet r to the n. It has been known for some time that, under this encoding, the sets ... [more ▼] If read digit by digit, a n-dimensional vector of integers represented in base r can be viewed as a word over the alphabet r to the n. It has been known for some time that, under this encoding, the sets of integer vectors recognizable by finite automata are exactly those definable in Presburger arithmetic if independence with respect to the base is required, and those definable in a slight extension of Presburger arithmetic if only a specific base is considered. Using the same encoding idea, but moving to infinite words, finite automata on infinite words can recognize sets of real vectors. This leads to the question of which sets of real vectors are recognizable by finite automata, which is the topic of this paper. We show that the recognizable sets of real vectors are those definable in the theory of reals and integers with addition and order, extended with a special base-dependent predicate that tests the value of a specified digit of a number. Furthermore, in the course of proving that sets of vectors defined in this theory are recognizable by finite automata, we show that linear equations and inequations have surprisingly compact representations by automata, which leads us to believe that automata accepting sets of real vectors can be of more than theoretical interest. [less ▲] Detailed reference viewed: 30 (0 ULg) |
||