In nD differential geometry, basic geometric structures and properties are described locally by differentiable functions and equations with indices that obey Einstein summation convention. Although symbolic manipulati...In nD differential geometry, basic geometric structures and properties are described locally by differentiable functions and equations with indices that obey Einstein summation convention. Although symbolic manipulation of such indexed functions is one of the oldest research topics in computer algebra, so far there exists no normal form reduction algorithm to judge whether two indexed polynomials involving indices of different coordinate systems are equal or not. It is a challenging task in computer algebra. In this paper, for a typical framework—the partial derivatives in coordinate transformation matrix involved are of order no more than two (such as local computations of ordinary curvatures and tor-sion), we put forward two algorithms, one on elimination of all redundant dummy indices of indexed polynomials, the other on normalization of such indexed polynomials, by which we can judge whether two indexed polynomials are equal or not. We implement the algorithms with Maple V.10 and use them to solve tensor verification problems in differential geometry, and to derive automatically the transformation rules of locally defined indexed functions under the change of local coordinates.展开更多
This paper surveys the new field of programming methodology and techniques for future quantum computers, including design of sequential and concurrent quantum programming languages, their semantics and implementations...This paper surveys the new field of programming methodology and techniques for future quantum computers, including design of sequential and concurrent quantum programming languages, their semantics and implementations. Several verification methods for quantum programs and communication protocols are also reviewed. The potential applications of programming techniques and related formal methods in quantum engineering are pointed out.展开更多
A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agent...A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.展开更多
Verification in quantum computations is crucial since quantum systems are extremely vulnerable to the environment.However,verifying directly the output of a quantum computation is difficult since we know that efficien...Verification in quantum computations is crucial since quantum systems are extremely vulnerable to the environment.However,verifying directly the output of a quantum computation is difficult since we know that efficiently simulating a large-scale quantum computation on a classical computer is usually thought to be impossible.To overcome this difficulty,we propose a self-testing system for quantum computations,which can be used to verify if a quantum computation is performed correctly by itself.Our basic idea is using some extra ancilla qubits to test the output of the computation.We design two kinds of permutation circuits into the original quantum circuit:one is applied on the ancilla qubits whose output indicates the testing information,the other is applied on all qubits(including ancilla qubits) which is aiming to uniformly permute the positions of all qubits.We show that both permutation circuits are easy to achieve.By this way,we prove that any quantum computation has an efficient self-testing system.In the end,we also discuss the relation between our self-testing system and interactive proof systems,and show that the two systems are equivalent if the verifier is allowed to have some quantum capacity.展开更多
An important task for quantum cloud computing is to make sure that there is a real quantum computer running,instead of classical simulation.Here we explore the applicability of a cryptographic verification scheme for ...An important task for quantum cloud computing is to make sure that there is a real quantum computer running,instead of classical simulation.Here we explore the applicability of a cryptographic verification scheme for verifying quantum cloud computing.We provided a theoretical extension and implemented the scheme on a 5-qubit NMR quantum processor in the laboratory and a 5-qubit and 16-qubit processors of the IBM quantum cloud.We found that the experimental results of the NMR processor can be verified by the scheme with about 1.4%error,after noise compensation by standard techniques.However,the fidelity of the IBM quantum cloud is currently too low to pass the test(about 42%error).This verification scheme shall become practical when servers claim to offer quantum-computing resources that can achieve quantum supremacy.展开更多
Widespread applications of 5G technology have prompted the outsourcing of computation dominated by the Internet of Things(IoT)cloud to improve transmission efficiency,which has created a novel paradigm for improving t...Widespread applications of 5G technology have prompted the outsourcing of computation dominated by the Internet of Things(IoT)cloud to improve transmission efficiency,which has created a novel paradigm for improving the speed of common connected objects in IoT.However,although it makes it easier for ubiquitous resource-constrained equipment that outsources computing tasks to achieve high-speed transmission services,security concerns,such as a lack of reliability and collusion attacks,still exist in the outsourcing computation.In this paper,we propose a reliable,anti-collusion outsourcing computation and verification protocol,which uses distributed storage solutions in response to the issue of centralized storage,leverages homomorphic encryption to deal with outsourcing computation and ensures data privacy.Moreover,we embed outsourcing computation results and a novel polynomial factorization algorithm into the smart contract of Ethereum,which not only enables the verification of the outsourcing result without a trusted third party but also resists collusion attacks.The results of the theoretical analysis and experimental performance evaluation demonstrate that the proposed protocol is secure,reliable,and more effective compared with state-of-the-art approaches.展开更多
基金supported by Major State Basic Research Development Program of China (Grant No.2004CB318001)Leading Academic Disciplines Program of Shanghai (Grant No. S30501)
文摘In nD differential geometry, basic geometric structures and properties are described locally by differentiable functions and equations with indices that obey Einstein summation convention. Although symbolic manipulation of such indexed functions is one of the oldest research topics in computer algebra, so far there exists no normal form reduction algorithm to judge whether two indexed polynomials involving indices of different coordinate systems are equal or not. It is a challenging task in computer algebra. In this paper, for a typical framework—the partial derivatives in coordinate transformation matrix involved are of order no more than two (such as local computations of ordinary curvatures and tor-sion), we put forward two algorithms, one on elimination of all redundant dummy indices of indexed polynomials, the other on normalization of such indexed polynomials, by which we can judge whether two indexed polynomials are equal or not. We implement the algorithms with Maple V.10 and use them to solve tensor verification problems in differential geometry, and to derive automatically the transformation rules of locally defined indexed functions under the change of local coordinates.
基金supported by the Australian Research Council(DP110103473)the National Natural Science Foundation of China(60736011)
文摘This paper surveys the new field of programming methodology and techniques for future quantum computers, including design of sequential and concurrent quantum programming languages, their semantics and implementations. Several verification methods for quantum programs and communication protocols are also reviewed. The potential applications of programming techniques and related formal methods in quantum engineering are pointed out.
文摘A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.
基金Project supported by the National Natural Science Foundation of China(Grant Nos.61372076,61971348,and 62001351)Foundation of Shaanxi Key Laboratory of Information Communication Network and Security(Grant No.ICNS201802)+1 种基金Natural Science Basic Research Program of Shaanxi,China(Grant No.2021JM-142)Key Research and Development Program of Shaanxi Province,China(Grant No.2019ZDLGY09-02)。
文摘Verification in quantum computations is crucial since quantum systems are extremely vulnerable to the environment.However,verifying directly the output of a quantum computation is difficult since we know that efficiently simulating a large-scale quantum computation on a classical computer is usually thought to be impossible.To overcome this difficulty,we propose a self-testing system for quantum computations,which can be used to verify if a quantum computation is performed correctly by itself.Our basic idea is using some extra ancilla qubits to test the output of the computation.We design two kinds of permutation circuits into the original quantum circuit:one is applied on the ancilla qubits whose output indicates the testing information,the other is applied on all qubits(including ancilla qubits) which is aiming to uniformly permute the positions of all qubits.We show that both permutation circuits are easy to achieve.By this way,we prove that any quantum computation has an efficient self-testing system.In the end,we also discuss the relation between our self-testing system and interactive proof systems,and show that the two systems are equivalent if the verifier is allowed to have some quantum capacity.
基金国家自然科学基金(the National Natural Science Foundation of China under Grant No.60373113)国家重点基础研究发展规划(973)(the National Grand Fundamental Research 973 Program of China under Grant No.2004CB318000)
基金supported by National Key Research and Development Program of China (2018YFA0306600)the National Natural Science Foundation of China (11661161018, and 11927811)+7 种基金Anhui Initiative in Quantum Information Technologies (AHY050000)supported in part by the Australian Research Council (DE180100156)supported by the Natural Science Foundation of Guangdong Province (2017B030308003)the Key R&D Program of Guangdong province (2018B030326001)the Science, Technology and Innovation Commission of Shenzhen Municipality (JCYJ20170412152620376, JCYJ20170817105046702 and KYTDPT20181011104202253)the National Natural Science Foundation of China (11875160 and U1801661)the Economy, Trade and Information Commission of Shenzhen Municipality (201901161512)Guangdong Provincial Key Laboratory (2019B121203002)
文摘An important task for quantum cloud computing is to make sure that there is a real quantum computer running,instead of classical simulation.Here we explore the applicability of a cryptographic verification scheme for verifying quantum cloud computing.We provided a theoretical extension and implemented the scheme on a 5-qubit NMR quantum processor in the laboratory and a 5-qubit and 16-qubit processors of the IBM quantum cloud.We found that the experimental results of the NMR processor can be verified by the scheme with about 1.4%error,after noise compensation by standard techniques.However,the fidelity of the IBM quantum cloud is currently too low to pass the test(about 42%error).This verification scheme shall become practical when servers claim to offer quantum-computing resources that can achieve quantum supremacy.
基金This work was supported by the National Natural Science Foundation of China under Grant Nos.61962009 and 62262058Science and Technology Major Support Program of Guizhou Province under Grant No.20183001+6 种基金Key Program of the National Natural Science Union Foundation of China under Grant No.U1836205Science and Technology Program of Guizhou Province under Grant No.ZK[2021]325Project of High-level Innovative Talents of Guizhou Province under Grant No.[2020]6008Youth Growth Fund by Guizhou Provincial Education Department under Grant No.KY[2017]318Foundation of Postgraduate of Guizhou Province under Grant No.YJSCXJH2019101Science and Technology Program of Guiyang under Grant No.[2021]1-5Science and Technology Planning Project of Tongren Municipality under Grant No.[2020]78.
文摘Widespread applications of 5G technology have prompted the outsourcing of computation dominated by the Internet of Things(IoT)cloud to improve transmission efficiency,which has created a novel paradigm for improving the speed of common connected objects in IoT.However,although it makes it easier for ubiquitous resource-constrained equipment that outsources computing tasks to achieve high-speed transmission services,security concerns,such as a lack of reliability and collusion attacks,still exist in the outsourcing computation.In this paper,we propose a reliable,anti-collusion outsourcing computation and verification protocol,which uses distributed storage solutions in response to the issue of centralized storage,leverages homomorphic encryption to deal with outsourcing computation and ensures data privacy.Moreover,we embed outsourcing computation results and a novel polynomial factorization algorithm into the smart contract of Ethereum,which not only enables the verification of the outsourcing result without a trusted third party but also resists collusion attacks.The results of the theoretical analysis and experimental performance evaluation demonstrate that the proposed protocol is secure,reliable,and more effective compared with state-of-the-art approaches.
