• Mingsheng YING

• Professor

• Department of Computer Science and Technology

• Joined Department: 1992

• Email:yingmsh@tsinghua.edu.cn

• URL:http://cs.tsinghua.edu.cn/~yingmsh

• Phone:+86-10-62779625

• Fax:+86-10-62782266

Education background

Diploma of Mathematics, Fuzhou Normal College, Jiangxi, China, 1981.

Social service

State Key Laboratory of Intelligent Technology and Systems: Chair of Academic Committee (2002-);

Artificial Intelligence Journal: Member of Editorial Board (2008-).

Areas of Research Interests/ Research Projects

Quantum Computation

Semantics of Programming Languages, Logics in AI

National Natural Science Foundation of China: Quantum Programming Methodologies (2008-2011).

Research Status

1.Topology in Process Algebras. Process algebras are among the most successful models of concurrent systems. One of the central notions of process algebras is bisimulation. However, it cannot be used to describe the approximate behaviour of concurrent systems. I proposed a new theory of topology in process algebras in order to describe the approximate correctness and evolution process of concurrent systems.

2.Floyd-Hoare Logic for Quantum Programs. Floyd-Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about the correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, I developed a full-fledged Hoare logic for both partial and total correctness of quantum programs. In particular, the (relative) completeness of this logic is proved. The proof techniques are quite different from those for classical programs and need mathematical tools.

Honors And Awards

National Natural Sciences Award, Second Class-Non-Classical Computation: Formal Models and Logical Foundations (2008);

Natural Sciences Award by Ministry of Education, First Class-Formal Methods for Complex Computer Systems and their Logical Foundations (2004);

China Association of Science and Technology: Young Scientists Award (1994).

Academic Achievement

[1] M. S. Ying, Quantum computation, quantum theory and AI (Invited Field Review), Artificial Intelligence, 174(2010)162-176.

[2] H. Zhang and M. S. Ying, Decidable fragments of first-order language under stable model semantics and circumscription, Proc. of the 24th AAAI Conference on Artificial Intelligence (AAAI-10), 2010.

[3] W. M. Liu, X. T. Zhang, S. J. Li and M. S. Ying, Reasoning about cardinal directions between extended objects, Artificial Intelligence, (In Press, Available online 15 June 2010).

[4] M. S. Ying, R. Y. Duan, Y. Feng and Z. F. Ji, Predicate transformer semantics of quantum programs (Invited Chapter), in S. Gay and I. Mackie (eds.), Semantic Techniques in Quantum Computation, Cambridge University Press, 2010, Cambridge, pp.311-360.

[5] M. S. Ying and Y. Feng, An algebraic language for distributed quantum computing, IEEE Transactions on Computers, 58(2009)728-743.

[6] M. S. Ying, Y. Feng, R. Y. Duan and Z. F. Ji, An algebra of quantum processes, ACM Transactions on Computational Logic, 10(2009) art. no. 19.

[7] R. Y. Duan, Y. Feng, X. Yu and M. S. Ying, Distinguishability of quantum states by separable operations, IEEE Transactions on Information Theory, 55(2009)1320-1330.

[8] R. Y. Duan, Y. Feng and M. S. Ying, Perfect distinguishability of quantum operations, Physical Review Letters, 103(2009) art. no. 210501.

[9] Z. F. Ji, G. M. Wang, R. Y. Duan, Y. Feng and M. S. Ying, Parameter estimation of quantum channels, IEEE Transactions on Information Theory, 54(2008)5172-5185.

[10] R. Y. Duan, Y. Feng and M. S. Ying, Local distinguishability of multipartite unitary operations, Physical Review Letters, 100(2008) art. No. 020503.

[11] S. J. Li and M. S. Ying, Soft constraint abstraction based on semiring homomorphism, Theoretical Computer Science, 403(2008)192-201.

[12] X. T. Zhang, W. M. Liu, S. J. Li and M. S. Ying, Reasoning with cardinal directions: An efficient algorithm, in: Proc. of the 23rd AAAI Conference on Artificial Intelligence (AAAI-08), 2008, pp. 387-392.

[13] M. S. Ying, Quantum logic and automata theory (Invited Chapter), in: D. Gabbay, D. Lehmann and K. Engesser (eds), Handbook of Quantum Logic and Quantum Structures, Elsevier, 2007, Amsterdam, pp.619-754.

[14] Y. Feng, R. Y. Duan, Z. F. Ji and M. S. Ying, Proof rules for correctness of quantum programs, Theoretical Computer Science, 386(2007)151-166.

[15] Y. Feng, R. Y. Duan, Z. F. Ji and M. S. Ying, Probabilistic bisimulations for quantum processes, Information and Computation, 104(2007)152-158.

