About: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors

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

About: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors 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	The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B\"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well. The distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a B\"{u}chi automaton. One approach to distributed accepting cycle detection is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally, and find out which of these work well. (en)
Title	How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors (en)
skos:prefLabel	How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors (en)
skos:notation	RIV/00216224:14330/06:00015453!RIV10-GA0-14330___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(1ET408050503), P(1M0545), P(GA201/03/0509), P(GD102/05/H050), Z(MSM0021622419)
http://linked.open...iv/cisloPeriodika	2
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Šimša, Jiří Moravec, Pavel Černá, Ivana 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	478302
http://linked.open...ai/riv/idVysledku	RIV/00216224:14330/06:00015453
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	accepting predecessors; LTL model checking (en)
http://linked.open.../riv/klicoveSlovo	LTL model checking accepting predecessors
http://linked.open...odStatuVydavatele	PT - Portugalská republika
http://linked.open...ontrolniKodProRIV	[18083FC1EC79]
http://linked.open...i/riv/nazevZdroje	Electronic Notes in Theoretical Computer Science
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	Institute for Theoretical Computer Science Integrated Approach to Education of PhD Students in the Area of Parallel and Distributed Systems Automated Verification of Parallel and Distributed Systems Techniques for automatic verification and validation of software and hardware systems
http://linked.open...UplatneniVysledku	2006
http://linked.open...v/svazekPeriodika	135
http://linked.open...iv/tvurceVysledku	Brim, Luboš Moravec, Pavel Černá, Ivana Šimša, Jiří
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	1571-0661
number of pages	15 (xsd:int)
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, 41 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software