Model Checking of RegCTL

ČERNÁ, Ivana a Tomáš BRÁZDIL. Model Checking of RegCTL. Computing and Informatics. 2006, roč. 25, č. 1, s. 81-97, 16 s. ISSN 1335-9150.

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

• Originální 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: Model checking, RegCTL temporal logic
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

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.

Anotace č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ů