<div class="csl-bib-body">
<div class="csl-entry">Chatterjee, K., Dvorak, W., Henzinger, M., & Svozil, A. (2019). Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs. In W. Fokkink & R. van Glabbeek (Eds.), <i>30th International Conference on Concurrency Theory, {CONCUR} 2019</i> (pp. 7:1-7:16). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2019.7</div>
</div>
-
dc.identifier.isbn
978-3-95977-121-4
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/57869
-
dc.description.abstract
The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often.
All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification.
Consider graphs/MDPs with n vertices, m edges, and a Streett objective with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants.
The current best-known algorithm for the problem requires time O(min(n^2, m sqrt(m log n)) + b log n). In this work, we present randomized near-linear time algorithms, with expected running time \widetilde{O}(m + b), where the \widetilde{O} notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors.
en
dc.language.iso
en
-
dc.publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)
-
dc.title
Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs
en
dc.type
Konferenzbeitrag
de
dc.type
Inproceedings
en
dc.relation.publication
30th International Conference on Concurrency Theory, {CONCUR} 2019
-
dc.relation.isbn
978-3-95977-121-4
-
dc.relation.issn
1868-8969
-
dc.description.startpage
7:1
-
dc.description.endpage
7:16
-
dc.type.category
Full-Paper Contribution
-
dc.publisher.place
140
-
tuw.booktitle
30th International Conference on Concurrency Theory, {CONCUR} 2019
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
-
tuw.relation.publisherplace
Dagstuhl
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-02 - Forschungsbereich Databases and Artificial Intelligence
-
tuw.publisher.doi
10.4230/LIPIcs.CONCUR.2019.7
-
dc.description.numberOfPages
16
-
tuw.event.name
CONCUR 2019 - The 30th International Conference on Concurrency Theory
-
tuw.event.startdate
26-08-2019
-
tuw.event.enddate
31-08-2019
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Amsterdam
-
tuw.event.country
NL
-
tuw.event.presenter
Chatterjee, Krishnendu
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.facultyfocus
Logic and Computation (LC)
de
wb.facultyfocus
Logic and Computation (LC)
en
wb.facultyfocus.faculty
E180
-
wb.presentation.type
science to science/art to art
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
crisitem.author.dept
E192-02 - Forschungsbereich Databases and Artificial Intelligence