Search Results

Documents authored by Parker, David

Artifact
Software
DOI: 10.4230/artifacts.27642
PRISM extension for deciding continuity of the probabilistic bisimilarity distance

Authors: Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel

Abstract
Cite as

Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, Franck van Breugel. PRISM extension for deciding continuity of the probabilistic bisimilarity distance (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27642,
   title = {{PRISM extension for deciding continuity of the probabilistic bisimilarity distance}}, 
   author = {Fatmi, Syyeda Zainab and Kiefer, Stefan and Parker, David and van Breugel, Franck},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:4efb0e4307476e883191835aed030dce0af9782c;origin=https://github.com/zainabfatmi/prism;visit=swh:1:snp:560420628621f81a7b83012aca7d95153508ac19;anchor=swh:1:rev:9486c774830b78b6ad0e491e0b56d6082d660cb7}{\texttt{swh:1:dir:4efb0e4307476e883191835aed030dce0af9782c}} (visited on 2026-08-24)},
   url = {https://github.com/zainabfatmi/prism/tree/concur},
   doi = {10.4230/artifacts.27642},
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2026.34
On the Continuity of the Probabilistic Bisimilarity Distance

Authors: Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract
The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity undermines its applicability to empirically derived models, where transition probabilities are often approximations. Recently, we introduced robust probabilistic bisimilarity as a sufficient condition for continuity at distance zero. In this paper, we show that it is also a necessary condition, that is, two states are robustly probabilistic bisimilar if and only if their probabilistic bisimilarity distance is small for any small enough perturbation of the transition probabilities. We further extend robustness to non-bisimilar state pairs to establish a complete characterization for continuity of the probabilistic bisimilarity distance. Based on this characterization, we develop a polynomial time algorithm to decide continuity. Finally, we complement our theoretical contributions with an experimental evaluation demonstrating the proposed approach in practice. Our results show that the extra step of deciding continuity requires minimal additional cost when compared to computing the probabilistic bisimilarity distance.
Cite as

Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel. On the Continuity of the Probabilistic Bisimilarity Distance. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fatmi_et_al:LIPIcs.CONCUR.2026.34,
  author =	{Fatmi, Syyeda Zainab and Kiefer, Stefan and Parker, David and van Breugel, Franck},
  title =	{{On the Continuity of the Probabilistic Bisimilarity Distance}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{34:1--34:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.34},
  URN =		{urn:nbn:de:0030-drops-273648},
  doi =		{10.4230/LIPIcs.CONCUR.2026.34},
  annote =	{Keywords: probabilistic model checking, labelled Markov chain, probabilistic bisimilarity distance}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.4
Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk)

Authors: Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined.
Cite as

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan. Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska_et_al:LIPIcs.MFCS.2022.4,
  author =	{Kwiatkowska, Marta and Norman, Gethin and Parker, David and Santos, Gabriel and Yan, Rui},
  title =	{{Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.4},
  URN =		{urn:nbn:de:0030-drops-168026},
  doi =		{10.4230/LIPIcs.MFCS.2022.4},
  annote =	{Keywords: Probabilistic model checking, stochastic games, equilibria}
}

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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