---
_id: '310'
abstract:
- lang: eng
text: 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.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Wolfgang
full_name: Dvorák, Wolfgang
last_name: Dvorák
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: Veronika
full_name: Loitzenbauer, Veronika
last_name: Loitzenbauer
citation:
ama: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Lower bounds for symbolic
computation on graphs: Strongly connected components, liveness, safety, and diameter.
In: ACM; 2018:2341-2356. doi:10.1137/1.9781611975031.151'
apa: 'Chatterjee, K., Dvorák, W., Henzinger, M. H., & Loitzenbauer, V. (2018).
Lower bounds for symbolic computation on graphs: Strongly connected components,
liveness, safety, and diameter (pp. 2341–2356). Presented at the SODA: Symposium
on Discrete Algorithms, New Orleans, Louisiana, United States: ACM. https://doi.org/10.1137/1.9781611975031.151'
chicago: 'Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika
Loitzenbauer. “Lower Bounds for Symbolic Computation on Graphs: Strongly Connected
Components, Liveness, Safety, and Diameter,” 2341–56. ACM, 2018. https://doi.org/10.1137/1.9781611975031.151.'
ieee: 'K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Lower bounds
for symbolic computation on graphs: Strongly connected components, liveness, safety,
and diameter,” presented at the SODA: Symposium on Discrete Algorithms, New Orleans,
Louisiana, United States, 2018, pp. 2341–2356.'
ista: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2018. Lower bounds
for symbolic computation on graphs: Strongly connected components, liveness, safety,
and diameter. SODA: Symposium on Discrete Algorithms, 2341–2356.'
mla: 'Chatterjee, Krishnendu, et al. Lower Bounds for Symbolic Computation on
Graphs: Strongly Connected Components, Liveness, Safety, and Diameter. ACM,
2018, pp. 2341–56, doi:10.1137/1.9781611975031.151.'
short: K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, ACM, 2018,
pp. 2341–2356.
conference:
end_date: 2018-01-10
location: New Orleans, Louisiana, United States
name: 'SODA: Symposium on Discrete Algorithms'
start_date: 2018-01-07
date_created: 2018-12-11T11:45:45Z
date_published: 2018-01-01T00:00:00Z
date_updated: 2023-09-13T08:50:16Z
day: '01'
department:
- _id: KrCh
doi: 10.1137/1.9781611975031.151
ec_funded: 1
external_id:
arxiv:
- '1711.09148'
isi:
- '000483921200152'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1711.09148
month: '01'
oa: 1
oa_version: Preprint
page: 2341 - 2356
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
grant_number: ICT15-003
name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: ACM
publist_id: '7555'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Lower bounds for symbolic computation on graphs: Strongly connected components,
liveness, safety, and diameter'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2018'
...