About: Designing Fast LTL Model Checking Algorithms for Many-core GPUs

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Designing Fast LTL Model Checking Algorithms for Many-core GPUs Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this paper we show how the algorithms for LTL model checking can be redesigned in order to accelerate LTL model checking on many-core GPU platforms. Our detailed experimental evaluation demonstrates that using the NVIDIA CUDA technology results in a significant speedup of the verification process. Together with state space generation based on shared hash-table and DFS exploration, our CUDA accelerated model checker is the fastest among state-of-the-art shared memory model checking tools. The effective utilisation of CUDA technology, however, is quite often reduced by the costly preparation of suitable data structures and limited to small or middle-sized instances due to space limitations, which is also the case of our CUDA-aware LTL Model Checking solutions. Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this paper we show how the algorithms for LTL model checking can be redesigned in order to accelerate LTL model checking on many-core GPU platforms. Our detailed experimental evaluation demonstrates that using the NVIDIA CUDA technology results in a significant speedup of the verification process. Together with state space generation based on shared hash-table and DFS exploration, our CUDA accelerated model checker is the fastest among state-of-the-art shared memory model checking tools. The effective utilisation of CUDA technology, however, is quite often reduced by the costly preparation of suitable data structures and limited to small or middle-sized instances due to space limitations, which is also the case of our CUDA-aware LTL Model Checking solutions. (en)
Title	Designing Fast LTL Model Checking Algorithms for Many-core GPUs Designing Fast LTL Model Checking Algorithms for Many-core GPUs (en)
skos:prefLabel	Designing Fast LTL Model Checking Algorithms for Many-core GPUs Designing Fast LTL Model Checking Algorithms for Many-core GPUs (en)
skos:notation	RIV/00216224:14330/12:00057210!RIV13-GA0-14330___
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(GA201/09/1389), P(GAP202/11/0312), P(GD102/09/H042), P(GP201/09/P497), S, Z(MSM0021622419)
http://linked.open...iv/cisloPeriodika	9
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Češka, Milan Barnat, Jiří Bauch, Petr Brim, Luboš
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Masarykova univerzita / Fakulta informatiky
http://linked.open...dnocenehoVysledku	130382
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/12:00057210
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Parallel model checking; Linear temporal logic; Massively parallel architectures; CUDA technology; Multiple CUDA devices (en)
http://linked.open.../riv/klicoveSlovo	CUDA technology Linear temporal logic Massively parallel architectures Multiple CUDA devices Parallel model checking
http://linked.open...odStatuVydavatele	CZ - Česká republika
http://linked.open...ontrolniKodProRIV	[C983D0F0BF26]
http://linked.open...i/riv/nazevZdroje	Journal of Parallel and Distributed Computing
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	4 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Verification and Analysis of Large-Scale Computer Systems Software Components in Embedded Systems: Development and Verification Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems Automated formal verification using modern hardware
http://linked.open...UplatneniVysledku	2012
http://linked.open...v/svazekPeriodika	72
http://linked.open...iv/tvurceVysledku	Barnat, Jiří Bauch, Petr Brim, Luboš Češka, Milan
http://linked.open...ain/vavai/riv/wos	000307156000005
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	0743-7315
number of pages	15 (xsd:int)
http://bibframe.org/vocab/doi	10.1016/j.jpdc.2011.10.015
http://localhost/t...ganizacniJednotka	14330

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software