Search Results

Documents authored by Turrini, Andrea

Document
DOI: 10.4230/LIPIcs.CONCUR.2017.35
Model Checking Omega-regular Properties for Quantum Markov Chains

Authors: Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking omega-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking omega-regular properties for quantum Markov chains.
Cite as

Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying. Model Checking Omega-regular Properties for Quantum Markov Chains. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{feng_et_al:LIPIcs.CONCUR.2017.35,
  author =	{Feng, Yuan and Hahn, Ernst Moritz and Turrini, Andrea and Ying, Shenggang},
  title =	{{Model Checking Omega-regular Properties for Quantum Markov Chains}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.35},
  URN =		{urn:nbn:de:0030-drops-77818},
  doi =		{10.4230/LIPIcs.CONCUR.2017.35},
  annote =	{Keywords: Quantum Markov chains, model checking, omega-regular properties, bottom strongly connected component}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.354
Lazy Probabilistic Model Checking without Determinisation

Authors: Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach - both explicit and symbolic versions - in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.
Cite as

Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy Probabilistic Model Checking without Determinisation. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 354-367, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hahn_et_al:LIPIcs.CONCUR.2015.354,
  author =	{Hahn, Ernst Moritz and Li, Guangyuan and Schewe, Sven and Turrini, Andrea and Zhang, Lijun},
  title =	{{Lazy Probabilistic Model Checking without Determinisation}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{354--367},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.354},
  URN =		{urn:nbn:de:0030-drops-53918},
  doi =		{10.4230/LIPIcs.CONCUR.2015.354},
  annote =	{Keywords: Markov decision processes, model checking, PLTL, determinisation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.435
Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time

Authors: Holger Hermanns and Andrea Turrini

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
Deciding in an efficient way weak probabilistic bisimulation in the context of probabilistic automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. This enables us to arrive at a polynomial time algorithm for deciding weak probabilistic bisimulation. We also present several extensions to interesting related problems setting the ground for the development of more effective and compositional analysis algorithms for probabilistic systems.
Cite as

Holger Hermanns and Andrea Turrini. Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 435-447, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{hermanns_et_al:LIPIcs.FSTTCS.2012.435,
  author =	{Hermanns, Holger and Turrini, Andrea},
  title =	{{Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{435--447},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.435},
  URN =		{urn:nbn:de:0030-drops-38794},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.435},
  annote =	{Keywords: Probabilistic Automata, Weak probabilsitic bisimulation, Linear Programming problem, Polynomial decision algorithm}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact