References of "Lecture Notes in Computer Science"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailOmega-regular model checking
Boigelot, Bernard ULg; Legay, A.; Wolper, Pierre ULg

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: 37 (10 ULg)
Full Text
Peer Reviewed
See detailHybrid Acceleration using Real Vector Automata
Boigelot, Bernard ULg; Herbreteau, Frédéric; Jodogne, Sébastien ULg

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: 15 (3 ULg)
Full Text
Peer Reviewed
See detailIterating transducers in the large
Boigelot, Bernard ULg; Legay, A.; Wolper, Pierre ULg

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: 27 (7 ULg)
Full Text
Peer Reviewed
See detailDecidability of invariant validation for paramaterized systems
Fontaine, Pascal; Gribomont, Pascal ULg

in Lecture Notes in Computer Science (2003), 2619

Detailed reference viewed: 17 (4 ULg)
Full Text
Peer Reviewed
See detailSmoothing the TCP rate by learning the delay versus window size dependency
El Khayat, Ibtissam; Leduc, Guy ULg

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: 27 (4 ULg)
Full Text
Peer Reviewed
See detailRADAR: Ring-based adaptive discovery of active neighbour routers
Martin, Sylvain ULg; Leduc, Guy ULg

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: 46 (4 ULg)
Full Text
See detailRepresenting arithmetic constraints with finite automata: An overview
Boigelot, Bernard ULg; Wolper, Pierre ULg

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: 25 (7 ULg)
Full Text
Peer Reviewed
See detailCharacterizing simpler recognizable sets of integers
Rigo, Michel ULg

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: 10 (5 ULg)
Full Text
Peer Reviewed
See detailA Stable and Flexible TCP-friendly congestion control protocol for layered multicast transmission
El Khayat, Ibtissam; Leduc, Guy ULg

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: 16 (1 ULg)
Full Text
Peer Reviewed
See detailCounting the Solutions of Presburger Equations without Enumerating Them
Boigelot, Bernard ULg; Latour, Louis

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: 5 (1 ULg)
Full Text
See detailConstructing Automata from Temporal Logic Formulas: A Tutorial
Wolper, Pierre ULg

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: 52 (7 ULg)
Full Text
Peer Reviewed
See detailOn the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables
Boigelot, Bernard ULg; Jodogne, Sébastien ULg; Wolper, Pierre ULg

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: 23 (5 ULg)
Full Text
Peer Reviewed
See detailConstitutive equations and numerical modelling of time effects in soft porous rocks
Datcheva, Maria; Charlier, Robert ULg; Collin, Frédéric ULg

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: 51 (30 ULg)
Full Text
Peer Reviewed
See detailAn Active Layered Multicast Adaptation Protocol
Yamamoto, Lidia; Leduc, Guy ULg

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: 14 (1 ULg)
Full Text
Peer Reviewed
See detailAn agent-inspired active network resource trading model applied to congestion control
Yamamoto, Lidia; Leduc, Guy ULg

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: 14 (1 ULg)
Full Text
See detailOn the construction of automata from linear arithmetic constraints
Wolper, Pierre ULg; Boigelot, Bernard ULg

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: 29 (5 ULg)
Full Text
Peer Reviewed
See detailOn the Expressiveness of Real and Integer Arithmetic Automata
Boigelot, Bernard ULg; Rassart, Stéphane; Wolper, Pierre ULg

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: 15 (0 ULg)
Full Text
See detailVerifying Systems with Infinite but Regular State Spaces
Wolper, Pierre ULg; Boigelot, Bernard ULg

in Lecture Notes in Computer Science (1998), 1427

Thanks to the development of a number of efficiency enhancing techniques, state-space exploration based verification, and in particular model checking, has been quite successful for finite-state systems ... [more ▼]

Thanks to the development of a number of efficiency enhancing techniques, state-space exploration based verification, and in particular model checking, has been quite successful for finite-state systems. This has prompted efforts to apply a similar approach to systems with infinite state spaces. Doing so amounts to developing algorithms for computing a symbolic representation of the infinite state space, as opposed to requiring the user to characterize the state space by assertions. Of course, in most cases, this can only be done at the cost of forgoing any general guarantee of success. The goal of this paper is to survey a number of results in this area and to show that a surprisingly common characteristic of the systems that can be analyzed with this approach is that their state space can be represented as a regular language. [less ▲]

Detailed reference viewed: 3 (1 ULg)
Full Text
See detailSea air land modelling operational network
Ghiot, C. B.; Bauler, P.; Beckers, Jean-Marie ULg et al

in Lecture Notes in Computer Science (1997), 1225

The purpose of the SALMON project is to develop a single model from three previously existing models (ocean, river and groundwater) for the description of environment quality in a whole system of regional ... [more ▼]

The purpose of the SALMON project is to develop a single model from three previously existing models (ocean, river and groundwater) for the description of environment quality in a whole system of regional scale including marine, river, groundwater and atmospheric inputs. The connection of the different models is done through a specific interface, a junction, designed to allow the data exchange between models based on different numerical methods. The software is developed on IBM RS/6000 computers (the SP2 parallel machine). [less ▲]

Detailed reference viewed: 86 (46 ULg)
Full Text
Peer Reviewed
See detailAutomatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs
Boigelot, Bernard ULg; Godefroid, Patrice

in Lecture Notes in Computer Science (1997), 1217

VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination ... [more ▼]

VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination problems between the concurrent processes of a system. In this paper, we present a method to synthesize a finite-state machine that simulates all the sequences of visible operations of a given process that were observed during a state-space exploration performed by VeriSoft. The examination of this machine makes it possible to discover the dynamic behavior of the process in its environment and to understand how it contributes to the global behavior of the system. [less ▲]

Detailed reference viewed: 1 (1 ULg)