Volume
LIPIcs, Volume 118
29th International Conference on Concurrency Theory (CONCUR 2018)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2018, September 4-7, 2018, Beijing, ChinaEditors
Publication Details
- published at: 2018-08-31
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-087-3
- DBLP: db/conf/concur/concur2018
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 118, CONCUR'18, Complete Volume
Abstract
LIPIcs, Volume 118, CONCUR'18, Complete Volume
Cite as
29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Proceedings{schewe_et_al:LIPIcs.CONCUR.2018,
title = {{LIPIcs, Volume 118, CONCUR'18, Complete Volume}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018},
URN = {urn:nbn:de:0030-drops-97431},
doi = {10.4230/LIPIcs.CONCUR.2018},
annote = {Keywords: 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
29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 0:i-0:xxi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{schewe_et_al:LIPIcs.CONCUR.2018.0,
author = {Schewe, Sven and Zhang, Lijun},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {0:i--0:xxi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.0},
URN = {urn:nbn:de:0030-drops-95386},
doi = {10.4230/LIPIcs.CONCUR.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
The Siren Song of Temporal Synthesis (Invited Talk)
Abstract
One of the most significant developments in the area of design verification over the last three decade is the development of algorithmic methods for verifying temporal specification of finite-state designs. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal is to use temporal specification in the design development process in order to guarantee the development of correct designs. This is called temporal synthesis. In this talk I will review 60 years of research on the temporal synthesis problem, describe the automata-theoretic approach developed to solve this problem, and describe both successes and failures of this research program [Zhu et al., 2017a and 2017b].
Cite as
Moshe Y. Vardi. The Siren Song of Temporal Synthesis (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{vardi:LIPIcs.CONCUR.2018.1,
author = {Vardi, Moshe Y.},
title = {{The Siren Song of Temporal Synthesis}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.1},
URN = {urn:nbn:de:0030-drops-95393},
doi = {10.4230/LIPIcs.CONCUR.2018.1},
annote = {Keywords: Formal Methods, Temporal Synthesis}
}
Document
Invited Paper
Bisimulations for Probabilistic and Quantum Processes (Invited Paper)
Abstract
Bisimulation is a fundamental concept in the classical concurrency theory for comparing the behaviour of nondeterministic processes. It admits elegant characterisations from various perspectives such as fixed point theory, modal logics, game theory, coalgebras etc. In this paper, we review some key ideas used in the formulations and characterisations of reasonable notions of bisimulations for both probabilistic and quantum processes. To some extent the transition from probabilistic to quantum concurrency theory is smooth and natural. However, new ideas need also to be introduced. We have not yet reached the stage of formally verifying quantum communication protocols and quantum algorithms using bisimulations implemented by automatic tools. We discuss some recent efforts in this direction.
Cite as
Yuxin Deng. Bisimulations for Probabilistic and Quantum Processes (Invited Paper). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{deng:LIPIcs.CONCUR.2018.2,
author = {Deng, Yuxin},
title = {{Bisimulations for Probabilistic and Quantum Processes}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {2:1--2:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.2},
URN = {urn:nbn:de:0030-drops-95406},
doi = {10.4230/LIPIcs.CONCUR.2018.2},
annote = {Keywords: Bisimulations, probabilistic processes, quantum processes}
}
Document
Invited Talk
Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk)
Abstract
A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent.
In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however.
This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.
Cite as
Rob van Glabbeek. Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{vanglabbeek:LIPIcs.CONCUR.2018.3,
author = {van Glabbeek, Rob},
title = {{Is Speed-Independent Mutual Exclusion Implementable?}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.3},
URN = {urn:nbn:de:0030-drops-95415},
doi = {10.4230/LIPIcs.CONCUR.2018.3},
annote = {Keywords: Mutual exclusion, speed independence, concurrent reading and writing, liveness, justness}
}
Document
Invited Talk
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)
Abstract
Arithmetic over large finite fields is indispensable in modern cryptography. For efficienty, these operations are often implemented in manually optimized assembly programs. Since these arithmetic assembly programs necessarily perform lots of non-linear computation, checking their correctness is a challenging verification problem. We develop techniques to verify such programs automatically in this paper. Using our techniques, we have successfully verified a number of assembly programs in OpenSSL. Moreover, our tool verifies the boringSSL Montgomery Ladderstep (about 1400 assembly instructions) in 1 hour. This is by far the fastest verification technique for such programs.
Cite as
Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{polyakov_et_al:LIPIcs.CONCUR.2018.4,
author = {Polyakov, Andy and Tsai, Ming-Hsien and Wang, Bow-Yaw and Yang, Bo-Yin},
title = {{Verifying Arithmetic Assembly Programs in Cryptographic Primitives}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {4:1--4:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.4},
URN = {urn:nbn:de:0030-drops-95425},
doi = {10.4230/LIPIcs.CONCUR.2018.4},
annote = {Keywords: Formal verification, Cryptography, Assembly Programs}
}
Document
Invited Tutorial
Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial)
Abstract
Coalgebra is a categorical modeling of state-based dynamics. Final coalgebras - as categorical greatest fixed points - play a central role in the theory; somewhat analogously, most coalgebraic proof techniques have been devoted to greatest fixed-point properties such as safety and bisimilarity. In this tutorial, I introduce our recent coalgebraic framework that accommodates those fixed-point specifications which are not necessarily the greatest. It does so specifically by characterizing the accepted languages of Büchi and parity automata in categorical terms. We present two characterizations of accepted languages. The proof for their coincidence offers a unique categorical perspective of the correspondence between (logical) fixed-point specifications and the (combinatorial) parity acceptance condition.
Cite as
Ichiro Hasuo. Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{hasuo:LIPIcs.CONCUR.2018.5,
author = {Hasuo, Ichiro},
title = {{Coalgebraic Theory of B\"{u}chi and Parity Automata: Fixed-Point Specifications, Categorically}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {5:1--5:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.5},
URN = {urn:nbn:de:0030-drops-95430},
doi = {10.4230/LIPIcs.CONCUR.2018.5},
annote = {Keywords: Coalgebra, category theory, fixed-point logic, automata, B\"{u}chi automata, parity automata}
}
Document
Universal Safety for Timed Petri Nets is PSPACE-complete
Abstract
A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central controller, since all automata are initially identical. We consider the universal safety problem for such controller-less timed networks, i.e., verifying that a bad event (enabling some given transition) is impossible regardless of the size of the network.
This universal safety problem is dual to the existential coverability problem for timed-arc Petri nets, i.e., does there exist a number m of tokens, such that starting with m tokens in a given place, and none in the other places, some given transition is eventually enabled.
We show that these problems are PSPACE-complete.
Cite as
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke. Universal Safety for Timed Petri Nets is PSPACE-complete. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2018.6,
author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Ciobanu, Radu and Mayr, Richard and Totzke, Patrick},
title = {{Universal Safety for Timed Petri Nets is PSPACE-complete}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {6:1--6:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.6},
URN = {urn:nbn:de:0030-drops-95447},
doi = {10.4230/LIPIcs.CONCUR.2018.6},
annote = {Keywords: timed networks, safety checking, Petri nets, coverability}
}
Document
It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"
Abstract
Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.
Cite as
Benedikt Bollig, Marie Fortin, and Paul Gastin. It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before". In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bollig_et_al:LIPIcs.CONCUR.2018.7,
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {{It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.7},
URN = {urn:nbn:de:0030-drops-95455},
doi = {10.4230/LIPIcs.CONCUR.2018.7},
annote = {Keywords: communicating finite-state machines, first-order logic, happened-before relation}
}
Document
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints
Abstract
We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process (MDP) with unknown probabilistic transition function and unknown reward function. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we show that in MDPs consisting of a single end component, two combinations of guarantees on the parity and mean-payoff objectives can be achieved depending on how much memory one is willing to use. (i) For all epsilon and gamma we can construct an online-learning finite-memory strategy that almost-surely satisfies the parity objective and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. (ii) Alternatively, for all epsilon and gamma there exists an online-learning infinite-memory strategy that satisfies the parity objective surely and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. We extend the above results to MDPs consisting of more than one end component in a natural way. Finally, we show that the aforementioned guarantees are tight, i.e. there are MDPs for which stronger combinations of the guarantees cannot be ensured.
Cite as
Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin. Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2018.8,
author = {Kret{\'\i}nsk\'{y}, Jan and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
title = {{Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.8},
URN = {urn:nbn:de:0030-drops-95468},
doi = {10.4230/LIPIcs.CONCUR.2018.8},
annote = {Keywords: Markov decision processes, Reinforcement learning, Beyond worst case}
}
Document
Deciding Probabilistic Bisimilarity Distance One for Probabilistic Automata
Abstract
Probabilistic bisimilarity, due to Segala and Lynch, is an equivalence relation that captures which states of a probabilistic automaton behave exactly the same. Deng, Chothia, Palamidessi and Pang proposed a robust quantitative generalization of probabilistic bisimilarity. Their probabilistic bisimilarity distances of states of a probabilistic automaton capture the similarity of their behaviour. The smaller the distance, the more alike the states behave. In particular, states are probabilistic bisimilar if and only if their distance is zero.
Although the complexity of computing probabilistic bisimilarity distances for probabilistic automata has already been studied and shown to be in NP cap coNP and PPAD, we are not aware of any practical algorithm to compute those distances. In this paper we provide several key results towards algorithms to compute probabilistic bisimilarity distances for probabilistic automata. In particular, we present a polynomial time algorithm that decides distance one. Furthermore, we give an alternative characterization of the probabilistic bisimilarity distances as a basis for a policy iteration algorithm.
Cite as
Qiyi Tang and Franck van Breugel. Deciding Probabilistic Bisimilarity Distance One for Probabilistic Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{tang_et_al:LIPIcs.CONCUR.2018.9,
author = {Tang, Qiyi and van Breugel, Franck},
title = {{Deciding Probabilistic Bisimilarity Distance One for Probabilistic Automata}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.9},
URN = {urn:nbn:de:0030-drops-95472},
doi = {10.4230/LIPIcs.CONCUR.2018.9},
annote = {Keywords: probabilistic automaton, probabilistic bisimilarity, distance}
}
Document
Non-deterministic Weighted Automata on Random Words
Abstract
We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We consider the probabilistic questions of computing the expected value and the cumulative distribution for such random variables.
The exact answers to the probabilistic questions for non-deterministic automata can be irrational and are uncomputable in general. To overcome this limitation, we propose an approximation algorithm for the probabilistic questions, which works in exponential time in the automaton and polynomial time in the Markov chain. We apply this result to show that non-deterministic automata can be effectively determinised with respect to the standard deviation metric.
Cite as
Jakub Michaliszyn and Jan Otop. Non-deterministic Weighted Automata on Random Words. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{michaliszyn_et_al:LIPIcs.CONCUR.2018.10,
author = {Michaliszyn, Jakub and Otop, Jan},
title = {{Non-deterministic Weighted Automata on Random Words}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {10:1--10:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.10},
URN = {urn:nbn:de:0030-drops-95481},
doi = {10.4230/LIPIcs.CONCUR.2018.10},
annote = {Keywords: quantitative verification, weighted automata, expected value}
}
Document
Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies
Abstract
Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payoff games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.
Cite as
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Yaron Velner. Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2018.11,
author = {Chatterjee, Krishnendu and Kafshdar Goharshady, Amir and Ibsen-Jensen, Rasmus and Velner, Yaron},
title = {{Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {11:1--11:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.11},
URN = {urn:nbn:de:0030-drops-95497},
doi = {10.4230/LIPIcs.CONCUR.2018.11},
annote = {Keywords: Crypto-currency, Quantitative Verification, Mean-payoff Games}
}
Document
Bounded Context Switching for Valence Systems
Abstract
We study valence systems, finite-control programs over infinite-state memories modeled in terms of graph monoids. Our contribution is a notion of bounded context switching (BCS). Valence systems generalize pushdowns, concurrent pushdowns, and Petri nets. In these settings, our definition conservatively generalizes existing notions. The main finding is that reachability within a bounded number of context switches is in NPTIME, independent of the memory (the graph monoid). Our proof is genuinely algebraic, and therefore contributes a new way to think about BCS. In addition, we exhibit a class of storage mechanisms for which BCS reachability belongs to PTIME.
Cite as
Roland Meyer, Sebastian Muskalla, and Georg Zetzsche. Bounded Context Switching for Valence Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{meyer_et_al:LIPIcs.CONCUR.2018.12,
author = {Meyer, Roland and Muskalla, Sebastian and Zetzsche, Georg},
title = {{Bounded Context Switching for Valence Systems}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {12:1--12:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.12},
URN = {urn:nbn:de:0030-drops-95500},
doi = {10.4230/LIPIcs.CONCUR.2018.12},
annote = {Keywords: valence systems, graph monoids, bounded context switching}
}
Document
Alternating Nonzero Automata
Abstract
We introduce a new class of automata on infinite trees called alternating nonzero automata, which extends the class of non-deterministic nonzero automata. The emptiness problem for this class is still open, however we identify a subclass, namely limited choice, for which we reduce the emptiness problem for alternating nonzero automata to the same problem for non-deterministic ones, which implies decidability. We obtain, as corollaries, algorithms for the satisfiability of a probabilistic temporal logic extending both CTL* and the qualitative fragment of pCTL*.
Cite as
Paulin Fournier and Hugo Gimbert. Alternating Nonzero Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{fournier_et_al:LIPIcs.CONCUR.2018.13,
author = {Fournier, Paulin and Gimbert, Hugo},
title = {{Alternating Nonzero Automata}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {13:1--13:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.13},
URN = {urn:nbn:de:0030-drops-95517},
doi = {10.4230/LIPIcs.CONCUR.2018.13},
annote = {Keywords: zero-automata, probabilities, temporal logics}
}
Document
Affine Extensions of Integer Vector Addition Systems with States
Abstract
We study the reachability problem for affine Z-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine Z-VASS with the finite-monoid property (afmp-Z-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-Z-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-Z-VASS reduces to reachability in a Z-VASS whose control-states grow polynomially in the size of the matrix monoid. Our construction shows that reachability relations of afmp-Z-VASS are semilinear, and in particular enables us to show that reachability in Z-VASS with transfers and Z-VASS with copies is PSPACE-complete.
Cite as
Michael Blondin, Christoph Haase, and Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.14,
author = {Blondin, Michael and Haase, Christoph and Mazowiecki, Filip},
title = {{Affine Extensions of Integer Vector Addition Systems with States}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.14},
URN = {urn:nbn:de:0030-drops-95520},
doi = {10.4230/LIPIcs.CONCUR.2018.14},
annote = {Keywords: Vector addition systems, affine transformations, reachability, semilinear sets, computational complexity}
}
Document
Verifying Quantitative Temporal Properties of Procedural Programs
Abstract
We address the problem of specifying and verifying quantitative properties of procedural programs. These properties typically involve constraints on the relative cumulated costs of executing various tasks (by invoking for instance some particular procedures) within the scope of the execution of some particular procedure. An example of such properties is "within the execution of each invocation of procedure P, the time spent in executing invocations of procedure Q is less than 20 % of the total execution time". We introduce specification formalisms, both automata-based and logic-based, for expressing such properties, and we study the links between these formalisms and their application in model-checking. On one side, we define Constrained Pushdown Systems (CPDS), an extension of pushdown systems with constraints, expressed in Presburger arithmetics, on the numbers of occurrences of each symbol in the alphabet within invocation intervals (subcomputations between matching pushes and pops), and on the other side, we introduce a higher level specification language that is a quantitative extension of CaRet (the Call-Return temporal logic) called QCaRet where nested quantitative constraints over procedure invocation intervals are expressible using Presburger arithmetics. Then, we investigate (1) the decidability of the reachability and repeated reachability problems for CPDS, and (2) the effective reduction of the model-checking problem of procedural programs (modeled as visibly pushdown systems) against QCaRet formulas to these problems on CPDS.
Cite as
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verifying Quantitative Temporal Properties of Procedural Programs. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{atig_et_al:LIPIcs.CONCUR.2018.15,
author = {Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
title = {{Verifying Quantitative Temporal Properties of Procedural Programs}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.15},
URN = {urn:nbn:de:0030-drops-95531},
doi = {10.4230/LIPIcs.CONCUR.2018.15},
annote = {Keywords: Verification, Formal Methods, Pushdown systems, Visibly pushdown, Quantitative Temporal Properties}
}
Document
Narrowing down the Hardness Barrier of Synthesizing Elementary Net Systems
Abstract
Elementary net system feasibility is the problem to decide for a given automaton A if there is a certain boolean Petri net with a state graph isomorphic to A. This is equivalent to the conjunction of the state separation property (SSP) and the event state separation property (ESSP). Since feasibility, SSP and ESSP are known to be NP-complete in general, there was hope that the restriction of graph parameters for A can lead to tractable and practically relevant subclasses. In this paper, we analyze event manifoldness, the amount of occurrences that an event can have in A, and state degree, the number of allowed successors and predecessors of states in A, as natural input restrictions. Recently, it has been shown that all three decision problems, feasibility, SSP and ESSP, remain NP-complete for linear A where every event occurs at most three times. Here, we show that these problems remain hard even if every event occurs at most twice. Nevertheless, this has to be paid by relaxing the restriction on state degree, allowing every state to have two successor and two predecessor states. As we also show that SSP becomes tractable for linear A where every event occurs at most twice the only open cases left are ESSP and feasibilty for the same input restriction.
Cite as
Ronny Tredup and Christian Rosenke. Narrowing down the Hardness Barrier of Synthesizing Elementary Net Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{tredup_et_al:LIPIcs.CONCUR.2018.16,
author = {Tredup, Ronny and Rosenke, Christian},
title = {{Narrowing down the Hardness Barrier of Synthesizing Elementary Net Systems}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {16:1--16:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.16},
URN = {urn:nbn:de:0030-drops-95546},
doi = {10.4230/LIPIcs.CONCUR.2018.16},
annote = {Keywords: Elementary net systems, Petri net synthesis, NP-completeness, Parameterized Complexity}
}
Document
Up-To Techniques for Behavioural Metrics via Fibrations
Abstract
Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way.
In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.
Cite as
Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2018.17,
author = {Bonchi, Filippo and K\"{o}nig, Barbara and Petrisan, Daniela},
title = {{Up-To Techniques for Behavioural Metrics via Fibrations}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.17},
URN = {urn:nbn:de:0030-drops-95552},
doi = {10.4230/LIPIcs.CONCUR.2018.17},
annote = {Keywords: behavioural metrics, bisimilarity, up-to techniques, coalgebras, fibrations}
}
Document
Completeness for Identity-free Kleene Lattices
Abstract
We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.
Cite as
Amina Doumane and Damien Pous. Completeness for Identity-free Kleene Lattices. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{doumane_et_al:LIPIcs.CONCUR.2018.18,
author = {Doumane, Amina and Pous, Damien},
title = {{Completeness for Identity-free Kleene Lattices}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.18},
URN = {urn:nbn:de:0030-drops-95564},
doi = {10.4230/LIPIcs.CONCUR.2018.18},
annote = {Keywords: Kleene algebra, Graph languages, Petri Automata, Kleene theorem}
}
Document
Reachability in Parameterized Systems: All Flavors of Threshold Automata
Abstract
Threshold automata, and the counter systems they define, were introduced as a framework for parameterized model checking of fault-tolerant distributed algorithms. This application domain suggested natural constraints on the automata structure, and a specific form of acceleration, called single-rule acceleration: consecutive occurrences of the same automaton rule are executed as a single transition in the counter system. These accelerated systems have bounded diameter, and can be verified in a complete manner with bounded model checking.
We go beyond the original domain, and investigate extensions of threshold automata: non-linear guards, increments and decrements of shared variables, increments of shared variables within loops, etc., and show that the bounded diameter property holds for several extensions. Finally, we put single-rule acceleration in the scope of flat counter automata: although increments in loops may break the bounded diameter property, the corresponding counter automaton is flattable, and reachability can be verified using more permissive forms of acceleration.
Cite as
Jure Kukovec, Igor Konnov, and Josef Widder. Reachability in Parameterized Systems: All Flavors of Threshold Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kukovec_et_al:LIPIcs.CONCUR.2018.19,
author = {Kukovec, Jure and Konnov, Igor and Widder, Josef},
title = {{Reachability in Parameterized Systems: All Flavors of Threshold Automata}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.19},
URN = {urn:nbn:de:0030-drops-95578},
doi = {10.4230/LIPIcs.CONCUR.2018.19},
annote = {Keywords: threshold \& counter automata, parameterized verification, reachability}
}
Document
Selective Monitoring
Abstract
We study selective monitors for labelled Markov chains. Monitors observe the outputs that are generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty. A monitor is selective if it skips observations in order to reduce monitoring overhead. We are interested in monitors that minimize the expected number of observations. We establish an undecidability result for selectively monitoring general Markov chains. On the other hand, we show for non-hidden Markov chains (where any output identifies the state the Markov chain is in) that simple optimal monitors exist and can be computed efficiently, based on DFA language equivalence. These monitors do not depend on the precise transition probabilities in the Markov chain. We report on experiments where we compute these monitors for several open-source Java projects.
Cite as
Radu Grigore and Stefan Kiefer. Selective Monitoring. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{grigore_et_al:LIPIcs.CONCUR.2018.20,
author = {Grigore, Radu and Kiefer, Stefan},
title = {{Selective Monitoring}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {20:1--20:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.20},
URN = {urn:nbn:de:0030-drops-95586},
doi = {10.4230/LIPIcs.CONCUR.2018.20},
annote = {Keywords: runtime monitoring, probabilistic systems, Markov chains, automata, language equivalence}
}
Document
Synchronizing the Asynchronous
Abstract
Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs.
Cite as
Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. Synchronizing the Asynchronous. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kragl_et_al:LIPIcs.CONCUR.2018.21,
author = {Kragl, Bernhard and Qadeer, Shaz and Henzinger, Thomas A.},
title = {{Synchronizing the Asynchronous}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {21:1--21:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.21},
URN = {urn:nbn:de:0030-drops-95591},
doi = {10.4230/LIPIcs.CONCUR.2018.21},
annote = {Keywords: concurrent programs, asynchronous programs, deductive verification, refinement, synchronization, mover types, atomic action, commutativity, Lipton reduction}
}
Document
A Semantics for Hybrid Iteration
Abstract
The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations. As a starting point we use an available notion of hybrid monad restricted to the category of sets, and modify it in order to obtain a suitable notion of guarded iteration with guardedness interpreted as progressiveness in time - we motivate this modification by our intention to capture Zeno behaviour in an arguably general and feasible way. We illustrate our results with a simple programming language for hybrid computations and interpret it over the developed semantic foundations.
Cite as
Sergey Goncharov, Julian Jakob, and Renato Neves. A Semantics for Hybrid Iteration. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{goncharov_et_al:LIPIcs.CONCUR.2018.22,
author = {Goncharov, Sergey and Jakob, Julian and Neves, Renato},
title = {{A Semantics for Hybrid Iteration}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {22:1--22:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.22},
URN = {urn:nbn:de:0030-drops-95604},
doi = {10.4230/LIPIcs.CONCUR.2018.22},
annote = {Keywords: Elgot iteration, guarded iteration, hybrid monad, Zeno behaviour}
}
Document
GPU Schedulers: How Fair Is Fair Enough?
Abstract
Blocking synchronisation idioms, e.g. mutexes and barriers, play an important role in concurrent programming. However, systems with semi-fair schedulers, e.g. graphics processing units (GPUs), are becoming increasingly common. Such schedulers provide varying degrees of fairness, guaranteeing enough to allow some, but not all, blocking idioms. While a number of applications that use blocking idioms do run on today's GPUs, reasoning about liveness properties of such applications is difficult as documentation is scarce and scattered.
In this work, we aim to clarify fairness properties of semi-fair schedulers. To do this, we define a general temporal logic formula, based on weak fairness, parameterised by a predicate that enables fairness per-thread at certain points of an execution. We then define fairness properties for three GPU schedulers: HSA, OpenCL, and occupancy-bound execution. We examine existing GPU applications and show that none of the above schedulers are strong enough to provide the fairness properties required by these applications. It hence appears that existing GPU scheduler descriptions do not entirely capture the fairness properties that are provided on current GPUs. Thus, we present two new schedulers that aim to support existing GPU applications. We analyse the behaviour of common blocking idioms under each scheduler and show that one of our new schedulers allows a more natural implementation of a GPU protocol.
Cite as
Tyler Sorensen, Hugues Evrard, and Alastair F. Donaldson. GPU Schedulers: How Fair Is Fair Enough?. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{sorensen_et_al:LIPIcs.CONCUR.2018.23,
author = {Sorensen, Tyler and Evrard, Hugues and Donaldson, Alastair F.},
title = {{GPU Schedulers: How Fair Is Fair Enough?}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.23},
URN = {urn:nbn:de:0030-drops-95619},
doi = {10.4230/LIPIcs.CONCUR.2018.23},
annote = {Keywords: GPU scheduling, Blocking synchronisation, GPU semantics}
}
Document
Linear Equations with Ordered Data
Abstract
Following a recently considered generalization of linear equations to unordered data vectors, we perform a further generalization to ordered data vectors. These generalized equations naturally appear in the analysis of vector addition systems (or Petri nets) extended with ordered data. We show that nonnegative-integer solvability of linear equations is computationally equivalent (up to an exponential blowup) to the reachability problem for (plain) vector addition systems. This high complexity is surprising, and contrasts with NP-completeness for unordered data vectors. This also contrasts with our second result, namely polynomial time complexity of the solvability problem when the nonnegative-integer restriction on solutions is relaxed.
Cite as
Piotr Hofman and Slawomir Lasota. Linear Equations with Ordered Data. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{hofman_et_al:LIPIcs.CONCUR.2018.24,
author = {Hofman, Piotr and Lasota, Slawomir},
title = {{Linear Equations with Ordered Data}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {24:1--24:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.24},
URN = {urn:nbn:de:0030-drops-95624},
doi = {10.4230/LIPIcs.CONCUR.2018.24},
annote = {Keywords: Linear equations, Petri nets, Petri nets with data, vector addition systems, sets with atoms, orbit-finite sets}
}
Document
A Coalgebraic Take on Regular and omega-Regular Behaviour for Systems with Internal Moves
Abstract
We present a general coalgebraic setting in which we define finite and infinite behaviour with Büchi acceptance condition for systems with internal moves. Since systems with internal moves are defined here as coalgebras for a monad, in the first part of the paper we present a construction of a monad suitable for modelling (in)finite behaviour. The second part of the paper focuses on presenting the concepts of a (coalgebraic) automaton and its (omega-) behaviour. We end the paper with coalgebraic Kleene-type theorems for (omega-) regular input. We discuss the setting in the context of non-deterministic (tree) automata and Segala automata.
Cite as
Tomasz Brengos. A Coalgebraic Take on Regular and omega-Regular Behaviour for Systems with Internal Moves. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{brengos:LIPIcs.CONCUR.2018.25,
author = {Brengos, Tomasz},
title = {{A Coalgebraic Take on Regular and omega-Regular Behaviour for Systems with Internal Moves}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {25:1--25:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.25},
URN = {urn:nbn:de:0030-drops-95632},
doi = {10.4230/LIPIcs.CONCUR.2018.25},
annote = {Keywords: coalgebras, regular languages, omega regular languages, automata, B\"{u}chi automata, silent moves, internal moves, monads, saturation}
}
Document
Relating Syntactic and Semantic Perturbations of Hybrid Automata
Abstract
We investigate how the semantics of a hybrid automaton deviates with respect to syntactic perturbations on the hybrid automaton. We consider syntactic perturbations of a hybrid automaton, wherein the syntactic representations of its elements, namely, initial sets, invariants, guards, and flows, in some logic are perturbed. Our main result establishes a continuity like property that states that small perturbations in the syntax lead to small perturbations in the semantics. More precisely, we show that for every real number epsilon>0 and natural number k, there is a real number delta>0 such that H^delta, the delta syntactic perturbation of a hybrid automaton H, is epsilon-simulation equivalent to H up to k transition steps. As a byproduct, we obtain a proof that a bounded safety verification tool such as dReach will eventually prove the safety of a safe hybrid automaton design (when only non-strict inequalities are used in all constraints) if dReach iteratively reduces the syntactic parameter delta that is used in checking approximate satisfiability. This has an immediate application in counter-example validation in a CEGAR framework, namely, when a counter-example is spurious, then we have a complete procedure for deducing the same.
Cite as
Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. Relating Syntactic and Semantic Perturbations of Hybrid Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{roohi_et_al:LIPIcs.CONCUR.2018.26,
author = {Roohi, Nima and Prabhakar, Pavithra and Viswanathan, Mahesh},
title = {{Relating Syntactic and Semantic Perturbations of Hybrid Automata}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {26:1--26:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.26},
URN = {urn:nbn:de:0030-drops-95644},
doi = {10.4230/LIPIcs.CONCUR.2018.26},
annote = {Keywords: Model Checking, Hybrid Automata, Approximation, Perturbation}
}
Document
Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks
Abstract
The paper extends Bayesian networks (BNs) by a mechanism for dynamic changes to the probability distributions represented by BNs. One application scenario is the process of knowledge acquisition of an observer interacting with a system. In particular, the paper considers condition/event nets where the observer's knowledge about the current marking is a probability distribution over markings. The observer can interact with the net to deduce information about the marking by requesting certain transitions to fire and observing their success or failure.
Aiming for an efficient implementation of dynamic changes to probability distributions of BNs, we consider a modular form of networks that form the arrows of a free PROP with a commutative comonoid structure, also known as term graphs. The algebraic structure of such PROPs supplies us with a compositional semantics that functorially maps BNs to their underlying probability distribution and, in particular, it provides a convenient means to describe structural updates of networks.
Cite as
Benjamin Cabrera, Tobias Heindel, Reiko Heckel, and Barbara König. Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{cabrera_et_al:LIPIcs.CONCUR.2018.27,
author = {Cabrera, Benjamin and Heindel, Tobias and Heckel, Reiko and K\"{o}nig, Barbara},
title = {{Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {27:1--27:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.27},
URN = {urn:nbn:de:0030-drops-95659},
doi = {10.4230/LIPIcs.CONCUR.2018.27},
annote = {Keywords: Petri nets, Bayesian networks, Probabilistic databases, Condition/Event nets, Probabilistic knowledge, Dynamic probability distributions}
}
Document
Reachability in Timed Automata with Diagonal Constraints
Abstract
We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called "zones". Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.
Cite as
Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in Timed Automata with Diagonal Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gastin_et_al:LIPIcs.CONCUR.2018.28,
author = {Gastin, Paul and Mukherjee, Sayan and Srivathsan, B.},
title = {{Reachability in Timed Automata with Diagonal Constraints}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.28},
URN = {urn:nbn:de:0030-drops-95660},
doi = {10.4230/LIPIcs.CONCUR.2018.28},
annote = {Keywords: Timed Automata, Reachability, Zones, Diagonal constraints}
}
Document
Parameterized complexity of games with monotonically ordered omega-regular objectives
Abstract
In recent years, two-player zero-sum games with multiple objectives have received a lot of interest as a model for the synthesis of complex reactive systems. In this framework, Player 1 wins if he can ensure that all objectives are satisfied against any behavior of Player 2. When this is not possible to satisfy all the objectives at once, an alternative is to use some preorder on the objectives according to which subset of objectives Player 1 wants to satisfy. For example, it is often natural to provide more significance to one objective over another, a situation that can be modelled with lexicographically ordered objectives for instance. Inspired by recent work on concurrent games with multiple omega-regular objectives by Bouyer et al., we investigate in detail turned-based games with monotonically ordered and omega-regular objectives. We study the threshold problem which asks whether player 1 can ensure a payoff greater than or equal to a given threshold w.r.t. a given monotonic preorder. As the number of objectives is usually much smaller than the size of the game graph, we provide a parametric complexity analysis and we show that our threshold problem is in FPT for all monotonic preorders and all classical types of omega-regular objectives. We also provide polynomial time algorithms for Büchi, coBüchi and explicit Muller objectives for a large subclass of monotonic preorders that includes among others the lexicographic preorder. In the particular case of lexicographic preorder, we also study the complexity of computing the values and the memory requirements of optimal strategies.
Cite as
Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. Parameterized complexity of games with monotonically ordered omega-regular objectives. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2018.29,
author = {Bruy\`{e}re, V\'{e}ronique and Hautem, Quentin and Raskin, Jean-Fran\c{c}ois},
title = {{Parameterized complexity of games with monotonically ordered omega-regular objectives}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {29:1--29:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.29},
URN = {urn:nbn:de:0030-drops-95673},
doi = {10.4230/LIPIcs.CONCUR.2018.29},
annote = {Keywords: two-player zero-sum games played on graphs, omega-regular objectives, ordered objectives, parameterized complexity}
}
Document
A Universal Session Type for Untyped Asynchronous Communication
Abstract
In the simply-typed lambda-calculus we can recover the full range of expressiveness of the untyped lambda-calculus solely by adding a single recursive type U = U -> U. In contrast, in the session-typed pi-calculus, recursion alone is insufficient to recover the untyped pi-calculus, primarily due to linearity: each channel just has two unique endpoints. In this paper, we show that shared channels with a corresponding sharing semantics (based on the language SILL_S developed in prior work) are enough to embed the untyped asynchronous pi-calculus via a universal shared session type U_S. We show that our encoding of the asynchronous pi-calculus satisfies operational correspondence and preserves observable actions (i.e., processes are weakly bisimilar to their encoding). Moreover, we clarify the expressiveness of SILL_S by developing an operationally correct encoding of SILL_S in the asynchronous pi-calculus.
Cite as
Stephanie Balzer, Frank Pfenning, and Bernardo Toninho. A Universal Session Type for Untyped Asynchronous Communication. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{balzer_et_al:LIPIcs.CONCUR.2018.30,
author = {Balzer, Stephanie and Pfenning, Frank and Toninho, Bernardo},
title = {{A Universal Session Type for Untyped Asynchronous Communication}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {30:1--30:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.30},
URN = {urn:nbn:de:0030-drops-95681},
doi = {10.4230/LIPIcs.CONCUR.2018.30},
annote = {Keywords: Session types, sharing, pi-calculus, bisimulation}
}
Document
Verification of Immediate Observation Population Protocols
Abstract
Population protocols (Angluin et al., PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint.
A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value.
In a previous paper we have shown that the problem whether a given protocol is well-specified and the problem whether it computes a given predicate are decidable. However, in the same paper we prove that both problems are at least as hard as the reachability problem for Petri nets. Since all known algorithms for Petri net reachability have non-primitive recursive complexity, in this paper we restrict attention to immediate observation (IO) population protocols, a class introduced and studied in (Angluin et al., PODC, 2006). We show that both problems are solvable in exponential space for IO protocols. This is the first syntactically defined, interesting class of protocols for which an algorithm not requiring Petri net reachability is found.
Cite as
Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy. Verification of Immediate Observation Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{esparza_et_al:LIPIcs.CONCUR.2018.31,
author = {Esparza, Javier and Ganty, Pierre and Majumdar, Rupak and Weil-Kennedy, Chana},
title = {{Verification of Immediate Observation Population Protocols}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {31:1--31:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.31},
URN = {urn:nbn:de:0030-drops-95695},
doi = {10.4230/LIPIcs.CONCUR.2018.31},
annote = {Keywords: Population protocols, Immediate Observation, Parametrized verification}
}
Document
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
Abstract
We investigate the satisfiability and finite satisfiability problem for probabilistic computation-tree logic (PCTL) where operators are not restricted by any step bounds. We establish decidability for several fragments containing quantitative operators and pinpoint the difficulties arising in more complex fragments where the decidability remains open.
Cite as
Jan Kretínský and Alexej Rotar. The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2018.32,
author = {Kret{\'\i}nsk\'{y}, Jan and Rotar, Alexej},
title = {{The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {32:1--32:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.32},
URN = {urn:nbn:de:0030-drops-95708},
doi = {10.4230/LIPIcs.CONCUR.2018.32},
annote = {Keywords: temporal logic, probabilistic verification, probabilistic computation tree logic, satisfiability}
}
Document
Automatic Analysis of Expected Termination Time for Population Protocols
Abstract
Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random.
In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.
Cite as
Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.33,
author = {Blondin, Michael and Esparza, Javier and Kucera, Anton{\'\i}n},
title = {{Automatic Analysis of Expected Termination Time for Population Protocols}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {33:1--33:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.33},
URN = {urn:nbn:de:0030-drops-95711},
doi = {10.4230/LIPIcs.CONCUR.2018.33},
annote = {Keywords: population protocols, performance analysis, expected termination time}
}
Document
On Runtime Enforcement via Suppressions
Abstract
Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime. We study the enforceability of Hennessy-Milner Logic with Recursion (muHML) with respect to suppression enforcement. We develop an operational framework for enforcement which we then use to formalise when a monitor enforces a muHML property. We also show that the safety syntactic fragment of the logic, sHML, is enforceable by providing an automated synthesis function that generates correct suppression monitors from sHML formulas.
Cite as
Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir. On Runtime Enforcement via Suppressions. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2018.34,
author = {Aceto, Luca and Cassar, Ian and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
title = {{On Runtime Enforcement via Suppressions}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {34:1--34:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.34},
URN = {urn:nbn:de:0030-drops-95729},
doi = {10.4230/LIPIcs.CONCUR.2018.34},
annote = {Keywords: Enforceability, Suppression Enforcement, Monitor Synthesis, Logic}
}
Document
Regular Separability of Well-Structured Transition Systems
Abstract
We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.
Cite as
Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2018.35,
author = {Czerwinski, Wojciech and Lasota, Slawomir and Meyer, Roland and Muskalla, Sebastian and Narayan Kumar, K. and Saivasan, Prakash},
title = {{Regular Separability of Well-Structured Transition Systems}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {35:1--35:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.35},
URN = {urn:nbn:de:0030-drops-95733},
doi = {10.4230/LIPIcs.CONCUR.2018.35},
annote = {Keywords: regular separability, wsts, coverability languages, Petri nets}
}
Document
Separable GPL: Decidable Model Checking with More Non-Determinism
Abstract
Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of branching probabilistic systems. We consider GPL over branching systems that also exhibit internal non-determinism under linear-time semantics (which is resolved by schedulers), and focus on the problem of finding the capacity (supremum probability over all schedulers) of a fuzzy formula. Model checking GPL is undecidable, in general, over such systems, and existing GPL model checking algorithms are limited to systems without internal non-determinism, or to checking non-recursive formulae. We define a subclass, called separable GPL, which includes recursive formulae and for which model checking is decidable. A large class of interesting and decidable problems, such as termination of 1-exit Recursive MDPs, reachability of Branching MDPs, and LTL model checking of MDPs, whose decidability has been studied independently, can be reduced to model checking separable GPL. Thus, GPL is widely applicable and, with a suitable extension of its semantics, yields a uniform framework for studying problems involving systems with non-deterministic and probabilistic behaviors.
Cite as
Andrey Gorlin and C. R. Ramakrishnan. Separable GPL: Decidable Model Checking with More Non-Determinism. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gorlin_et_al:LIPIcs.CONCUR.2018.36,
author = {Gorlin, Andrey and Ramakrishnan, C. R.},
title = {{Separable GPL: Decidable Model Checking with More Non-Determinism}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {36:1--36:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.36},
URN = {urn:nbn:de:0030-drops-95743},
doi = {10.4230/LIPIcs.CONCUR.2018.36},
annote = {Keywords: Modal mu-calculus, probabilistic logics, probabilistic systems, branching systems, model checking}
}
Document
(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras
Abstract
Behavioural equivalences can be characterized via bisimulations, modal logics and spoiler-defender games. In this paper we review these three perspectives in a coalgebraic setting, which allows us to generalize from the particular branching type of a transition system. We are interested in qualitative notions (classical bisimulation) as well as quantitative notions (bisimulation metrics).
Our first contribution is to introduce a spoiler-defender bisimulation game for coalgebras in the classical case. Second, we introduce such games for the metric case and furthermore define a real-valued modal coalgebraic logic, from which we can derive the strategy of the spoiler. For this logic we show a quantitative version of the Hennessy-Milner theorem.
Cite as
Barbara König and Christina Mika-Michalski. (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{konig_et_al:LIPIcs.CONCUR.2018.37,
author = {K\"{o}nig, Barbara and Mika-Michalski, Christina},
title = {{(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {37:1--37:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.37},
URN = {urn:nbn:de:0030-drops-95757},
doi = {10.4230/LIPIcs.CONCUR.2018.37},
annote = {Keywords: coalgebra, bisimulation games, spoiler-defender games, behavioural metrics, modal logic}
}
Document
The Complexity of Rational Synthesis for Concurrent Games
Abstract
In this paper, we investigate the rational synthesis problem for concurrent game structures for a variety of objectives ranging from reachability to Muller condition. We propose a new algorithm that establishes the decidability of the non cooperative rational synthesis problem that relies solely on game theoretic techniques as opposed to previous approaches that are logic based. Given an instance of the rational synthesis problem, we construct a zero-sum turn-based game that can be adapted to each one of the class of objectives. We obtain new complexity results. In particular, we show that in the cases of reachability, safety, Büchi, and co-Büchi objectives the problem is in PSpace, providing a tight upper-bound to the PSpace-hardness already established for turn-based games. In the case of Muller objective the problem is in ExpTime. We also obtain positive results when we assume a fixed number of agents, in which case the problem falls into PTime for reachability, safety, Büchi, and co-Büchi objectives.
Cite as
Rodica Condurache, Youssouf Oualhadj, and Nicolas Troquard. The Complexity of Rational Synthesis for Concurrent Games. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 38:1-38:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{condurache_et_al:LIPIcs.CONCUR.2018.38,
author = {Condurache, Rodica and Oualhadj, Youssouf and Troquard, Nicolas},
title = {{The Complexity of Rational Synthesis for Concurrent Games}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {38:1--38:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.38},
URN = {urn:nbn:de:0030-drops-95766},
doi = {10.4230/LIPIcs.CONCUR.2018.38},
annote = {Keywords: Synthesis, concurrent games, Nash equilibria}
}
Document
Logics Meet 1-Clock Alternating Timed Automata
Abstract
This paper investigates a decidable and highly expressive real time logic QkMSO which is obtained by extending MSO[<] with guarded quantification using block of less than k metric quantifiers. The resulting logic is shown to be expressively equivalent to 1-clock ATA where loops are without clock resets, as well as, RatMTL, a powerful extension of MTL[U_I] with regular expressions. We also establish 4-variable property for QkMSO and characterize the expressive power of its 2-variable fragment. Thus, the paper presents progress towards expressively complete logics for 1-clock ATA.
Cite as
Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Logics Meet 1-Clock Alternating Timed Automata. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{krishna_et_al:LIPIcs.CONCUR.2018.39,
author = {Krishna, Shankara Narayanan and Madnani, Khushraj and Pandya, Paritosh K.},
title = {{Logics Meet 1-Clock Alternating Timed Automata}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {39:1--39:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.39},
URN = {urn:nbn:de:0030-drops-95779},
doi = {10.4230/LIPIcs.CONCUR.2018.39},
annote = {Keywords: Metric Temporal Logic, Alternating Timed Automata, MSO, Regular Expressions, Expressive Completeness}
}
Document
Progress-Preserving Refinements of CTA
Abstract
We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints - in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems, such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.
Cite as
Massimo Bartoletti, Laura Bocchi, and Maurizio Murgia. Progress-Preserving Refinements of CTA. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bartoletti_et_al:LIPIcs.CONCUR.2018.40,
author = {Bartoletti, Massimo and Bocchi, Laura and Murgia, Maurizio},
title = {{Progress-Preserving Refinements of CTA}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {40:1--40:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.40},
URN = {urn:nbn:de:0030-drops-95786},
doi = {10.4230/LIPIcs.CONCUR.2018.40},
annote = {Keywords: protocol implementation, communicating timed automata, message passing}
}
Document
Automated Detection of Serializability Violations Under Weak Consistency
Abstract
While a number of weak consistency mechanisms have been developed in recent years to improve performance and ensure availability in distributed, replicated systems, ensuring the correctness of transactional applications running on top of such systems remains a difficult and important problem. Serializability is a well-understood correctness criterion for transactional programs; understanding whether applications are serializable when executed in a weakly-consistent environment, however remains a challenging exercise. In this work, we combine a dependency graph-based characterization of serializability and leverage the framework of abstract executions to develop a fully-automated approach for statically finding bounded serializability violations under any weak consistency model. We reduce the problem of serializability to satisfiability of a formula in First-Order Logic (FOL), which allows us to harness the power of existing SMT solvers. We provide rules to automatically construct the FOL encoding from programs written in SQL (allowing loops and conditionals) and express consistency specifications as FOL formula. In addition to detecting bounded serializability violations, we also provide two orthogonal schemes to reason about unbounded executions by providing sufficient conditions (again, in the form of FOL formulae) whose satisfiability implies the absence of anomalies in any arbitrary execution. We have applied the proposed technique on TPC-C, a real-world database program with complex application logic, and were able to discover anomalies under Parallel Snapshot Isolation (PSI), and verify serializability for unbounded executions under Snapshot Isolation (SI), two consistency mechanisms substantially weaker than serializability.
Cite as
Kartik Nagar and Suresh Jagannathan. Automated Detection of Serializability Violations Under Weak Consistency. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{nagar_et_al:LIPIcs.CONCUR.2018.41,
author = {Nagar, Kartik and Jagannathan, Suresh},
title = {{Automated Detection of Serializability Violations Under Weak Consistency}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {41:1--41:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.41},
URN = {urn:nbn:de:0030-drops-95799},
doi = {10.4230/LIPIcs.CONCUR.2018.41},
annote = {Keywords: Weak Consistency, Serializability, Database Applications}
}
Document
Effective Divergence Analysis for Linear Recurrence Sequences
Abstract
We study the growth behaviour of rational linear recurrence sequences. We show that for low-order sequences, divergence is decidable in polynomial time. We also exhibit a polynomial-time algorithm which takes as input a divergent rational linear recurrence sequence and computes effective fine-grained lower bounds on the growth rate of the sequence.
Cite as
Shaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, and James Worrell. Effective Divergence Analysis for Linear Recurrence Sequences. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 42:1-42:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2018.42,
author = {Almagor, Shaull and Chapman, Brynmor and Hosseini, Mehran and Ouaknine, Jo\"{e}l and Worrell, James},
title = {{Effective Divergence Analysis for Linear Recurrence Sequences}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {42:1--42:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Schewe, Sven and Zhang, Lijun},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.42},
URN = {urn:nbn:de:0030-drops-95802},
doi = {10.4230/LIPIcs.CONCUR.2018.42},
annote = {Keywords: Linear recurrence sequences, Divergence, Algebraic numbers, Positivity}
}