47 Search Results for "Fokkink, Wan"

Volume

LIPIcs, Volume 140

30th International Conference on Concurrency Theory (CONCUR 2019)

CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands

Editors: Wan Fokkink and Rob van Glabbeek

Document
DOI: 10.4230/LIPIcs.CSL.2021.8
Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?

Authors: Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy’s merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. This study provides a negative answer to that question based on three reasonable assumptions.
Cite as

Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2021.8,
  author =	{Aceto, Luca and Castiglioni, Valentina and Fokkink, Wan and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
  title =	{{Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.8},
  URN =		{urn:nbn:de:0030-drops-134425},
  doi =		{10.4230/LIPIcs.CSL.2021.8},
  annote =	{Keywords: Equational logic, CCS, bisimulation, parallel composition, non-finitely based algebras}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2019
LIPIcs, Volume 140, CONCUR'19, Complete Volume

Authors: Wan Fokkink and Rob van Glabbeek

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
LIPIcs, Volume 140, CONCUR'19, Complete Volume
Cite as

30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{fokkink_et_al:LIPIcs.CONCUR.2019,
  title =	{{LIPIcs, Volume 140, CONCUR'19, Complete Volume}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019},
  URN =		{urn:nbn:de:0030-drops-112105},
  doi =		{10.4230/LIPIcs.CONCUR.2019},
  annote =	{Keywords: Theory of computation, Concurrency}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Wan Fokkink and Rob van Glabbeek

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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

30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{fokkink_et_al:LIPIcs.CONCUR.2019.0,
  author =	{Fokkink, Wan and van Glabbeek, Rob},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.0},
  URN =		{urn:nbn:de:0030-drops-109026},
  doi =		{10.4230/LIPIcs.CONCUR.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2019.1
Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper)

Authors: Marta Z. Kwiatkowska

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Computing systems are becoming ever more complex, increasingly often incorporating deep learning components. Since deep learning is unstable with respect to adversarial perturbations, there is a need for rigorous software development methodologies that encompass machine learning. This paper describes progress with developing automated verification techniques for deep neural networks to ensure safety and robustness of their decisions with respect to input perturbations. This includes novel algorithms based on feature-guided search, games, global optimisation and Bayesian methods.
Cite as

Marta Z. Kwiatkowska. Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper). In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.CONCUR.2019.1,
  author =	{Kwiatkowska, Marta Z.},
  title =	{{Safety Verification for Deep Neural Networks with Provable Guarantees}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{1:1--1:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.1},
  URN =		{urn:nbn:de:0030-drops-109036},
  doi =		{10.4230/LIPIcs.CONCUR.2019.1},
  annote =	{Keywords: Neural networks, robustness, formal verification, Bayesian neural networks}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2019.2
Synthesis of Safe, Optimal and Compact Strategies for Stochastic Hybrid Games (Invited Paper)

Authors: Kim G. Larsen

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
UPPAAL-Stratego is a recent branch of the verification tool UPPAAL allowing for synthesis of safe and optimal strategies for stochastic timed (hybrid) games. We describe newly developed learning methods, allowing for synthesis of significantly better strategies and with much improved convergence behaviour. Also, we describe novel use of decision trees for learning orders-of-magnitude more compact strategy representation. In both cases, the seek for optimality does not compromise safety.
Cite as

Kim G. Larsen. Synthesis of Safe, Optimal and Compact Strategies for Stochastic Hybrid Games (Invited Paper). In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 2:1-2:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{larsen:LIPIcs.CONCUR.2019.2,
  author =	{Larsen, Kim G.},
  title =	{{Synthesis of Safe, Optimal and Compact Strategies for Stochastic Hybrid Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{2:1--2:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.2},
  URN =		{urn:nbn:de:0030-drops-109048},
  doi =		{10.4230/LIPIcs.CONCUR.2019.2},
  annote =	{Keywords: Timed automata, Stochastic hybrid grame, Symbolic synthesis, Reinforcement learning, Q-learning, M-learning}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2019.3
Program Invariants (Invited Talk)

Authors: Joël Ouaknine

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Automated invariant generation is a fundamental challenge in program analysis and verification, going back many decades, and remains a topic of active research. In this talk I'll present a select overview and survey of work on this problem, and discuss unexpected connections to other fields including algebraic geometry, group theory, and quantum computing. (No previous knowledge of these topics will be assumed.) This is joint work with Ehud Hrushovski, Amaury Pouly, and James Worrell.
Cite as

Joël Ouaknine. Program Invariants (Invited Talk). In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ouaknine:LIPIcs.CONCUR.2019.3,
  author =	{Ouaknine, Jo\"{e}l},
  title =	{{Program Invariants}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.3},
  URN =		{urn:nbn:de:0030-drops-109056},
  doi =		{10.4230/LIPIcs.CONCUR.2019.3},
  annote =	{Keywords: Automated invariant generation, program analysis and verification}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2019.4
Concurrent Algorithms and Data Structures for Model Checking (Invited Talk)

Authors: Jaco van de Pol

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Model checking is a successful method for checking properties on the state space of concurrent, reactive systems. Since it is based on exhaustive search, scaling this method to industrial systems has been a challenge since its conception. Research has focused on clever data structures and algorithms, to reduce the size of the state space or its representation; smart search heuristics, to reveal potential bugs and counterexamples early; and high-performance computing, to deploy the brute force processing power of clusters of compute-servers. The main challenge is to combine these approaches - brute-force alone (when implemented carefully) can bring a linear speedup in the number of processors. This is great, since it reduces model-checking times from days to minutes. On the other hand, proper algorithms and data structures can lead to exponential gains. Therefore, the parallelization bonus is only real if we manage to speedup clever algorithms. There are some obstacles though: many linear-time graph algorithms depend on a depth-first exploration order, which is hard to parallelize. Examples include the detection of strongly connected components (SCC) and the nested depth-first-search (NDFS) algorithm. Both are used in model checking LTL properties. Symbolic representations, like binary decision diagrams (BDDs), reduce model checking to "pointer-chasing", leading to irregular memory-access patterns. This poses severe challenges on achieving actual speedup in (clusters of) modern multi-core computer architectures. This talk presents some of the solutions found over the last 10 years, which led to the high-performance model checker LTSmin [Gijs Kant et al., 2015]. These include parallel NDFS (based on the PhD thesis of Alfons Laarman [Alfons Laarman, 2014]), the parallel detection of SCCs with concurrent Union-Find (based on the PhD thesis of Vincent Bloemen [Vincent Bloemen, 2019]), and concurrent BDDs (based on the PhD thesis of Tom van Dijk [Tom van Dijk, 2016]). Finally, I will sketch a perspective on moving forward from high-performance model checking to high-performance synthesis algorithms. Examples include parameter synthesis for stochastic and timed systems, and strategy synthesis for (stochastic and timed) games.
Cite as

Jaco van de Pol. Concurrent Algorithms and Data Structures for Model Checking (Invited Talk). In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{vandepol:LIPIcs.CONCUR.2019.4,
  author =	{van de Pol, Jaco},
  title =	{{Concurrent Algorithms and Data Structures for Model Checking}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.4},
  URN =		{urn:nbn:de:0030-drops-109066},
  doi =		{10.4230/LIPIcs.CONCUR.2019.4},
  annote =	{Keywords: model checking, parallel algorithms, concurrent datastructures}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.5
Of Cores: A Partial-Exploration Framework for Markov Decision Processes

Authors: Jan Křetínský and Tobias Meggendorfer

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
We introduce a framework for approximate analysis of Markov decision processes (MDP) with bounded-, unbounded-, and infinite-horizon properties. The main idea is to identify a "core" of an MDP, i.e., a subsystem where we provably remain with high probability, and to avoid computation on the less relevant rest of the state space. Although we identify the core using simulations and statistical techniques, it allows for rigorous error bounds in the analysis. Consequently, we obtain efficient analysis algorithms based on partial exploration for various settings, including the challenging case of strongly connected systems.
Cite as

Jan Křetínský and Tobias Meggendorfer. Of Cores: A Partial-Exploration Framework for Markov Decision Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2019.5,
  author =	{K\v{r}et{\'\i}nsk\'{y}, Jan and Meggendorfer, Tobias},
  title =	{{Of Cores: A Partial-Exploration Framework for Markov Decision Processes}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.5},
  URN =		{urn:nbn:de:0030-drops-109076},
  doi =		{10.4230/LIPIcs.CONCUR.2019.5},
  annote =	{Keywords: Markov Decision Processes, Reachability, Approximation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.6
Combinations of Qualitative Winning for Stochastic Parity Games

Authors: Krishnendu Chatterjee and Nir Piterman

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games.
Cite as

Krishnendu Chatterjee and Nir Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.6,
  author =	{Chatterjee, Krishnendu and Piterman, Nir},
  title =	{{Combinations of Qualitative Winning for Stochastic Parity Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.6},
  URN =		{urn:nbn:de:0030-drops-109089},
  doi =		{10.4230/LIPIcs.CONCUR.2019.6},
  annote =	{Keywords: Two Player Games, Stochastic Games, Parity Winning Conditions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.7
Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs

Authors: Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time O(min(n^2, m sqrt{m log n}) + b log n). In this work we present randomized near-linear time algorithms, with expected running time O~(m + b), where the O~ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors.
Cite as

Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil. Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.7,
  author =	{Chatterjee, Krishnendu and Dvo\v{r}\'{a}k, Wolfgang and Henzinger, Monika and Svozil, Alexander},
  title =	{{Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.7},
  URN =		{urn:nbn:de:0030-drops-109093},
  doi =		{10.4230/LIPIcs.CONCUR.2019.7},
  annote =	{Keywords: model checking, graph games, Streett games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.8
Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives

Authors: Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The window mechanism was introduced by Chatterjee et al. [Krishnendu Chatterjee et al., 2015] to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.
Cite as

Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.8,
  author =	{Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael},
  title =	{{Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.8},
  URN =		{urn:nbn:de:0030-drops-109103},
  doi =		{10.4230/LIPIcs.CONCUR.2019.8},
  annote =	{Keywords: Markov decision processes, window mean-payoff, window parity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.9
Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

Authors: Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch’s probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon’s simple policy iteration on these games. The correctness of Condon’s approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central rôle.
Cite as

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing Probabilistic Bisimilarity Distances for Probabilistic Automata. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.CONCUR.2019.9,
  author =	{Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim G. and Mardare, Radu and Tang, Qiyi and van Breugel, Franck},
  title =	{{Computing Probabilistic Bisimilarity Distances for Probabilistic Automata}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.9},
  URN =		{urn:nbn:de:0030-drops-109119},
  doi =		{10.4230/LIPIcs.CONCUR.2019.9},
  annote =	{Keywords: Probabilistic automata, Behavioural metrics, Simple stochastic games, Simple policy iteration algorithm}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.10
Asymmetric Distances for Approximate Differential Privacy

Authors: Dmitry Chistikov, Andrzej S. Murawski, and David Purser

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Differential privacy is a widely studied notion of privacy for various models of computation, based on measuring differences between probability distributions. We consider (epsilon,delta)-differential privacy in the setting of labelled Markov chains. For a given epsilon, the parameter delta can be captured by a variant of the total variation distance, which we call lv_{alpha} (where alpha = e^{epsilon}). First we study lv_{alpha} directly, showing that it cannot be computed exactly. However, the associated approximation problem turns out to be in PSPACE and #P-hard. Next we introduce a new bisimilarity distance for bounding lv_{alpha} from above, which provides a tighter bound than previously known distances while remaining computable with the same complexity (polynomial time with an NP oracle). We also propose an alternative bound that can be computed in polynomial time. Finally, we illustrate the distances on case studies.
Cite as

Dmitry Chistikov, Andrzej S. Murawski, and David Purser. Asymmetric Distances for Approximate Differential Privacy. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2019.10,
  author =	{Chistikov, Dmitry and Murawski, Andrzej S. and Purser, David},
  title =	{{Asymmetric Distances for Approximate Differential Privacy}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.10},
  URN =		{urn:nbn:de:0030-drops-109121},
  doi =		{10.4230/LIPIcs.CONCUR.2019.10},
  annote =	{Keywords: Bisimilarity distances, Differential privacy, Labelled Markov chains}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.11
Event Structures for Mixed Choice

Authors: Marc de Visme

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
In the context of models with mixed nondeterministic and probabilistic choice, we present a concurrent model based on partial orders, more precisely Winskel’s event structures. We study its relationship with the interleaving-based model of Segala’s probabilistic automata. Lastly, we use this model to give a truly concurrent semantics to an extension of CCS with probabilistic choice, and relate this concurrent semantics to the usual interleaving semantics, thus generalising existing results on CCS, event structures and labelled transition systems.
Cite as

Marc de Visme. Event Structures for Mixed Choice. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{devisme:LIPIcs.CONCUR.2019.11,
  author =	{de Visme, Marc},
  title =	{{Event Structures for Mixed Choice}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.11},
  URN =		{urn:nbn:de:0030-drops-109137},
  doi =		{10.4230/LIPIcs.CONCUR.2019.11},
  annote =	{Keywords: probability, nondeterminism, concurrency, event structures, CCS}
}
  • Refine by Author
  • 5 Fokkink, Wan
  • 3 Chatterjee, Krishnendu
  • 3 Larsen, Kim G.
  • 3 van Glabbeek, Rob
  • 2 Bertrand, Nathalie
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 Structural Operational Semantics
  • 3 Synthesis
  • 3 model checking
  • 2 CCS
  • 2 Compositionality
  • Show More...

  • Refine by Type
  • 46 document
  • 1 volume

  • Refine by Publication Year
  • 44 2019
  • 2 2017
  • 1 2021

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