Reference : Iterating transducers in the large
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/18766
Iterating transducers in the large
English
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Legay, A. [Université de Liège - ULG > Dept. d'electricté, électronique et informatique > informatique > >]
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données) >]
2003
Lecture Notes in Computer Science
Springer
2725
Computer Aided Verification
223-235
Yes
No
International
0302-9743
1611-3349
Berlin
Germany
Computer Aided Verification, 15th International Conference, CAV 2003
July 8-12
Boulder
CO
[en] verification ; Infinite state ; transducer iteration
[en] 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.
Communauté française de Belgique - Direction de la recherche scientifique - Actions de recherche concertées ; European IST-FET project ADVANCE (IST-1999-29082).
Researchers
http://hdl.handle.net/2268/18766
10.1007/b11831

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Restricted access
BLW03-cav.pdfPublisher postprint234.13 kBRequest copy
Open access
BLW03-cav.pdfAuthor postprint167.9 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.