Reference : Domain-specific regular acceleration
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/135057
Domain-specific regular acceleration
English
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
2012
International Journal on Software Tools for Technology Transfer
Springer
14
2
193-206
Yes (verified by ORBi)
International
1433-2779
1433-2787
[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
http://hdl.handle.net/2268/135057
10.1007/s10009-011-0206-x
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
paper.pdfAuthor postprint231.22 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.