License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2019.37
URN: urn:nbn:de:0030-drops-115993
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11599/
Chini, Peter ;
Meyer, Roland ;
Saivasan, Prakash
Complexity of Liveness in Parameterized Systems
Abstract
We investigate the fine-grained complexity of liveness verification for leader contributor systems. These consist of a designated leader thread and an arbitrary number of identical contributor threads communicating via a shared memory. The liveness verification problem asks whether there is an infinite computation of the system in which the leader reaches a final state infinitely often. Like its reachability counterpart, the problem is known to be NP-complete. Our results show that, even from a fine-grained point of view, the complexities differ only by a polynomial factor.
Liveness verification decomposes into reachability and cycle detection. We present a fixed point iteration solving the latter in polynomial time. For reachability, we reconsider the two standard parameterizations. When parameterized by the number of states of the leader L and the size of the data domain D, we show an (L + D)^O(L + D)-time algorithm. It improves on a previous algorithm, thereby settling an open problem. When parameterized by the number of states of the contributor C, we reuse an O^*(2^C)-time algorithm. We show how to connect both algorithms with the cycle detection to obtain algorithms for liveness verification. The running times of the composed algorithms match those of reachability, proving that the fine-grained lower bounds for liveness verification are met.
BibTeX - Entry
@InProceedings{chini_et_al:LIPIcs:2019:11599,
author = {Peter Chini and Roland Meyer and Prakash Saivasan},
title = {{Complexity of Liveness in Parameterized Systems}},
booktitle = {39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
pages = {37:1--37:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-131-3},
ISSN = {1868-8969},
year = {2019},
volume = {150},
editor = {Arkadev Chattopadhyay and Paul Gastin},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2019/11599},
URN = {urn:nbn:de:0030-drops-115993},
doi = {10.4230/LIPIcs.FSTTCS.2019.37},
annote = {Keywords: Liveness Verification, Fine-Grained Complexity, Parameterized Systems}
}
|
Keywords: |
|
Liveness Verification, Fine-Grained Complexity, Parameterized Systems |
|
Collection: |
|
39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019) |
|
Issue Date: |
|
2019 |
|
Date of publication: |
|
04.12.2019 |
