Distributed Extended Beam Search for Quantitative Model Checking

  • A. J. Wijs
  • B. Lisser
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)


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.


directed model checking distributed model checking scheduling beam search 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. In: EATCS Monograph, Springer, Heidelberg (2002)Google Scholar
  2. 2.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T.: Efficient Guiding Towards Cost-Optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Behrmann, G., Hune, T., Vaandrager, F.: Distributing Timed Model Checking - How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 216–231. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Bergstra, J., Klop, J.: Algebra of Communicating Processes with Abstraction. Theor. Comput. Sci. 37, 77–121 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Bisiani, R.: Beam Search. In: Encyclopedia of Artificial Intelligence, pp. 1467–1568. Wiley Interscience Publication, Chichester (1992)Google Scholar
  6. 6.
    Blom, S., Orzan, S.: A Distributed Algorithm for Strong Bisimulation Reduction of State Spaces. In: Proc. of PDMC 2002, ENTCS, vol. 68 (4), Elsevier, Amsterdam (2002)Google Scholar
  7. 7.
    Blom, S.C.C., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.C.: μCRL: A Toolset for Analysing Algebraic Specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)Google Scholar
  8. 8.
    Blom, S.C.C., Ioustinova, N., Sidorova, N.: Timed verification with μCRL. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 178–192. Springer, Heidelberg (2003)Google Scholar
  9. 9.
    Bolch, G., Greiner, S., de Meer, H., Trivedi, K.S.: Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications, 2nd edn. Wiley, Chichester (2006)zbMATHGoogle Scholar
  10. 10.
    Brucker, P., Jurisch, B., Sievers, B.: A branch and bound algorithm for the job-shop scheduling problem. Discrete Applied Mathematics 49(6), 107–127 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Ciardo, G., Gluckman, J., Nicol, D.: Distributed State Space Generation of Discrete-State Stochastic Models. INFORMS Journal on Computing 10(1), 82–93 (1998)CrossRefGoogle Scholar
  12. 12.
    Della Croce, F., T’kindt, V.: A recovering beam search algorithm for the one-machine dynamic total completion time scheduling problem. Journal of the Operational Research Society 53, 1275–1280 (2002)zbMATHCrossRefGoogle Scholar
  13. 13.
    Dill, D.: The Murφ Verification System. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)Google Scholar
  14. 14.
    Dudeney, H.E.: Amusements in Mathematics, chapter 9, Dover Publications, Inc., pp. 112–114(1958)Google Scholar
  15. 15.
    Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed Explicit-state Model Checking in the Validation of Communication Protocols. STTT 5, 247–267 (2003)Google Scholar
  16. 16.
    Felner, A., Kraus, S., Korf, R.E.: KBFS: K-Best-First Search. AMAI 39(1-2), 19–39 (2003)zbMATHMathSciNetGoogle Scholar
  17. 17.
    Fox, M.S.: Constraint-Directed Search: A Case Study of Job-Shop Scheduling. PhD thesis, CMU (1983)Google Scholar
  18. 18.
    Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol. 2057, pp. 217–234. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Godefroid, P., Khurshid, S.: Exploring Very Large State Spaces Using Genetic Algorithms. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 266–280. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  20. 20.
    Groce, A., Visser, W.: Heuristics for Model Checking Java Programs. STTT 6(4), 260–276 (2004)CrossRefGoogle Scholar
  21. 21.
    Groote, J.F., Reniers, M.A.: Handbook of Process Algebra, 17, pp. 1151–1208. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  22. 22.
    Huth, M., Kwiatkowska, M.: Quantitative Analysis and Model Checking. In: Proc. LICS 1997, pp. 111–127. IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  23. 23.
    Jabbar, S., Edelkamp, S.: Parallel External Directed Model Checking With Linear I/O. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 237–251. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  24. 24.
    Korf, R.E.: Uniform-cost Search. In: Shapiro, S.C. (ed.) Encyclopedia of Artificial Intelligence, pp. 1461–1462. Wiley-Interscience, New York (1992)Google Scholar
  25. 25.
    Korf, R.E.: Linear-space best-first search. Artificial Intelligence 62, 41–78 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Lerda, F., Sista, R.: Distributed-Memory model checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) Theoretical and Practical Aspects of SPIN Model Checking. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  27. 27.
    Lowerre, B.T.: The HARPY speech recognition system. PhD thesis, CMU (1976)Google Scholar
  28. 28.
    Niebert, P., Tripakis, S., Yovine, S.: Minimum-time reachability for timed automata. In: Proc. MED 2000, IEEE Press, Los Alamitos (2000)Google Scholar
  29. 29.
    Oechsner, S., Rose, O.: Scheduling Cluster Tools Using Filtered Beam Search and Recipe Comparison. In: Proc. 2005 Winter Simulation Conference, pp. 2203–2210. IEEE Computer Society Press, Los Alamitos (2005)CrossRefGoogle Scholar
  30. 30.
    Ow, P.S., Morton, E.T.: Filtered beam search in scheduling. International Journal of Production Research 26, 35–62 (1988)CrossRefGoogle Scholar
  31. 31.
    Ow, P.S., Smith, S.F.: Viewing scheduling as an opportunistic problem-solving process. Annals of Operations Research 12, 85–108 (1988)CrossRefGoogle Scholar
  32. 32.
    Peled, D., Pratt, V., Holzmann, G. (eds.): Partial Order Methods in Verification, vol. 29 of DIMACS series in discrete mathematics and theoretical computer science. AMS (1996)Google Scholar
  33. 33.
    Pohl, I.: Heuristic Search Viewed as Path Finding in a Graph. Artificial Intelligence 1, 193–204 (1970)zbMATHCrossRefMathSciNetGoogle Scholar
  34. 34.
    Roscoe, A.W.: Model-checking CSP. In: A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 353–378. Prentice-Hall, Englewood Cliffs (1994)Google Scholar
  35. 35.
    Rubin, S.: The ARGOS Image Understanding System. PhD thesis, CMU (1978)Google Scholar
  36. 36.
    Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice-Hall, Englewood Cliffs (1995)zbMATHGoogle Scholar
  37. 37.
    Ruys, T.C.: Optimal scheduling using Branch-and-Bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol. 2648, pp. 1–17. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  38. 38.
    Sabuncuoglu, I., Bayiz, M.: Job shop scheduling with beam search. European Journal of Operational Research 118, 390–412 (1999)zbMATHCrossRefGoogle Scholar
  39. 39.
    Dashti, T. M., Wijs, A.J.: Pruning State Spaces Using Extended Beam Search (2006). (to be published),
  40. 40.
    Wijs, A.J., Fokkink, W.J.: From \(\chi_{\textbf{t}}\) to μCRL: Combining Performance and Functional Analysis. In: Proc. ICECCS 2005, pp. 184–193. IEEE Computer Society Press, Los Alamitos (2005)Google Scholar
  41. 41.
    Wijs, A.J., van de Pol, J.C., Bortnik, E.: Solving Scheduling Problems by Untimed Model Checking. In: Proc. FMICS 2005, pp. 54–61. ACM Press, 2005. Extended version as CWI technical report SEN-R0608,
  42. 42.
    Zann, R.A.: The Zebra Finch - A Synthesis of Field and Laboratory Studies. Oxford University Press Inc, Oxford (1996)Google Scholar
  43. 43.
    Zhou, R., Hansen, E.A.: Beam-Stack Search: Integrating Backtracking with Beam Search. In: Proc. ICAPS 2005, pp. 90–98. AAAI (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • A. J. Wijs
    • 1
  • B. Lisser
    • 1
  1. 1.CWI, P.O. Box 94079, 1090 GB AmsterdamThe Netherlands

Personalised recommendations