Computing Bottom SCCs Symbolically Using Transition Guided
Reduction

D 2021

Computing Bottom SCCs Symbolically Using Transition Guided Reduction

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA and David ŠAFRÁNEK

Basic information

Original name

Computing Bottom SCCs Symbolically Using Transition Guided Reduction

Authors

BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, belonging to the institution)

Edition

Neuveden, Computer Aided Verification - 33rd International Conference, CAV 2021, p. 505-528, 24 pp. 2021

Publisher

Springer Nature

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/21:00121980

Organization unit

Faculty of Informatics

ISBN

978-3-030-81684-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-81685-8_24

UT WoS

000698732400024

Keywords in English

Bottom SCC; Symbolic algorithm; Boolean network

Abstract

V originále

Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamical systems. However, these graphs’ size is often entirely out of reach for algorithms using explicit state-space exploration, necessitating alternative approaches such as the symbolic one. Symbolic methods for BSCC detection often show impressive performance, but can sometimes take a long time to converge in large graphs. In this paper, we provide a symbolic state-space reduction method for labelled transition systems, called interleaved transition guided reduction (ITGR), which aims to alleviate current problems of BSCC detection by efficiently identifying large portions of the non-BSCC states. We evaluate the suggested heuristic on an extensive collection of 125 real-world biologically motivated systems. We show that ITGR can easily handle all these models while being either the only method to finish, or providing at least an order-of-magnitude speedup over existing state-of-the-art methods. We then use a set of synthetic benchmarks to demonstrate that the technique also consistently scales to graphs with more than 2^1000 vertices, which was not possible using previous methods.

Links

MUNI/A/1108/2020, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X. (Acronym: SV-FI MAV X.)

Investor: Masaryk University

MUNI/A/1549/2020, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21 (Acronym: SKOMU)

Investor: Masaryk University

Citovat

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA and David ŠAFRÁNEK. Computing Bottom SCCs Symbolically Using Transition Guided Reduction. Online. In Alexandra Silva, K. Rustan, M. Leino. Computer Aided Verification - 33rd International Conference, CAV 2021. Neuveden: Springer Nature, 2021, p. 505-528. ISBN 978-3-030-81684-1. Available from: https://dx.doi.org/10.1007/978-3-030-81685-8_24.

@inproceedings{1783802,
   author = {Beneš, Nikola and Brim, Luboš and Pastva, Samuel and Šafránek, David},
   address = {Neuveden},
   booktitle = {Computer Aided Verification - 33rd International Conference, CAV 2021},
   doi = {http://dx.doi.org/10.1007/978-3-030-81685-8_24},
   editor = {Alexandra Silva, K. Rustan, M. Leino},
   keywords = {Bottom SCC; Symbolic algorithm; Boolean network},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-030-81684-1},
   pages = {505-528},
   publisher = {Springer Nature},
   title = {Computing Bottom SCCs Symbolically Using Transition Guided Reduction},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-81685-8_24},
   year = {2021}
}

TY  - JOUR
ID  - 1783802
AU  - Beneš, Nikola - Brim, Luboš - Pastva, Samuel - Šafránek, David
PY  - 2021
TI  - Computing Bottom SCCs Symbolically Using Transition Guided Reduction
PB  - Springer Nature
CY  - Neuveden
SN  - 9783030816841
KW  - Bottom SCC
KW  - Symbolic algorithm
KW  - Boolean network
UR  - https://link.springer.com/chapter/10.1007/978-3-030-81685-8_24
N2  - Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamical systems. However, these graphs’ size is often entirely out of reach for algorithms using explicit state-space exploration, necessitating alternative approaches such as the symbolic one. Symbolic methods for BSCC detection often show impressive performance, but can sometimes take a long time to converge in large graphs. In this paper, we provide a symbolic state-space reduction method for labelled transition systems, called interleaved transition guided reduction (ITGR), which aims to alleviate current problems of BSCC detection by efficiently identifying large portions of the non-BSCC states. We evaluate the suggested heuristic on an extensive collection of 125 real-world biologically motivated systems. We show that ITGR can easily handle all these models while being either the only method to finish, or providing at least an order-of-magnitude speedup over existing state-of-the-art methods. We then use a set of synthetic benchmarks to demonstrate that the technique also consistently scales to graphs with more than 2^1000 vertices, which was not possible using previous methods.
ER  -

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA and David ŠAFRÁNEK. Computing Bottom SCCs Symbolically Using Transition Guided Reduction. Online. In Alexandra Silva, K. Rustan, M. Leino. \textit{Computer Aided Verification - 33rd International Conference, CAV 2021}. Neuveden: Springer Nature, 2021, p.~505-528. ISBN~978-3-030-81684-1. Available from: https://dx.doi.org/10.1007/978-3-030-81685-8\_{}24.

Detailed Information on Publication Record