CLoDeM on Thursday, July 15th

09:00‑10:00 Invited talk
Location: AT 2.14
09:00 Moshe Vardi (Rice University, US)
Symbolic Techniques in Propositional Satisfiability Solving
10:30‑11:30 Contributed talks
Location: AT 2.14
10:30 Oliver Friedmann and Markus Latte
Decision Procedures for CTL*

We give an overview over three serious attempts to devise an effective decision method for CTL*, namely Emerson and Jutla's automata-theoretic decision procedure, Reynolds' tableau search method and our recent approach based on an infinite tableau system with natural rules and with global conditions on the branches.

11:00 Rajeev Gore and Florian Widmann
An Experimental Comparison of Theorem Provers for CTL

We compare existing implementations of four automatic theorem provers for CTL based on tree-tableaux, BDDs, resolution and games using formula-classes from the literature

11:30‑12:30 Invited talk
Location: AT 2.14
11:30 Jerome Leroux (Labri Bordeaux, France)
Presburger Automata
14:00‑15:00 Contributed talks
Location: AT 2.14
14:00 Aiswarya Cyriac
A New Version of Focus Games for LTL Satisfiability

We study the connections between game theoretic method and automata theoretic method for the satisfiability problem of LTL. We also introduce a one-player focus game as an intermediate formalism between the two.

14:30 Lukasz Kaiser and Tobias Ganzow
New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures

Weak monadic second-order logic is a very expressive logic which has been used successfully for verification of software and hardware systems. Moreover, structures of bounded clique width have a decidable weak MSO theory which allows to specify and verify detailed correctness properties. However, one obstacle to a wide application of WMSO verification techniques in practice is that the prevalent model-checking algorithms are based on tree automata, and hence require to encode the structure of interest in the binary tree which is often a cause of inefficiency.

We present a new algorithm for model-checking weak MSO on inductive structures, a certain kind of structures of bounded clique width, together with a proof of its decidability which follows from Shelah's composition method. Our algorithm directly manipulates formulas and checks them on the structure of interest without the need to encode it in the binary tree. In fact, the model-checking problem is reduced to solving a finite reachability game. Our algorithm exposes both similarities and differences between the standard automata techniques and certain formula conversions used for decomposition.

15:30‑16:30 Invited talk
Location: AT 2.14
15:30 Yevgeny Kazhakov (Oxford University, UK)
Consequence-Based Reasoning for Description Logic Ontologies