Model-checking linear-time properties of quantum systems

Mingsheng Ying; Yangjia Li; Nengkun Yu; Yuan Feng

doi:10.1145/2629680

Model-checking linear-time properties of quantum systems

Mingsheng Ying
, Yangjia Li
, Nengkun Yu
, Yuan Feng

Computer Science

Stony Brook University

Research output: Contribution to journal › Article › peer-review

24 Scopus citations

Abstract

We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω?properties recognizable by reversible Büchi automata.

Original language	English
Article number	22
Journal	ACM Transactions on Computational Logic
Volume	15
Issue number	3
DOIs	https://doi.org/10.1145/2629680
State	Published - Jul 8 2014

Keywords

Invariants
Liveness
Model-checking
Persistence properties
Quantum automata
Quantum engineering systems
Safety

Access to Document

10.1145/2629680

Cite this

@article{ebcd2f186de3435c8938217b655ba71c,

title = "Model-checking linear-time properties of quantum systems",

abstract = "We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω?properties recognizable by reversible B{\"u}chi automata.",

keywords = "Invariants, Liveness, Model-checking, Persistence properties, Quantum automata, Quantum engineering systems, Safety",

author = "Mingsheng Ying and Yangjia Li and Nengkun Yu and Yuan Feng",

note = "Publisher Copyright: {\textcopyright} 2014 ACM.",

year = "2014",

month = jul,

day = "8",

doi = "10.1145/2629680",

language = "English",

volume = "15",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery",

number = "3",

}

TY - JOUR

T1 - Model-checking linear-time properties of quantum systems

AU - Ying, Mingsheng

AU - Li, Yangjia

AU - Yu, Nengkun

AU - Feng, Yuan

PY - 2014/7/8

Y1 - 2014/7/8

N2 - We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω?properties recognizable by reversible Büchi automata.

AB - We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain (closed) subspaces of state Hilbert spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then, an automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and ω?properties recognizable by reversible Büchi automata.

KW - Invariants

KW - Liveness

KW - Model-checking

KW - Persistence properties

KW - Quantum automata

KW - Quantum engineering systems

KW - Safety

UR - https://www.scopus.com/pages/publications/84907587265

U2 - 10.1145/2629680

DO - 10.1145/2629680

M3 - Article

SN - 1529-3785

VL - 15

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 3

M1 - 22

ER -

Model-checking linear-time properties of quantum systems

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this