From Distributed Memory Cycle Detection to Parallel LTL Model Checking | Zendy

Jǐŕı Barnat | Zendy; Luboš Brim | Zendy; Jakub Chaloupka | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

From Distributed Memory Cycle Detection to Parallel LTL Model Checking

Author(s) -

Jǐŕı Barnat,

Luboš Brim,

Jakub Chaloupka

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2004.08.056

Subject(s) - computer science , model checking , counterexample , distributed memory , workstation , reduction (mathematics) , parallel computing , graph , partial order reduction , theoretical computer science , algorithm , shared memory , mathematics , operating system , discrete mathematics , geometry

In [J. Barnat, L. Brim, and J. Chaloupka. Parallel Breadth-First Search LTL Model-Checking. In 18th IEEE International Conference on Automated Software Engineering (ASE'03), pages 106–115. IEEE Computer Society, Oct. 2003.] we proposed 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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research