J 2006

Model Checking of RegCTL

ČERNÁ, Ivana a Tomáš BRÁZDIL

Základní údaje

Originální název

Model Checking of RegCTL

Název česky

Ověřování pro RegCTL

Autoři

ČERNÁ, Ivana (203 Česká republika, garant) a Tomáš BRÁZDIL (203 Česká republika)

Vydání

Computing and Informatics, 2006, 1335-9150

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Slovensko

Utajení

není předmětem státního či obchodního tajemství

Impakt faktor

Impact factor: 0.136

Kód RIV

RIV/00216224:14330/06:00015466

Organizační jednotka

Fakulta informatiky

UT WoS

000237134000005

Klíčová slova anglicky

model checking; RegCTL temporal logic

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 8. 6. 2009 16:06, prof. RNDr. Ivana Černá, CSc.

Anotace

ORIG CZ

V originále

The paper is devoted to the problem of extending the temporal logic CTL so that it is more expressive and complicated properties can be expressed in a more readable form. The specification language RegCTL, an extension of CTL, is proposed. In RegCTL every CTL temporal operator is augmented with a regular expression, thus restricting moments when the validity is required. We propose a local distributed model checking algorithm for RegCTL and exactly state the complexity of model checking RegCTL formulas.

Česky

Práce se věnuje rozšíření temporální logiky CTL o regulární operátory. Výslední logika je expresivnější než CTL a komplikované vlastnosti v můžou být vyjádřeny v přehlednější formě. Pro logiku RegCTL je v práci navržen lokální distribuovaný algoritmus ověřování.

Návaznosti

GA201/06/1338, projekt VaV
Název: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV
Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů