Distributed extended beam search for quantitative model checking

A.J. Wijs, B. Lisser

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

11 Citations (Scopus)


In this paper, we mainly focus on solving scheduling problems with model checking, where a finite number of entities needs to be processed as efficiently as possible, for instance by a machine. To solve these problems, we model them in untimed process algebra, where time is modelled using a special tick action. We propose a set of distributed state space explorations to find schedules for the modelled problems, building on the traditional notion of beam search. The basic approach is called distributed (detailed) beam search, which prunes parts of the state space while searching using an evaluation function in order to find near-optimal schedules in very large state spaces. Variations on this approach are presented, such as distributed flexible, distributed g-synchronised, and distributed priority beam search, which can also practically be used in combinations.
Original languageEnglish
Title of host publicationProceedings of the 4th Workshop on Model Checking and Artificial Intelligence
EditorsS. Edelkamp, A. Lomuscio
Place of PublicationHeidelberg
ISBN (Print)978-3-540-74128-2
Publication statusPublished - 2006

Publication series

NameLecture Notes in Artificial Intelligence
ISSN (Print)1611-3349


Dive into the research topics of 'Distributed extended beam search for quantitative model checking'. Together they form a unique fingerprint.

Cite this