The workshop "Methods for Modalities" (M4M) aims to bring together researchers interested in developing algorithms, verification methods and tools based on modal logic. Here the term "modal logics" is conceived broadly, including description logic, guarded fragments, conditional logic, temporal and hybrid logic, etc.

To stimulate interaction and transfer of expertise, M4M will feature a number of invited talks by leading scientists, research presentation aimed at highlighting new developments, and submissions of system demonstrations. We strongly encourage young researchers and students to submit papers and posters, especially for experimental and prototypical software tools which are related to modal logics.

To register for the workshop, please visit he local site http://www.lsv.ens-cachan.fr/M4M5

The list of invited speakers include

• Balder ten Cate (University of Amsterdam)
  Title: XML from the viewpoint of modal logic
• Wiebe van der Hoek (University of Liverpool) Title: Extended Modal Logic for Social Software
• Koen Claessen (Chalmers University of Technology)
  Title: Finite Model Finding: Implementation Techniques and Non-standard Applications
• Patricia Bouyer (Laboratoire Specification et Verification)
  Title: Model-Checking Timed Temporal Logics
• Ahmed Bouajjani (University of Paris 7)
  Title: Rewrite systems with data : A framework for reasoning about systems with unbounded structures and data domains

Final versions of accepted papers will be published online in an Elsevier ENTCS volume. A preliminary version of the proceedings will also be available at the workshop.

Instructions for preparing your paper with the ENTCS style for M4M5 can be found at http://www.entcs.org/prelim.html where the generic package can be downloaded. You should also use the file entcsmacro.sty that is dedicated to the M4M5 proceedings.

This is the final list of accepted papers:

• Regular Papers:
  • P. Abate, R. Gore and F. Widmann.
    An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability
  • T. Ågotnes, W. van der Hoek and M. Wooldridge.
    Completeness and Complexity of Multi-Dimensional CTL
  • G. Aucher, P. Balbiani, L. Fariñas del Cerro and A. Herzig.
    Global and local graph modifiers
  • P. Balbiani, J. Broersen and J. Brunel.
    Decision procedures for a deontic logic modeling temporal inheritance of obligations
  • M. Bauland, M. Mundhenk, T. Schneider, H. Schnoor, I. Schnoor and H. Vollmer.
    The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments
  • W. Bekker and V. Goranko.
    Symbolic model checking of tense logics on rational Kripke models
  • T. Bolander and P. Blackburn.
    Terminating Tableau Calculi for Hybrid Logics extending K
  • L. Bozzelli.
    CARET with Forgettable Past
  • K. Brünnler and T. Studer.
    Syntactic Cut-Elimination for Common Knowledge
  • W. Conradie.
    Completeness and Correspondence in Hybrid Logic via an extension of SQEMA
  • M. Kaminski and G. Smolka.
    Hybrid Tableaux for the Difference Modality
  • J. Reed and F. Pfenning.
    Intuitionistic Letcc via Labelled Deduction
  • P. Sala, A. Montanari, V. Goranko and D. Bresolin.
    Tableau-based decision procedure for the logic of proper subinterval structures over dense orderings
  • I. Seylan and R. Cenk Erdur.
    A Tableau Decision Procedure for ALC with Monotonic Modal Operators and Constant Domains
  • T. Tulenheimo and M. Rebuschi.
    Equivalence Criteria for Compositional IF Modal Logics
• System Descriptions:
  • P. Abate and R. Gore.
    The Tableau Workbench
  • G. Calin, R. Myers, D. Pattinson and L. Schröder.
    COLOSS: The Coalgebraic Logic Satisfiability Solver
  • G. Hoffmann and C. Areces.
    HTab: A Terminating Tableaux System for Hybrid Logic
  • M. Sadrzadeh and S. Richards.
    Aximo: automated axiomatic reasoning for information update
  • D. Sustretov, G. Hoffmann, C. Areces and P. Blackburn.
    Experiments in Theorem Proving for Topological Hybrid Logic
• Presentation-Only Papers:
  • T. de Lima, H. van Ditmarsch and A. Herzig.
    An Optimal Method for Reasoning about Actions and Knowledge
  • L. Giordano, V. Gliozzi, N. Olivetti and G. Pozzato.
    Extension of Description Logics for Reasoning About Typicality

Keep in mind the following dates:

• Extended Deadline for submissions: September 15th, 2007
• Notification of acceptance: October 15th, 2007
• Camera ready versions due: November 5th, 2007
• Workshop dates: November 29-30th, 2007

The program committee for M4M consists of

• Natasha Alechina, University of Nottingham;
• Carlos Areces, INRIA Lorraine (co-chair);
• Philippe Balbiani, IRIT;
• Nicole Bidoit, Université Paris-Sud;
• Patrick Blackburn, INRIA Lorraine;
• Torben Braüner, Roskilde University;
• Stéphane Demri, ENS de Cachan; (co-chair);
• Maarten de Rijke, University of Amsterdam;
• Valentin Goranko, University of the Witwatersrand;
• Rajeev Goré, The Australian National University;
• Carsten Lutz, Dresden University of Technology;
• Nicolas Markey, ENS de Cachan;
• Angelo Montanari, University of Udine;
• Ulrike Sattler, University of Manchester;
• Holger Schlingloff, Humboldt University / FIRST;
• Renate Schmidt, University of Manchester;
• Johan van Benthem, University of Amsterdam / Stanford University.