Methods for Modalities 6
Copenhagen, Denmark. November 12-14, 2009
Photos
Photos from the event taken by Jørgen Villadsen are available.
Program
The full workshop program is available.
Theme
The workshop series 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 logic" is conceived broadly, including description logic, guarded fragments, conditional logic, temporal and hybrid logic, etc.
Special Features
To stimulate interaction and transfer of expertise, M4M will feature a number of invited talks by leading scientists, research presentations aimed at highlighting new developments, and submissions of system demonstrations. We strongly encourage young researchers and students to submit papers, especially for experimental and prototypical software tools which are related to modal logics.

Mini-Course: Autumn School on Modal Logic
M4M-6 will be preceded by a two-day mini-course called "Autumn School on Modal Logic" aimed at preparing PhD students and other researchers for participation in the workshop. The autumn school will be taught by Carlos Areces, Patrick Blackburn, Valentin Goranko, Renate Schmidt, and Carsten Schürmann. Consult the autumn school home page for further information:

http://hylocore.ruc.dk/m4m6school.html

The autumn school is associated with the FIRST research school (http://first.dk).

Submissions
Authors are invited to submit papers in the following three categories.
  • Regular papers up to 15 pages, describing original research.
  • System descriptions of up to 12 pages, describing new systems or significant upgrades of existing ones.
  • Presentation-only papers, describing work recently published or submitted (no page limit). These will not be included in the proceedings, but pre-prints or post-prints can be made available to participants.

Submissions should be made via EasyChair at the following address:

http://www.easychair.org/conferences/?conf=m4m6

Final versions of accepted papers will be published online in an Elsevier ENTCS volume. A preliminary version of the proceedings will be provided at the workshop. Instructions for preparing your paper can be found at the web page of ENTCS (http://www.entcs.org). Please remember to use the file prentcsmacro.sty that is dedicated to the M4M proceedings.

The Call for Papers is available.

Registration
To register for the workshop and/or the preceding autumn school on modal logic, please visit the following site:

http://hylocore.ruc.dk/m4m6registration.html

Registration opens on September 1st. The deadline for early registration is October 19th.

Venue and Travelling
M4M-6 will take place at the IDA Conference Center on Kalvebod Brygge 31-33 in the center of Copenhagen. The conference center is located 1 km from Copenhagen Central Station. There is a direct train connection between Copenhagen Airport and Copenhagen Central Station. The train is of type "Re". Copenhagen Central Station is called "Hovedbanegården" or sometimes "København H" in Danish. The following map shows how to get from the central station to the workshop venue:


View Larger Map

Note that the workshop venue is not the same as the venue for the autumn school on modal logic. Travelling information pertaining to the autumn school venue can be found at the autumn school home page.

To find cheap plane tickets to Copenhagen, please visit Momondo. For the local weather forecast, please visit DMI.

Accommodation
The following hotels are all within walking distance from both Copenhagen Central Station and the workshop venue:
  • Cabinn City. A relatively inexpensive hotel located within 600 meters from both the workshop venue and Copenhagen Central Station.
  • Wakeup Copenhagen. Located 250 meters from the workshop venue and 1 km from Copenhagen Central Station.
  • Danhostel Copenhagen City. A hostel offering very cheap dorm bed accommodation and accommodation for 4+ people in one room. Located within 1 km from both the workshop venue and Copenhagen Central Station.
  • Choice Hotels. Choice Hotels offer two reasonably priced 3 star hotels right next to Copenhagen Central Station and 1 km from the workshop venue. They are called Comfort Hotel Europa and Comfort Hotel Excelsior.
If you would like to consider further accommodation options, please consult booking.com. This page also allows you to make online bookings of any of the hotels mentioned above.
Important Dates
Keep in mind the following dates:
  • Deadline for submissions: September 1, 2009 (extended deadline)
  • Notification of acceptance: October 5th, 2009
  • Camera ready versions due: October 26th, 2009
  • Workshop dates: November 12-14th, 2009
Invited Speakers
The invited speakers of M4M-6 are:
Accepted Papers
Below is the final list of accepted papers.

Regular Papers:

  • Sergey Babenyshev, Vladimir Rybakov, Renate A. Schmidt and Dmitry Tishkovsky. A Tableau Method for Checking Rule Admissibility in S4.
  • Philippe Balbiani, Fahima Cheikh and Guillaume Feuillade. Controller/orchestrator synthesis via filtration.
  • Mario Benevides and Luis Menasché Schechter. A Propositional Dynamic Logic for Concurrent Programs Based on the Pi-Calculus.
  • Samuel Bucheli, Roman Kuznets and Thomas Studer. Two ways to common knowledge.
  • Dario Della Monica, Davide Bresolin, Valentin Goranko, Angelo Montanari and Guido Sciavicco. Undecidability of the Logic of Overlap Relation over Discrete Linear Orderings.
  • Jens Ulrik Hansen. Terminating tableaux for dynamic epistemic logics.
  • Antti Kuusisto and Lauri Hella. Monadic Sigma 1 1 and Modal Logic with Quantified Binary Relations.
  • Andrea Masini, Luca Viganò and Marco Volpe. A History of Until.
  • Kurt Ranalter. Embedding constructive K into intuitionistic K.
  • Inanc Seylan and Wojciech Jamroga. Coalition Description Logic with Individuals.

System Descriptions:

  • Régis Alenda, Nicola Olivetti and Gian Luca Pozzato. CSL-lean: A theorem-Prover for the logic of Comparative Concept Similarity.
  • Oliver Friedmann and Martin Lange. A Solver for Modal Fixpoint Logics.
  • Valentin Goranko, Angelo Kyrilov and Dmitry Shkatov. Tableau tool for testing satisfiability in LTL: Implementation and experimental analysis.
  • Daniel Götzmann, Mark Kaminski and Gert Smolka. Spartacus: A Tableau Prover for Hybrid Logic.
  • Daniel Hausmann and Lutz Schroeder. Optimizing Conditional Logic Reasoning within CoLoSS.
  • Gert van Valkenhoef, Elske van der Vaart and Rineke Verbrugge. OOPS: An S5n Prover for Educational Settings.

Presentation-Only Papers:

  • John Jeremy Meyers. Hybrid Ontology.
Local Organisers and Support
The local organisers of M4M-6 are:

The workshop is supported by the research project Hybrid Logic, Computation, and Reasoning Methods (HYLOCORE).

Program Committee
The program committee for M4M-6 consists of:
  • Carlos Areces, INRIA Lorraine
  • Lars Birkedal, IT University of Copenhagen
  • Patrick Blackburn, INRIA Lorraine
  • Thomas Bolander (co-chair), Technical University of Denmark
  • Julian Bradfield, University of Edinburgh
  • Torben Braüner (co-chair), Roskilde University
  • Balder ten Cate, University of Amsterdam
  • Stephane Demri, ENS de Cachan
  • Hans van Ditmarsch, University of Otago
  • Melvin Fitting, City University of New York
  • John Gallagher, Roskilde University
  • Mai Gehrke, Radboud University Nijmegen
  • Silvio Ghilardi, University of Milano
  • Valentin Goranko, University of the Witwatersrand
  • Rajeev Goré, ANU
  • Michael R. Hansen, Technical University of Denmark
  • Andreas Herzig, IRIT
  • Wiebe van der Hoek, University of Liverpool
  • Martin Lange, LMU München
  • Carsten Lutz, Dresden University of Technology
  • Angelo Montanari, University of Udine
  • Valeria de Paiva, Cuill Inc.
  • Thomas Schneider, University of Manchester
  • Carsten Schürmann, IT University of Copenhagen
  • Gert Smolka, Saarland University
  • Anders Søgaard, University of Copenhagen
  • Jørgen Villadsen, Technical University of Denmark
  • Frank Wolter, University of Liverpool
  • Thomas Ågotnes, Bergen University College