Volume
LIPIcs, Volume 85
28th International Conference on Concurrency Theory (CONCUR 2017)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2017, September 5-8, 2017, Berlin, GermanyEditors
Publication Details
- published at: 2017-09-01
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-048-4
- DBLP: db/conf/concur/concur2017
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 85, CONCUR'17, Complete Volume
Abstract
LIPIcs, Volume 85, CONCUR'17, Complete Volume
Cite as
28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Proceedings{meyer_et_al:LIPIcs.CONCUR.2017,
title = {{LIPIcs, Volume 85, CONCUR'17, Complete Volume}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017},
URN = {urn:nbn:de:0030-drops-79070},
doi = {10.4230/LIPIcs.CONCUR.2017},
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
28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{meyer_et_al:LIPIcs.CONCUR.2017.0,
author = {Meyer, Roland and Nestmann, Uwe},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {0:i--0:xx},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.0},
URN = {urn:nbn:de:0030-drops-77693},
doi = {10.4230/LIPIcs.CONCUR.2017.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Forward Progress on GPU Concurrency (Invited Talk)
Abstract
The tutorial at CONCUR will provide a practical overview of work undertaken over the last six years in the Multicore Programming Group at Imperial College London, and with collaborators internationally, related to understanding and reasoning about concurrency in software designed for acceleration on GPUs. In this article we provide an overview of this work, which includes contributions to data race analysis, compiler testing, memory model understanding and formalisation, and most recently efforts to enable portable GPU implementations of algorithms that require forward progress guarantees.
Cite as
Alastair F. Donaldson, Jeroen Ketema, Tyler Sorensen, and John Wickerson. Forward Progress on GPU Concurrency (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 1:1-1:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{donaldson_et_al:LIPIcs.CONCUR.2017.1,
author = {Donaldson, Alastair F. and Ketema, Jeroen and Sorensen, Tyler and Wickerson, John},
title = {{Forward Progress on GPU Concurrency}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {1:1--1:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.1},
URN = {urn:nbn:de:0030-drops-78055},
doi = {10.4230/LIPIcs.CONCUR.2017.1},
annote = {Keywords: GPUs, concurrency, formal verification, memory models, data races}
}
Document
Invited Talk
Admissibility in Games with Imperfect Information (Invited Talk)
Abstract
In this invited paper, we study the concept of admissible strategies for two player win/lose infinite sequential games with imperfect information. We show that in stark contrast with the perfect information variant, admissible strategies are only guaranteed to exist when players have objectives that are closed sets. As a consequence, we also study decision problems related to the existence of admissible strategies for regular games as well as finite duration games.
Cite as
Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur. Admissibility in Games with Imperfect Information (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{brenguier_et_al:LIPIcs.CONCUR.2017.2,
author = {Brenguier, Romain and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
title = {{Admissibility in Games with Imperfect Information}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {2:1--2:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.2},
URN = {urn:nbn:de:0030-drops-78066},
doi = {10.4230/LIPIcs.CONCUR.2017.2},
annote = {Keywords: Admissibility, non-zero sum games, reactive synthesis, imperfect infor- mation}
}
Document
Invited Talk
Probabilistic Programming (Invited Talk)
Abstract
Probabilistic programming refers to the idea of using standard programming constructs for specifying probabilistic models from machine learning and statistics, and employing generic inference algorithms for answering various queries on these models, such as posterior inference and estimation of model evidence. Although this idea itself is not new and was, in fact, explored by several programming-language and statistics researchers in the early 2000, it is only in the last few years that probabilistic programming has gained a large amount of attention among researchers in machine learning and programming languages, and that expressive and efficient probabilistic programming systems (such as Anglican, Church, Figaro, Infer.net, PSI, PyMC, Stan, and Venture) started to appear and have been taken up by a nontrivial number of users.
The primary goal of my talk is to introduce probabilistic programming to the CONCUR/QUEST/FORMATS audience. At the end of my talk, I want the audience to understand basic results and techniques in probabilistic programming and to feel that these results and techniques are relevant or at least related to what she or he studies, although they typically come from foreign research areas, such as machine learning and statistics. My talk will contain both technical materials and lessons that I learnt from my machine-learning colleagues in Oxford, who are developing a highly-expressive higher-order probabilistic programming language, called Anglican. It will also include my work on the denotational semantics of higher-order probabilistic programming languages and their inference algorithms, which are jointly pursued with colleagues in Cambridge, Edinburgh, Oxford and Tubingen.
Cite as
Hongseok Yang. Probabilistic Programming (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{yang:LIPIcs.CONCUR.2017.3,
author = {Yang, Hongseok},
title = {{Probabilistic Programming}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.3},
URN = {urn:nbn:de:0030-drops-78088},
doi = {10.4230/LIPIcs.CONCUR.2017.3},
annote = {Keywords: Probabilistic programming, Machine learning, Denotational semantics}
}
Document
Invited Talk
A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk)
Abstract
This paper presents a high level overview of Proof Spaces [Farzan, Kincaid, and Podelski, 2015] as an instance of a new approach to compositional verification of concurrent programs and discusses potential future work extending the approach beyond its current scope of applicability.
Cite as
Azadeh Farzan and Zachary Kincaid. A New Notion of Compositionality for Concurrent Program Proofs (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 4:1-4:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{farzan_et_al:LIPIcs.CONCUR.2017.4,
author = {Farzan, Azadeh and Kincaid, Zachary},
title = {{A New Notion of Compositionality for Concurrent Program Proofs}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {4:1--4:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.4},
URN = {urn:nbn:de:0030-drops-78097},
doi = {10.4230/LIPIcs.CONCUR.2017.4},
annote = {Keywords: Concurrency, Proofs, Dynamic Memory, Recursion}
}
Document
Bidirectional Nested Weighted Automata
Abstract
Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications.
Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input
words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.
Cite as
Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Bidirectional Nested Weighted Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2017.5,
author = {Chatterjee, Krishnendu and Henzinger, Thomas A. and Otop, Jan},
title = {{Bidirectional Nested Weighted Automata}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {5:1--5:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.5},
URN = {urn:nbn:de:0030-drops-77763},
doi = {10.4230/LIPIcs.CONCUR.2017.5},
annote = {Keywords: weighted automata, nested weighted automata, complexity, bidirectional}
}
Document
k-Bounded Petri Net Synthesis from Modal Transition Systems
Abstract
We present a goal-oriented algorithm that can synthesise k-bounded Petri nets (k in N^+) from hyper modal transition systems (hMTS), an extension of labelled transition systems with optional and required behaviour. The algorithm builds a potential reachability graph of a Petri net from scratch, extending it stepwise with required behaviour from the given MTS and over-approximating the result to a new valid reachability graph. Termination occurs if either the MTS yields no additional requirements or the resulting net of the second step shows a conflict with the behaviour allowed by the MTS, making it non-sythesisable.
Cite as
Uli Schlachter and Harro Wimmel. k-Bounded Petri Net Synthesis from Modal Transition Systems. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{schlachter_et_al:LIPIcs.CONCUR.2017.6,
author = {Schlachter, Uli and Wimmel, Harro},
title = {{k-Bounded Petri Net Synthesis from Modal Transition Systems}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {6:1--6:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.6},
URN = {urn:nbn:de:0030-drops-77802},
doi = {10.4230/LIPIcs.CONCUR.2017.6},
annote = {Keywords: Modal transition system, bounded Petri net, synthesis}
}
Document
A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic
Abstract
Open bisimilarity is a strong bisimulation congruence for the pi-calculus. In open bisimilarity, free names in processes are treated as variables that may be instantiated; in contrast to late bisimilarity where free names are constants. An established modal logic due to Milner, Parrow, and Walker characterises late bisimilarity, that is, two processes satisfy the same set of formulae if and only if they are bisimilar. We propose an intuitionistic variation of this modal logic and prove that it characterises open bisimilarity. The soundness proof is mechanised in Abella. The completeness proof provides an algorithm for generating distinguishing formulae, useful for explaining and certifying whenever processes are non-bisimilar.
Cite as
Ki Yung Ahn, Ross Horne, and Alwen Tiu. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{ahn_et_al:LIPIcs.CONCUR.2017.7,
author = {Ahn, Ki Yung and Horne, Ross and Tiu, Alwen},
title = {{A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.7},
URN = {urn:nbn:de:0030-drops-77899},
doi = {10.4230/LIPIcs.CONCUR.2017.7},
annote = {Keywords: bisimulation, modal logic, intuitionistic logic}
}
Document
Consistently-Detecting Monitors
Abstract
We study a contextual definition for deterministic monitoring based on consistent detections. It is defined in terms of the observed behaviour of the monitor when instrumented over arbitrary systems. We give an alternative, coinductive definition based on controllability which does not rely on system quantifications, and show that it is fully-abstract with respect to the former definition. We then develop a symbolic counterpart to the controllability definition to facilitate an automated analysis for controllable monitors involving data.
Cite as
Adrian Francalanza. Consistently-Detecting Monitors. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{francalanza:LIPIcs.CONCUR.2017.8,
author = {Francalanza, Adrian},
title = {{Consistently-Detecting Monitors}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {8:1--8:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.8},
URN = {urn:nbn:de:0030-drops-77722},
doi = {10.4230/LIPIcs.CONCUR.2017.8},
annote = {Keywords: Runtime Monitoring, Deterministic Behaviour, Controllability, Compositional Reasoning, Symbolic Analysis}
}
Document
Flow Logic
Abstract
A flow network is a directed graph in which each edge has a capacity, bounding the amount of flow that can travel through it. Flow networks have attracted a lot of research in computer science. Indeed, many questions in numerous application areas can be reduced to questions about flow networks. This includes direct applications, namely a search for a maximal flow in networks, as well as less direct applications, like maximal matching or optimal scheduling. Many of these applications would benefit from a framework in which one can formally reason about properties of flow networks that go beyond their maximal flow.
We introduce Flow Logics: modal logics that treat flow functions as explicit first-order objects and enable the specification of rich properties of flow networks. The syntax of our logic BFL* (Branching Flow Logic) is similar to the syntax of the temporal logic CTL*, except that atomic assertions may be flow propositions, like > \gamma or \geq \gamma, for \gamma \in \N, which refer to the value of the flow in a vertex, and that first-order quantification can be applied both to paths and to flow functions. For example, the BFL* formula \Ef ((\geq 100) \wedge AG({\it low} \rightarrow (\leq 20)) states that there is a legal flow function in which the flow is above 100 and in all paths, the amount of flow that travels through vertices with low security is at most 20.
We present an exhaustive study of the theoretical and practical aspects of BFL*, as well as extensions and fragments of it. Our extensions include flow quantifications that range over non-integral flow functions or over maximal flow functions, path quantification that ranges over paths along which non-zero flow travels, past operators, and first-order quantification of flow values. We focus on the model-checking problem and show that it is PSPACE-complete, as it is for CTL*. Handling of flow quantifiers, however, increases the complexity in terms of the network to P^{NP}, even for the LFL and BFL fragments, which are the flow-counterparts of LTL and CTL. We are still able to point to a useful fragment of BFL* for which the model-checking problem can be solved in polynomial time.
Cite as
Orna Kupferman and Gal Vardi. Flow Logic. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2017.9,
author = {Kupferman, Orna and Vardi, Gal},
title = {{Flow Logic}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.9},
URN = {urn:nbn:de:0030-drops-77796},
doi = {10.4230/LIPIcs.CONCUR.2017.9},
annote = {Keywords: Flow Network, Temporal Logic}
}
Document
Rule Formats for Nominal Process Calculi
Abstract
The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specification of the early pi-calculus. Our study stems from the recent Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.
Cite as
Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, and Yolanda Ortega-Mallén. Rule Formats for Nominal Process Calculi. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2017.10,
author = {Aceto, Luca and F\'{a}bregas, Ignacio and Garc{\'\i}a-P\'{e}rez, \'{A}lvaro and Ing\'{o}lfsd\'{o}ttir, Anna and Ortega-Mall\'{e}n, Yolanda},
title = {{Rule Formats for Nominal Process Calculi}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {10:1--10:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.10},
URN = {urn:nbn:de:0030-drops-77869},
doi = {10.4230/LIPIcs.CONCUR.2017.10},
annote = {Keywords: nominal sets, nominal structural operational semantics, process algebra, nominal transition systems, scope opening, rule formats}
}
Document
Divergence and Unique Solution of Equations
Abstract
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the ‘up-to techniques’). Finally, we study the theorems in name-passing calculi such as the asynchronous pi-calculus, and revisit the completeness proof of Milner’s encoding of the lambda-calculus into the pi-calculus for Lévy-Longo Trees.
Cite as
Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and Unique Solution of Equations. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{durier_et_al:LIPIcs.CONCUR.2017.11,
author = {Durier, Adrien and Hirschkoff, Daniel and Sangiorgi, Davide},
title = {{Divergence and Unique Solution of Equations}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.11},
URN = {urn:nbn:de:0030-drops-77849},
doi = {10.4230/LIPIcs.CONCUR.2017.11},
annote = {Keywords: Bisimilarity, unique solution of equations, termination, process calculi}
}
Document
Controlling a Population
Abstract
We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller, the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player chooses actions, and the second player resolves non-determinism for each agent. The game with m agents is called the m-population game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can playerone control the m-population game for all m in N whatever playertwo does?
In this paper, we prove that the population control problem is decidable, and it is a EXPTIME-complete problem. As far as we know, this is one of the first results on parameterized control. Our algorithm, not based on cut-off techniques, produces winning strategies which are symbolic, that i they do not need to count precisely how the population is spread between states. We also show that if the is no winning strategy, then there is a population size cutoff such that playerone wins the m-population game if and only if m< \cutoff. Surprisingly, \cutoff can be doubly exponential in the number of states of the NFA, with tight upper and lower bounds.
Cite as
Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, and Hugo Gimbert. Controlling a Population. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2017.12,
author = {Bertrand, Nathalie and Dewaskar, Miheer and Genest, Blaise and Gimbert, Hugo},
title = {{Controlling a Population}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {12:1--12:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.12},
URN = {urn:nbn:de:0030-drops-78000},
doi = {10.4230/LIPIcs.CONCUR.2017.12},
annote = {Keywords: Model-checking, control, parametric systems}
}
Document
The Robot Routing Problem for Collecting Aggregate Stochastic Rewards
Abstract
We propose a new model for formalizing reward collection problems on graphs with dynamically generated rewards which may appear and disappear based on a stochastic model. The robot routing problem is modeled as a graph whose nodes are stochastic processes generating potential rewards over discrete time. The rewards are generated according to the stochastic process, but at each step, an existing reward disappears with a given probability. The edges in the graph encode the (unit-distance) paths between the rewards' locations. On visiting a node, the robot collects the accumulated reward at the node at that time, but traveling between the nodes takes time. The optimization question asks to compute an optimal (or epsilon-optimal) path that maximizes the expected collected rewards.
We consider the finite and infinite-horizon robot routing problems. For finite-horizon, the goal is to maximize the total expected reward, while for infinite horizon we consider limit-average objectives. We study the computational and strategy complexity of these problems, establish NP-lower bounds and show that optimal strategies require memory in general. We also provide an algorithm for computing epsilon-optimal infinite paths for arbitrary epsilon > 0.
Cite as
Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu, and Sadegh Esmaeil Zadeh Soudjani. The Robot Routing Problem for Collecting Aggregate Stochastic Rewards. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{dimitrova_et_al:LIPIcs.CONCUR.2017.13,
author = {Dimitrova, Rayna and Gavran, Ivan and Majumdar, Rupak and Prabhu, Vinayak S. and Soudjani, Sadegh Esmaeil Zadeh},
title = {{The Robot Routing Problem for Collecting Aggregate Stochastic Rewards}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.13},
URN = {urn:nbn:de:0030-drops-77920},
doi = {10.4230/LIPIcs.CONCUR.2017.13},
annote = {Keywords: Path Planning, Graph Games, Quantitative Objectives, Discounting}
}
Document
Coverability Synthesis in Parametric Petri Nets
Abstract
We study Parametric Petri Nets (PPNs), i.e., Petri nets for which some arc weights can be parameters. In that setting, we address a problem of parameter synthesis, which consists in computing the exact set of values for the parameters such that a given marking is coverable in the instantiated net.
Since the emptiness of that solution set is already undecidable for general PPNs, we address a special case where parameters are used only as input weights (preT-PPNs), and consequently for which the solution set is
downward-closed. To this end, we invoke a result for the representation of
upward closed set from Valk and Jantzen.
To use this procedure, we show we need to decide universal coverability,
that is decide if some marking is coverable for every possible values of the parameters.
We therefore provide a proof of its EXPSPACE-completeness,
thus settling the previously open problem of its decidability.
We also propose an adaptation of this reasoning to the case of
parameters used only as output weights (postT-PPNs).
In this case, the condition to use this procedure can be reduced to the decidability of the existential coverability,
that is decide if there exists values of the parameters making a given marking coverable.
This problem is known decidable but we provide here a cleaner proof, providing its EXPSPACE-completeness, by reduction to Omega Petri Nets.
Cite as
Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Coverability Synthesis in Parametric Petri Nets. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{david_et_al:LIPIcs.CONCUR.2017.14,
author = {David, Nicolas and Jard, Claude and Lime, Didier and Roux, Olivier H.},
title = {{Coverability Synthesis in Parametric Petri Nets}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {14:1--14:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.14},
URN = {urn:nbn:de:0030-drops-77831},
doi = {10.4230/LIPIcs.CONCUR.2017.14},
annote = {Keywords: Petri net, Parameters, Coverability, Unboundedness, Synthesis}
}
Document
Divide and Congruence III: Stability & Divergence
Abstract
In two earlier papers we derived congruence formats for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. Here this work is extended with important stability and divergence requirements. Stability refers to the absence of a tau-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. Divergence, which refers to the presence of an infinite sequence of tau-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.
Cite as
Wan Fokkink, Rob van Glabbeek, and Bas Luttik. Divide and Congruence III: Stability & Divergence. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{fokkink_et_al:LIPIcs.CONCUR.2017.15,
author = {Fokkink, Wan and van Glabbeek, Rob and Luttik, Bas},
title = {{Divide and Congruence III: Stability \& Divergence}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {15:1--15:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.15},
URN = {urn:nbn:de:0030-drops-77855},
doi = {10.4230/LIPIcs.CONCUR.2017.15},
annote = {Keywords: Structural Operational Semantics, Compositionality, Congruence, Modal Logic, Modal Decomposition, Weak Semantics, Divergence}
}
Document
Checking Linearizability of Concurrent Priority Queues
Abstract
Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Unfortunately their correctness criteria — linearizability with respect to given ADT specifications — are hard to verify. Verifying linearizability is undecidable in general, even on classes of implementations where the usual control-state reachability is decidable. In this work we consider concurrent priority queues which are fundamental to many multi-threaded applications like task scheduling or discrete event simulation, and show that verifying linearizability of such implementations is reducible to control-state reachability. This reduction entails the first decidability results for verifying concurrent priority queues with an unbounded number of threads, and it enables the application of existing safety-verification tools for establishing their correctness.
Cite as
Ahmed Bouajjani, Constantin Enea, and Chao Wang. Checking Linearizability of Concurrent Priority Queues. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bouajjani_et_al:LIPIcs.CONCUR.2017.16,
author = {Bouajjani, Ahmed and Enea, Constantin and Wang, Chao},
title = {{Checking Linearizability of Concurrent Priority Queues}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {16:1--16:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.16},
URN = {urn:nbn:de:0030-drops-78079},
doi = {10.4230/LIPIcs.CONCUR.2017.16},
annote = {Keywords: Concurrency, Linearizability, Model Checking}
}
Document
Nash Equilibrium and Bisimulation Invariance
Abstract
Game theory provides a well-established framework for the analysis of concurrent and multi-agent systems. The basic idea is that concurrent processes (agents) can be understood as corresponding to players in a game; plays represent the possible computation runs of the system; and strategies define the behaviour of agents. Typically, strategies are modelled as functions from sequences of system states to player actions. Analysing a system in such a way involves computing the set of (Nash) equilibria in the game. However, we show that, with respect to the above model of strategies---the standard model in the literature---bisimilarity does not preserve the existence of Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic perspective, and which from a logical perspective satisfy the same temporal formulae, nevertheless have fundamentally different properties from a game theoretic perspective. In this paper we explore the issues raised by this discovery, and investigate three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We also use some of these models of strategies to provide new semantic foundations for logics for strategic reasoning, and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of Nash equilibria with respect to the conventional model of strategies in the literature.
Cite as
Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, and Michael Wooldridge. Nash Equilibrium and Bisimulation Invariance. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gutierrez_et_al:LIPIcs.CONCUR.2017.17,
author = {Gutierrez, Julian and Harrenstein, Paul and Perelli, Giuseppe and Wooldridge, Michael},
title = {{Nash Equilibrium and Bisimulation Invariance}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {17:1--17:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.17},
URN = {urn:nbn:de:0030-drops-77902},
doi = {10.4230/LIPIcs.CONCUR.2017.17},
annote = {Keywords: Bisumulation, Nash equilibrium, Multiagent systems, Strategy logic}
}
Document
Goal-Driven Unfolding of Petri Nets
Abstract
Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.
Cite as
Thomas Chatain and Loïc Paulevé. Goal-Driven Unfolding of Petri Nets. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{chatain_et_al:LIPIcs.CONCUR.2017.18,
author = {Chatain, Thomas and Paulev\'{e}, Lo\"{i}c},
title = {{Goal-Driven Unfolding of Petri Nets}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {18:1--18:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.18},
URN = {urn:nbn:de:0030-drops-77730},
doi = {10.4230/LIPIcs.CONCUR.2017.18},
annote = {Keywords: model reduction; reachability; concurrency; unfoldings; Petri nets; automata networks}
}
Document
Probabilistic Automata of Bounded Ambiguity
Abstract
Probabilistic automata are a computational model introduced by Michael Rabin, extending nondeterministic finite automata with probabilistic transitions. Despite its simplicity, this model is very expressive and many of the associated algorithmic questions are undecidable. In this work we focus on the emptiness problem, which asks whether a given probabilistic automaton accepts some word with probability higher than a given threshold. We consider a natural and well-studied structural restriction on automata, namely the degree of ambiguity, which is defined as the maximum number of accepting runs over all words. We observe that undecidability of the emptiness problem requires infinite ambiguity and so we focus on the case of finitely ambiguous probabilistic automata.
Our main results are to construct efficient algorithms for analysing finitely ambiguous probabilistic automata through a reduction to a multi-objective optimisation problem, called the stochastic path problem. We obtain a polynomial time algorithm for approximating the value of finitely ambiguous probabilistic automata and a quasi-polynomial time algorithm for the emptiness problem for 2-ambiguous probabilistic automata.
Cite as
Nathanaël Fijalkow, Cristian Riveros, and James Worrell. Probabilistic Automata of Bounded Ambiguity. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{fijalkow_et_al:LIPIcs.CONCUR.2017.19,
author = {Fijalkow, Nathana\"{e}l and Riveros, Cristian and Worrell, James},
title = {{Probabilistic Automata of Bounded Ambiguity}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {19:1--19:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.19},
URN = {urn:nbn:de:0030-drops-77716},
doi = {10.4230/LIPIcs.CONCUR.2017.19},
annote = {Keywords: Probabilistic Automata, Emptiness Problem, Stochastic Path Problem, Multi-Objective Optimisation Problems}
}
Document
Two Lower Bounds for BPA
Abstract
Branching bisimilarity of normed Basic Process Algebra (nBPA) was claimed to be EXPTIME-hard in previous papers without any explicit proof. Recently it has been pointed out by Petr Jancar that the claim lacked proper justification. In this paper, we develop a new complete proof for the EXPTIME-hardness of branching bisimilarity of nBPA. We also prove that the associated regularity problem of nBPA is PSPACE-hard. This improves previous P-hard result.
Cite as
Mingzhang Huang and Qiang Yin. Two Lower Bounds for BPA. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{huang_et_al:LIPIcs.CONCUR.2017.20,
author = {Huang, Mingzhang and Yin, Qiang},
title = {{Two Lower Bounds for BPA}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {20:1--20:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.20},
URN = {urn:nbn:de:0030-drops-77772},
doi = {10.4230/LIPIcs.CONCUR.2017.20},
annote = {Keywords: BPA, branching bisimulation, regularity}
}
Document
Infinite-Duration Bidding Games
Abstract
Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games [Lazarus1999,Lazarus2012]. There, a central question is the existence and computation of threshold budgets; namely, a value t \in [0,1] such that if \PO's budget exceeds t, he can win the game, and if \PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games.
Cite as
Guy Avni, Thomas A. Henzinger, and Ventsislav Chonev. Infinite-Duration Bidding Games. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{avni_et_al:LIPIcs.CONCUR.2017.21,
author = {Avni, Guy and Henzinger, Thomas A. and Chonev, Ventsislav},
title = {{Infinite-Duration Bidding Games}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {21:1--21:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.21},
URN = {urn:nbn:de:0030-drops-77741},
doi = {10.4230/LIPIcs.CONCUR.2017.21},
annote = {Keywords: Bidding Games, Parity Games, Mean-Payoff Games, Richman Games}
}
Document
On the Power of Name-Passing Communication
Abstract
It is shown that generally higher order process calculi cannot be interpreted in name-passing calculi in a robust way.
Cite as
Yuxi Fu. On the Power of Name-Passing Communication. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 22:1-22:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{fu:LIPIcs.CONCUR.2017.22,
author = {Fu, Yuxi},
title = {{On the Power of Name-Passing Communication}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {22:1--22:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.22},
URN = {urn:nbn:de:0030-drops-77786},
doi = {10.4230/LIPIcs.CONCUR.2017.22},
annote = {Keywords: Interaction theory, expressiveness, bisimulation}
}
Document
The Power of Convex Algebras
Abstract
Probabilistic automata (PA) combine probability and nondeterminism.
They can be given different semantics, like strong bisimilarity,
convex bisimilarity, or (more recently) distribution bisimilarity.
The latter is based on the view of PA as transformers of probability
distributions, also called belief states, and promotes distributions
to first-class citizens.
We give a coalgebraic account of the latter semantics, and explain
the genesis of the belief-state transformer from a PA. To do so, we
make explicit the convex algebraic structure present in PA and
identify belief-state transformers as transition systems with state
space that carries a convex algebra. As a consequence of our abstract
approach, we can give a sound proof technique which we call
bisimulation up-to convex hull.
Cite as
Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2017.23,
author = {Bonchi, Filippo and Silva, Alexandra and Sokolova, Ana},
title = {{The Power of Convex Algebras}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {23:1--23:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.23},
URN = {urn:nbn:de:0030-drops-77966},
doi = {10.4230/LIPIcs.CONCUR.2017.23},
annote = {Keywords: belief-state transformers, bisimulation up-to, coalgebra, convex algebra, convex powerset monad, probabilistic automata}
}
Document
Refinement for Signal Flow Graphs
Abstract
The symmetric monoidal theory of Interacting Hopf Algebras provides a sound and complete axiomatisation for linear relations over a given field. As is the case for ordinary relations, linear relations have a natural order that coincides with inclusion. In this paper, we give a presentation for this ordering by extending the theory of Interacting Hopf Algebras with a single additional inequation. We show that the extended theory gives rise to an abelian bicategory—a concept due to Carboni and Walters—and highlight similarities with the algebra of relations. Most importantly, the ordering leads to a well-behaved notion of refinement for signal flow graphs.
Cite as
Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Pawel Sobocinski. Refinement for Signal Flow Graphs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2017.24,
author = {Bonchi, Filippo and Holland, Joshua and Pavlovic, Dusko and Sobocinski, Pawel},
title = {{Refinement for Signal Flow Graphs}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {24:1--24:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.24},
URN = {urn:nbn:de:0030-drops-77758},
doi = {10.4230/LIPIcs.CONCUR.2017.24},
annote = {Keywords: Signal flow graphs, refinement, operational semantics, string diagrams, symmetric monoidal inequality theory}
}
Document
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages
Abstract
Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem that relates a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours.
Cite as
Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kappe_et_al:LIPIcs.CONCUR.2017.25,
author = {Kapp\'{e}, Tobias and Brunet, Paul and Luttik, Bas and Silva, Alexandra and Zanasi, Fabio},
title = {{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.25},
URN = {urn:nbn:de:0030-drops-77913},
doi = {10.4230/LIPIcs.CONCUR.2017.25},
annote = {Keywords: Kleene theorem, Series-rational expressions, Automata, Brzozowski derivatives, Concurrency, Pomsets}
}
Document
Algebraic Laws for Weak Consistency
Abstract
Modern distributed systems often rely on so called weakly consistent databases, which achieve scalability by weakening consistency guarantees of distributed transaction processing. The semantics of such databases have been formalised in two different styles, one based on abstract executions and the other based on dependency graphs. The choice between these styles has been made according to intended applications. The former has been used for specifying and verifying the implementation of the databases, while the latter for proving properties of client programs of the databases.
In this paper, we present a set of novel algebraic laws (inequalities) that connect these two styles of specifications. The laws relate binary relations used in a specification based on abstract executions to those used in a specification based on dependency graphs. We then show that this algebraic connection gives rise to so called robustness criteria: conditions which ensure that a client program of a weakly consistent database does not exhibit anomalous behaviours due to weak consistency. These criteria make it easy to reason about these client programs, and may become a basis for dynamic or static program analyses.
For a certain class of consistency models specifications, we prove a full
abstraction result that connects the two styles of specifications.
Cite as
Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Algebraic Laws for Weak Consistency. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cerone_et_al:LIPIcs.CONCUR.2017.26,
author = {Cerone, Andrea and Gotsman, Alexey and Yang, Hongseok},
title = {{Algebraic Laws for Weak Consistency}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.26},
URN = {urn:nbn:de:0030-drops-77946},
doi = {10.4230/LIPIcs.CONCUR.2017.26},
annote = {Keywords: Weak Consistency Models, Distributed Databases, Dependency Graphs}
}
Document
Algorithms to Compute Probabilistic Bisimilarity Distances for Labelled Markov Chains
Abstract
In the late nineties, Desharnais, Gupta, Jagadeesan and Panangaden presented probabilistic bisimilarity distances on the states of a labelled Markov chain. This provided a quantitative generalisation of probabilistic bisimilarity introduced by Larsen and Skou a decade earlier. In the last decade, several algorithms to approximate and compute these probabilistic bisimilarity distances have been put forward. In this paper, we correct, improve and generalise some of these algorithms. Furthermore, we compare their performance experimentally.
Cite as
Qiyi Tang and Franck van Breugel. Algorithms to Compute Probabilistic Bisimilarity Distances for Labelled Markov Chains. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{tang_et_al:LIPIcs.CONCUR.2017.27,
author = {Tang, Qiyi and van Breugel, Franck},
title = {{Algorithms to Compute Probabilistic Bisimilarity Distances for Labelled Markov Chains}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {27:1--27:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.27},
URN = {urn:nbn:de:0030-drops-77983},
doi = {10.4230/LIPIcs.CONCUR.2017.27},
annote = {Keywords: labelled Markov chain, probabilistic bisimilarity, pseudometric, policy iteration}
}
Document
On Decidability of Concurrent Kleene Algebra
Abstract
Concurrent Kleene algebras support equational reasoning about
computing systems with concurrent behaviours. Their natural
semantics is given by series(-parallel) rational pomset languages, a
standard true concurrency semantics, which is often associated with
processes of Petri nets. We use constructions on Petri nets to
provide two decision procedures for such pomset languages motivated
by the equational and the refinement theory of concurrent Kleene
algebra. The contribution to the first problem lies in a much
simpler algorithm and an EXPSPACE complexity bound. Decidability
of the second, more interesting problem is new and, in fact,
EXPSPACE-complete.
Cite as
Paul Brunet, Damien Pous, and Georg Struth. On Decidability of Concurrent Kleene Algebra. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{brunet_et_al:LIPIcs.CONCUR.2017.28,
author = {Brunet, Paul and Pous, Damien and Struth, Georg},
title = {{On Decidability of Concurrent Kleene Algebra}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {28:1--28:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.28},
URN = {urn:nbn:de:0030-drops-77881},
doi = {10.4230/LIPIcs.CONCUR.2017.28},
annote = {Keywords: Concurrent Kleene algebra, series-parallel pomsets, Petri nets}
}
Document
Model-Checking Counting Temporal Logics on Flat Structures
Abstract
We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.
Cite as
Normann Decker, Peter Habermehl, Martin Leucker, Arnaud Sangnier, and Daniel Thoma. Model-Checking Counting Temporal Logics on Flat Structures. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{decker_et_al:LIPIcs.CONCUR.2017.29,
author = {Decker, Normann and Habermehl, Peter and Leucker, Martin and Sangnier, Arnaud and Thoma, Daniel},
title = {{Model-Checking Counting Temporal Logics on Flat Structures}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {29:1--29:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.29},
URN = {urn:nbn:de:0030-drops-77709},
doi = {10.4230/LIPIcs.CONCUR.2017.29},
annote = {Keywords: Counting Temporal Logic, Model checking, Flat Kripke Structure}
}
Document
Concurrent Reversible Sessions
Abstract
We present a calculus for concurrent reversible multiparty sessions, which improves on recent proposals in several respects: it allows for concurrent and sequential composition within processes and types, it gives a compact representation of the past of processes and types, which facilitates the definition of rollback, and it implements a fine-tuned strategy for backward computation. We propose a refined session type system for our calculus and show that it enforces the expected properties of session fidelity, forward and backward progress, as well as causal consistency. In conclusion, our calculus is a conservative extension of previous proposals, offering enhanced expressive power and refined analysis techniques.
Cite as
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Concurrent Reversible Sessions. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{castellani_et_al:LIPIcs.CONCUR.2017.30,
author = {Castellani, Ilaria and Dezani-Ciancaglini, Mariangiola and Giannini, Paola},
title = {{Concurrent Reversible Sessions}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {30:1--30:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.30},
URN = {urn:nbn:de:0030-drops-77877},
doi = {10.4230/LIPIcs.CONCUR.2017.30},
annote = {Keywords: Communication-centric Systems, Reversible Computation, Process Calculi, Multiparty Session Types}
}
Document
Unbounded Product-Form Petri Nets
Abstract
Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \Pi^3-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \Pi^3-nets to obtain the class of open \Pi^3-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \Pi^3-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.
Cite as
Patricia Bouyer, Serge Haddad, and Vincent Jugé. Unbounded Product-Form Petri Nets. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2017.31,
author = {Bouyer, Patricia and Haddad, Serge and Jug\'{e}, Vincent},
title = {{Unbounded Product-Form Petri Nets}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {31:1--31:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.31},
URN = {urn:nbn:de:0030-drops-77957},
doi = {10.4230/LIPIcs.CONCUR.2017.31},
annote = {Keywords: Performance evaluation, infinite-state systems, Petri nets, steady-state distribution}
}
Document
Efficient Coalgebraic Partition Refinement
Abstract
We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time O(m log n) where n and m are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems.
Cite as
Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient Coalgebraic Partition Refinement. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{dorsch_et_al:LIPIcs.CONCUR.2017.32,
author = {Dorsch, Ulrich and Milius, Stefan and Schr\"{o}der, Lutz and Wi{\ss}mann, Thorsten},
title = {{Efficient Coalgebraic Partition Refinement}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {32:1--32:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.32},
URN = {urn:nbn:de:0030-drops-77939},
doi = {10.4230/LIPIcs.CONCUR.2017.32},
annote = {Keywords: markov chains, deterministic finite automata, partition refinement, generic algorithm, paige-tarjan algorithm, transition systems}
}
Document
The Complexity of Flat Freeze LTL
Abstract
We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.
Cite as
Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The Complexity of Flat Freeze LTL. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bollig_et_al:LIPIcs.CONCUR.2017.33,
author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud},
title = {{The Complexity of Flat Freeze LTL}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {33:1--33:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.33},
URN = {urn:nbn:de:0030-drops-77993},
doi = {10.4230/LIPIcs.CONCUR.2017.33},
annote = {Keywords: one-counter automata, freeze LTL, model checking}
}
Document
Higher-Order Linearisability
Abstract
Linearisability is a central notion for verifying concurrent libraries: a library is proven correct if its operational history can be rearranged into a sequential one that satisfies a given specification.
Until now, linearisability has been examined for libraries in which method arguments and method results were of ground type.
In this paper we extend linearisability to the general higher-order setting, where methods of arbitrary type can be passed as arguments and returned as values, and establish its soundness.
Cite as
Andrzej S. Murawski and Nikos Tzevelekos. Higher-Order Linearisability. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{murawski_et_al:LIPIcs.CONCUR.2017.34,
author = {Murawski, Andrzej S. and Tzevelekos, Nikos},
title = {{Higher-Order Linearisability}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {34:1--34:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.34},
URN = {urn:nbn:de:0030-drops-78035},
doi = {10.4230/LIPIcs.CONCUR.2017.34},
annote = {Keywords: Linearisability, Concurrency, Higher-Order Computation}
}
Document
Model Checking Omega-regular Properties for Quantum Markov Chains
Abstract
Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking omega-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model.
For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking omega-regular properties for quantum Markov chains.
Cite as
Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying. Model Checking Omega-regular Properties for Quantum Markov Chains. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{feng_et_al:LIPIcs.CONCUR.2017.35,
author = {Feng, Yuan and Hahn, Ernst Moritz and Turrini, Andrea and Ying, Shenggang},
title = {{Model Checking Omega-regular Properties for Quantum Markov Chains}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {35:1--35:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.35},
URN = {urn:nbn:de:0030-drops-77818},
doi = {10.4230/LIPIcs.CONCUR.2017.35},
annote = {Keywords: Quantum Markov chains, model checking, omega-regular properties, bottom strongly connected component}
}
Document
Uniform Sampling for Networks of Automata
Abstract
We call network of automata a family of partially synchronised automata, i.e. a family of deterministic automata which are synchronised via shared letters, and evolve independently otherwise. We address the problem of uniform random sampling of words recognised by a network of automata.
To that purpose, we define the reduced automaton of the model, which involves only the product of the synchronised part of the component automata. We provide uniform sampling algorithms which are polynomial with respect to the size of the reduced automaton, greatly improving on the best known algorithms. Our sampling algorithms rely on combinatorial and probabilistic methods and are of three different types: exact, Boltzmann and Parry sampling.
Cite as
Nicolas Basset, Jean Mairesse, and Michèle Soria. Uniform Sampling for Networks of Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{basset_et_al:LIPIcs.CONCUR.2017.36,
author = {Basset, Nicolas and Mairesse, Jean and Soria, Mich\`{e}le},
title = {{Uniform Sampling for Networks of Automata}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {36:1--36:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.36},
URN = {urn:nbn:de:0030-drops-77977},
doi = {10.4230/LIPIcs.CONCUR.2017.36},
annote = {Keywords: Partially synchronised automata, uniform sampling; recursive method, Boltzmann sampling, Parry measure}
}
Document
Tractability of Separation Logic with Inductive Definitions: Beyond Lists
Abstract
In 2011, Cook et al. showed that the satisfiability and entailment can be checked in polynomial time for a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. In this paper, we investigate whether the tractability results can be extended to more expressive fragments of separation logic that allow defining data structures beyond linked lists. To this end, we introduce separation logic with a simply-nonlinear compositional inductive predicate where source, destination, and static parameters are identified explicitly (SLID[snc]). We show that if the inductive predicate has more than one source (destination) parameter, the satisfiability problem for SLID[snc] becomes intractable in general. This is exemplified by an inductive predicate for doubly linked list segments. By contrast, if the inductive predicate has only one source (destination) parameter, the satisfiability and entailment problems for SLID[snc] are tractable. In particular, the tractability results hold for inductive predicates that define list segments with tail pointers and trees with one hole.
Cite as
Taolue Chen, Fu Song, and Zhilin Wu. Tractability of Separation Logic with Inductive Definitions: Beyond Lists. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CONCUR.2017.37,
author = {Chen, Taolue and Song, Fu and Wu, Zhilin},
title = {{Tractability of Separation Logic with Inductive Definitions: Beyond Lists}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {37:1--37:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.37},
URN = {urn:nbn:de:0030-drops-77826},
doi = {10.4230/LIPIcs.CONCUR.2017.37},
annote = {Keywords: Separation logic, Inductive definitions, Satisfiability, Entailment}
}
Document
Data Multi-Pushdown Automata
Abstract
We extend the classical model of multi-pushdown systems by considering systems that operate on a finite set of variables ranging over natural numbers. The conditions on variables are defined via gap-order constraints that allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. Furthermore, each message inside a stack is equipped with a data item representing its value. When a message is pushed to the stack, its value may be defined by a variable. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in multiple dimensions, namely we have a number of stacks that may contain an unbounded number of messages each of which is equipped with a natural number.
It is well-known that the verification of any non-trivial property of multi-pushdown systems is undecidable, even for two stacks and for a finite data-domain. In this paper, we show the decidability of the reachability problem for the classes of data multi-pushdown system that admit a bounded split-width (or equivalently a bounded tree-width). As an immediate consequence, we obtain decidability for several subclasses of data multi-pushdown systems. These include systems with single stacks, restricted ordering policies on stack operations, bounded scope, bounded phase, and bounded context switches.
Cite as
Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig. Data Multi-Pushdown Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2017.38,
author = {Abdulla, Parosh Aziz and Aiswarya, C. and Atig, Mohamed Faouzi},
title = {{Data Multi-Pushdown Automata}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {38:1--38:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.38},
URN = {urn:nbn:de:0030-drops-78049},
doi = {10.4230/LIPIcs.CONCUR.2017.38},
annote = {Keywords: Pushdown Systems, Model-Checking, Gap-Order, Bounded Split-Width}
}
Document
Towards an Efficient Tree Automata Based Technique for Timed Systems
Abstract
The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.
Cite as
S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Ilias Sarkar. Towards an Efficient Tree Automata Based Technique for Timed Systems. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 39:1-39:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2017.39,
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias},
title = {{Towards an Efficient Tree Automata Based Technique for Timed Systems}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {39:1--39:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.39},
URN = {urn:nbn:de:0030-drops-78017},
doi = {10.4230/LIPIcs.CONCUR.2017.39},
annote = {Keywords: Timed automata, tree automata, pushdown systems, tree-width}
}
Document
On Petri Nets with Hierarchical Special Arcs
Abstract
We investigate the decidability of termination, reachability, coverability and deadlock-freeness of Petri nets endowed with a hierarchy of places, and with inhibitor arcs, reset arcs and transfer arcs that respect this hierarchy. We also investigate what happens when we have a mix of these special arcs, some of which respect the hierarchy, while others do not. We settle the decidability status of the above four problems for all combinations of hierarchy, inhibitor, reset and transfer arcs, except the termination problem for two combinations. For both these combinations, we show that deciding termination is as hard as deciding the positivity problem on linear recurrence sequences -- a long-standing open problem.
Cite as
S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath, and Sai Sandeep. On Petri Nets with Hierarchical Special Arcs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2017.40,
author = {Akshay, S. and Chakraborty, Supratik and Das, Ankush and Jagannath, Vishal and Sandeep, Sai},
title = {{On Petri Nets with Hierarchical Special Arcs}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {40:1--40:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Meyer, Roland and Nestmann, Uwe},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.40},
URN = {urn:nbn:de:0030-drops-78026},
doi = {10.4230/LIPIcs.CONCUR.2017.40},
annote = {Keywords: Petri Nets, Hierarchy, Reachability, Coverability, Termination, Positivity}
}