Skip to main content
SpringerLink
Log in

Heuristic Search for the Analysis of Graph Transition Systems

  • Conference paper
Graph Transformations (ICGT 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4178))

Included in the following conference series:

Abstract

Graphs are suitable modeling formalisms for software and hardware systems involving aspects such as communication, object orientation, concurrency, mobility and distribution. State spaces of such systems can be represented by graph transition systems, which are basically transition systems whose states and transitions represent graphs and graph morphisms. Heuristic search is a successful Artificial Intelligence technique for solving exploration problems implicitly present in games, planning, and formal verification. Heuristic search exploits information about the problem being solved to guide the exploration process. The main benefits are significant reductions in the search effort and the size of solutions. We propose the application of heuristic search for the analysis of graph transition systems. We define algorithms and heuristics and present experimental results.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baldan, P., Corradini, A., König, B., König, B.: Verifying a behavioural logic for graph transformation systems. In: CoMeta 2003. ENTCS (2004)

    Google Scholar 

  2. Bonet, B., Geffner, H.: Planning as heuristic search. Artificial Intelligence 129(1–2), 5–33 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  3. Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. Comput. 186(2), 194–235 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  4. Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 597–610. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  6. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)

    MATH  Google Scholar 

  7. Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Basic concepts and double push-out approach. In: Algebraic approaches to graph transformation, vol. 1. World Scientific, Singapore (1997)

    Google Scholar 

  8. Courcelle, B.: Handbook of graph grammars and computing by graph transformations. Foundations, ch. 5, vol. 1, pp. 313–400. World Scientific, Singapore (1997)

    Book  Google Scholar 

  9. Demmer, M.J., Herlihy, M.: The arrow distributed directory protocol. In: Kutten, S. (ed.) DISC 1998. LNCS, vol. 1499, pp. 119–133. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  10. Edelkamp, S.: Planning with pattern databases. In: ECP, pp. 13–24 (2001)

    Google Scholar 

  11. Edelkamp, S.: Taming numbers and durations in the model checking integrated planning system. JAIR 20, 195–238 (2003)

    MATH  Google Scholar 

  12. Edelkamp, S., Jabbar, S., Lluch Lafuente, A.: Cost-algebraic heuristic search, pp. 1362–1367. AAAI, Menlo Park (2005)

    Google Scholar 

  13. Edelkamp, S., Leue, S., Lluch Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT 5(2-3), 247–267 (2003)

    Google Scholar 

  14. Edelkamp, S., Lluch Lafuente, A.: Abstraction databases in theory and model checking practice. In: ICAPS Workshop on Connecting Planning Theory with Practice (2004)

    Google Scholar 

  15. Gadducci, F., Lluch Lafuente, A.: Graphical verification of a spatial logic for the pi-calculus. In: Graph Transformation for Verification and Concurrency. ENTCS (to appear, 2005)

    Google Scholar 

  16. Groce, A., Visser, W.: Model checking Java programs using structural heuristics. In: ISSTA. ACM Press, New York (2002)

    Google Scholar 

  17. Gyapay, S., Schmidt, Á., Varró, D.: Joint optimization and reachability analysis in graph transformation systems with time. In: GT-VMT. ENTCS, vol. 109, pp. 137–147. Elsevier, Amsterdam (2004)

    Google Scholar 

  18. Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for heuristic determination of minimum path cost. IEEE Trans. on Systems Science and Cybernetics 4, 100–107 (1968)

    Article  Google Scholar 

  19. Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Hirsch, D., Lluch Lafuente, A., Tuosto, E.: A logic for application level QoS. In: Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages

    Google Scholar 

  21. Hoffmann, J., Nebel, B.: Fast plan generation through heuristic search. JAIR 14, 253–302 (2001)

    MATH  Google Scholar 

  22. Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)

    Google Scholar 

  23. Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: SPIN, pp. 299–305 (2006)

    Google Scholar 

  24. Korf, R.E.: Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence 27(1), 97–109 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  25. Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6, 1–35 (1995)

    Article  Google Scholar 

  26. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  27. Pearl, J.: Heuristics. Addison-Wesley, Reading (1985)

    Google Scholar 

  28. Rensink, A.: Towards model checking graph grammars. In: Automated Verification of Critical Systems, Tech. Report DSSE-TR-2003, pp. 150–160 (2003)

    Google Scholar 

  29. Rensink, A.: Time and space issues in the generation of graph transition systems. In: GraBaTs. ENTCS, vol. 127, pp. 127–139. Elsevier, Amsterdam (2005)

    Google Scholar 

  30. Rensink, A., Distefano, D.: Abstract graph transformation. In: SVV. ENTCS (to appear, 2005)

    Google Scholar 

  31. Rozenberg, G. (ed.): Handbook of graph grammars and computing by graph transformations. World Scientific, Singapore (1997)

    MATH  Google Scholar 

  32. Sobrinho, J.L.: Algebra and algorithms for QoS path computation and hop-by-hop routing in the internet. IEEE/ACM Trans. Netw. 10(4), 541–550 (2002)

    Article  Google Scholar 

  33. Varrò, D.: Automated formal verification of visual modeling languages by model checking. Journal on Software and Systems Modeling (2003)

    Google Scholar 

  34. Wegener, I.: Komplexitätstheorie. Springer, Heidelberg (2003) (in German)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, University of Dortmund, Dortmund, Germany

    Stefan Edelkamp & Shahid Jabbar

  2.  , via del Giardino A 58, I-50053, Empoli, Italy

    Alberto Lluch Lafuente

Authors
  1. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shahid Jabbar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Lluch Lafuente
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Business Communication and Information Science, University of Southern Denmark, 6000, Kolding, Denmark

    Andrea Corradini

  2. Technische Universität Berlin, Germany

    Hartmut Ehrig

  3. Dipartimento di Informatica, Università di Pisa,  

    Ugo Montanari

  4. Instituto de Informática, Universidade Federal do Rio Grande do Sul, Porto Alegre, Brazil

    Leila Ribeiro

  5. Leiden Center of Advanced Computer Science (LIACS), Leiden University, Niels Bohrweg 1, 2333, Leiden, CA, The Netherlands

    Grzegorz Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Edelkamp, S., Jabbar, S., Lafuente, A.L. (2006). Heuristic Search for the Analysis of Graph Transition Systems. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds) Graph Transformations. ICGT 2006. Lecture Notes in Computer Science, vol 4178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11841883_29

Download citation

  • DOI: https://doi.org/10.1007/11841883_29

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-38870-8

  • Online ISBN: 978-3-540-38872-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation