Well-Structured Graph Transformation Systems with Negative Application Conditions

详细信息    查看全文

• 作者：Barbara K?nig (20)
  Jan Stückrath (20)
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2012
• 出版时间：2012
• 年：2012
• 卷：7562
• 期：1
• 页码：96-110
• 全文大小：257KB
• 参考文献：1. Abdulla, P.A., ?erāns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proc. of LICS 1996, pp. 313-21. IEEE (1996)
  2. Bertrand, N., Delzanno, G., K?nig, B., Sangnier, A., Stückrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: Proc. of RTA 2012. LIPIcs. Schloss Dagstuhl -Leibniz Center for Informatics (2012)
  3. Bouajjani, A., Mayr, R.: Model Checking Lossy Vector Addition Systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol.?1563, pp. 323-33. Springer, Heidelberg (1999) CrossRef
  4. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer (2006)
  5. Esparza, J., Nielsen, M.: Decidability issues for Petri nets. Technical Report RS-94-8, BRICS (May 1994)
  6. Fellows, M.R., Hermelin, D., Rosamond, F.A.: Well-Quasi-Orders in Subclasses of Bounded Treewidth Graphs. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol.?5917, pp. 149-60. Springer, Heidelberg (2009) CrossRef
  7. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science?256(1-2), 63-2 (2001) CrossRef
  8. Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inf.?26(3-4), 287-13 (1996)
  9. Habel, A., Pennemann, K.-H.: Nested Constraints and Application Conditions for High-Level Structures. In: Kreowski, H.-J., Montanari, U., Yu, Y., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol.?3393, pp. 293-08. Springer, Heidelberg (2005) CrossRef
  10. Joshi, S., K?nig, B.: Applying the graph minor theorem to the verification of graph transformation systems. Technical Report 2012-01, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universit?t Duisburg-Essen (2012)
  11. Joshi, S., K?nig, B.: Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.?5123, pp. 214-26. Springer, Heidelberg (2008) CrossRef
  12. K?nig, B., Stückrath, J.: Well-structured graph transformation systems with negative application conditions. Technical Report 2012-03, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universit?t Duisburg-Essen (2012)
  13. L?we, M.: Algebraic approach to single-pushout graph transformation. Theoretical Computer Science?109, 181-24 (1993) CrossRef
  14. Rensink, A.: Representing First-Order Logic Using Graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol.?3256, pp. 319-35. Springer, Heidelberg (2004) CrossRef
  15. Robertson, N., Seymour, P.: Graph minors XX. Wagner’s conjecture. Journal of Combinatorial Theory Series B?92, 325-57 (2004) CrossRef
  16. Robertson, N., Seymour, P.: Graph minors XXIII. Nash-Williams-immersion conjecture. Journal of Combinatorial Theory Series B?100, 181-05 (2010) CrossRef
  17. Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol.?1. World Scientific (1997)
  
• 作者单位：Barbara K?nig (20)
  Jan Stückrath (20)
  
  20. Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universit?t?Duisburg-Essen, Germany
  

文摘

Given a transition system and a partial order on its states, the coverability problem is the question to decide whether a state can be reached that is larger than some given state. For graphs, a typical such partial order is the minor ordering, which allows to specify “bad graphs-as those graphs having a given graph as a minor. Well-structuredness of the transition system enables a finite representation of upward-closed sets and gives rise to a backward search algorithm for deciding coverability. It is known that graph tranformation systems without negative application conditions form well-structured transition systems (WSTS) if the minor ordering is used and certain condition on the rules are satisfied. We study graph transformation systems with negative application conditions and show under which conditions they are well-structured and are hence amenable to a backwards search decision procedure for checking coverability.