V 2008

Partial Order Reduction for State/Event LTL

BENEŠ, Nikola, Luboš BRIM, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ et. al.

Základní údaje

Originální název

Partial Order Reduction for State/Event LTL

Název česky

Metoda partial order redukce pro State/Event LTL

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí), Jiří SOCHOR (203 Česká republika, domácí), Pavlína VAŘEKOVÁ (203 Česká republika, domácí) a Barbora ZIMMEROVÁ (203 Česká republika, garant, domácí)

Vydání

Brno, Czech Republic, 21 s. Technical report FIMU-RS-2008-07, 2008

Nakladatel

Faculty of Informatics, Masaryk University

Další údaje

Jazyk

angličtina

Typ výsledku

Výzkumná zpráva

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Odkazy

Kód RIV

RIV/00216224:14330/08:00024265

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

Partial order reduction; state/event LTL; formal verification

Štítky

Příznaky

Mezinárodní význam
Změněno: 18. 9. 2015 12:32, prof. Ing. Jiří Sochor, CSc.

Anotace

ORIG CZ

V originále

The paper introduces a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.

Česky

Článek představuje novou metodu partial order reduction pro verifikaci vlastností logiky state/event LTL. Jádrem metody je nová definice stuttering ekvivalence, kterou nazýváme state/event stuttering ekvivalence.

Návaznosti

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
1ET400300504, projekt VaV
Název: Realistická aplikace formálních metod v komponentových systémech
Investor: Akademie věd ČR, Realistická aplikace formálních metod v komponentových systémech
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ů