Model Checking Large Finite-State Systems and Beyond

BRIM, Luboš a Mojmír KŘETÍNSKÝ. Model Checking Large Finite-State Systems and Beyond. In 33rd Conference on Current Trends in Theory and Practice of Computer Science. Berlin: Springer-Verlag. s. 9-28. ISBN 978-3-540-69506-6. 2007.

Základní údaje

• Originální název: Model Checking Large Finite-State Systems and Beyond
• Název česky: Ověřování modelu pro rozsáhlé konečně stavové systémy a za jejich hranicemi
• Autoři: BRIM, Luboš (203 Česká republika, garant) a Mojmír KŘETÍNSKÝ (203 Česká republika).
• Vydání: Berlin, 33rd Conference on Current Trends in Theory and Practice of Computer Science, od s. 9-28, 20 s. 2007.
• Nakladatel: Springer-Verlag

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/07:00019356
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-3-540-69506-6
• UT WoS: 000244537600002
• Klíčová slova anglicky: finite and infinite-state systems; reachability; linear time logic; model checking; decidability
• Štítky: decidability, finite and infinite-state systems, linear time logic, Model checking, reachability
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS), possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based Linear Temporal Logic (LTL) a Hennessy-Milner branching time logic.

Anotace česky

Je ustanovena hranice rozhodnutelnosti pro problém ověřování modelu pro fragmenty logik HM resp. LTL a nekonečně stavové systémy generované tzv. procesovými přepisovacími systémy (eventuelně rozšířenými o tzv.slabou 59dic9 jednotku.

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ů

• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky