Print Shortlink

REPORT: Methods for Modalities

The 6th workshop on Methods for Modalities – Copenhagen, November 2009

The workshop Methods for Modalities 6 (M4M-6) was held form the 12th to the 14th of November 2009 in Copenhagen, Denmark. The aim of the workshop was to bring together researchers interested in developing algorithms, verification methods and tools based on modal logic, where modal logic was understood in a broad sense.

The workshop started out with an invited talk by Renate Schmidt about two different approaches, via first-order resolution methods and the direct tableau synthesis framework, to automatically generate proof systems for a variety of modal logics. This was followed by a contributed talk by Dmitry Tishkovsky discussing admissibility in the same framework. Resolution methods were discussed several times the first day whereas tableau methods remained a central theme throughout the workshop. Filtration also played a considerable role in ensuring termination of tableaux in the framework of Renate Schmidt, but filtration is also relevant for problems related to controller synthesis and orchestrator synthesis, as was discussed by Guillaume Feuillade afterwards. The morning session of the first day was ended by a talk by Antti Kuutsisto on a result in definability theory of modal logic that has application to proving decidability results in multi-modal logic.

After the lunch the magic took over as invited speaker Stéphane Demri gave a talk on separation logic and what he called “the magic ward”. After this knowledge entered the picture as Jens Ulrik Hansen talked about tableaux for dynamic epistemic logics, and thereafter Thomas Studer talked about two different approaches to proof systems for common knowledge. Luis Menasché Schechter then followed by a talk about PDL based on the pi-calculus, before Martin Lange ended the first day with a system description of a tool for checking satisfiability and validity for modal fixpoint logics. In the end of the day the discussion of tableau vs. resolution methods was replaced by a discussion between tableau methods and methods based on automatas.

The second day started out with an invited talk by Kim Guldstrand Larsen about model checking for various extensions of CTL (Computational Tree Logic), and the usage of these in hardware and software verification and specification. The tool he presented for this was UPPAAL. Angelo Kyrilov continued in the temporal path with a system description of a tool for testing satisfiability for LTL (Linear Temporal Logic) followed by a talk concerning a new way of defining the Until operator using a “history” operator, given by Marco Volpe. Afterwards Valentin Goranko shifted the focus from point based to interval based temporal logics by discussing the undecidability of logics containing a modality for interval overlab. The last talk before lunch was a presentation on Hybrid Ontology by John Jeremy Meyers.

After lunch the second day, invited speaker Yde Venema turned to coalgebraic logics when discussing Moss' cover modality and cut-free Gentzen proof systems based on a modal distributive law. Following this Kurt Ranalter talked about embedding natural deduction for constructive modal logic into intuitionistic modal logic. The day was ended with two system descriptions, Daniel Hausmann talking about CoLoSS which was based on a coalgebraic semantics, and Gert van Valkenhoef presenting a simple to use multi S5 tableau prover. At the second day tableau calculus still played a central role, but natural deduction and automata methods was also widely discussed.

The last day started a little later because of the previous nights conference dinner at restaurant Koefoed, where we where also educated on the wonderful Danish island of Bornholm. Franz Baarder opened the last day with an invited talk about how light-weighted description logics such as EL had nice complexity properties while still remaining useful in applications such as in biomedical ontologies. Description logic stayed in the picture as Wojciech Jamroga continued talking about adding coalition logic machinery to it. Mark Kaminski then gave a systems description of Spartacus, a tableau based prover for hybrid logic, and the discussion again was about designing blocking mechanisms. Tableaux and blocking continued to play a role as the last talk of the workshop by Régis Alenda concerned a theorem-prover for logic of comparative concept similarity called CSL-lean.

The location of the workshop was the IDA Conference Center nicely located at the docks in the center of Copenhagen, which besides providing a beautiful view also served delicious breakfast, lunch, cakes and coffee. The last day of the conference we where presented with a typical Danish lunch at the conference center before a nice walk (no rain!) though central Copenhagen took us to the Soeren Kierkegaard research center. Here the very last talk of the conference was about the life of the famous Danish philosopher Soeren Kierkegaard. This was however not the end of the conference; we still had a visit to a Danish Brewery, but the details are left as an exercise for the reader…

For more on the workshop and the full program see the webpage: