English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Verifying quantum systems has attracted a lot of interest in the lastdecades. In this paper, we study the quantitative model-checking of quantumcontinuous-time Markov chains (quantum CTMCs). The branching-time properties ofquantum CTMCs are specified by continuous stochastic logic (CSL), which isfamous for verifying real-time systems, including classical CTMCs. The core ofchecking the CSL formulas lies in tackling multiphase until formulas. Wedevelop an algebraic method using proper projection, matrix exponentiation, anddefinite integration to symbolically calculate the probability measures of pathformulas. Thus the decidability of CSL is established. To be efficient,numerical methods are incorporated to guarantee that the time complexity ispolynomial in the encoding size of the input model and linear in the size ofthe input formula. A running example of Apollonian networks is further providedto demonstrate our method.

Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains