Paper Info
Title
Heuristic Model Checking using a Monte-Carlo Tree Search Algorithm
Abstract
Monte-Carlo Tree Search algorithms have proven extremely effective at playing games that were once thought to be difficult for AI techniques owing to the very large number of possible game states. The key feature of these algorithms is that rather than exhaustively searching game states, the algorithm navigates the tree using information returned from a relatively small number of random game simulations. A practical limitation of software model checking is the very large number of states that a model can take. Motivated by an analogy between exploring game states and checking model states, we propose that Monte-Carlo Tree Search algorithms might also be applied in this domain to efficiently navigate the model state space with the objective of finding counterexamples which correspond to potential software faults. We describe such an approach based on Nested Monte-Carlo Search---a tree search algorithm applicable to single player games---and compare its efficiency to traditional heuristic search algorithms when using Java PathFinder to locate deadlocks in 12 Java programs.
Year
DOI
Venue
2015
10.1145/2739480.2754767
Genetic and Evolutionary Computation Conference
Keywords
Field
DocType
Model Checking, Monte-Carlo Tree Search, Search-Based Software Engineering
Incremental heuristic search,Model checking,Search algorithm,Computer science,Theoretical computer science,Artificial intelligence,Iterative deepening depth-first search,Mathematical optimization,Monte Carlo tree search,Tree traversal,Algorithm,Beam search,Machine learning,Search-based software engineering
Conference
Citations 
PageRank 
References 
4
0.40
10
Authors
2
Name
Order
Citations
PageRank
Simon M. Poulding113610.72
Robert Feldt2965.77