AutoTab'09

TABLEAUX 2009 Workshop on
Tableaux versus automata as logical decision methods

Terminating semantic tableaux have served for a long time as one of the practically most efficient types of decision procedures for a wide range of logical systems. On the other hand, over the past two decades automata-based methods for testing satisfiability and model checking for various modal and temporal logics of computations have gained very wide recognition and popularity, because they provide uniform, elegant, and often optimal decision procedures. Furthermore, a number of increasingly efficient automata-based tools have been implemented, and there seems to be a growing perception amongst the formal verification community that these tools are superior and preferable to the tableau-based tools. That perception, however, is not based on systematic comparative analysis, and some practical experience with well-designed tableau-based tools suggest that such perception can be misleading. Moreover, various optimization techniques, such as on-the-fly methods, draw automata-based algorithms very close to tableau-like procedures, thus strongly suggesting that tableaux and automata are closely related formalisms for deciding logical satisfiability. Yet, few formal technical results to that effect are known, and the scientific discussion on the pros and cons, similarities and differences, comparisons of applicability, efficiency, and performance between tableaux and automata has so far been rather sporadic. The purpose of this workshop is to provide an expert forum for such discussion, to provoke and foster discussion between the automata and tableaux communities, and to stimulate further research on the topic.