40 Search Results for "Jagadeesan, Radha"

Volume

LIPIcs, Volume 59

27th International Conference on Concurrency Theory (CONCUR 2016)

CONCUR 2016, August 23-26, 2016, Québec City, Canada

Editors: Josée Desharnais and Radha Jagadeesan

Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2016
LIPIcs, Volume 59, CONCUR'16, Complete Volume

Authors: Josée Desharnais and Radha Jagadeesan

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
LIPIcs, Volume 59, CONCUR'16, Complete Volume
Cite as

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

Copy BibTex To Clipboard

@Proceedings{desharnais_et_al:LIPIcs.CONCUR.2016,
  title =	{{LIPIcs, Volume 59, CONCUR'16, Complete Volume}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016},
  URN =		{urn:nbn:de:0030-drops-65871},
  doi =		{10.4230/LIPIcs.CONCUR.2016},
  annote =	{Keywords: Software, Data, Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2016.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Josée Desharnais and Radha Jagadeesan

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

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

27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 0:i-0:xxii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.CONCUR.2016.0,
  author =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{0:i--0:xxii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.0},
  URN =		{urn:nbn:de:0030-drops-61535},
  doi =		{10.4230/LIPIcs.CONCUR.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2016.1
Bayesian Inversion by Omega-Complete Cone Duality (Invited Paper)

Authors: Fredrik Dahlqvist, Vincent Danos, Ilias Garnier, and Ohad Kammar

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
The process of inverting Markov kernels relates to the important subject of Bayesian modelling and learning. In fact, Bayesian update is exactly kernel inversion. In this paper, we investigate how and when Markov kernels (aka stochastic relations, or probabilistic mappings, or simply kernels) can be inverted. We address the question both directly on the category of measurable spaces, and indirectly by interpreting kernels as Markov operators: - For the direct option, we introduce a typed version of the category of Markov kernels and use the so-called "disintegration of measures". Here, one has to specialise to measurable spaces borne from a simple class of topological spaces -e.g. Polish spaces (other choices are possible). Our method and result greatly simplify a recent development in Ref. [4]. - For the operator option, we use a cone version of the category of Markov operators (kernels seen as predicate transformers). That is to say, our linear operators are not just continuous, but are required to satisfy the stronger condition of being $\om$-chain-continuous. Prior work shows that one obtains an adjunction in the form of a pair of contravariant and inverse functors between the categories of $L_1$- and $L_\infty$-cones [3]. Inversion, seen through the operator prism, is just adjunction. No topological assumption is needed. - We show that both categories (Markov kernels and $\om$-chain-continuous Markov operators) are related by a family of contravariant functors $T_p$ for $1\leq p\leq\infty$. The $T_p$'s are Kleisli extensions of (duals of) conditional expectation functors introduced in Ref. [3]. - With this bridge in place, we can prove that both notions of inversion agree when both defined: if $f$ is a kernel, and $f\dg$ its direct inverse, then $T_\infty(f)\dg=T_1(f\dg)$.
Cite as

Fredrik Dahlqvist, Vincent Danos, Ilias Garnier, and Ohad Kammar. Bayesian Inversion by Omega-Complete Cone Duality (Invited Paper). In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dahlqvist_et_al:LIPIcs.CONCUR.2016.1,
  author =	{Dahlqvist, Fredrik and Danos, Vincent and Garnier, Ilias and Kammar, Ohad},
  title =	{{Bayesian Inversion by Omega-Complete Cone Duality}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{1:1--1:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.1},
  URN =		{urn:nbn:de:0030-drops-61909},
  doi =		{10.4230/LIPIcs.CONCUR.2016.1},
  annote =	{Keywords: probabilistic models, bayesian learning, markov operators}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2016.2
Ethical Preference-Based Decision Support Systems (Invited Paper)

Authors: Francesca Rossi

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
The future will see autonomous intelligent systems acting in the same environment as humans, in areas as diverse as driving, assistive technology, and health care. Think of self-driving cars, companion robots, and medical diagnosis support systems. Also, humans and machines will often need to work together and agree on common decisions. Thus hybrid collective decision making systems will be in great need. In these scenarios, both machines and collective decision making systems should follow some form of moral values and ethical principles (appropriate to where they will act but always aligned to humans'). In fact, humans would accept and trust more machines that behave as ethically as other humans in the same environment. Also, these principles would make it easier for machines to determine their actions and explain their behavior in terms understandable by humans. Moreover, often machines and humans will need to make decisions together, either through consensus or by reaching a compromise. This would be facilitated by shared moral values and ethical principles. In this paper we introduce some issues in embedding morality into intelligent systems. A few research questions are defined, with the hope that the discussion raised by the questions will shed some light onto the possible answers.
Cite as

Francesca Rossi. Ethical Preference-Based Decision Support Systems (Invited Paper). In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 2:1-2:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{rossi:LIPIcs.CONCUR.2016.2,
  author =	{Rossi, Francesca},
  title =	{{Ethical Preference-Based Decision Support Systems}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{2:1--2:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.2},
  URN =		{urn:nbn:de:0030-drops-61870},
  doi =		{10.4230/LIPIcs.CONCUR.2016.2},
  annote =	{Keywords: preferences, decision making, multi-agent systems}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2016.3
Consistency in 3D (Invited Paper)

Authors: Marc Shapiro, Masoud Saeida Ardekani, and Gustavo Petri

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Comparisons of different consistency models often try to place them in a linear strong-to-weak order. However this view is clearly inadequate, since it is well known, for instance, that Snapshot Isolation and Serialisability are incomparable. In the interest of a better understanding, we propose a new classification, along three dimensions, related to: a total order of writes, a causal order of reads, and transactional composition of multiple operations. A model may be stronger than another on one dimension and weaker on another. We believe that this new classification scheme is both scientifically sound and has good explicative value. The current paper presents the three-dimensional design space intuitively.
Cite as

Marc Shapiro, Masoud Saeida Ardekani, and Gustavo Petri. Consistency in 3D (Invited Paper). In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{shapiro_et_al:LIPIcs.CONCUR.2016.3,
  author =	{Shapiro, Marc and Ardekani, Masoud Saeida and Petri, Gustavo},
  title =	{{Consistency in 3D}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{3:1--3:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.3},
  URN =		{urn:nbn:de:0030-drops-61889},
  doi =		{10.4230/LIPIcs.CONCUR.2016.3},
  annote =	{Keywords: Consistency models, replicated data, structural invariants, correctness of distributed systems}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2016.4
Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control (Invited Paper)

Authors: Junxing Yang, Radu Grosu, Scott A. Smolka, and Ashish Tiwari

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We present a new formulation of the V-formation problem for migrating birds in terms of model predictive control (MPC). In our approach, to drive a collection of birds towards a desired formation, an optimal velocity adjustment (acceleration) is performed at each time-step on each bird's current velocity using a model-based prediction window of $T$ time-steps. We present both centralized and distributed versions of this approach. The optimization criteria we consider are based on fitness metrics of candidate accelerations that birds in a V-formations are known to benefit from, including velocity matching, clear view, and upwash benefit. We validate our MPC-based approach by showing that for a significant majority of simulation runs, the flock succeeds in forming the desired formation. Our results help to better understand the emergent behavior of formation flight, and provide a control strategy for flocks of autonomous aerial vehicles.
Cite as

Junxing Yang, Radu Grosu, Scott A. Smolka, and Ashish Tiwari. Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control (Invited Paper). In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.CONCUR.2016.4,
  author =	{Yang, Junxing and Grosu, Radu and Smolka, Scott A. and Tiwari, Ashish},
  title =	{{Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{4:1--4:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.4},
  URN =		{urn:nbn:de:0030-drops-61896},
  doi =		{10.4230/LIPIcs.CONCUR.2016.4},
  annote =	{Keywords: bird flocking, v-formation, model predictive control, particle swarm optimization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.5
The Benefits of Duality in Verifying Concurrent Programs under TSO

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We address the problem of verifying safety properties of concurrent programs running over the TSO memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO model that is more amenable for efficient algorithmic verification and for extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows to obtain a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. The Benefits of Duality in Verifying Concurrent Programs under TSO. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2016.5,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Bouajjani, Ahmed and Ngo, Tuan Phong},
  title =	{{The Benefits of Duality in Verifying Concurrent Programs under TSO}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.5},
  URN =		{urn:nbn:de:0030-drops-61710},
  doi =		{10.4230/LIPIcs.CONCUR.2016.5},
  annote =	{Keywords: Weak Memory Models, Reachability Problem, Parameterized Systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.6
Local Linearizability for Concurrent Container-Type Data Structures

Authors: Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations.
Cite as

Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. Local Linearizability for Concurrent Container-Type Data Structures. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{haas_et_al:LIPIcs.CONCUR.2016.6,
  author =	{Haas, Andreas and Henzinger, Thomas A. and Holzer, Andreas and Kirsch, Christoph M. and Lippautz, Michael and Payer, Hannes and Sezgin, Ali and Sokolova, Ana and Veith, Helmut},
  title =	{{Local Linearizability for Concurrent Container-Type Data Structures}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.6},
  URN =		{urn:nbn:de:0030-drops-61809},
  doi =		{10.4230/LIPIcs.CONCUR.2016.6},
  annote =	{Keywords: (concurrent) data structures, relaxed semantics, linearizability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.7
Robustness against Consistency Models with Atomic Visibility

Authors: Giovanni Bernardi and Alexey Gotsman

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
To achieve scalability, modern Internet services often rely on distributed databases with consistency models for transactions weaker than serializability. At present, application programmers often lack techniques to ensure that the weakness of these consistency models does not violate application correctness. We present criteria to check whether applications that rely on a database providing only weak consistency are robust, i.e., behave as if they used a database providing serializability. When this is the case, the application programmer can reap the scalability benefits of weak consistency while being able to easily check the desired correctness properties. Our results handle systematically and uniformly several recently proposed weak consistency models, as well as a mechanism for strengthening consistency in parts of an application.
Cite as

Giovanni Bernardi and Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bernardi_et_al:LIPIcs.CONCUR.2016.7,
  author =	{Bernardi, Giovanni and Gotsman, Alexey},
  title =	{{Robustness against Consistency Models with Atomic Visibility}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.7},
  URN =		{urn:nbn:de:0030-drops-61652},
  doi =		{10.4230/LIPIcs.CONCUR.2016.7},
  annote =	{Keywords: Robustness, Replication, Consistency models, Transactions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.8
Optimal Assumptions for Synthesis

Authors: Romain Brenguier

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Controller synthesis is the automatic construction a correct system from its specification. This often requires assumptions about the behaviour of the environment. It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary. As a consequence the generated controllers are suboptimal in terms of robustness. In this work, given a specification, we identify the weakest assumptions that ensure the existence of a controller. We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that restricts only inputs of the systems. We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorse-free strategies depending on the classes. Using these correspondences, we then propose an algorithm for computing optimal assumptions that can be ensured by the environment.
Cite as

Romain Brenguier. Optimal Assumptions for Synthesis. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brenguier:LIPIcs.CONCUR.2016.8,
  author =	{Brenguier, Romain},
  title =	{{Optimal Assumptions for Synthesis}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{8:1--8:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.8},
  URN =		{urn:nbn:de:0030-drops-61742},
  doi =		{10.4230/LIPIcs.CONCUR.2016.8},
  annote =	{Keywords: Controller synthesis, Parity games, Admissible strategies}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.9
Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis

Authors: Shaull Almagor, Orna Kupferman, and Yaron Velner

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
In Boolean synthesis, we are given an LTL specification, and the goal is to construct a transducer that realizes it against an adversarial environment. Often, a specification contains both Boolean requirements that should be satisfied against an adversarial environment, and multi-valued components that refer to the quality of the satisfaction and whose expected cost we would like to minimize with respect to a probabilistic environment. In this work we study, for the first time, mean-payoff games in which the system aims at minimizing the expected cost against a probabilistic environment, while surely satisfying an omega-regular condition against an adversarial environment. We consider the case the omega-regular condition is given as a parity objective or by an LTL formula. We show that in general, optimal strategies need not exist, and moreover, the limit value cannot be approximated by finite-memory strategies. We thus focus on computing the limit-value, and give tight complexity bounds for synthesizing epsilon-optimal strategies for both finite-memory and infinite-memory strategies. We show that our game naturally arises in various contexts of synthesis with Boolean and multi-valued objectives. Beyond direct applications, in synthesis with costs and rewards to certain behaviors, it allows us to compute the minimal sensing cost of omega-regular specifications -- a measure of quality in which we look for a transducer that minimizes the expected number of signals that are read from the input.
Cite as

Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2016.9,
  author =	{Almagor, Shaull and Kupferman, Orna and Velner, Yaron},
  title =	{{Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{9:1--9:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.9},
  URN =		{urn:nbn:de:0030-drops-61689},
  doi =		{10.4230/LIPIcs.CONCUR.2016.9},
  annote =	{Keywords: Stochastic and Quantitative Synthesis, Mean Payoff Games, Sensing.}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.10
Stability in Graphs and Games

Authors: Tomas Brazdil, Vojtech Forejt, Antonin Kucera, and Petr Novotny

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system.
Cite as

Tomas Brazdil, Vojtech Forejt, Antonin Kucera, and Petr Novotny. Stability in Graphs and Games. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.CONCUR.2016.10,
  author =	{Brazdil, Tomas and Forejt, Vojtech and Kucera, Antonin and Novotny, Petr},
  title =	{{Stability in Graphs and Games}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.10},
  URN =		{urn:nbn:de:0030-drops-61784},
  doi =		{10.4230/LIPIcs.CONCUR.2016.10},
  annote =	{Keywords: Games, Stability, Mean-Payoff, Window Objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.11
On the Complexity of Heterogeneous Multidimensional Games

Authors: Veronique Bruyere, Quentin Hautem, and Jean-Francois Raskin

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We study two-player zero-sum turn-based games played on multidimensional weighted graphs with heterogeneous quantitative objectives. Our objectives are defined starting from the measures Inf, Sup, LimInf, and LimSup of the weights seen along the play, as well as on the window mean-payoff (WMP) measure recently introduced in [Krishnendu,Doyen,Randour,Raskin, Inf. Comput., 2015]. Whereas multidimensional games with Boolean combinations of classical mean-payoff objectives are undecidable [Velner, FOSSACS, 2015], we show that CNF/DNF Boolean combinations for heterogeneous measures taken among {WMP, Inf, Sup, LimInf, LimSup} lead to EXPTIME-completeness with exponential memory strategies for both players. We also identify several interesting fragments with better complexities and memory requirements, and show that some of them are solvable in PTIME.
Cite as

Veronique Bruyere, Quentin Hautem, and Jean-Francois Raskin. On the Complexity of Heterogeneous Multidimensional Games. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2016.11,
  author =	{Bruyere, Veronique and Hautem, Quentin and Raskin, Jean-Francois},
  title =	{{On the Complexity of Heterogeneous Multidimensional Games}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{11:1--11:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.11},
  URN =		{urn:nbn:de:0030-drops-61618},
  doi =		{10.4230/LIPIcs.CONCUR.2016.11},
  annote =	{Keywords: wo-player zero-sum games played on graphs, quantitative objectives, multidimensional heterogeneous objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.12
Soundness in Negotiations

Authors: Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In a former paper, Esparza and Desel have shown that deciding soundness of a negotiation is PSPACE-complete, and in PTIME if the negotiation is deterministic. They have also provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open. In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. In the second part we solve the open question of Esparza and Desel's paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.
Cite as

Javier Esparza, Denis Kuperberg, Anca Muscholl, and Igor Walukiewicz. Soundness in Negotiations. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 12:1-12:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2016.12,
  author =	{Esparza, Javier and Kuperberg, Denis and Muscholl, Anca and Walukiewicz, Igor},
  title =	{{Soundness in Negotiations}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{12:1--12:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.12},
  URN =		{urn:nbn:de:0030-drops-61636},
  doi =		{10.4230/LIPIcs.CONCUR.2016.12},
  annote =	{Keywords: Negotiations, workflows, soundness, verification, concurrency}
}
  • Refine by Author
  • 2 Dahlqvist, Fredrik
  • 2 Danos, Vincent
  • 2 Desharnais, Josée
  • 2 Garnier, Ilias
  • 2 Henzinger, Thomas A.
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 verification
  • 2 Consistency models
  • 2 Stability
  • 2 bisimulation
  • 2 concurrency
  • Show More...

  • Refine by Type
  • 39 document
  • 1 volume

  • Refine by Publication Year
  • 40 2016

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