Theory: Algebraic and Logical Design Methods
Complexity and verification
How hard is it to verify the correctness of programs? This question is of overriding concern to many researchers in the Logic and Computation group at Swansea, from the most generic investigations into the complexity of proofs, to the specific problem of finding the (theoretically and practically) fastest solution to the ubiquitous Satisfiability Problem. Of equal concern are questions regarding the complexity of equivalence and model checking of systems, particularly those spanning infinitely many states.
Infinite state automata theory
Verification tools for modelling systems typically rely on such models being finite state, so as to allow for the complete exploration of state spaces. The aim of F G Moller's research is to develop structural techniques which not only extend automated verification to infinite state systems (which, e.g., encode infinite data types), but which also circumvent the state space explosion problem. Two important tools developed in this study are structural decomposition techniques, and the exploitation of game theoretic interpretations of the various verification problems. Much of this work is done in collaboration with P Jancar (Ostrava) and Y Hirshfeld (Tel Aviv).
Modal and temporal logics
F G Moller has developed various program logics for reasoning about reactive systems which have been implemented in a number of tools used effectively in the verification of practical systems. The aim of F G Moller's research is to characterise and interrelate the expressive power of the various logical frameworks, particularly involving fixed point logics. The main tool in this work is the use of Ehrenfeucht-Fraisse games, which characterise the semantic content of these logics. Much of this work is done in collaboration with A Rabinovich (Tel Aviv).
Proof complexity
Proof complexity analyses the structure of proofs for various proof systems. Research in proof complexity tries to understand the complexity of proofs of formulas in specific proof systems, and to classify the relative complexity of proofs of formulas within different proof systems. The major open question in propositional proof complexity initiated by S Cook (University of Toronto), which is equivalent to an importent question in computational complexity theory, is whether or not there is a proof system in which all propositional tautologies have polynomial-size proofs.
Propositional proof complexity has some beautiful connections to bounded arithmetic. A Beckmann's contribution in propositional proof complexity are mainly on proof systems related to bounded arithmetic like constant depth Frege systems. He has started research on height-restricted proof systems which naturally links to dynamic ordinal analysis. He has collaborated with S Buss (UCSD) on improvements of separation in such proof systems (paper). A Beckmann has coined the term "cut reduction by switching" for a cut reduction method which uses methods from boolean complexity theory, the so-called switching lemmas.
Satisfiability problems
Satisfiability problems are at the heart of many practical verification techniques. They are also a key to the P = NP Problem. O Kullmann has developed general methods for upper bounds on satisfiability problems requiring exponential time, leading to new tools for satisfiability (e.g., specialisations and extensions of resolution). The theory of autarkies has been initiated to detect redundancies in propositional formulae. New applications of linear programming, matching theory and matroid theory have been found, unifying and strengthening results on several important classes of propositional formulas with polynomial time satisfiability decision. Recently, with the "combinatorics of conflicts" O Kullmann has opened a new area of interactions between combinatorics, graph theory, research on SAT algorithms and algebra. And thorough theoretical and practical investigations into the nature of phase transitions and the interactions of SAT and Statistical Physics have started. O Kullmann is also developing the OKlibrary, a generative C++ library for generalised SAT solving, combining innovative new algorithms with advanced implementation and design techniques, and based on the award-winning OKsolver.
