D 2002

Local Distributed Model Checking of RegCTL

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

Základní údaje

Originální název

Local Distributed Model Checking of RegCTL

Autoři

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

Vydání

The Netherlands, PDMC 2002 Parallel and Distributed Model Checking, s. 1-14, 2002

Nakladatel

Elsevier Science Publishers

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

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

Kód RIV

RIV/00216224:14330/02:00006437

Organizační jednotka

Fakulta informatiky

ISBN

0444512918

Klíčová slova anglicky

model checking

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 15:07, prof. RNDr. Ivana Černá, CSc.

Anotace

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 more succinctly. The specification language RegCTL, an extension of CTL, is proposed. In RegCTL every CTL temporal operator is augmented with a regular expression restricting thus moments when the validity is required. The resulting logic is more expressive than previous extensions of CTL with regular expressions. RegCTL can be model-checked on-the-fly and the model checking algorithm is well distributable.

Návaznosti

GA201/00/1023, projekt VaV
Název: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů