---------------------------------------------------------------- IFIP Working Group 1.6 on Term Rewriting Report of the annual meeting: August 10, 2006 (Seattle, WA, USA) Chair: Claude Kirchner Vice-Chair: Juergen Giesl Secretary: Laurent Vigneron Participants: F. Baader, D. Dougherty (invited), J. Giesl, B. Gramlich, C. Kirchner, H. Kirchner, S. Lucas, C. Lynch (invited), A. Middeldorp, U. Montanari, Y. Toyama, L. Vigneron, H. Zantema ---------------------------------------------------------------------- Agenda: 1. Technical Presentations 2. Progress Reports 3. International School on Rewriting 3. General discussion: new trends in rewriting research and applications 4. Business Meeting ---------------------------------------------------------------------- 1. Technical Presentations. ----------------------------------------- * Salvador Lucas: Context-Sensitive Dependency Pairs. Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. It is useful, for example, for studying the termination of OBJ and Maude programs. Although there is a good number of techniques for proving termination of context-sensitive rewriting (CSR), the dependency pair approach, one of the most powerful techniques for proving termination of rewriting, has not been investigated in connection with proofs of termination of CSR. The use of dependency pairs in proofs of termination of CSR is shown. The implementation and practical use of the developed techniques yield a novel and powerful framework which improves the current state-of-the-art of methods for proving termination of CSR. ----------------------------------------- * Christopher Lynch: Cryptographic Protocol Analysis with Rigid Theorem Proving. Protocols can be represented as Horn clauses. Using rigid variables permits to bound the number of sessions without limiting the Intruder capabilities. As a rigid variable is a variable that can be instantiated only once, only one session is considered. This is compatible with the use of algebraic properties (exclusive-or, associtativity of concatenation,...), provided the unification algorithm is extended to consider them. Deductions are done by applying rigid resolution with some restrictions. ----------------------------------------- * Daniel Dougherty: Reasoning about Policies for Programs. Access-control policies have grown from simple matrices to non-trivial specifications written in sophisticated languages. The increasing complexity of these policies demands correspondingly strong automated reasoning techniques for understanding and debugging them. The need for these techniques is even more pressing given the rich and dynamic nature of the environments in which these policies evaluate. A framework is defined to represent the behavior of access-control policies in a dynamic environment: policy rules are defined as datalog programs. Several interesting, decidable analyses using first-order temporal logic are specified. This illustrates the subtle interplay between logical and state-based methods, particularly in the presence of three-valued policies. A notion of policy equivalence is also defined; it is especially useful for modular reasoning. Those techniques have been implemented in Margrave. What has to be considered now is obligations and business rules. This brings intriguing applications for term rewriting systems and automated deduction. ----------------------------------------- * Ugo Montanari: Some Recent Developments about Tile Systems. Tiles combine horizontal and vertical structures through interfaces. They can be considered like rewriting, but they require synchronisation between some rules. Tiles can be combined horizontally, vertically and in parallel. Horizontal arrows define term contexts, and represent suitable classes of graphs; vertical arrows define actions, and represent partial orders. Tiles can be represented by monoidal theories, and so can be transformed to algebraic theories. Operations apply on objects, arrows and cells. An abstract semantics is provided by the definitino of tile bisimulation and decomposition property (used for having congruences). Tile systems can be seen as co-algebras or bi-algebras. ----------------------------------------- * Hans Zantema: Adding Constants to String Rewriting. Considering a signature where all symbols are either unary or constants, every term can be transformed into a corresponding string by just reading all symbols in the term from left to right, ignoring the optional variable. By lifting this transformation to rewrite rules, any term rewriting system (TRS) over such a signatures is transformed into a corresponding string rewriting system (SRS). The preservation of properties by this transformation is investigated. It turns out that any TRS over such a signature is terminating if and only if the corresponding SRS is terminating. In this way tools for proving termination of string rewriting like TORPA can be applied for proving termination of TRSs over such a signature. For other properties like CR, WCR, WN and UN, a corresponding preservation property does not hold. ---------------------------------------------------------------------- 2. Progress Reports. All participants report about their recent work advances and about their teaching activities related to rewriting. ---------------------------------------------------------------------- 3. International School on Rewriting. A report on the first ISR has been presented at the business meeting of RTA 2006. Proposition by Aart Middeldorp to organize the 2008 ISR in Obergurgl, Austria, together with the annual meeting of the WG. The 2008 RTA conference has also been proposed (and chosen) to be hosted in Austria, in Hagenberg next to Linz. Juergen Giesl has proposed some bylaws for ISR. They are discussed and modified. The new version will be sent to the WG members for validation. Discussion about the frequency of ISR: either every year, or every other year. The main problem is to be sure to get enough students if done every year. On the other side, to become recognized, the school should need to occur several consecutive years. Claude Kirchner proposes to host the 2007 ISR in Nancy again, using the 2006 experience. The vote to the question "Should there be a ISR in 2007 in Nancy?" gives the following result: YES:6 NO:4 NO_OPINION:2 The vote to the questions "Should there be a ISR and the WG meeting in 2008 in Obergurgl..." gives the following results: - "if RTA is in Austria?": YES:10 NO:0 NO_OPINION:2 - "if RTA is not in Austria?": YES:7 NO:0 NO_OPINION:5 As a conclusion, in 2007 the second ISR will hold in Nancy, and in 2008 the third ISR will hold in Obergurgl. The periodicity of ISR will be decided later, according to the experience of those three years. Improvements proposed for the next ISRs: to propose grants for students; to propose parallel tracks for taking into account the level of the participants; to try to attract industrials and researchers/students of other domains to participate. ---------------------------------------------------------------------- 4. Business meeting ----------------------------------------- * News from the WG Chair: - Juergen Giesl has been nominated as WG Vice-Chair. ----------------------------------------- * News from the IFIP: - There is a new TC1 Chair since January 2006: Michael Hinchey (NASA). - A new presentation of the IFIP is available online: http://www.ifip.org/archive/presentation/ ----------------------------------------- * Rewriting activities: Past conferences and workshops: - TERMGRAPH: Vienna, April 2006 8 talks, 1 invited talk. - WRLA: Vienna, April 2006 13 talks, 1 invited talks. - RTA: Seattle, August 2006 59 submissions, 28 accepted papers (including 4 system presentations), 80 participants. - HOR: Seattle, August 2006 6 talks, 2 invited talks, 2 participants. - RULE: Seattle, August 2006 7 talks, 2 invited talks, 14 participants. - UNIF: Seattle, August 2006 9 talks, 19 participants. - WRS: Seattle, August 2006 7 talks, 2 invited talks, 20 participants. - WST: Seattle, August 2006 15 talks, 2 invited talks, 30 participants. Rewriting lectures: - ISR: Nancy, July 2006 37 participants, 12 speakers. Upcoming workshops and conferences: - RDP 2007: RTA and TLCA, in Paris, with many workshops related to rewriting (HOR, RULE, SecReT, UNIF, WRS, WST). ----------------------------------------- * Membership: Dan Dougherty and Chris Lynch have been invited to the WG meeting and have long standing research activities in rewriting. It is proposed to admit them as full members of the WG. ----------------------------------------- * Next meeting: In 2007, either in Paris (RDP) or in Nancy (ISR). ----------------------------------------------------------------------