Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/s10009-011-0206-x | STTT |
Keywords | Field | DocType |
domain-specific regular acceleration,symbolic representation,regular model-checking approach,initial set,so-called acceleration operator,transition relation,regular model-checking · infinite-state systems · state-space exploration · acceleration techniques,transition graph,regular state-space exploration,computation step infinitely,regular language,acceleration operator,verification,acceleration | Integer,FIFO (computing and electronics),Computer science,Algorithm,Communication channel,Acceleration,Operator (computer programming),Fixed point,Regular language,Computation | Journal |
Volume | Issue | ISSN |
14 | 2 | 1433-2787 |
Citations | PageRank | References |
2 | 0.37 | 35 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernard Boigelot | 1 | 707 | 48.59 |