Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{563033, author = {Barnat, Jiří and Brim, Luboš and Chaloupka, Jakub}, address = {Linz, Austria}, booktitle = {Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004)}, keywords = {LTL model checking; breadth first search; distributed memory}, language = {eng}, location = {Linz, Austria}, isbn = {3-902457-03-1}, pages = {17-34}, publisher = {Institute for Systems Engineering & Automation, Kepler university Linz}, title = {From Distributed Memory Cycle Detection to Parallel LTL Model Checking}, year = {2004} }
TY - JOUR ID - 563033 AU - Barnat, Jiří - Brim, Luboš - Chaloupka, Jakub PY - 2004 TI - From Distributed Memory Cycle Detection to Parallel LTL Model Checking PB - Institute for Systems Engineering & Automation, Kepler university Linz CY - Linz, Austria SN - 3902457031 KW - LTL model checking KW - breadth first search KW - distributed memory N2 - We propose a parallel graph algorithm for detecting cycles in very large directed graphs distributed over a network of workstations. The algorithm employs back-level edges as computed by the breadth first search. In this paper we describe how to turn the algorithm into an explicit state distributed memory LTL model checker by extending it with detection of accepting cycles, counterexample generation and partial order reduction. We discuss these extensions and show experimental results. ER -
BARNAT, Jiří, Luboš BRIM a Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. In \textit{Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004)}. Linz, Austria: Institute for Systems Engineering \&{} Automation, Kepler university Linz, 2004, s.~17-34. ISBN~3-902457-03-1.
|