2010 Algorithm and Information Day

Institute of Software, Chinese Academy of Sciences

Beijing, May 26, 2010

Program

Location: Lecture Room, 3th Floor, Building #5, ISCAS (北京市中关村南四街4号，中科院软件所5号楼3层报告厅)

Contact: Angsheng Li

Phone: 62661629

Title:　　 On simultaneous resettability conjecture
Speaker: 　Dongdai Lin 林东岱
Abstract:　
In this talk, we will report the progress on the study of simultaneous resettability conjecture which was proposed by Barak et al. at FOCS 2001. We will first introduce a new primitives called instance-dependent verifiable random function, and then show its construction and applications in the study of simultaneous resettable conjecture.

Title:　　 Algebraic property test
Speaker: 　Yicheng Pan 潘祎诚
Abstract:　
Property test is the task to decide efficiently whether a given function f belongs to a function family that possesses a property or far from it. We consider the algebraic property named the linear- and affine-invariance, which is the property of a function family that is closed under linear- and affine- transformations on the domain, and closed under linear combination of functions, respectively. It is a significant generalization of the well-known linearity and low-degree tests. Kaufman and Sudan started this study by introducing the notions of "constraint" and "characterization" to characterize the locally testable affine- and linear-invariant families of functions over finite fields of constant size. We consider the locality k and field size q as parameters, and show that for any affine-invariant family over prime field, the four notions of "the constraint", "the characterization", "the formal characterization" and "the local testability" are equivalent modulo a poly(k,q) of the corresponding localities; and that for any linear-invariant family over prime field, the notions of "the characterization", "the formal characterization" and "the local testability" are equivalent modulo a poly(k,q) of the corresponding localities.
We also give some negative results. We prove that for any non-Boolean finite field of size q, there exists a linear-invariant function family which has a strong 2-local constraint, but is not locally testable. We also give a counterexample for the case of affine-invariant family over extension field which has small local constraints, but no test of locality of size independent of the field size.
Biography:
Yicheng Pan is a Ph.D student in the State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. His supervisor is Prof. Angsheng Li. His research interests include computational complexity and algorithms.

Title:　　 A cut-off approach for bounded verification of parameterized systems
Speaker: 　Qiusong Yang 杨秋松
Abstract:　
The features in multi-threaded programs, such as recursion, dynamic creation and communication, pose a great challenge to formal verification. A widely adopted strategy is to verify tentatively a system with a smaller size, by limiting the depth of recursion or the number of replicated processes, to find errors without ensuring the full correctness. The model checking of parameterized systems, a parametric infinite family of systems, is to decide if a property holds in every size instance. There has been a quest for finding cut-offs for the verification of parameterized systems. The basic idea is to find a cut-off on the number of replicated processes or on the maximum length of paths needed to prove a property, standing a chance of improving verification efficiency substantially if one can come up with small or modest cut-offs. In this paper, a novel approach, called Forward Bounded Reachability Analysis (FBRA), based upon the cut-off on the maximum lengths of paths is proposed for the verification of parameterized systems. Experimental results show that verification efficiency has been significantly improved as a result of the introduction of our new cut-offs.
Biography:
Qiusong Yang received a B.S. degree in computer science from Central South University China in 2000 and a Ph.D. degree in Computer Science from the Institute of Software Chinese Academy of Sciences (ISCAS), in 2008. Now he is an assistant professor of ISCAS. His research interests include software process technologies, formal methods, and model checking.

Title:　   Formal semantics of framed temporal logic programming language MSVL
Speaker:  Xiaoxiao Yang 杨潇潇
Abstract:　
Temporal logic programming is a new paradigm for describing concurrent systems, in which the implementation of systems and property of systems can be specified in one logic. Though researchers developed interpreters to execute temporal logic programs, and temporal logic and its executed subsets are widely applied to the areas of concurrent programs verification, however, there has not formalized an integrated formal semantics for temporal logic programs, at least for interval temporal logic programming languages. Therefore, we are motivated to investigate the formal semantics of interval temporal logic programming language MSVL, including its minimal model, operational and axiomatic semantics.
Firstly, a Projection Temporal Logic is discussed and some of its laws are given. After that, an executable temporal logic programming language, called Modeling Simulation and Verification Language (MSVL), is formalized. Since framing destroys monotonicity, canonical models ---used to define the semantics of non-framed programs --- are no longer appropriate. To deal with this, a minimal model theory is developed, using which the temporal semantics of framed programs is captured. The existence of a minimal model for a given framed program is demonstrated. Further a synchronous communication mechanism for concurrent programs is provided by means of the framing technique and minimal model semantics. Secondly, we investigate an operational semantics of MSVL. The consistency between minimal model semantics and operational semantics are proved. Based on the operational rules, an interpreter for MSVL is developed in C++. Thirdly, for the purpose of verifying the properties of concurrent programs in a unified notation, we investigate the axiomatic semantics of MSVL. To deduce a program over an interval, a set of rules in terms of triple like Hoare logic is formalized. The axiom system is proved to be sound and relative complete with regard to an operational model of MSVL. Further, a prototype verifier based on PVS is employed to indicate the semi-automatical verification using MSVL.
Biography:
I am a postdoc researcher at State Key Laboratory of Computer Science in Institute of Software, Chinese Academy of Science. I received my Bachelor Degree (July, 2004) and PhD ( June, 2009) in Computer Science and Technology from Xidian University, China. My research interests centre on the formal semantics of programming languages, temporal logic and temporal logic programming and model checking.
My homepage is: http://lcs.ios.ac.cn/~xxyang/

Title:　 　On the complexity and approximability of the minimum contamination problems
Speaker:  Linqing Tang 唐林清
Abstract: 
In this talk, we present some results about the complexity and approximability of the Minimum Contamination Problems, which are derived from diffusion control areas and has been wildly studied recently. We show that both the Minimum Average Contamination Problem and the Minimum Worst Contamination Problem are NP-hard problems in determinstic setting. For anyε>0, we give (1+ε, O(log n))-bicriteria approximation algorithms for both the Minimum Average Contamination Problem and the Minimum Worst Contamination Problem. Moreover, we show that the Minimum Average Contamination Problem is NP-hard to be approximated within 5/3-εand the Minimum Worst Contamination Problem is NP-hard to be approximated within 4-ε, for any ε>0. We also consider the contamination cost minimization problem and present an O(log n) approximation algorithm for this problem.
Biography:
Linqing Tang is a PHD student of ISCAS. His major research interests include approximation algorithms and hardness of approximation for Max CSPs and optimization combinational problem over social networks.

Title:　 　Open problems in counting complexity
Speaker:  Mingji Xia 夏盟佶
Abstract:
In the past several years, there are quite a few complexity dichotomy theorems for counting problem classes of #CSP, counting graph homomorphisms, and Holant problems. We introduce some of them. For more general counting problem classes, the dichotomy theorems are still unknown.
We introduce one important method in this area, Valiant's holographic reduction, and a domain changed application of holographic reduction. We don't know whether it is computable to decide a counting problem is hard or easy, assuming #P is not equal to FP. Maybe this application gives some idea to this open question. The converse of holographic reduction is open, although we known it holds for some cases.
Biography:
Mingji Xia received his B.S. degree in Mathematics from College of Mathematics Science, Shandong Normal University, Shandong, P.R.China in 2002, and received his Ph.D. degree in Computer Science from Institute of Software, Chinese Academy of Sciences in 2008.