DROPS

Artifact

Software

SiRop

Authors: Éléanore Meyer, Jürgen Giesl, and Sophia Greiwe

Abstract

Cite as

Éléanore Meyer, Jürgen Giesl, Sophia Greiwe. SiRop (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24333,
   title = {{SiRop}}, 
   author = {Meyer, \'{E}l\'{e}anore and Giesl, J\"{u}rgen and Greiwe, Sophia},
   note = {Software, DFG-Research Training Group 2236 UnRAVeL, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:3ca664cebef79bfeb95ec944ddc8441d3b528bf6;origin=https://github.com/aprove-developers/SiRop;visit=swh:1:snp:51bec07ab5b5061e7a0cf5e251adcc2ce0cc1986;anchor=swh:1:rev:d15dac241fed869ede4ad1c432f547a6c3c70b68}{\texttt{swh:1:dir:3ca664cebef79bfeb95ec944ddc8441d3b528bf6}} (visited on 2025-08-20)},
   url = {https://github.com/aprove-developers/SiRop},
   doi = {10.4230/artifacts.24333},
}

Document

DOI: 10.4230/LIPIcs.MFCS.2025.76

Deciding Termination of Simple Randomized Loops

Authors: Éléanore Meyer and Jürgen Giesl

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract

We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a program is finite for all inputs. Our class contains all programs that consist of a single loop, with a linear loop guard and a loop body composed of two linear commuting and diagonalizable updates. In each iteration of the loop, the update to be carried out is picked at random, according to a fixed probability. We show the decidability of UPAST for this class of programs, where the program’s variables and inputs may range over various sub-semirings of the real numbers. In this way, we extend a line of research initiated by Tiwari in 2004 into the realm of randomized programs.

Cite as

Éléanore Meyer and Jürgen Giesl. Deciding Termination of Simple Randomized Loops. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 76:1-76:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.MFCS.2025.76,
  author =	{Meyer, \'{E}l\'{e}anore and Giesl, J\"{u}rgen},
  title =	{{Deciding Termination of Simple Randomized Loops}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{76:1--76:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.76},
  URN =		{urn:nbn:de:0030-drops-241833},
  doi =		{10.4230/LIPIcs.MFCS.2025.76},
  annote =	{Keywords: decision procedures, randomized programs, linear loops, positive almost sure termination}
}

Search Results

Documents authored by Meyer, Éléanore

SiRop

Abstract

Cite as

Deciding Termination of Simple Randomized Loops

Abstract

Cite as

Thanks for your feedback!

Could not send message