About: CUDA Accelerated LTL Model Checking

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

About: CUDA Accelerated LTL Model Checking - Revisited 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	Recently, the massively parallel architecture has been used to significantly accelerate many computation demanding tasks. For example, in [Baier, Kateon, The MIT Press, 2009; Barnat, Brim, Ceska, ICPADS 2009] we have shown how CUDA technology can be employed to accelerate the process of Linear Temporal Logic (LTL) Model Checking. In this paper we redesign the One-Way-Catch-Them-Young (OWCTY) algorithm [Cerna, Pelanek, SPIN'03] in order to devise a new CUDA accelerated OWCTY algorithm that will significantly outperform the original CUDA accelerated algorithm and will be resistant to slowdown caused by improper ordering of the input data representation. Recently, the massively parallel architecture has been used to significantly accelerate many computation demanding tasks. For example, in [Baier, Kateon, The MIT Press, 2009; Barnat, Brim, Ceska, ICPADS 2009] we have shown how CUDA technology can be employed to accelerate the process of Linear Temporal Logic (LTL) Model Checking. In this paper we redesign the One-Way-Catch-Them-Young (OWCTY) algorithm [Cerna, Pelanek, SPIN'03] in order to devise a new CUDA accelerated OWCTY algorithm that will significantly outperform the original CUDA accelerated algorithm and will be resistant to slowdown caused by improper ordering of the input data representation. (en)
Title	CUDA Accelerated LTL Model Checking - Revisited CUDA Accelerated LTL Model Checking - Revisited (en)
skos:prefLabel	CUDA Accelerated LTL Model Checking - Revisited CUDA Accelerated LTL Model Checking - Revisited (en)
skos:notation	RIV/00216224:14330/11:00049765!RIV12-GA0-14330___
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(GA201/09/1389), P(GD102/09/H042)
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Češka, Milan Bauch, Petr
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
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	192444
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/11:00049765
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Linear Temporal Logic (LTL) Model Checking; massively parallel architecture; One Way Catch Them Young (OWCTY) algorithm (en)
http://linked.open.../riv/klicoveSlovo	Linear Temporal Logic (LTL) Model Checking One Way Catch Them Young (OWCTY) algorithm massively parallel architecture
http://linked.open...ontrolniKodProRIV	[441913A8AC59]
http://linked.open...v/mistoKonaniAkce	Dagstuhl, Germany
http://linked.open...i/riv/mistoVydani	Dagstuhl, Germany
http://linked.open...i/riv/nazevZdroje	Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...vavai/riv/projekt	Verification and Analysis of Large-Scale Computer Systems Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems
http://linked.open...UplatneniVysledku	2011
http://linked.open...iv/tvurceVysledku	Bauch, Petr Češka, Milan
http://linked.open...vavai/riv/typAkce	CST - Celostátní
http://linked.open.../riv/zahajeniAkce	2011-01-01 (xsd:date)
issn	2190-6807
number of pages	8 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
https://schema.org/isbn	978-3-939897-22-4
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