DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.38

Progress, Justness and Fairness in Modal μ-Calculus Formulae

Authors: Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

When verifying liveness properties on a transition system, it is often necessary to discard spurious violating paths by making assumptions on which paths represent realistic executions. Capturing that some property holds under such an assumption in a logical formula is challenging and error-prone, particularly in the modal μ-calculus. In this paper, we present template formulae in the modal μ-calculus that can be instantiated to a broad range of liveness properties. We consider the following assumptions: progress, justness, weak fairness, strong fairness, and hyperfairness, each with respect to actions. The correctness of these formulae has been proven.

Cite as

Myrthe S. C. Spronck, Bas Luttik, and Tim A. C. Willemse. Progress, Justness and Fairness in Modal μ-Calculus Formulae. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 38:1-38:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{spronck_et_al:LIPIcs.CONCUR.2024.38,
  author =	{Spronck, Myrthe S. C. and Luttik, Bas and Willemse, Tim A. C.},
  title =	{{Progress, Justness and Fairness in Modal \mu-Calculus Formulae}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{38:1--38:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak 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.CONCUR.2024.38},
  URN =		{urn:nbn:de:0030-drops-208102},
  doi =		{10.4230/LIPIcs.CONCUR.2024.38},
  annote =	{Keywords: Modal \mu-calculus, Property specification, Completeness criteria, Progress, Justness, Fairness, Liveness properties}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2023.5

Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers

Authors: Myrthe S. C. Spronck and Bas Luttik

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract

We present process-algebraic models of multi-writer multi-reader safe, regular and atomic registers. We establish the relationship between our models and alternative versions presented in the literature. We use our models to formally analyse by model checking to what extent several well-known mutual exclusion algorithms are robust for relaxed atomicity requirements. Our analyses refute correctness claims made about some of these algorithms in the literature.

Cite as

Myrthe S. C. Spronck and Bas Luttik. Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{spronck_et_al:LIPIcs.CONCUR.2023.5,
  author =	{Spronck, Myrthe S. C. and Luttik, Bas},
  title =	{{Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.5},
  URN =		{urn:nbn:de:0030-drops-189995},
  doi =		{10.4230/LIPIcs.CONCUR.2023.5},
  annote =	{Keywords: mutual exclusion, model checking, non-atomic reads and writes, regular register}
}

Search Results

Documents authored by Spronck, Myrthe S. C.

Progress, Justness and Fairness in Modal μ-Calculus Formulae

Abstract

Cite as

Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers

Abstract

Cite as

Thanks for your feedback!

Could not send message