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, 2007, s. 9-28. ISBN 978-3-540-69506-6.

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

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

V originále

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.

Č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