Research Interests: Formal verification, algorithmsand complexity
Office Phone: 86-10-6275 0359
Wang, Hanpin now is a professor in the Department of Computer Science and technology, School of EECS, and has served as a vice director of Institute of Software and the head of Laboratory of Theoretical Computer Science since 2003. He obtained his B.Sc. from Anhui Normal University in 1985, and Ph.D. from Beijing Normal University in 1993 respectively. His research interests include formal semantics and verification of computer systems, algorithms and computational complexity.
Dr. Wang has published more than 70 research papers, and some of them are published in important conferences and journals, such as ICALP, IFIP, TCS, DBLP and Information and Computation. He is serving as the head of the Department of Discrete Intelligence Computing, China Association of Artificial Intelligence. He was awarded the first class Natural Science Prize for Science & technology Achievement of the Ministry of Education of China in 2011.
Dr. Wang’s research has got more than 8 financial support projects, including NSFC, 973 programs, 863 project, etc. His research achievements are summarized as follows:
1) Duration Calculus (DC in abbreviation) is an elegant kind of logic to describe timed or hybrid systems. But in classical DC, the time intervals involved are limited to be finite. This makes it impossible to describe the infinitely running systems such as operating systems. I incorporated DC with infinite intervals as a solution. Also, fixed-point operators was added to DC to give the semantics of loop statements. These two changes extend the expressiveness of DC.
2) There has been considerable interest in several frameworks for studying the complexity of counting problems. One natural framework is the counting Constraint Satisfaction Problem (#CSP). Another is Graph Homomorphism (GH) which can be seen as a special case of #CSP. Such frameworks express a large class of counting problems in the Sum-of-Product form. It is known that if P is not equal to NP, then there exists a problem that is neither in P nor NP-complete. And there is an analogue of Ladner's Theorem for the class #P. However, for these frameworks, various beautiful dichotomy theorems have been proved, classifying all problems in the broad class into those which are computable in polynomial time (in P) and those which are #P-hard. A natural question is: For how broad a class of counting problems can one prove a dichotomy theorem? We prove a complexity dichotomy theorem for Holant problems over Boolean domain with non-negative weights. It is the first complete Holant dichotomy where constraint functions are not necessarily symmetric.