Volume
LIPIcs, Volume 59
27th International Conference on Concurrency Theory (CONCUR 2016)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2016, August 23-26, 2016, Québec City, CanadaEditors
Publication Details
- published at: 2016-08-24
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-017-0
- DBLP: db/conf/concur/concur2016
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 59, CONCUR'16, Complete Volume
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.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
Front Matter, Table of Contents, Preface, Conference Organization
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.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
Bayesian Inversion by Omega-Complete Cone Duality (Invited Paper)
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.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
Ethical Preference-Based Decision Support Systems (Invited Paper)
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.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
Consistency in 3D (Invited Paper)
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.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
Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control (Invited Paper)
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.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
The Benefits of Duality in Verifying Concurrent Programs under TSO
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.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
Local Linearizability for Concurrent Container-Type Data Structures
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.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
Robustness against Consistency Models with Atomic Visibility
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.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
Optimal Assumptions for Synthesis
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.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
Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis
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.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
Stability in Graphs and Games
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.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
On the Complexity of Heterogeneous Multidimensional Games
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.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
Soundness in Negotiations
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.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}
}
Document
Deciding Hyperproperties
Abstract
Hyperproperties, like observational determinism or symmetry, cannot be expressed as properties of individual computation traces, because they describe a relation between multiple computation traces. HyperLTL is a temporal logic that captures such relations through trace variables, which are introduced through existential and universal trace quantifiers and can be used to refer to multiple computations at the same time. In this paper, we study the satisfiability problem of HyperLTL. We show that the problem is PSPACE-complete for alternation-free formulas (and, hence, no more expensive than LTL satisfiability), EXPSPACE-complete for exists-forall-formulas, and undecidable for forall-exists-formulas. Many practical hyperproperties can be expressed as alternation-free formulas. Our results show that both satisfiability and implication are decidable for such properties.
Cite as
Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{finkbeiner_et_al:LIPIcs.CONCUR.2016.13,
author = {Finkbeiner, Bernd and Hahn, Christopher},
title = {{Deciding Hyperproperties}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {13:1--13: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.13},
URN = {urn:nbn:de:0030-drops-61706},
doi = {10.4230/LIPIcs.CONCUR.2016.13},
annote = {Keywords: temporal logics, satisfiability, hyperproperties, complexity}
}
Document
Homogeneous Equations of Algebraic Petri Nets
Abstract
Algebraic Petri nets are a formalism for modeling distributed systems and algorithms, describing control and data flow by combining Petri nets and algebraic specification. One way to specify correctness of an algebraic Petri net model "N" is to specify a linear equation "E" over the places of "N" based on term substitution, and coefficients from an abelian group "G". Then, "E" is valid in "N" iff "E" is valid in each reachable marking of "N". Due to the expressive power of Algebraic Petri nets, validity is generally undecidable. Stable linear equations form a class of linear equations for which validity is decidable. Place invariants yield a well-understood but incomplete characterization of all stable linear equations. In this paper, we provide a complete characterization of stability for the subclass of homogeneous linear equations, by restricting ourselves to the interpretation of terms over the Herbrand structure without considering further equality axioms. Based thereon, we show that stability is decidable for homogeneous linear equations if "G" is a cyclic group.
Cite as
Marvin Triebel and Jan Sürmeli. Homogeneous Equations of Algebraic Petri Nets. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 14:1-14:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{triebel_et_al:LIPIcs.CONCUR.2016.14,
author = {Triebel, Marvin and S\"{u}rmeli, Jan},
title = {{Homogeneous Equations of Algebraic Petri Nets}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {14:1--14: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.14},
URN = {urn:nbn:de:0030-drops-61574},
doi = {10.4230/LIPIcs.CONCUR.2016.14},
annote = {Keywords: Algebraic Petri Nets, Invariants, Linear Equations, Validity, Stability}
}
Document
Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable
Abstract
In this paper, the synthesis of bounded Petri nets from deterministic modal transition systems is shown to be undecidable. The proof is built from three components. First, it is shown that the problem of synthesising bounded Petri nets satisfying a given formula of the conjunctive nu-calculus (a suitable fragment of the mu-calculus) is undecidable. Then, an equivalence between deterministic modal transition systems and a language-based formalism called modal specifications is developed. Finally, the claim follows from a known equivalence between the conjunctive nu-calculus and modal specifications.
Cite as
Uli Schlachter. Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{schlachter:LIPIcs.CONCUR.2016.15,
author = {Schlachter, Uli},
title = {{Bounded Petri Net Synthesis from Modal Transition Systems is Undecidable}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {15:1--15: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.15},
URN = {urn:nbn:de:0030-drops-61603},
doi = {10.4230/LIPIcs.CONCUR.2016.15},
annote = {Keywords: Petri net synthesis, conjunctive nu-Calculus, modal transition systems}
}
Document
Decentralized Asynchronous Crash-Resilient Runtime Verification
Abstract
Runtime Verification (RV) is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed monitors, only if sufficiently many different verdicts can be emitted by each monitor. We revisit this impossibility result in the context of LTL semantics for RV. We show that employing the four-valued logic Rv-LTL will result in inconsistent distributed monitoring for some formulas. Our first main contribution is a family of logics, called Ltl2k+4, that refines Rv-Ltl incorporating 2k + 4 truth values, for each k >= 0. The truth values of Ltl2k+4 can be effectively used by each monitor to reach a consistent global set of verdicts for each given formula, provided k is sufficiently large. Our second main contribution is an algorithm for monitor construction enabling fault-tolerant distributed monitoring based on the aggregation of the individual verdicts by each monitor.
Cite as
Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers. Decentralized Asynchronous Crash-Resilient Runtime Verification. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bonakdarpour_et_al:LIPIcs.CONCUR.2016.16,
author = {Bonakdarpour, Borzoo and Fraigniaud, Pierre and Rajsbaum, Sergio and Rosenblueth, David A. and Travers, Corentin},
title = {{Decentralized Asynchronous Crash-Resilient Runtime Verification}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {16:1--16: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.16},
URN = {urn:nbn:de:0030-drops-61856},
doi = {10.4230/LIPIcs.CONCUR.2016.16},
annote = {Keywords: Runtime monitoring, Distributed algorithms, Fault-tolerance}
}
Document
Lazy Reachability Analysis in Distributed Systems
Abstract
We address the problem of reachability in distributed systems, modelled as networks of finite automata and propose and prove a new algorithm to solve it efficiently in many cases. This algorithm allows to decompose the reachability objective among the components, and proceeds by constructing partial products by lazily adding new components when required. It thus constructs more and more precise over-approximations of the complete product. This permits early termination in many cases, in particular when the objective is not reachable, which often is an unfavorable case in reachability analysis. We have implemented this algorithm in an early prototype and provide some very encouraging experimental results.
Cite as
Loïg Jezequel and Didier Lime. Lazy Reachability Analysis in Distributed Systems. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{jezequel_et_al:LIPIcs.CONCUR.2016.17,
author = {Jezequel, Lo\"{i}g and Lime, Didier},
title = {{Lazy Reachability Analysis in Distributed Systems}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {17:1--17: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.17},
URN = {urn:nbn:de:0030-drops-61545},
doi = {10.4230/LIPIcs.CONCUR.2016.17},
annote = {Keywords: Reachability analysis, Compositional verification, Automata}
}
Document
Causally Consistent Dynamic Slicing
Abstract
We offer a lattice-theoretic account of the problem of dynamic slicing for pi-calculus, building on prior work in the sequential setting. For any particular run of a concurrent program, we exhibit a
Galois connection relating forward and backward slices of the initial and terminal configurations. We prove that, up to lattice isomorphism, the same Galois connection arises for any causally
equivalent execution, allowing an efficient concurrent implementation of slicing via a standard interleaving semantics. Our approach has been formalised in the dependently-typed programming language Agda.
Cite as
Roly Perera, Deepak Garg, and James Cheney. Causally Consistent Dynamic Slicing. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{perera_et_al:LIPIcs.CONCUR.2016.18,
author = {Perera, Roly and Garg, Deepak and Cheney, James},
title = {{Causally Consistent Dynamic Slicing}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {18:1--18: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.18},
URN = {urn:nbn:de:0030-drops-61584},
doi = {10.4230/LIPIcs.CONCUR.2016.18},
annote = {Keywords: pi-calculus; dynamic slicing; causal equivalence; Galois connection}
}
Document
Topological Self-Stabilization with Name-Passing Process Calculi
Abstract
Topological self-stabilization is the ability of a distributed system to have its nodes themselves establish a meaningful overlay network. Independent from the initial network topology, it converges to the desired topology via forwarding, inserting, and deleting links to neighboring nodes.
We adapt a linearization algorithm, originally designed for a shared memory model, to asynchronous message-passing. We use an extended localized pi-calculus to model the algorithm and to formally prove its essential self-stabilization properties: closure and weak convergence for every arbitrary initial configuration, and strong convergence for restricted cases.
Cite as
Christina Rickmann, Christoph Wagner, Uwe Nestmann, and Stefan Schmid. Topological Self-Stabilization with Name-Passing Process Calculi. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 19:1-19:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{rickmann_et_al:LIPIcs.CONCUR.2016.19,
author = {Rickmann, Christina and Wagner, Christoph and Nestmann, Uwe and Schmid, Stefan},
title = {{Topological Self-Stabilization with Name-Passing Process Calculi}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {19:1--19: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.19},
URN = {urn:nbn:de:0030-drops-61761},
doi = {10.4230/LIPIcs.CONCUR.2016.19},
annote = {Keywords: Distributed Algorithms, Fault Tolerance, Topological Self-Stabilization, Linearization, Process Calculi}
}
Document
Linear Distances between Markov Chains
Abstract
We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results.
Cite as
Przemyslaw Daca, Thomas A. Henzinger, Jan Kretinsky, and Tatjana Petrov. Linear Distances between Markov Chains. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{daca_et_al:LIPIcs.CONCUR.2016.20,
author = {Daca, Przemyslaw and Henzinger, Thomas A. and Kretinsky, Jan and Petrov, Tatjana},
title = {{Linear Distances between Markov Chains}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {20:1--20: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.20},
URN = {urn:nbn:de:0030-drops-61829},
doi = {10.4230/LIPIcs.CONCUR.2016.20},
annote = {Keywords: probabilistic systems, verification, statistical model checking, temporal logic, behavioural equivalence}
}
Document
Complete Axiomatization for the Bisimilarity Distance on Markov Chains
Abstract
In this paper we propose a complete axiomatization of the bisimilarity distance of Desharnais et al. for the class of finite labelled Markov chains. Our axiomatization is given in the style of a quantitative extension of equational logic recently proposed by Mardare, Panangaden, and Plotkin (LICS'16) that uses equality relations t =_e s indexed by rationals, expressing that "t is approximately equal to s up to an error e".
Notably, our quantitative deductive system extends in a natural way the equational system for probabilistic bisimilarity given by Stark and Smolka by introducing an axiom for dealing with the Kantorovich distance between probability distributions.
Cite as
Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Complete Axiomatization for the Bisimilarity Distance on Markov Chains. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 21:1-21:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bacci_et_al:LIPIcs.CONCUR.2016.21,
author = {Bacci, Giorgio and Bacci, Giovanni and G. Larsen, Kim and Mardare, Radu},
title = {{Complete Axiomatization for the Bisimilarity Distance on Markov Chains}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {21:1--21: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.21},
URN = {urn:nbn:de:0030-drops-61569},
doi = {10.4230/LIPIcs.CONCUR.2016.21},
annote = {Keywords: Markov chains, Behavioral distances, Axiomatization}
}
Document
Computing Probabilistic Bisimilarity Distances via Policy Iteration
Abstract
A transformation mapping a labelled Markov chain to a simple stochastic game is presented. In the resulting simple stochastic game, each vertex corresponds to a pair of states of the labelled Markov chain. The value of a vertex of the simple stochastic game is shown to be equal to the probabilistic bisimilarity distance, a notion due to Desharnais, Gupta, Jagadeesan and Panangaden, of the corresponding pair of states of the labelled Markov chain. Bacci, Bacci, Larsen and Mardare introduced an algorithm to compute the probabilistic bisimilarity distances for a labelled Markov chain. A modification of a basic version of their algorithm for a labelled Markov chain is shown to be the policy iteration algorithm applied to the corresponding simple stochastic game. Furthermore, it is shown that this algorithm takes exponential time in the worst case.
Cite as
Qiyi Tang and Franck van Breugel. Computing Probabilistic Bisimilarity Distances via Policy Iteration. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 22:1-22:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{tang_et_al:LIPIcs.CONCUR.2016.22,
author = {Tang, Qiyi and van Breugel, Franck},
title = {{Computing Probabilistic Bisimilarity Distances via Policy Iteration}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {22:1--22: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.22},
URN = {urn:nbn:de:0030-drops-61837},
doi = {10.4230/LIPIcs.CONCUR.2016.22},
annote = {Keywords: labelled Markov chain, simple stochastic game, probabilistic bisimilarity, pseudometric, value function, policy iteration}
}
Document
Robustly Parameterised Higher-Order Probabilistic Models
Abstract
We present a method for constructing robustly parameterised families of higher-order probabilistic models. Parameter spaces and models are represented by certain classes of functors in the category of Polish spaces. Maps from parameter spaces to models (parameterisations) are continuous and natural transformations between such functors. Naturality ensures that parameterised models are invariant by change of granularity -- ie that parameterisations are intrinsic. Continuity ensures that models are robust with respect to their parameterisation. Our method allows one to build models from a set of basic functors among which the Giry probabilistic functor, spaces of cadlag trajectories (in continuous and discrete time), multisets and compact powersets. These functors can be combined by guarded composition, product and coproduct. Parameter spaces range over the polynomial closure of Giry-like functors. Thus we obtain a class of robust parameterised models which includes the Dirichlet process, various point processes (random sequences with values in Polish spaces) and other classical objects of probability theory. By extending techniques developed in prior work, we show how to reduce the questions of existence, uniqueness, naturality, and continuity of a parameterised model to combinatorial questions only involving finite spaces.
Cite as
Fredrik Dahlqvist, Vincent Danos, and Ilias Garnier. Robustly Parameterised Higher-Order Probabilistic Models. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{dahlqvist_et_al:LIPIcs.CONCUR.2016.23,
author = {Dahlqvist, Fredrik and Danos, Vincent and Garnier, Ilias},
title = {{Robustly Parameterised Higher-Order Probabilistic Models}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {23:1--23: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.23},
URN = {urn:nbn:de:0030-drops-61737},
doi = {10.4230/LIPIcs.CONCUR.2016.23},
annote = {Keywords: Probability, category theory, Giry monad}
}
Document
Coalgebraic Trace Semantics for Buechi and Parity Automata
Abstract
Despite its success in producing numerous general results on state-based dynamics, the theory of coalgebra has struggled to accommodate the Buechi acceptance condition---a basic notion in the
theory of automata for infinite words or trees. In this paper we present a clean answer to the question that builds on the "maximality" characterization of infinite traces (by Jacobs and Cirstea): the accepted language of a Buechi automaton is characterized by two commuting diagrams, one for a least homomorphism and the other for a greatest, much like in a system of (least and greatest) fixed-point equations. This characterization works uniformly for the nondeterministic branching and the probabilistic one; and for words and trees alike. We present our results in terms of the parity acceptance condition that generalizes Buechi's.
Cite as
Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic Trace Semantics for Buechi and Parity Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{urabe_et_al:LIPIcs.CONCUR.2016.24,
author = {Urabe, Natsuki and Shimizu, Shunsuke and Hasuo, Ichiro},
title = {{Coalgebraic Trace Semantics for Buechi and Parity Automata}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {24:1--24: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.24},
URN = {urn:nbn:de:0030-drops-61867},
doi = {10.4230/LIPIcs.CONCUR.2016.24},
annote = {Keywords: coalgebra, Buechi automaton, parity automaton, probabilistic automaton, tree automaton}
}
Document
Bisimulations and Unfolding in P-Accessible Categorical Models
Abstract
In this paper, we propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal and al. via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueing of paths. We prove that transitions systems and pre sheaf models are a particular case of our framework. We also prove that in our framework, several characterizations of bisimulation coincide, in particular an "operational one" akin to the standard definition in transition systems. Also, accessibility is preserved by coreflexions. We then design a notion of unfolding, which has good properties in the accessible case: its is a right adjoint and is a universal covering, i.e., initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, coincides with an unfolding, when the category of path shapes is well chosen.
Cite as
Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. Bisimulations and Unfolding in P-Accessible Categorical Models. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 25:1-25:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{dubut_et_al:LIPIcs.CONCUR.2016.25,
author = {Dubut, J\'{e}r\'{e}my and Goubault, Eric and Goubault-Larrecq, Jean},
title = {{Bisimulations and Unfolding in P-Accessible Categorical Models}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {25:1--25: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.25},
URN = {urn:nbn:de:0030-drops-61555},
doi = {10.4230/LIPIcs.CONCUR.2016.25},
annote = {Keywords: categorical models, bisimulation, coreflexions, unfolding, universal covering}
}
Document
A Uniform Framework for Timed Automata
Abstract
Timed automata, and machines alike, currently lack a general mathematical characterisation. In this paper we provide a uniform coalgebraic understanding of these devices. This framework encompasses known behavioural equivalences for timed automata and paves the way for the extension of these notions to new timed behaviours and for the instantiation of established results from the coalgebraic theory as well. Key to this work is the use of lax functors for they allow us to model time flow as a context property and hence offer a general and expressive setting where to study timed systems: the index category encodes "how step sequences form executions" (e.g. whether steps duration get accumulated or kept distinct) whereas the base category encodes "step nature and composition" (e.g. non-determinism and labels). Finally, we develop the notion of general saturation for lax functors and show how equivalences of interest for timed behaviours are instances of this notion. This characterisation allows us to reason about the expressiveness of said notions within a uniform framework and organise them in a spectrum independent from the behavioural aspects encoded in the base category.
Cite as
Tomasz Brengos and Marco Peressotti. A Uniform Framework for Timed Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{brengos_et_al:LIPIcs.CONCUR.2016.26,
author = {Brengos, Tomasz and Peressotti, Marco},
title = {{A Uniform Framework for Timed Automata}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {26:1--26: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.26},
URN = {urn:nbn:de:0030-drops-61690},
doi = {10.4230/LIPIcs.CONCUR.2016.26},
annote = {Keywords: coalgebras, lax functors, general saturation, timed behavioural equivalence, timed language equivalence}
}
Document
Analyzing Timed Systems Using Tree Automata
Abstract
Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. Such graphs can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).
Cite as
S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. Analyzing Timed Systems Using Tree Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2016.27,
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan},
title = {{Analyzing Timed Systems Using Tree Automata}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {27:1--27: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.27},
URN = {urn:nbn:de:0030-drops-61775},
doi = {10.4230/LIPIcs.CONCUR.2016.27},
annote = {Keywords: Timed automata, tree automata, pushdown systems, tree-width}
}
Document
On the Expressiveness of QCTL
Abstract
QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QkCTL, with at most k nested blocks of quantifiers, is (k+1)-EXPTIME-complete), very few results are known about the expressiveness of this logic.
We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
Cite as
Amélie David, Francois Laroussinie, and Nicolas Markey. On the Expressiveness of QCTL. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{david_et_al:LIPIcs.CONCUR.2016.28,
author = {David, Am\'{e}lie and Laroussinie, Francois and Markey, Nicolas},
title = {{On the Expressiveness of QCTL}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {28:1--28: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.28},
URN = {urn:nbn:de:0030-drops-61643},
doi = {10.4230/LIPIcs.CONCUR.2016.28},
annote = {Keywords: Specification, Verification, Temporal Logic, Expressiveness, Tree automata}
}
Document
Model Checking Flat Freeze LTL on One-Counter Automata
Abstract
Freeze LTL is a temporal logic with registers that is suitable for specifying properties of data words. In this paper we study the model checking problem for Freeze LTL on one-counter automata. This problem is known to be undecidable in full generality and PSPACE-complete for the special case of deterministic one-counter automata. Several years ago, Demri and Sangnier investigated the model checking problem for the flat fragment of Freeze LTL on several classes of counter automata and posed the decidability of model checking flat Freeze LTL on one-counter automata as an open problem. In this paper we resolve this problem positively, utilising a known reduction to a reachability problem on one-counter automata with parameterised equality and disequality tests. Our main technical contribution is to show decidability of the latter problem by translation to Presburger arithmetic.
Cite as
Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, and James Worrell. Model Checking Flat Freeze LTL on One-Counter Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 29:1-29:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{lechner_et_al:LIPIcs.CONCUR.2016.29,
author = {Lechner, Antonia and Mayr, Richard and Ouaknine, Jo\"{e}l and Pouly, Amaury and Worrell, James},
title = {{Model Checking Flat Freeze LTL on One-Counter Automata}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {29:1--29: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.29},
URN = {urn:nbn:de:0030-drops-61841},
doi = {10.4230/LIPIcs.CONCUR.2016.29},
annote = {Keywords: one-counter automata, disequality tests, reachability, freeze LTL, Presburger arithmetic}
}
Document
Parameterized Systems in BIP: Design and Model Checking
Abstract
BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to systems parameterized in the number of components. We show that FOIL captures classical parameterized architectures such as token-passing rings, cliques of identical components communicating with rendezvous or broadcast, and client-server systems.
Although the BIP framework includes efficient verification tools for statically-defined systems, none are available for parameterized systems with an unbounded number of components. The parameterized model checking literature contains a wealth of techniques for systems of classical architectures. However, application of these results requires a deep understanding of parameterized model checking techniques and their underlying mathematical models. To overcome these difficulties, we introduce a framework that automatically identifies parameterized model checking techniques applicable to a BIP design. To our knowledge, it is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.
Cite as
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis. Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{konnov_et_al:LIPIcs.CONCUR.2016.30,
author = {Konnov, Igor and Kotek, Tomer and Wang, Qiang and Veith, Helmut and Bliudze, Simon and Joseph Sifakis},
title = {{Parameterized Systems in BIP: Design and Model Checking}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {30:1--30:16},
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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.30},
URN = {urn:nbn:de:0030-drops-61670},
doi = {10.4230/LIPIcs.CONCUR.2016.30},
annote = {Keywords: Rigorous system design, BIP, verification, parameterized model checking}
}
Document
Private Names in Non-Commutative Logic
Abstract
We present an expressive but decidable first-order system (named MAV1) defined by using the calculus of structures, a generalisation of the sequent calculus. In addition to first-order universal and existential quantifiers the system incorporates a de Morgan dual pair of nominal quantifiers called `new' and `wen', distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of the operators `new' and `wen' is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as predicates in MAV1. Modelling processes as predicates in MAV1 has the advantage that linear implication defines a precongruence over processes that fully respects causality and branching. The transitivity of this precongruence is established by novel techniques for handling first-order quantifiers in the cut elimination proof.
Cite as
Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. Private Names in Non-Commutative Logic. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{horne_et_al:LIPIcs.CONCUR.2016.31,
author = {Horne, Ross and Tiu, Alwen and Aman, Bogdan and Ciobanu, Gabriel},
title = {{Private Names in Non-Commutative Logic}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {31:1--31:16},
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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.31},
URN = {urn:nbn:de:0030-drops-61759},
doi = {10.4230/LIPIcs.CONCUR.2016.31},
annote = {Keywords: process calculi, calculus of structures, nominal logic, causal consistency}
}
Document
Causality vs. Interleavings in Concurrent Game Semantics
Abstract
We investigate relationships between interleaving and causal notions of game semantics for concurrent programming languages, focusing on the existence of canonical compact causal representations of the interleaving game semantics of programs.
We perform our study on an affine variant of Idealized Parallel Algol (IPA), for which we present two games model: and interleaving model (an adaptation of Ghica and Murawski’s fully abstract games model for IPA up to may-testing), and a causal model (a variant of Rideau and Winskel’s games on event structures). Both models are sound and adequate for affine IPA. Then, we relate the two models. First we give a causality-forgetting operation mapping functorially the causal model to the interleaving one. We show that from an interleaving strategy we can reconstruct a causal strategy, from which it follows that the interleaving model is the observational quotient of the causal one. Then, we investigate several reconstructions of causal strategies from interleaving ones, showing finally that there are programs which are inherently causally ambiguous, with several distinct minimal causal representations.
Cite as
Simon Castellan and Pierre Clairambault. Causality vs. Interleavings in Concurrent Game Semantics. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{castellan_et_al:LIPIcs.CONCUR.2016.32,
author = {Castellan, Simon and Clairambault, Pierre},
title = {{Causality vs. Interleavings in Concurrent Game Semantics}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {32:1--32: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.32},
URN = {urn:nbn:de:0030-drops-61620},
doi = {10.4230/LIPIcs.CONCUR.2016.32},
annote = {Keywords: Game semantics, concurrency, causality, event structures}
}
Document
Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types
Abstract
Wadler introduced Classical Processes (CP), a calculus based on a propositions-as-types correspondence between propositions of classical linear logic and session types. Carbone et al. introduced Multiparty Classical Processes, a calculus that generalises CP to multiparty session types, by replacing the duality of classical linear logic (relating two types) with a more general notion of coherence (relating an arbitrary number of types). This paper introduces variants of CP and MCP, plus a new intermediate calculus of Globally-governed Classical Processes (GCP). We show a tight relation between these three calculi, giving semantics-preserving translations from GCP to CP and from MCP to GCP. The translation from GCP to CP interprets a coherence proof as an arbiter process that mediates communications in a session, while MCP adds annotations that permit processes to communicate directly without centralised control.
Cite as
Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{carbone_et_al:LIPIcs.CONCUR.2016.33,
author = {Carbone, Marco and Lindley, Sam and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Wadler, Philip},
title = {{Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {33:1--33: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.33},
URN = {urn:nbn:de:0030-drops-61811},
doi = {10.4230/LIPIcs.CONCUR.2016.33},
annote = {Keywords: Multiparty Session Types, Linear Logic, Propositions as Types}
}
Document
Global Caching for the Alternation-free µ-Calculus
Abstract
We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free mu-calculus. The algorithm supports global caching with intermediate propagation and runs in time 2^O(n). In game-theoretic terms, our algorithm integrates the steps for constructing and solving the Büchi game arising from the input tableau into a single procedure; this is done on-the-fly, i.e. may terminate before the game has been fully constructed. This suggests a slogan to the effect that global caching = game solving on-the-fly. A prototypical implementation shows promising initial results.
Cite as
Daniel Hausmann, Lutz Schröder, and Christoph Egger. Global Caching for the Alternation-free µ-Calculus. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{hausmann_et_al:LIPIcs.CONCUR.2016.34,
author = {Hausmann, Daniel and Schr\"{o}der, Lutz and Egger, Christoph},
title = {{Global Caching for the Alternation-free µ-Calculus}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {34:1--34: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.34},
URN = {urn:nbn:de:0030-drops-61724},
doi = {10.4230/LIPIcs.CONCUR.2016.34},
annote = {Keywords: modal logic, fixpoint logic, satisfiability, global caching, coalgebraic logic}
}
Document
Up-To Techniques for Generalized Bisimulation Metrics
Abstract
Bisimulation metrics allow us to compute distances between the behaviors of probabilistic systems. In this paper we present enhancements of the proof method based on bisimulation metrics, by extending the theory of up-to techniques to (pre)metrics on discrete probabilistic concurrent processes.
Up-to techniques have proved to be a powerful proof method for showing that two systems are bisimilar, since they make it possible to build (and thereby check) smaller relations in bisimulation proofs. We define soundness conditions for up-to techniques on metrics, and study compatibility properties that allow us to safely compose up-to techniques with each other. As an example, we derive the soundness of the up-to-bisimilarity-metric-and-context technique.
The study is carried out for a generalized version of the bisimulation metrics, in which the Kantorovich lifting is parametrized with respect to a distance function. The standard bisimulation metrics, as well as metrics aimed at capturing multiplicative properties such as differential privacy, are specific instances of this general definition.
Cite as
Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli. Up-To Techniques for Generalized Bisimulation Metrics. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 35:1-35:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{chatzikokolakis_et_al:LIPIcs.CONCUR.2016.35,
author = {Chatzikokolakis, Konstantinos and Palamidessi, Catuscia and Vignudelli, Valeria},
title = {{Up-To Techniques for Generalized Bisimulation Metrics}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {35:1--35: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.35},
URN = {urn:nbn:de:0030-drops-61793},
doi = {10.4230/LIPIcs.CONCUR.2016.35},
annote = {Keywords: bisimulation, metrics, up-to techniques, Kantorovich, differential privacy}
}
Document
Modal Decomposition on Nondeterministic Probabilistic Processes
Abstract
We propose a SOS-based method for decomposing modal formulae for nondeterministic probabilistic processes.
The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from its decomposition.
By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.
Cite as
Valentina Castiglioni, Daniel Gebler, and Simone Tini. Modal Decomposition on Nondeterministic Probabilistic Processes. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{castiglioni_et_al:LIPIcs.CONCUR.2016.36,
author = {Castiglioni, Valentina and Gebler, Daniel and Tini, Simone},
title = {{Modal Decomposition on Nondeterministic Probabilistic Processes}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {36:1--36: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.36},
URN = {urn:nbn:de:0030-drops-61665},
doi = {10.4230/LIPIcs.CONCUR.2016.36},
annote = {Keywords: SOS, nondeterministic probabilistic process algebras, logical characterization, decomposition of modal formulae}
}
Document
Diagnosis in Infinite-State Probabilistic Systems
Abstract
In a recent work, we introduced four variants of diagnosability
(FA, IA, FF, IF) in (finite) probabilistic
systems (pLTS) depending whether one considers (1) finite or
infinite runs and (2) faulty or all runs. We studied their
relationship and established that the corresponding decision
problems are PSPACE-complete. A key ingredient of the decision
procedures was a characterisation of diagnosability by the fact that
a random run almost surely lies in an open set whose specification
only depends on the qualitative behaviour of the pLTS. Here we
investigate similar issues for infinite pLTS. We first show that
this characterisation still holds for FF-diagnosability but
with a G-delta set instead of an open set and also for IF-
and IA-diagnosability when pLTS are finitely branching. We also
prove that surprisingly FA-diagnosability cannot be
characterised in this way even in the finitely branching case. Then
we apply our characterisations for a partially observable
probabilistic extension of visibly pushdown automata (POpVPA),
yielding EXPSPACE procedures for solving diagnosability problems.
In addition, we establish some computational lower bounds and show
that slight extensions of POpVPA lead to undecidability.
Cite as
Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. Diagnosis in Infinite-State Probabilistic Systems. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 37:1-37:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2016.37,
author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel},
title = {{Diagnosis in Infinite-State Probabilistic Systems}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {37:1--37: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.37},
URN = {urn:nbn:de:0030-drops-61597},
doi = {10.4230/LIPIcs.CONCUR.2016.37},
annote = {Keywords: probabilistic systems, infinite-state systems, pushdown automata, diagnosis, partial observation}
}