56 Search Results for "Kov�cs, Laura"

Document
DOI: 10.4230/LIPIcs.STACS.2024.41
Linear Loop Synthesis for Quadratic Invariants

Authors: S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.
Cite as

S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hitarth_et_al:LIPIcs.STACS.2024.41,
  author =	{Hitarth, S. and Kenison, George and Kov\'{a}cs, Laura and Varonka, Anton},
  title =	{{Linear Loop Synthesis for Quadratic Invariants}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.41},
  URN =		{urn:nbn:de:0030-drops-197512},
  doi =		{10.4230/LIPIcs.STACS.2024.41},
  annote =	{Keywords: program synthesis, loop invariants, verification, Diophantine equations}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2020
LIPIcs, Volume 171, CONCUR 2020, Complete Volume

Authors: Igor Konnov and Laura Kovács

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
LIPIcs, Volume 171, CONCUR 2020, Complete Volume
Cite as

31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 1-984, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{konnov_et_al:LIPIcs.CONCUR.2020,
  title =	{{LIPIcs, Volume 171, CONCUR 2020, Complete Volume}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{1--984},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020},
  URN =		{urn:nbn:de:0030-drops-128115},
  doi =		{10.4230/LIPIcs.CONCUR.2020},
  annote =	{Keywords: LIPIcs, Volume 171, CONCUR 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Igor Konnov and Laura Kovács

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{konnov_et_al:LIPIcs.CONCUR.2020.0,
  author =	{Konnov, Igor and Kov\'{a}cs, Laura},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.0},
  URN =		{urn:nbn:de:0030-drops-128125},
  doi =		{10.4230/LIPIcs.CONCUR.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.1
On Privacy and Accuracy in Data Releases (Invited Paper)

Authors: Mário S. Alvim, Natasha Fernandes, Annabelle McIver, and Gabriel H. Nunes

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
In this paper we study the relationship between privacy and accuracy in the context of correlated datasets. We use a model of quantitative information flow to describe the the trade-off between privacy of individuals' data and and the utility of queries to that data by modelling the effectiveness of adversaries attempting to make inferences after a data release. We show that, where correlations exist in datasets, it is not possible to implement optimal noise-adding mechanisms that give the best possible accuracy or the best possible privacy in all situations. Finally we illustrate the trade-off between accuracy and privacy for local and oblivious differentially private mechanisms in terms of inference attacks on medium-scale datasets.
Cite as

Mário S. Alvim, Natasha Fernandes, Annabelle McIver, and Gabriel H. Nunes. On Privacy and Accuracy in Data Releases (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{alvim_et_al:LIPIcs.CONCUR.2020.1,
  author =	{Alvim, M\'{a}rio S. and Fernandes, Natasha and McIver, Annabelle and Nunes, Gabriel H.},
  title =	{{On Privacy and Accuracy in Data Releases}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{1:1--1:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.1},
  URN =		{urn:nbn:de:0030-drops-128130},
  doi =		{10.4230/LIPIcs.CONCUR.2020.1},
  annote =	{Keywords: Privacy/utility trade-off, Quantitative Information Flow, inference attacks}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.2
A Survey of Bidding Games on Graphs (Invited Paper)

Authors: Guy Avni and Thomas A. Henzinger

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
Cite as

Guy Avni and Thomas A. Henzinger. A Survey of Bidding Games on Graphs (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.CONCUR.2020.2,
  author =	{Avni, Guy and Henzinger, Thomas A.},
  title =	{{A Survey of Bidding Games on Graphs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.2},
  URN =		{urn:nbn:de:0030-drops-128147},
  doi =		{10.4230/LIPIcs.CONCUR.2020.2},
  annote =	{Keywords: Bidding games, Richman bidding, poorman bidding, mean-payoff, parity}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.3
Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper)

Authors: Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This paper concerns the efficient construction of a safety shield for reinforcement learning. We specifically target scenarios that incorporate uncertainty and use Markov decision processes (MDPs) as the underlying model to capture such problems. Reinforcement learning (RL) is a machine learning technique that can determine near-optimal policies in MDPs that may be unknown before exploring the model. However, during exploration, RL is prone to induce behavior that is undesirable or not allowed in safety- or mission-critical contexts. We introduce the concept of a probabilistic shield that enables RL decision-making to adhere to safety constraints with high probability. We employ formal verification to efficiently compute the probabilities of critical decisions within a safety-relevant fragment of the MDP. These results help to realize a shield that, when applied to an RL algorithm, restricts the agent from taking unsafe actions, while optimizing the performance objective. We discuss tradeoffs between sufficient progress in the exploration of the environment and ensuring safety. In our experiments, we demonstrate on the arcade game PAC-MAN and on a case study involving service robots that the learning efficiency increases as the learning needs orders of magnitude fewer episodes.
Cite as

Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem. Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{jansen_et_al:LIPIcs.CONCUR.2020.3,
  author =	{Jansen, Nils and K\"{o}nighofer, Bettina and Junges, Sebastian and Serban, Alex and Bloem, Roderick},
  title =	{{Safe Reinforcement Learning Using Probabilistic Shields}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{3:1--3:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.3},
  URN =		{urn:nbn:de:0030-drops-128155},
  doi =		{10.4230/LIPIcs.CONCUR.2020.3},
  annote =	{Keywords: Safe Reinforcement Learning, Formal Verification, Safe Exploration, Model Checking, Markov Decision Process}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.4
Modern Applications of Game-Theoretic Principles (Invited Paper)

Authors: Catuscia Palamidessi and Marco Romanelli

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Game theory is the study of the strategic behavior of rational decision makers who are aware that their decisions affect one another. Its simple but universal principles have found applications in the most diverse disciplines, including economics, social sciences, evolutionary biology, as well as logic, system science and computer science. Despite its long-standing tradition and its many advances, game theory is still a young and developing science. In this paper, we describe some recent and exciting applications in the fields of machine learning and privacy.
Cite as

Catuscia Palamidessi and Marco Romanelli. Modern Applications of Game-Theoretic Principles (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{palamidessi_et_al:LIPIcs.CONCUR.2020.4,
  author =	{Palamidessi, Catuscia and Romanelli, Marco},
  title =	{{Modern Applications of Game-Theoretic Principles}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{4:1--4:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.4},
  URN =		{urn:nbn:de:0030-drops-128167},
  doi =		{10.4230/LIPIcs.CONCUR.2020.4},
  annote =	{Keywords: Game theory, machine learning, privacy, security}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.5
CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper)

Authors: Luca Aceto, Jos Baeten, Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This short article announces the recipients of the CONCUR Test-of-Time Award 2020.
Cite as

Luca Aceto, Jos Baeten, Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva. CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2020.5,
  author =	{Aceto, Luca and Baeten, Jos and Bouyer-Decitre, Patricia and Hermanns, Holger and Silva, Alexandra},
  title =	{{CONCUR Test-Of-Time Award 2020 Announcement}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{5:1--5:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.5},
  URN =		{urn:nbn:de:0030-drops-128172},
  doi =		{10.4230/LIPIcs.CONCUR.2020.5},
  annote =	{Keywords: Concurrency, CONCUR Test-of-Time Award}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.6
Reactive Bisimulation Semantics for a Process Algebra with Time-Outs

Authors: Rob van Glabbeek

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.
Cite as

Rob van Glabbeek. Reactive Bisimulation Semantics for a Process Algebra with Time-Outs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{vanglabbeek:LIPIcs.CONCUR.2020.6,
  author =	{van Glabbeek, Rob},
  title =	{{Reactive Bisimulation Semantics for a Process Algebra with Time-Outs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.6},
  URN =		{urn:nbn:de:0030-drops-128181},
  doi =		{10.4230/LIPIcs.CONCUR.2020.6},
  annote =	{Keywords: Process algebra, time-outs, labelled transition systems, reactive bisimulation semantics, Hennessy-Milner logic, modal characterisations, recursion, complete axiomatisations}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.7
How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation

Authors: Clément Aubert and Ioana Cristescu

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Reversible computation opens up the possibility of overcoming some of the hardware’s current physical limitations. It also offers theoretical insights, as it enriches multiple paradigms and models of computation, and sometimes retrospectively enlightens them. Concurrent reversible computation, for instance, offered interesting extensions to the Calculus of Communicating Systems, but was still lacking a natural and pertinent bisimulation to study processes equivalences. Our paper formulates an equivalence exploiting the two aspects of reversibility: backward moves and memory mechanisms. This bisimulation captures classical equivalences relations for denotational models of concurrency (history- and hereditary history-preserving bisimulation, (H)HPB), that were up to now only partially characterized by process algebras. This result gives an insight on the expressiveness of reversibility, as both backward moves and a memory mechanism - providing "backward determinism" - are needed to capture HHPB.
Cite as

Clément Aubert and Ioana Cristescu. How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aubert_et_al:LIPIcs.CONCUR.2020.7,
  author =	{Aubert, Cl\'{e}ment and Cristescu, Ioana},
  title =	{{How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.7},
  URN =		{urn:nbn:de:0030-drops-128196},
  doi =		{10.4230/LIPIcs.CONCUR.2020.7},
  annote =	{Keywords: Formal semantics, Process algebras and calculi, Distributed and reversible computation, Configuration structures, Reversible CCS, Bisimulation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.8
A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains

Authors: David N. Jansen, Jan Friso Groote, Ferry Timmers, and Pengfei Yang

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This article improves the time bound for calculating the weak/branching bisimulation minimisation quotient on state-labelled discrete-time Markov chains from O(m n) to an expected-time O(m log⁴ n), where n is the number of states and m the number of transitions. For these results we assume that the set of state labels AP is small (|AP| ∈ O(m/n log⁴ n)). It follows the ideas of Groote et al. (ACM ToCL 2017) in combination with an efficient algorithm to handle decremental strongly connected components (Bernstein et al., STOC 2019).
Cite as

David N. Jansen, Jan Friso Groote, Ferry Timmers, and Pengfei Yang. A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{jansen_et_al:LIPIcs.CONCUR.2020.8,
  author =	{Jansen, David N. and Groote, Jan Friso and Timmers, Ferry and Yang, Pengfei},
  title =	{{A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.8},
  URN =		{urn:nbn:de:0030-drops-128209},
  doi =		{10.4230/LIPIcs.CONCUR.2020.8},
  annote =	{Keywords: Behavioural Equivalence, weak Bisimulation, Markov Chain}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.9
Characterizing Consensus in the Heard-Of Model

Authors: A. R. Balasubramanian and Igor Walukiewicz

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm.
Cite as

A. R. Balasubramanian and Igor Walukiewicz. Characterizing Consensus in the Heard-Of Model. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{balasubramanian_et_al:LIPIcs.CONCUR.2020.9,
  author =	{Balasubramanian, A. R. and Walukiewicz, Igor},
  title =	{{Characterizing Consensus in the Heard-Of Model}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.9},
  URN =		{urn:nbn:de:0030-drops-128217},
  doi =		{10.4230/LIPIcs.CONCUR.2020.9},
  annote =	{Keywords: consensus problem, Heard-Of model, verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.10
A Classification of Weak Asynchronous Models of Distributed Computing

Authors: Javier Esparza and Fabian Reiter

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We conduct a systematic study of asynchronous models of distributed computing consisting of identical finite-state devices that cooperate in a network to decide if the network satisfies a given graph-theoretical property. Models discussed in the literature differ in the detection capabilities of the agents residing at the nodes of the network (detecting the set of states of their neighbors, or counting the number of neighbors in each state), the notion of acceptance (acceptance by halting in a particular configuration, or by stable consensus), the notion of step (synchronous move, interleaving, or arbitrary timing), and the fairness assumptions (non-starving, or stochastic-like). We study the expressive power of the combinations of these features, and show that the initially twenty possible combinations fit into seven equivalence classes. The classification is the consequence of several equi-expressivity results with a clear interpretation. In particular, we show that acceptance by halting configuration only has non-trivial expressive power if it is combined with counting, and that synchronous and interleaving models have the same power as those in which an arbitrary set of nodes can move at the same time. We also identify simple graph properties that distinguish the expressive power of the seven classes.
Cite as

Javier Esparza and Fabian Reiter. A Classification of Weak Asynchronous Models of Distributed Computing. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2020.10,
  author =	{Esparza, Javier and Reiter, Fabian},
  title =	{{A Classification of Weak Asynchronous Models of Distributed Computing}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.10},
  URN =		{urn:nbn:de:0030-drops-128229},
  doi =		{10.4230/LIPIcs.CONCUR.2020.10},
  annote =	{Keywords: Asynchrony, Concurrency theory, Weak models of distributed computing}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.11
Scalable Termination Detection for Distributed Actor Systems

Authors: Dan Plyukhin and Gul Agha

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Automatic garbage collection (GC) prevents certain kinds of bugs and reduces programming overhead. GC techniques for sequential programs are based on reachability analysis. However, testing reachability from a root set is inadequate for determining whether an actor is garbage because an unreachable actor may send a message to a reachable actor. Instead, it is sufficient to check termination (sometimes also called quiescence): an actor is terminated if it is not currently processing a message and cannot receive a message in the future. Moreover, many actor frameworks provide all actors with access to file I/O or external storage; without inspecting an actor’s internal code, it is necessary to check that the actor has terminated to ensure that it may be garbage collected in these frameworks. Previous algorithms to detect actor garbage require coordination mechanisms such as causal message delivery or nonlocal monitoring of actors for mutation. Such coordination mechanisms adversely affect concurrency and are therefore expensive in distributed systems. We present a low-overhead reference listing technique (called DRL) for termination detection in actor systems. DRL is based on asynchronous local snapshots and message-passing between actors. This enables a decentralized implementation and transient network partition tolerance. The paper provides a formal description of DRL, shows that all actors identified as garbage have indeed terminated (safety), and that all terminated actors - under certain reasonable assumptions - will eventually be identified (liveness).
Cite as

Dan Plyukhin and Gul Agha. Scalable Termination Detection for Distributed Actor Systems. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{plyukhin_et_al:LIPIcs.CONCUR.2020.11,
  author =	{Plyukhin, Dan and Agha, Gul},
  title =	{{Scalable Termination Detection for Distributed Actor Systems}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.11},
  URN =		{urn:nbn:de:0030-drops-128231},
  doi =		{10.4230/LIPIcs.CONCUR.2020.11},
  annote =	{Keywords: actors, concurrency, termination detection, quiescence detection, garbage collection, distributed systems}
}
  • Refine by Author
  • 6 Kovács, Laura
  • 3 Worrell, James
  • 2 Aceto, Luca
  • 2 Almagor, Shaull
  • 2 Czerwiński, Wojciech
  • Show More...

  • Refine by Classification
  • 9 Theory of computation → Concurrency
  • 7 Theory of computation → Formal languages and automata theory
  • 7 Theory of computation → Logic and verification
  • 6 Theory of computation → Automata over infinite objects
  • 5 Theory of computation → Verification by model checking
  • Show More...

  • Refine by Keyword
  • 3 Bisimulation
  • 3 vector addition systems
  • 2 Asynchrony
  • 2 Axiomatisation
  • 2 Model Checking
  • Show More...

  • Refine by Type
  • 56 document

  • Refine by Publication Year
  • 52 2020
  • 1 2013
  • 1 2017
  • 1 2023
  • 1 2024

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 Imprint Privacy Contact