Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains Article Swipe
Jingyi Mei
,
Ming Xu
,
Ji Guan
,
Yuxin Deng
,
Nengkun Yu
·
YOU?
·
· 2025
· Open Access
·
· DOI: https://doi.org/10.46298/lmcs-21(4:22)2025
YOU?
·
· 2025
· Open Access
·
· DOI: https://doi.org/10.46298/lmcs-21(4:22)2025
Verifying quantum systems has attracted a lot of interest in the last decades.In this paper, we study the quantitative model-checking of quantum continuous-time Markov chains (quantum CTMCs). The branching-time properties of quantum CTMCs are specified by continuous stochastic logic (CSL), which is well-known for verifying real-time systems, including classical CTMCs. The core of checking the CSL formulas lies in tackling multiphase until formulas. We develop an algebraic method using proper projection, matrix exponentiation, and definite integration to symbolically calculate the probability measures of path formulas. Thus the decidability of CSL is established. To be efficient, numerical methods are incorporated to guarantee that the time complexity is polynomial in the encoding size of the input model and linear in the size of the input formula. A running example of Apollonian networks is further provided to demonstrate our method.
Related Topics
Concepts
Metadata
- Type
- preprint
- Language
- en
- Landing Page
- https://doi.org/10.46298/lmcs-21(4:22)2025
- https://lmcs.episciences.org/16897/pdf
- OA Status
- diamond
- Cited By
- 1
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W4221143203
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W4221143203Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.46298/lmcs-21(4:22)2025Digital Object Identifier
- Title
-
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov ChainsWork title
- Type
-
preprintOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2025Year of publication
- Publication date
-
2025-11-11Full publication date if available
- Authors
-
Jingyi Mei, Ming Xu, Ji Guan, Yuxin Deng, Nengkun YuList of authors in order
- Landing page
-
https://doi.org/10.46298/lmcs-21(4:22)2025Publisher landing page
- PDF URL
-
https://lmcs.episciences.org/16897/pdfDirect link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
diamondOpen access status per OpenAlex
- OA URL
-
https://lmcs.episciences.org/16897/pdfDirect OA link when available
- Concepts
-
Markov chain, Model checking, Computer science, Time complexity, Algebraic number, Algorithm, Mathematics, Discrete mathematics, Mathematical analysis, Machine learningTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
1Total citation count in OpenAlex
- Citations by year (recent)
-
2022: 1Per-year citation counts (last 5 years)
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W4221143203 |
|---|---|
| doi | https://doi.org/10.46298/lmcs-21(4:22)2025 |
| ids.doi | https://doi.org/10.48550/arxiv.2202.05412 |
| ids.openalex | https://openalex.org/W4221143203 |
| fwci | 0.0 |
| type | preprint |
| title | Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains |
| biblio.issue | |
| biblio.volume | Volume 21, Issue 4 |
| biblio.last_page | |
| biblio.first_page | |
| topics[0].id | https://openalex.org/T10142 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9994000196456909 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1703 |
| topics[0].subfield.display_name | Computational Theory and Mathematics |
| topics[0].display_name | Formal Methods in Verification |
| topics[1].id | https://openalex.org/T11005 |
| topics[1].field.id | https://openalex.org/fields/22 |
| topics[1].field.display_name | Engineering |
| topics[1].score | 0.9858999848365784 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/2208 |
| topics[1].subfield.display_name | Electrical and Electronic Engineering |
| topics[1].display_name | Radiation Effects in Electronics |
| topics[2].id | https://openalex.org/T10363 |
| topics[2].field.id | https://openalex.org/fields/22 |
| topics[2].field.display_name | Engineering |
| topics[2].score | 0.9847999811172485 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/2208 |
| topics[2].subfield.display_name | Electrical and Electronic Engineering |
| topics[2].display_name | Low-power high-performance VLSI design |
| is_xpac | False |
| apc_list | |
| apc_paid | |
| concepts[0].id | https://openalex.org/C98763669 |
| concepts[0].level | 2 |
| concepts[0].score | 0.6069112420082092 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q176645 |
| concepts[0].display_name | Markov chain |
| concepts[1].id | https://openalex.org/C110251889 |
| concepts[1].level | 2 |
| concepts[1].score | 0.5144493579864502 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q1569697 |
| concepts[1].display_name | Model checking |
| concepts[2].id | https://openalex.org/C41008148 |
| concepts[2].level | 0 |
| concepts[2].score | 0.5060972571372986 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[2].display_name | Computer science |
| concepts[3].id | https://openalex.org/C311688 |
| concepts[3].level | 2 |
| concepts[3].score | 0.42624929547309875 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q2393193 |
| concepts[3].display_name | Time complexity |
| concepts[4].id | https://openalex.org/C9376300 |
| concepts[4].level | 2 |
| concepts[4].score | 0.4173060357570648 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q168817 |
| concepts[4].display_name | Algebraic number |
| concepts[5].id | https://openalex.org/C11413529 |
| concepts[5].level | 1 |
| concepts[5].score | 0.40757033228874207 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q8366 |
| concepts[5].display_name | Algorithm |
| concepts[6].id | https://openalex.org/C33923547 |
| concepts[6].level | 0 |
| concepts[6].score | 0.37037307024002075 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q395 |
| concepts[6].display_name | Mathematics |
| concepts[7].id | https://openalex.org/C118615104 |
| concepts[7].level | 1 |
| concepts[7].score | 0.3387913703918457 |
| concepts[7].wikidata | https://www.wikidata.org/wiki/Q121416 |
| concepts[7].display_name | Discrete mathematics |
| concepts[8].id | https://openalex.org/C134306372 |
| concepts[8].level | 1 |
| concepts[8].score | 0.0 |
| concepts[8].wikidata | https://www.wikidata.org/wiki/Q7754 |
| concepts[8].display_name | Mathematical analysis |
| concepts[9].id | https://openalex.org/C119857082 |
| concepts[9].level | 1 |
| concepts[9].score | 0.0 |
| concepts[9].wikidata | https://www.wikidata.org/wiki/Q2539 |
| concepts[9].display_name | Machine learning |
| keywords[0].id | https://openalex.org/keywords/markov-chain |
| keywords[0].score | 0.6069112420082092 |
| keywords[0].display_name | Markov chain |
| keywords[1].id | https://openalex.org/keywords/model-checking |
| keywords[1].score | 0.5144493579864502 |
| keywords[1].display_name | Model checking |
| keywords[2].id | https://openalex.org/keywords/computer-science |
| keywords[2].score | 0.5060972571372986 |
| keywords[2].display_name | Computer science |
| keywords[3].id | https://openalex.org/keywords/time-complexity |
| keywords[3].score | 0.42624929547309875 |
| keywords[3].display_name | Time complexity |
| keywords[4].id | https://openalex.org/keywords/algebraic-number |
| keywords[4].score | 0.4173060357570648 |
| keywords[4].display_name | Algebraic number |
| keywords[5].id | https://openalex.org/keywords/algorithm |
| keywords[5].score | 0.40757033228874207 |
| keywords[5].display_name | Algorithm |
| keywords[6].id | https://openalex.org/keywords/mathematics |
| keywords[6].score | 0.37037307024002075 |
| keywords[6].display_name | Mathematics |
| keywords[7].id | https://openalex.org/keywords/discrete-mathematics |
| keywords[7].score | 0.3387913703918457 |
| keywords[7].display_name | Discrete mathematics |
| language | en |
| locations[0].id | doi:10.46298/lmcs-21(4:22)2025 |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S114379355 |
| locations[0].source.issn | 1860-5974 |
| locations[0].source.type | journal |
| locations[0].source.is_oa | True |
| locations[0].source.issn_l | 1860-5974 |
| locations[0].source.is_core | True |
| locations[0].source.is_in_doaj | True |
| locations[0].source.display_name | Logical Methods in Computer Science |
| locations[0].source.host_organization | https://openalex.org/P4310313916 |
| locations[0].source.host_organization_name | Logical Methods in Computer Science e.V. |
| locations[0].source.host_organization_lineage | https://openalex.org/P4310313916 |
| locations[0].source.host_organization_lineage_names | Logical Methods in Computer Science e.V. |
| locations[0].license | cc-by |
| locations[0].pdf_url | https://lmcs.episciences.org/16897/pdf |
| locations[0].version | publishedVersion |
| locations[0].raw_type | journal-article |
| locations[0].license_id | https://openalex.org/licenses/cc-by |
| locations[0].is_accepted | True |
| locations[0].is_published | True |
| locations[0].raw_source_name | Logical Methods in Computer Science |
| locations[0].landing_page_url | https://doi.org/10.46298/lmcs-21(4:22)2025 |
| locations[1].id | pmh:oai:arXiv.org:2202.05412 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306400194 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | True |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | arXiv (Cornell University) |
| locations[1].source.host_organization | https://openalex.org/I205783295 |
| locations[1].source.host_organization_name | Cornell University |
| locations[1].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[1].license | |
| locations[1].pdf_url | https://arxiv.org/pdf/2202.05412 |
| locations[1].version | submittedVersion |
| locations[1].raw_type | text |
| locations[1].license_id | |
| locations[1].is_accepted | False |
| locations[1].is_published | False |
| locations[1].raw_source_name | |
| locations[1].landing_page_url | http://arxiv.org/abs/2202.05412 |
| locations[2].id | doi:10.48550/arxiv.2202.05412 |
| locations[2].is_oa | True |
| locations[2].source.id | https://openalex.org/S4306400194 |
| locations[2].source.issn | |
| locations[2].source.type | repository |
| locations[2].source.is_oa | True |
| locations[2].source.issn_l | |
| locations[2].source.is_core | False |
| locations[2].source.is_in_doaj | False |
| locations[2].source.display_name | arXiv (Cornell University) |
| locations[2].source.host_organization | https://openalex.org/I205783295 |
| locations[2].source.host_organization_name | Cornell University |
| locations[2].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[2].license | cc-by |
| locations[2].pdf_url | |
| locations[2].version | |
| locations[2].raw_type | article |
| locations[2].license_id | https://openalex.org/licenses/cc-by |
| locations[2].is_accepted | False |
| locations[2].is_published | |
| locations[2].raw_source_name | |
| locations[2].landing_page_url | https://doi.org/10.48550/arxiv.2202.05412 |
| indexed_in | arxiv, crossref, datacite, doaj |
| authorships[0].author.id | https://openalex.org/A5071969266 |
| authorships[0].author.orcid | https://orcid.org/0000-0002-4665-9818 |
| authorships[0].author.display_name | Jingyi Mei |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Mei, Jingyi |
| authorships[0].is_corresponding | False |
| authorships[1].author.id | https://openalex.org/A5060776618 |
| authorships[1].author.orcid | https://orcid.org/0000-0002-9906-5677 |
| authorships[1].author.display_name | Ming Xu |
| authorships[1].author_position | middle |
| authorships[1].raw_author_name | Xu, Ming |
| authorships[1].is_corresponding | False |
| authorships[2].author.id | https://openalex.org/A5081435269 |
| authorships[2].author.orcid | https://orcid.org/0000-0002-3490-0029 |
| authorships[2].author.display_name | Ji Guan |
| authorships[2].author_position | middle |
| authorships[2].raw_author_name | Guan, Ji |
| authorships[2].is_corresponding | False |
| authorships[3].author.id | https://openalex.org/A5022036342 |
| authorships[3].author.orcid | https://orcid.org/0000-0003-0753-418X |
| authorships[3].author.display_name | Yuxin Deng |
| authorships[3].author_position | middle |
| authorships[3].raw_author_name | Deng, Yuxin |
| authorships[3].is_corresponding | False |
| authorships[4].author.id | https://openalex.org/A5088217238 |
| authorships[4].author.orcid | https://orcid.org/0000-0003-1188-3032 |
| authorships[4].author.display_name | Nengkun Yu |
| authorships[4].author_position | last |
| authorships[4].raw_author_name | Yu, Nengkun |
| authorships[4].is_corresponding | False |
| has_content.pdf | True |
| has_content.grobid_xml | False |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://lmcs.episciences.org/16897/pdf |
| open_access.oa_status | diamond |
| open_access.any_repository_has_fulltext | False |
| created_date | 2022-04-03T00:00:00 |
| display_name | Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-23T05:10:03.516525 |
| primary_topic.id | https://openalex.org/T10142 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9994000196456909 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1703 |
| primary_topic.subfield.display_name | Computational Theory and Mathematics |
| primary_topic.display_name | Formal Methods in Verification |
| related_works | https://openalex.org/W4391375266, https://openalex.org/W1538854713, https://openalex.org/W4235160909, https://openalex.org/W1660242800, https://openalex.org/W2041209185, https://openalex.org/W1484021165, https://openalex.org/W3021865842, https://openalex.org/W1519201794, https://openalex.org/W1629505938, https://openalex.org/W2767824041 |
| cited_by_count | 1 |
| counts_by_year[0].year | 2022 |
| counts_by_year[0].cited_by_count | 1 |
| locations_count | 3 |
| best_oa_location.id | doi:10.46298/lmcs-21(4:22)2025 |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S114379355 |
| best_oa_location.source.issn | 1860-5974 |
| best_oa_location.source.type | journal |
| best_oa_location.source.is_oa | True |
| best_oa_location.source.issn_l | 1860-5974 |
| best_oa_location.source.is_core | True |
| best_oa_location.source.is_in_doaj | True |
| best_oa_location.source.display_name | Logical Methods in Computer Science |
| best_oa_location.source.host_organization | https://openalex.org/P4310313916 |
| best_oa_location.source.host_organization_name | Logical Methods in Computer Science e.V. |
| best_oa_location.source.host_organization_lineage | https://openalex.org/P4310313916 |
| best_oa_location.source.host_organization_lineage_names | Logical Methods in Computer Science e.V. |
| best_oa_location.license | cc-by |
| best_oa_location.pdf_url | https://lmcs.episciences.org/16897/pdf |
| best_oa_location.version | publishedVersion |
| best_oa_location.raw_type | journal-article |
| best_oa_location.license_id | https://openalex.org/licenses/cc-by |
| best_oa_location.is_accepted | True |
| best_oa_location.is_published | True |
| best_oa_location.raw_source_name | Logical Methods in Computer Science |
| best_oa_location.landing_page_url | https://doi.org/10.46298/lmcs-21(4:22)2025 |
| primary_location.id | doi:10.46298/lmcs-21(4:22)2025 |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S114379355 |
| primary_location.source.issn | 1860-5974 |
| primary_location.source.type | journal |
| primary_location.source.is_oa | True |
| primary_location.source.issn_l | 1860-5974 |
| primary_location.source.is_core | True |
| primary_location.source.is_in_doaj | True |
| primary_location.source.display_name | Logical Methods in Computer Science |
| primary_location.source.host_organization | https://openalex.org/P4310313916 |
| primary_location.source.host_organization_name | Logical Methods in Computer Science e.V. |
| primary_location.source.host_organization_lineage | https://openalex.org/P4310313916 |
| primary_location.source.host_organization_lineage_names | Logical Methods in Computer Science e.V. |
| primary_location.license | cc-by |
| primary_location.pdf_url | https://lmcs.episciences.org/16897/pdf |
| primary_location.version | publishedVersion |
| primary_location.raw_type | journal-article |
| primary_location.license_id | https://openalex.org/licenses/cc-by |
| primary_location.is_accepted | True |
| primary_location.is_published | True |
| primary_location.raw_source_name | Logical Methods in Computer Science |
| primary_location.landing_page_url | https://doi.org/10.46298/lmcs-21(4:22)2025 |
| publication_date | 2025-11-11 |
| publication_year | 2025 |
| referenced_works_count | 0 |
| abstract_inverted_index.A | 124 |
| abstract_inverted_index.a | 5 |
| abstract_inverted_index.To | 92 |
| abstract_inverted_index.We | 63 |
| abstract_inverted_index.an | 65 |
| abstract_inverted_index.be | 93 |
| abstract_inverted_index.by | 35 |
| abstract_inverted_index.in | 9, 58, 107, 117 |
| abstract_inverted_index.is | 41, 90, 105, 130 |
| abstract_inverted_index.of | 7, 20, 30, 52, 82, 88, 111, 120, 127 |
| abstract_inverted_index.to | 76, 99, 133 |
| abstract_inverted_index.we | 15 |
| abstract_inverted_index.CSL | 55, 89 |
| abstract_inverted_index.The | 27, 50 |
| abstract_inverted_index.and | 73, 115 |
| abstract_inverted_index.are | 33, 97 |
| abstract_inverted_index.for | 43 |
| abstract_inverted_index.has | 3 |
| abstract_inverted_index.lot | 6 |
| abstract_inverted_index.our | 135 |
| abstract_inverted_index.the | 10, 17, 54, 79, 86, 102, 108, 112, 118, 121 |
| abstract_inverted_index.Thus | 85 |
| abstract_inverted_index.core | 51 |
| abstract_inverted_index.last | 11 |
| abstract_inverted_index.lies | 57 |
| abstract_inverted_index.path | 83 |
| abstract_inverted_index.size | 110, 119 |
| abstract_inverted_index.that | 101 |
| abstract_inverted_index.this | 13 |
| abstract_inverted_index.time | 103 |
| abstract_inverted_index.CTMCs | 32 |
| abstract_inverted_index.input | 113, 122 |
| abstract_inverted_index.logic | 38 |
| abstract_inverted_index.model | 114 |
| abstract_inverted_index.study | 16 |
| abstract_inverted_index.until | 61 |
| abstract_inverted_index.using | 68 |
| abstract_inverted_index.which | 40 |
| abstract_inverted_index.(CSL), | 39 |
| abstract_inverted_index.CTMCs. | 49 |
| abstract_inverted_index.Markov | 23 |
| abstract_inverted_index.chains | 24 |
| abstract_inverted_index.linear | 116 |
| abstract_inverted_index.matrix | 71 |
| abstract_inverted_index.method | 67 |
| abstract_inverted_index.paper, | 14 |
| abstract_inverted_index.proper | 69 |
| abstract_inverted_index.CTMCs). | 26 |
| abstract_inverted_index.develop | 64 |
| abstract_inverted_index.example | 126 |
| abstract_inverted_index.further | 131 |
| abstract_inverted_index.method. | 136 |
| abstract_inverted_index.methods | 96 |
| abstract_inverted_index.quantum | 1, 21, 31 |
| abstract_inverted_index.running | 125 |
| abstract_inverted_index.systems | 2 |
| abstract_inverted_index.(quantum | 25 |
| abstract_inverted_index.checking | 53 |
| abstract_inverted_index.definite | 74 |
| abstract_inverted_index.encoding | 109 |
| abstract_inverted_index.formula. | 123 |
| abstract_inverted_index.formulas | 56 |
| abstract_inverted_index.interest | 8 |
| abstract_inverted_index.measures | 81 |
| abstract_inverted_index.networks | 129 |
| abstract_inverted_index.provided | 132 |
| abstract_inverted_index.systems, | 46 |
| abstract_inverted_index.tackling | 59 |
| abstract_inverted_index.Verifying | 0 |
| abstract_inverted_index.algebraic | 66 |
| abstract_inverted_index.attracted | 4 |
| abstract_inverted_index.calculate | 78 |
| abstract_inverted_index.classical | 48 |
| abstract_inverted_index.formulas. | 62, 84 |
| abstract_inverted_index.guarantee | 100 |
| abstract_inverted_index.including | 47 |
| abstract_inverted_index.numerical | 95 |
| abstract_inverted_index.real-time | 45 |
| abstract_inverted_index.specified | 34 |
| abstract_inverted_index.verifying | 44 |
| abstract_inverted_index.Apollonian | 128 |
| abstract_inverted_index.complexity | 104 |
| abstract_inverted_index.continuous | 36 |
| abstract_inverted_index.decades.In | 12 |
| abstract_inverted_index.efficient, | 94 |
| abstract_inverted_index.multiphase | 60 |
| abstract_inverted_index.polynomial | 106 |
| abstract_inverted_index.properties | 29 |
| abstract_inverted_index.stochastic | 37 |
| abstract_inverted_index.well-known | 42 |
| abstract_inverted_index.demonstrate | 134 |
| abstract_inverted_index.integration | 75 |
| abstract_inverted_index.probability | 80 |
| abstract_inverted_index.projection, | 70 |
| abstract_inverted_index.decidability | 87 |
| abstract_inverted_index.established. | 91 |
| abstract_inverted_index.incorporated | 98 |
| abstract_inverted_index.quantitative | 18 |
| abstract_inverted_index.symbolically | 77 |
| abstract_inverted_index.branching-time | 28 |
| abstract_inverted_index.model-checking | 19 |
| abstract_inverted_index.continuous-time | 22 |
| abstract_inverted_index.exponentiation, | 72 |
| cited_by_percentile_year.max | 94 |
| cited_by_percentile_year.min | 89 |
| countries_distinct_count | 0 |
| institutions_distinct_count | 5 |
| citation_normalized_percentile.value | 0.00286399 |
| citation_normalized_percentile.is_in_top_1_percent | False |
| citation_normalized_percentile.is_in_top_10_percent | False |