[logic-ml] JAIST Verification Seminars by Yijia Chen and Yohji Akama (Jan 31, Feb 9)

[Nao Hirokawa]

みなさま

1月31日(火)と2月9日(木)にJAISTで行われます、計算量・組合せ理論についての
２つセミナーをご案内致します。どうぞお気軽にお越しください。

  http://www.jaist.ac.jp/is/labs/ogawa-lab/vs12.html

廣川

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Seminars of Research Center for Software Verification, JAIST
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

== Seminar I ==

Date: 31st Jan (Tue) 13:00-17:00 (closing time is flexible)
Place: JAIST IS school collaboration room 7 (5F)

1. Prof.Yijia Chen (Shanghai Jiao Tong University) 
   "Parameterized complexity of SAT"

   Many natural computational problems are NP-hard, hence they have no
   polynomial time algorithms assuming NP \ne P. The traditional
   approaches for coping with such problems are heuristic and
   approximation algorithms. Nevertheless, the heuristic algorithms
   often lack a rigorous analysis, while the approximation algorithms
   cannot guarantee exact solutions. Parameterized algorithms offer
   another approach which achieves both criteria. The key observation
   is that many natural problem instances come with some parameters
   which can be expected to be small, e.g., the size of a vertex
   cover, the length of a database query, and the tree width of a
   graph. If an exponential time algorithm has its superpolynomial
   behavior restricted by the parameters, it might well be efficient
   in practice. As an example, there is an algorithm for SAT which is
   exponential in the tree width tw(\alpha) of a given instance \alpha
   and at the same time linear in the size of \alpha. Therefore, if
   there is a constant upper bound on tw(\alpha), we can solve the
   corresponding SAT in linear time.

   In this talk I will survey some major tools for designing
   parameterized algorithms, including bounded search tree,
   kernelization, tree width method, and algorithmic meta-theorems,
   etc, with a focus on applications to SAT. In passing, I will also
   discuss some corresponding lower bound results.

2. Dr. Yohji Akama (Tohoku University) 
   "A new order theory of set systems, WQO and BQO"

   A set system over a set $T$, a subfamily of the power set $P(T)$,
   is a topic of (extremal) combinatorics, as well as a target of an
   algorithm to learn in computational learning theory of languages.

   A well quasi-ordering (WQO for short) is introduced by Higman and
   employed in algebra, combinatorics, formal language theory, and so
   on. A better quasi-ordering (BQO for short) is introduced by 
   Nash-Williams and employed in infinitary combinatorics and
   verification of infinite-state systems.

   We generalize WQOs and BQOs by using set systems, define the order
   type of a set system from game-theoretic viewpoint and study
   nondeterministic, combinatorial operations on set systems, such as
   monotone (continuous) image and unbounded unions of set systems. 
   The motivating examples are the union of two colored arithmetical
   progressions, and the discolorization, and new useful examples are
   shuffle-product and shuffle-closure from formal language theory

   Furthermore, we provide a neat correspondence :
   quasi-orderings vs finitely branching simulations, and 
   set systems     vs linear, monotone, continuous functions.

   Next, we introduce a set system that has order type and corresponds
   to a BQO. We prove that the class of set systems corresponding to
   BQOs is closed by any monotone function. In  (Shinohara and
   Arimura. ``Inductive inference of unbounded unions of pattern
   languages from positive data.'', Theoretical Computer Science,
   pp.191-209, 2000), for any set system $L$, they considered the class
   of arbitrary (finite) unions of members of $L$. From viewpoint of
   WQOs and BQOs, we characterize the set systems $L$ such that the
   class of arbitrary (finite) unions of members of $L$ has order type.


== Seminar II ==

Date: 9th Feb (Thu) 13:00-15:00  (closing time is flexible)
Place: JAIST IS school collaboration room 7 (5F)

*  Prof.Yijia Chen (Shanghai Jiao Tong University) 
   "A Logic for PTIME and a Parameterized Halting Problem"

   Whether there is a logic for polynomial time (PTIME) is the central
   problem in finite model theory. When formalizing this problem,
   Gurevich (1988), together with Blass, actually proposed a logic
   LFP_inv, which is a version of least fixed-point logic plus some
   additional invariance condition. Although they don't believe that
   LFP_inv captures PTIME, no proof was given. Later, in a work of
   Nash, Remmel, and Vianu (2005), it was shown that whether LFP_inv
   captures PTIME is equivalent to the parameterized complexity of a
   halting problem:

     input: A nondeterministic Turing machine M and a natural number n
     in unary.
     parameter: |M|, i.e., the size of M
     question: does M accept the empty input in at most n steps?

   Our recent work (2010-11) reveals that it is even equivalent to an
   open problem in proof complexity, i.e., whether there is a
   polynomial optimal proof system for the set TAUT of tautologies of 
   propositional logic.

   In this talk, I will discuss all these equivalences and their
   extensions to some other complexity classes beside PTIME. It turns
   out that Levin's optimal inverters (1973) play a central role in
   the proofs.

   This is joint work with Joerg Flum.