Diplomová práce

Partial Order Reduction in Parallel Model Checking

Bc. Petr Ročkai, učo 139761
Anotace

Hlavním zaměřením této práce je technika redukce částečným uspořádáním pro paralelní LTL model checking. Přínos techniky spočívá v její paralelní implementaci, poskytující skutečně dynamickou heuristiku se sekvenční složitostí v O(n). Naproti tomu, tradiční techniku založenou na DFS nelze používat s paralelními algoritmy a existující heuristiky vhodné pro paralelní prostředí vyžadují super-lineární …více

Abstract

The main focus of this thesis is a partial order reduction technique for parallel LTL model checking. The novelty of our technique lies in its parallel implementation, and in providing truly dynamic heuristic with serial time complexity in O(n). In contrast, the traditional DFS-based techniques cannot be used with parallel algorithms. Moreover, the existing heuristics amenable to parallel execution …více

Klíčová slova
Model Checking Parallel Algorithms Implementation Multi-Threading Multi-Core Shared Memory Symmetric Multiprocessing Distributed Memory Clusters State Space Reductions Partial Order Reduction
Zadání práce
Cílem diplomové práce je vytvořit heuristiku pro redukci částečným uspořádáním, která bude nezávislá na prohledávání do hloubky, a tedy použitelná v paralelních algoritmech pro enumerativní LTL model checking. Práce by měla tuto heuristiku formálně popsat a zdůvodnit její korektnost. Dále by výstupem měla být funkční implementace potřebných algoritmů, vhodná k začlenění do existujícího paralelního nástroje DiVinE. Na základě této implementace by měla práce obsahovat také experimentální srovnání s klasickou sekvenční heuristikou.
Administrativní informace
Práce zkontrolována:
13. 1. 2010 15:11, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
550,1 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
10. 2. 2010
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponent

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Petr Ročkai FI N-IN PDS, učo 139761 p04i0/6
Ročkai, P.
6. 1. 2010
Složky
Soubory
Anotace anglicky annotation_english.txt
Ročkai, P.
6. 1. 2010
Anotace česky annotation.txt
Ročkai, P.
6. 1. 2010
Klíčová slova keywords.txt
Ročkai, P.
6. 1. 2010
posudek_oponenta.pdf
Strejček, J.
5. 2. 2010
thesis.pdf main.pdf
Ročkai, P.
6. 1. 2010

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.