Browse ORBi by ORBi project

- Background
- Content
- Benefits and challenges
- Legal aspects
- Functions and services
- Team
- Help and tutorials

On the Use of Automata-based Techniques in Symbolic Model Checking: invited address ; Wolper, Pierre 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: 55 (9 ULg)Handling Liveness Properties in (ω-)Regular Model Checking ; ; Wolper, Pierre 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: 62 (3 ULg)Combining Non-stably Infinite, Non-first Order Theories ; Gribomont, Pascal in Electronic Notes in Theoretical Computer Science (2005), 125(3), 37-51 Detailed reference viewed: 21 (6 ULg)A direct symbolic approach to model checking pushdown systems ; ; Wolper, Pierre et al in Electronic Notes in Theoretical Computer Science (1997), 9 Detailed reference viewed: 9 (0 ULg) |
||