CLoDeM on Thursday, July 15th

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.

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

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.

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.