---
res:
bibo_abstract:
- A model of computation that is widely used in the formal analysis of reactive
systems is symbolic algorithms. In this model the access to the input graph is
restricted to consist of symbolic operations, which are expensive in comparison
to the standard RAM operations. We give lower bounds on the number of symbolic
operations for basic graph problems such as the computation of the strongly connected
components and of the approximate diameter as well as for fundamental problems
in model checking such as safety, liveness, and coliveness. Our lower bounds are
linear in the number of vertices of the graph, even for constant-diameter graphs.
For none of these problems lower bounds on the number of symbolic operations were
known before. The lower bounds show an interesting separation of these problems
from the reachability problem, which can be solved with O(D) symbolic operations,
where D is the diameter of the graph. Additionally we present an approximation
algorithm for the graph diameter which requires Õ(n/D) symbolic steps to achieve
a (1 +ϵ)-approximation for any constant > 0. This compares to O(n/D) symbolic
steps for the (naive) exact algorithm and O(D) symbolic steps for a 2-approximation.
Finally we also give a refined analysis of the strongly connected components algorithms
of [15], showing that it uses an optimal number of symbolic steps that is proportional
to the sum of the diameters of the strongly connected components.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Wolfgang
foaf_name: Dvorák, Wolfgang
foaf_surname: Dvorák
- foaf_Person:
foaf_givenName: Monika H
foaf_name: Henzinger, Monika H
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=540c9bbd-f2de-11ec-812d-d04a5be85630
orcid: 0000-0002-5008-6530
- foaf_Person:
foaf_givenName: Veronika
foaf_name: Loitzenbauer, Veronika
foaf_surname: Loitzenbauer
bibo_doi: 10.1137/1.9781611975031.151
dct_date: 2018^xs_gYear
dct_identifier:
- UT:000483921200152
dct_language: eng
dct_publisher: ACM@
dct_title: 'Lower bounds for symbolic computation on graphs: Strongly connected
components, liveness, safety, and diameter@'
...