References of "Legay, Axel"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailOn (Omega-)regular model checking
Legay, Axel; Wolper, Pierre ULg

in ACM Transactions on Computational Logic (2010), 12(1), 46

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable 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 set of reachable 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, for example, 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 article, 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 performances. [less ▲]

Detailed reference viewed: 63 (13 ULg)
Full Text
Peer Reviewed
See detailComputing Convex Hulls by Automata Iteration
Cantin, François ULg; Legay, Axel; Wolper, Pierre ULg

in International Journal of Foundations of Computer Science (2009), 20(4), 647-667

This paper considers the problem of computing the real convex hull of a finite set of n-dimensional integer vectors. The starting point is a finite-automaton representation of the initial set of vectors ... [more ▼]

This paper considers the problem of computing the real convex hull of a finite set of n-dimensional integer vectors. The starting point is a finite-automaton representation of the initial set of vectors. The proposed method consists in computing a sequence of automata representing approximations of the convex hull and using extrapolation techniques to compute the limit of this sequence. The convex hull can then be directly computed from this limit in the form of an automaton-based representation of the corresponding set of real vectors. The technique is quite general and has been implemented. [less ▲]

Detailed reference viewed: 91 (23 ULg)
Full Text
Peer Reviewed
See detailComputing Convex Hulls by Automata Iteration
Cantin, François ULg; Legay, Axel; Wolper, Pierre ULg

in Lecture Notes in Computer Science (2008, July), 5148

This paper considers the problem of computing the real convex hull of a finite set of n-dimensional integer vectors. The starting point is a finite-automaton representation of the initial set of vectors ... [more ▼]

This paper considers the problem of computing the real convex hull of a finite set of n-dimensional integer vectors. The starting point is a finite-automaton representation of the initial set of vectors. The proposed method consists in computing a sequence of automata representing approximations of the convex hull and using extrapolation techniques to compute the limit of this sequence. The convex hull can then be directly computed from this limit in the form of an automatonbased representation of the corresponding set of real vectors. The technique is quite general and has been implemented. Also, our result fits in a wider scheme whose objective is to improve the techniques for converting automata-based representation of constraints to formulas. [less ▲]

Detailed reference viewed: 114 (37 ULg)
Full Text
See detailOn the Use of Automata-based Techniques in Symbolic Model Checking: invited address
Legay, Axel; Wolper, Pierre ULg

in Electronic Notes in Theoretical Computer Science (2006, March 09), 150(1), 3-8

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 survey two generic techniques that have been presented in [B. Boigelot and A. Legay and P. Wolper, Iterating Transducers in the Large, Proc. 15th Int. Conf. on Computer Aided Verification, Boulder, USA, Lecture Notes in Computer Science, volume 2725, year 2003, pages 223–235] and [B. Boigelot and A. Legay and P. Wolper, Omega-Regular Model Checking, Proc. 10th Int. Conf. on Tools and and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, Lecture Notes in Computer Science, volume 2988, year 2004, pages 561–575]. Those techniques build 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: 70 (9 ULg)
Full Text
Peer Reviewed
See detailHandling Liveness Properties in (ω-)Regular Model Checking
Bouajjani, Ahmed; Legay, Axel; Wolper, Pierre ULg

in Electronic Notes in Theoretical Computer Science (2005, December 28), 138(3), 101-115

Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that liveness ... [more ▼]

Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that liveness properties could also be checked within this framework, little has been done about working out the corresponding details, and experimentally evaluating the approach. This paper addresses these issues in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and solves the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic. Several experiments showing the applicability of the approach were successfully conducted. [less ▲]

Detailed reference viewed: 79 (3 ULg)