Reachability analysis plays a central role in system design and verification. The reachability problem, denoted ◊jΦ, asks whether the system will meet the property Φ after some time in a given time interval j. Recently, it has been considered on a novel kind of real-time systems — quantum continuous-time Markov chains (QCTMCs), and embedded into the model-checking algorithm. In this paper, we further study the repeated reachability problem in QCTMCs, denoted □Ι◊jΦ, which concerns whether the system starting from each absolute time in Ι meet the property Φ after some coming relative time in j. First of all, we reduce it to the real root isolation of a class of real-valued functions (exponential polynomials), whose solvability is conditional to Schanuel’s conjecture being true. To speed up the procedure, we employ the strategy of sampling. The original problem is shown to be equivalent to the existence of a finite collection of satisfying samples. We then present a sample-driven procedure, which can effectively refine the sample space after each time of sampling, no matter whether the sample itself is satisfying or conflicting. The improvement on efficiency is validated by randomly generated instances. Hence the proposed method would be promising to attack the repeated reachability problems together with checking other ω -regular properties in a wide scope of real-time systems.

Verifying quantum programs has attracted a lot of interest in recent years. In this article, we consider the following two categories of termination problems of quantum programs with nondeterminism, namely: (1) (termination) Is an input of a program terminating with probability one under all schedulers? If not, how can a scheduler be synthesized to evidence the nontermination? (2) (universal termination) Are all inputs terminating with probability one under their respective schedulers? If yes, a further question asks whether there is a scheduler that forces all inputs to be terminating with probability one together with how to synthesize it; otherwise, how can an input be provided to refute the universal termination? For the effective verification of the first category, we over-approximate the reachable set of quantum program states by the reachable subspace, whose algebraic structure is a linear space. On the other hand, we study the set of divergent states from which the program terminates with probability zero under some scheduler. The divergent set also has an explicit algebraic structure. Exploiting these explicit algebraic structures, we address the decision problem by a necessary and sufficient condition, i.e., the disjointness of the reachable subspace and the divergent set. Furthermore, the scheduler synthesis is completed in exponential time, whose bottleneck lies in computing the divergent set reported for the first time. For the second category, we reduce the decision problem to the existence of an invariant subspace, from which the program terminates with probability zero under all schedulers. The invariant subspace is characterized by linear equations and thus can be efficiently computed. The states on that invariant subspace are evidence of the nontermination. Furthermore, the scheduler synthesis is completed by seeking a pattern of finite schedulers that forces all inputs to be terminating with positive probability. The repetition of that pattern yields the desired universal scheduler that forces all inputs to be terminating with probability one. All the problems in the second category are shown, also for the first time, to be solved in polynomial time. Finally, we demonstrate the aforementioned methods via a running example—the quantum Bernoulli factory protocol.

We consider a class of univariate real functions---poly-powers---that extend integer exponents to real algebraic exponents for polynomials. Our purpose is to isolate positive roots of such a function into disjoint intervals, which can be further easily computed up to any desired precision. To this end, we first classify poly-powers into simple and non-simple ones, depending on the number of linearly independent exponents. For the former, we present a complete isolation method based on Gelfond--Schneider theorem. For the latter, the completeness depends on Schanuel's conjecture. Finally experiential results demonstrate the effectivity of the proposed method.

ABSTRACT Optimal signatures (generating signatures as short as possible), which achieve the optimal bandwidth for communication, are extremely useful in bandwidth‐critical networks. Previous approaches use the random permutations with large block size as building blocks, which incurs less efficient implementations in the real world. Meanwhile, all the practical signature schemes are not optimal in bandwidth including PSS‐R (probabilistic signature scheme with message recovery ), FDH ( Full Domain Hash), and DSA (Digital Signature Algorithm). This paper presents three constructions for optimal signature schemes. All the proposals use both the random oracles and the ideal ciphers with smaller block sizes as building blocks to obtain optimal paddings for signature schemes. The ideal ciphers in our schemes can be implemented by real block ciphers (e.g., AES (Advanced Encryption Standard)‐256). Concrete implementations of these signature schemes can utilize the trapdoor permutations of Rabin and RSA, respectively. Surprisingly, RSA and Rabin (trapdoor permutations) lead to not only optimality in bandwidth but also a tight security. Therefore, besides yielding secure signatures with high efficiency, our proposals can also be flexibly applied to the bandwidth‐limited networks that reduces the communication cost as less as possible. Copyright © 2014 John Wiley & Sons, Ltd.