Informační systém Masarykovy univerzity 

Model Checking Large Finite-State Systems and Beyond

česky | in English

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, 20 s. ISBN 978-3-540-69506-6.
Další formáty:   BibTeX LaTeX RIS
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 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
Změnil Změnil: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Změněno: 12. 6. 2008 09:40.
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 VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 23. 9. 2018 06:42

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 23. 9. 2018 06:42, 38. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému