Using Assumptions to Distribute CTL Model Checking

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F02%3A00006432" target="_blank" >RIV/00216224:14330/02:00006432 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Using Assumptions to Distribute CTL Model Checking

Popis výsledku v původním jazyce

In this work we discuss the problem of performing distributed CTL model checking by splitting the given state space into several ``partial state spaces''. The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about the truth of formulas and the computers exchangeassumptions about relevant states as they compute more precis

Název v anglickém jazyce

Using Assumptions to Distribute CTL Model Checking

Popis výsledku anglicky

In this work we discuss the problem of performing distributed CTL model checking by splitting the given state space into several ``partial state spaces''. The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about the truth of formulas and the computers exchangeassumptions about relevant states as they compute more precis

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F00%2F1023" target="_blank" >GA201/00/1023: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2002

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

1st International Workshop on Parallel and Distributed Model Checking (PDMC 2002)

ISBN

0444512918

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

80

Název nakladatele

Elsevier

Místo vydání

Brno, Czech Republic

Místo konání akce

August 19, 2002, Brno, Czech republic

Datum konání akce

1. 1. 2002

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—