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. |
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 | 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 |
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 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 |
VytisknoutZobrazeno: 12. 10. 2024 08:20