Abstract
We propose a discrete time quantum Markov chain (QMC) related to previous proposals but yet with a different semantics.
A probability measure is defined similar to as for DTMCs in contrast to e.g.\ the super operator valued measure.
Our work is based on a simple imperative quantum pseudo programming language and its denotational semantics which naturally leads to a definition of a QMC.
As a novelty we demonstrate how reachability events of a QMC expressed in a simple temporal logic like notation may be checked similar to as
for DTMCs as transient state probabilities and how probability intervals of such events may be computed by smallest fixed-point solutions to linear equations.
A probability measure is defined similar to as for DTMCs in contrast to e.g.\ the super operator valued measure.
Our work is based on a simple imperative quantum pseudo programming language and its denotational semantics which naturally leads to a definition of a QMC.
As a novelty we demonstrate how reachability events of a QMC expressed in a simple temporal logic like notation may be checked similar to as
for DTMCs as transient state probabilities and how probability intervals of such events may be computed by smallest fixed-point solutions to linear equations.
| Originalsprog | Dansk |
|---|---|
| Publikationsdato | aug. 2025 |
| Antal sider | 20 |
| Status | Udgivet - aug. 2025 |
| Begivenhed | Formal Methods for Quantum Computing 2025 - Aarhus Universitet, Aarhus , Danmark Varighed: 25 aug. 2025 → 25 aug. 2025 Konferencens nummer: 1 https://fmqc-workshop.github.io/2025 |
Workshop
| Workshop | Formal Methods for Quantum Computing 2025 |
|---|---|
| Nummer | 1 |
| Lokation | Aarhus Universitet |
| Land/Område | Danmark |
| By | Aarhus |
| Periode | 25/08/2025 → 25/08/2025 |
| Internetadresse |
Emneord
- Quantum Markov Chains
- Reachability Properties
- Model Checking