[16] R. Y. Duan, Y. Feng and M. S. Ying, Entanglement is not necessary for perfect discrimination between unitary operations, Physical Review Letters, 98(10)(2007), art. No. 100503.

[17] L. R. Xia, J. Lang and M. S. Ying, Strongly decomposable voting rules on multi-attribute domains, in: Proceedings, 22nd National Conference on Artificial Intelligence (AAAI'07).

[18] M. S. Ying, Linguistic quantifiers modeled by Sugeno integrals, Artificial Intelligence, 170(6-7)(2006), 581-606.

[19] Z. F. Ji, Y. Feng, R. Y. Duan and M. S. Ying, Identification and distance measures of measurement apparatus, Physical Review Letters, 96(20)(2006), art. No. 200401.

[20] R. Y. Duan, Y. Feng and M. S. Ying, Partial recovery of quantum entanglement, IEEE Transactions on Information Theory, 52(7)(2006), 3080-3104.

[21] Y. Z. Cao and M. S. Ying, Similarity-based supervisory control of discrete-event systems, IEEE Transactions on Automatic Control, 51 (2)(2006), 325-330.

[22] M. S. Ying, A theory of computation based on quantum logic (I), Theoretical Computer Science, 344(2-3)(2005) 134-207.

[23] M. S. Ying, Pi-calculus with noisy channels, Acta Informatica, 41(9)(2005), 525-593.

[24] M. S. Ying, Knowledge transformation and fusion for system diagnosis, Artificial Intelligence, 163(1)(2005)1-45.

[25] Y. Feng, R. Y. Duan and M. S. Ying, Catalyst-assisted probabilistic entanglement transformations, IEEE Transactions on Information Theory, 51(3)(2005), 1090-1101.

[26] X. M. Sun, R. Y. Duan, and M. S. Ying, The existence of quantum entanglement catalysts, IEEE Transactions on Information Theory, 51(1)(2005), 75-80.

[27] S. J. Li and M. S. Ying, Generalized region calculus, Artificial Intelligence, 160(1-2)(2004), 1-34.

[28] D. W. Qiu and M. S. Ying, Characterization of quantum automata, Theoretical Computer Science, 312(2-3) (2004)479-489.

[29] M. S. Ying, Reasoning about probabilistic sequential programs in a probabilistic logic, Acta Informatica, 39(5) (2003), 318-389.

[30] S. J. Li and M. S. Ying, Region connection calculus: its models and composition table, Artificial Intelligence, 145(1-2)(2003), 121-146.

[31] M. S. Ying, Bisimulation indexes and their applications, Theoretical Computer Science, 275(1-2) (2002), 1-68.

[32] M. S. Ying, Additive models for probabilistic processes, Theoretical Computer Science, 275(1-2) (2002), 481-519.

[33] M. S. Ying and H. Q. Wang, A lattice-theoretical model of consequences, conjectures and hypotheses, Artificial Intelligence, 139(2) (2002), 253-267.

[34] M. S. Ying, Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs (Research Monograph), Springer-Verlag, New York, February 2001.

[35] M. S. Ying, M. Wirsing, Recursive equations in higher-order process calculi, Theoretical Computer Science, 266(1-2) (2001), 389-352.

[36] M. S. Ying, Weak confluence and -inertness, Theoretical Computer Science, 238(1-2)( 2000), 465-475.

[37] L. Biacino, G. Gerla and M. S. Ying, Approximate reasoning based on similarity, Mathematical Logic Quarterly, 46(1)(2000), 77-86.

[38] M. S. Ying, A shorter proof to uniqueness of solutions of equations, Theoretical Computer Science, 216(1-2) (1999), 395-397.

[39] M. S. Ying, When is the ideal completion of abstract basis algebraic, Theoretical Computer Science, 159(2) (1996), 355-356.

[40] M. S. Ying, A logic for approximate reasoning, The Journal of Symbolic Logic, 59(3)(1994), 830-837.

[41] M. S. Ying, The fundamental theorem of ultraproduct in Pavelka's logic, Zeitschr. f. math. Logik und Grundlagen d. Math., 38(3)(1992), 197-201.

[42] M. S. Ying, Compactness, the Lowenheim-Skolem property and the direct product of lattices of truth values, Zeitschr. f. math. Logik und Grundlagen d. Math., 38(5-6)(1992), 521-524.

[43] M. S. Ying, Deduction theorem for many-valued inference, Zeitschr. f. math. Logik und Grundlagen d. Math., 37(6)(1991), 533-537.

[44] M. S. Ying, On a class of non-causal triangle functions, Mathematical Proceedings of Cambridge Philosophical Society, 106(3)(1989), 467-469.