Jianxin Wu - Model Checking Quantum Systems: Principles and Algorithms

Model checking is one of the most successful verification techniques and has been widely adopted in traditional computing and communication hardware and software industries.

This book provides the first systematic introduction to model-checking techniques applicable to quantum systems, with broad potential applications in the emerging industry of quantum computing and quantum communication as well as quantum physics.

Suitable for use as a course textbook and for self-study, graduate and senior undergraduate students will appreciate the step-by-step explanations and the exercises included. Researchers and engineers in the related fields can further develop these techniques in their own work, with the final chapter outlining potential future applications.

MINGSHENG YING is Distinguished Professor in the Centre for Quantum Software and Information, University of Technology Sydney; Deputy Director for Research of the Institute of Software, Chinese Academy of Sciences; and Cheung Kong Chair Professor in the Department of Computer Science and Technology, Tsinghua University. His research interests are quantum computing, programming theory and logics in artificial intelligence. He is the author of the books Foundations of Quantum Programming(2016) and Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs(2001). Currently, he serves as (Co-)Editor-in-Chief of ACM Transactions on Quantum Computing.

YUAN FENG is Professor in the Centre for Quantum Software and Information, University of Technology Sydney. His research interests include formal verification of quantum systems, the theory of quantum programming, quantum information and computation and probabilistic systems. He has published more than 70 research papers in international leading journals and mainstream conferences. He was awarded an ARC (Australian Research Council) Future Fellowship in 2010.

MINGSHENG YING

University of Technology Sydney

YUAN FENG

University of Technology Sydney

University Printing House, Cambridge CB2 8BS, United Kingdom

One Liberty Plaza, 20th Floor, New York, NY 10006, USA

477 Williamstown Road, Port Melbourne, VIC 3207, Australia

314321, 3rd Floor, Plot 3, Splendor Forum, Jasola District Centre, New Delhi 110025, India

79 Anson Road, #0604/06, Singapore 079906

Cambridge University Press is part of the University of Cambridge.

It furthers the Universitys mission by disseminating knowledge in the pursuit of education, learning, and research at the highest international levels of excellence.

www.cambridge.org

Information on this title: www.cambridge.org/9781108484305

DOI: 10.1017/9781108613323

Mingsheng Ying and Yuan Feng 2021

This publication is in copyright. Subject to statutory exception and to the provisions of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press.

First published 2021

Printed in the United Kingdom by TJ Books Limited, Padstow Cornwall

A catalogue record for this publication is available from the British Library.

Library of Congress Cataloging-in-Publication Data

Names: Ying, Mingsheng, author. | Feng, Yuan, 1977 author.

Title: Model checking quantum systems : principles and algorithms / Mingsheng Ying, University of Technology, Sydney, Yuan Feng, University of Technology, Sydney.

Description: Cambridge, UK ; New York, NY : Cambridge University Press, 2020. | Includes bibliographical references and index.

Identifiers: LCCN 2020041998 (print) | LCCN 2020041999 (ebook) | ISBN 9781108484305 (hardback) | ISBN 9781108613323 (epub)

Subjects: LCSH: Quantum computing. | Computer systemsVerification.

Classification: LCC QA76.889 .Y564 2020 (print) | LCC QA76.889 (ebook) | DDC 006.3/843dc23

LC record available at https://lccn.loc.gov/2020041998

LC ebook record available at https://lccn.loc.gov/2020041999