----------------------------------------------------------------
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).
----------------------------------------------------------------------