Computing Bottom SCCs Symbolically Using Transition Guided Reduction

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F21%3A00121980" target="_blank" >RIV/00216224:14330/21:00121980 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-81685-8_24" target="_blank" >http://dx.doi.org/10.1007/978-3-030-81685-8_24</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-81685-8_24" target="_blank" >10.1007/978-3-030-81685-8_24</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Computing Bottom SCCs Symbolically Using Transition Guided Reduction

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Computing Bottom SCCs Symbolically Using Transition Guided Reduction

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Computer Aided Verification - 33rd International Conference, CAV 2021

ISBN

9783030816841

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

24

Strana od-do

505-528

Název nakladatele

Springer Nature

Místo vydání

Neuveden

Místo konání akce

Virtual event

Datum konání akce

23. 7. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000698732400024