D 2021

Computing Bottom SCCs Symbolically Using Transition Guided Reduction

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

Základní údaje

Originální název

Computing Bottom SCCs Symbolically Using Transition Guided Reduction

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Samuel PASTVA (703 Slovensko, domácí) a David ŠAFRÁNEK (203 Česká republika, domácí)

Vydání

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

Nakladatel

Springer Nature

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/21:00121980

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-81684-1

ISSN

DOI

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

UT WoS

000698732400024

Klíčová slova anglicky

Bottom SCC; Symbolic algorithm; Boolean network

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 11. 10. 2021 07:52, prof. RNDr. Luboš Brim, CSc.

Anotace

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.

Návaznosti

MUNI/A/1108/2020, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X. (Akronym: SV-FI MAV X.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X.
MUNI/A/1549/2020, interní kód MU
Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21 (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21
Zobrazeno: 16. 11. 2024 02:48