Using verified property to partition the state space in LTL model-checking

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F02%3A00006604" target="_blank" >RIV/00216224:14330/02:00006604 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Using verified property to partition the state space in LTL model-checking
Original language description
We propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA201%2F00%2F1023" target="_blank" >GA201/00/1023: Algorithms and tools for practical verification of concurrent systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

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

Article name in the collection
F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes
ISBN
—
ISSN
—
e-ISSN
—
Number of pages
6
Pages from-to
262
Publisher name
IRCCyN, Ecole Centrale de Nantes
Place of publication
Nantes, France
Event location
Nantes, France, June 2002
Event date
Jan 1, 2002
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)