Reference : Domain-specific regular acceleration
Scientific journals : Article
Engineering, computing & technology : Computer science
Domain-specific regular acceleration
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
International Journal on Software Tools for Technology Transfer
Yes (verified by ORBi)
[en] verification ; infinite-state systems ; acceleration
[en] The regular model-checking approach is a set of techniques aimed at exploring symbolically infinite state spaces. These techniques proceed by representing sets of configurations of the system under analysis by regular languages, and the transition relation between these configurations by a transformation over such languages. The set of reachable configurations can then be computed by repeatedly applying the transition relation, starting from a representation of the initial set of configurations, until a fixed point is reached. In order for this computation to terminate, it is generally needed to introduce so-called acceleration operators, the purpose of which is to explore in one computation step infinitely many paths in the transition graph of the system. A simple form of acceleration operator is one that is associated to a cycle in the transition graph, computing the set of states that can be obtained by following this cycle arbitrarily many times. The computation of acceleration operators is strongly dependent on the type of the data values that are manipulated by the system, and on the symbolic representation chosen for handling sets of such values. In this survey, we describe acceleration operators suited for the regular state-space exploration of systems relying on FIFO communication channels, as well as those based on integer and real variables.
Work partially supported by the Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office, and by the grants 2.4530.02 and 2.4607.08 of the Belgian Fund for Scientific Research (F.R.S.-FNRS).
Researchers ; Professionals ; Students
The original publication is available at

File(s) associated to this reference

Fulltext file(s):

Open access
paper.pdfAuthor postprint231.22 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.