About: On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties

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

About: On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties 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	One of the most important open problems of parallel LTL model checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would provide the same optimality we have in sequential LTL model checking. In this paper we give a partial solution to the problem: we propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Buchi automata. In addition to the previous version of the paper, we demonstrate how our new algorithm can be efficiently combined with a particular parallel technique for Partial Order Reduction and report on additional experiments. One of the most important open problems of parallel LTL model checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would provide the same optimality we have in sequential LTL model checking. In this paper we give a partial solution to the problem: we propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Buchi automata. In addition to the previous version of the paper, we demonstrate how our new algorithm can be efficiently combined with a particular parallel technique for Partial Order Reduction and report on additional experiments. (en)
Title	On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties (en)
skos:prefLabel	On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties (en)
skos:notation	RIV/00216224:14330/12:00057076!RIV13-AV0-14330___
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(1ET400300504), P(1ET408050503), P(GA201/09/1389), P(GP201/09/P497), S, Z(MSM0021622419)
http://linked.open...iv/cisloPeriodika	12
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Barnat, Jiří Brim, Luboš Ročkai, Petr
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	156583
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/12:00057076
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction (en)
http://linked.open.../riv/klicoveSlovo	Parallel Explicit Model Checking On-the-fly Partial Order Reduction
http://linked.open...odStatuVydavatele	US - Spojené státy americké
http://linked.open...ontrolniKodProRIV	[AD40717C8E9D]
http://linked.open...i/riv/nazevZdroje	Science of Computer Programming
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	3 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Verification and Analysis of Large-Scale Computer Systems Automated formal verification using modern hardware Techniques for automatic verification and validation of software and hardware systems Realistic application of formal methods in component systems
http://linked.open...UplatneniVysledku	2012
http://linked.open...v/svazekPeriodika	77
http://linked.open...iv/tvurceVysledku	Barnat, Jiří Brim, Luboš Ročkai, Petr
http://linked.open...ain/vavai/riv/wos	000308732800004
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	0167-6423
number of pages	17 (xsd:int)
http://bibframe.org/vocab/doi	10.1016/j.scico.2011.03.001
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, 112 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software