Advertisement

Mcta: Heuristics and Search for Timed Systems

  • Martin Wehrle
  • Sebastian Kupferschmid
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)

Abstract

Mcta is a directed model checking tool for concurrent systems of timed automata. This paper reviews Mcta and its new developments from an implementation point of view. The new developments include both heuristics and search techniques that define the state of the art in directed model checking. In particular, Mcta features the powerful class of pattern database heuristics for efficiently finding shortest possible error traces. Furthermore, Mcta offers new search techniques based on multi-queue search algorithms. Our evaluation demonstrates that Mcta is able to significantly outperform previous versions of Mcta as well as related state-of-the-art tools like Uppaal and Uppaal/Dmc.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Behrmann, G., Bengtsson, J.E., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL Implementation Secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 3–22. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Culberson, J.C., Schaeffer, J.: Pattern databases. Comp. Int. 14(3), 318–334 (1998)MathSciNetGoogle Scholar
  5. 5.
    Dierks, H.: Comparing model-checking and logical reasoning for real-time systems. Formal Aspects of Computing 16(2), 104–120 (2004)zbMATHCrossRefGoogle Scholar
  6. 6.
    Dierks, H.: Time, Abstraction and Heuristics – Automatic Verification and Planning of Timed Systems using Abstraction and Heuristics. Habilitation thesis, University of Oldenburg, Germany (2005)Google Scholar
  7. 7.
    Edelkamp, S.: Planning with pattern databases. In: Proc. ECP, pp. 13–24 (2001)Google Scholar
  8. 8.
    Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT 5(2), 247–267 (2004)CrossRefGoogle Scholar
  9. 9.
    Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on Directed Model Checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol. 5348, pp. 65–89. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Floyd, R.W.: Algorithm 97: Shortest path. Communications of the ACM 5(6), 345 (1962)CrossRefGoogle Scholar
  11. 11.
    Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for the heuristic determination of minimum cost paths. IEEE Trans. Systems Science and Cybernetics 4(2), 100–107 (1968)CrossRefGoogle Scholar
  12. 12.
    Hart, P.E., Nilsson, N.J., Raphael, B.: Correction to a formal basis for the heuristic determination of minimum cost paths. SIGART Newsletter 37, 28–29 (1972)Google Scholar
  13. 13.
    Helmert, M.: The Fast Downward planning system. JAIR 26, 191–246 (2006)zbMATHGoogle Scholar
  14. 14.
    Hoffmann, J., Nebel, B.: The FF planning system: Fast plan generation through heuristic search. JAIR 14, 253–302 (2001)zbMATHGoogle Scholar
  15. 15.
    Krieg-Brückner, B., Peleska, J., Olderog, E.R., Baer, A.: The UniForM workbench, a universal development environment for formal methods. In: Proc. MF, pp. 1186–1205. Springer (1999)Google Scholar
  16. 16.
    Kupferschmid, S., Dräger, K., Hoffmann, J., Finkbeiner, B., Dierks, H., Podelski, A., Behrmann, G.: Uppaal/DMC – Abstraction-Based Heuristics for Directed Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 679–682. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI Planning Heuristic for Directed Model Checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 35–52. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Kupferschmid, S., Wehrle, M.: Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 276–290. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  19. 19.
    Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster Than Uppaal? In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 552–555. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  20. 20.
    Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proc. PLDI, pp. 446–455. ACM Press (2007)Google Scholar
  21. 21.
    Olderog, E.R., Dierks, H.: Moby/RT: A tool for specification and verification of real-time systems. J. UCS 9(2), 88–105 (2003)Google Scholar
  22. 22.
    Pearl, J.: Heuristics: Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley (1984)Google Scholar
  23. 23.
    Röger, G., Helmert, M.: The more, the merrier: Combining heuristic estimators for satisficing planning. In: Proc. ICAPS, pp. 246–249. AAAI Press (2010)Google Scholar
  24. 24.
    Wehrle, M., Kupferschmid, S.: Context-Enhanced Directed Model Checking. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 88–105. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  25. 25.
    Wehrle, M., Kupferschmid, S., Podelski, A.: Useless actions are useful. In: Proc. ICAPS, pp. 388–395. AAAI Press (2008)Google Scholar
  26. 26.
    Wehrle, M., Kupferschmid, S., Podelski, A.: Transition-Based Directed Model Checking. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 186–200. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Martin Wehrle
    • 1
  • Sebastian Kupferschmid
    • 2
  1. 1.University of BaselSwitzerland
  2. 2.ATRiCS Advanced Traffic Solutions GmbHFreiburgGermany

Personalised recommendations