Zusammenfassung: |
The dissertation aims at developing heuristic search algorithms that explicitly manage the memory hierarchy and can deal with state spaces that cannot fit into the main memory. Such algorithms are very effective in the domains WHERE input size is considerably large for the internal memory and a major part has to reside on the hard disk. The dissertation presents External A*, an external memory variant of A* algorithm and discusses its I/O complexity. Originally designed for undirected graphs, it has been successfully extended and applied in model checking WHERE one is faced with directed and weighted graphs. The algorithms developed in this dissertation have been successfully implemented in some of the state-of-the-art tools including Spin model checker, FF planning system and Uppaal-Cora for real-time scheduling. The largest exploration reported consumed 3 Terabytes of hard disk space while using only 3 Gigabytes of RAM and running for 196 hours. |