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 Článek ve sborníku
Obor Informatika
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: 14. 12. 2017 09:20

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 14. 12. 2017 09:20, 50. (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