BARNAT, Jiří. Using verified property to partition the state space in LTL model-checking. In F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes. Nantes, France: IRCCyN, Ecole Centrale de Nantes, 2002, p. 262-267. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{406263, author = {Barnat, Jiří}, address = {Nantes, France}, booktitle = {F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes}, keywords = {model-checking; distributed model-checking; verification}, language = {eng}, location = {Nantes, France}, pages = {262-267}, publisher = {IRCCyN, Ecole Centrale de Nantes}, title = {Using verified property to partition the state space in LTL model-checking}, year = {2002} }
TY - JOUR ID - 406263 AU - Barnat, Jiří PY - 2002 TI - Using verified property to partition the state space in LTL model-checking PB - IRCCyN, Ecole Centrale de Nantes CY - Nantes, France KW - model-checking KW - distributed model-checking KW - verification N2 - We propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm. ER -
BARNAT, Jiří. Using verified property to partition the state space in LTL model-checking. In \textit{F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes}. Nantes, France: IRCCyN, Ecole Centrale de Nantes, 2002, p.~262-267.
|