BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL and Radek PELÁNEK. Distributed LTL Model-Checking Based on Negative Cycle Detection. In FST-TCS 2001. Bangalore, India: Springer, 2001, p. 96-110. LNCS 2245. ISBN 3-540-43002-4. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{371119, author = {Brim, Luboš and Černá, Ivana and Krčál, Pavel and Pelánek, Radek}, address = {Bangalore, India}, booktitle = {FST-TCS 2001}, location = {Bangalore, India}, isbn = {3-540-43002-4}, pages = {96-110}, publisher = {Springer}, title = {Distributed LTL Model-Checking Based on Negative Cycle Detection}, year = {2001} }
TY - JOUR ID - 371119 AU - Brim, Luboš - Černá, Ivana - Krčál, Pavel - Pelánek, Radek PY - 2001 TI - Distributed LTL Model-Checking Based on Negative Cycle Detection VL - LNCS 2245 PB - Springer CY - Bangalore, India SN - 3540430024 N2 - This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All the known methods for automata based model checking are based on depth first traversal of the state space which is difficult to parallelise as the ordering in which vertices are visited plays an important role. We come up with entirely different approach which is dependent on locating cycles with negative length in a directed graph with real number length of edges. Our method allows reasonable distribution and the experimental results confirm its usefulness for distributed model checking. ER -
BRIM, Luboš, Ivana ČERNÁ, Pavel KRČÁL and Radek PELÁNEK. Distributed LTL Model-Checking Based on Negative Cycle Detection. In \textit{FST-TCS 2001}. Bangalore, India: Springer, 2001, p.~96-110. LNCS 2245. ISBN~3-540-43002-4.
|