BENEŠ, Nikola, Ivana ČERNÁ a Jan KŘETÍNSKÝ. Modal Transition Systems: Composition and LTL Model Checking. In ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium. Heidelberg Dordrecht London New York: Springer, 2011. s. 228-242. ISBN 978-3-642-24371-4.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Modal Transition Systems: Composition and LTL Model Checking
Autoři BENEŠ, Nikola (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí).
Vydání Heidelberg Dordrecht London New York, ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium, od s. 228-242, 15 s. 2011.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Kód RIV RIV/00216224:14330/11:00049982
Organizační jednotka Fakulta informatiky
ISBN 978-3-642-24371-4
UT WoS 000306498800017
Klíčová slova anglicky modal transition systems; model checking; refinement; conjunction
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Nikola Beneš, Ph.D., učo 72525. Změněno: 24. 10. 2013 16:21.
Anotace
Modal transition systems (MTS) is a~well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we provide algorithms showing that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we identify an error in a~previous attempt at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition. Secondly, we give a~solution to the common implementation and conjunctive composition problems lowering the complexity from EXPTIME to PTIME.
Návaznosti
GAP202/11/0312, projekt VaVNázev: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
GD102/09/H042, projekt VaVNázev: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
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, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0914/2009, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
Typ Název Vložil/a Vloženo Práva
paper_51-1_hqkmdxut.pdf  Černá, I. 2. 12. 2011

Vlastnosti

Adresa v ISu
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.pdf
Adresa ze světa
https://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.pdf
Adresa do Správce
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.pdf?info
Ze světa do Správce
https://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.pdf?info
Vloženo
Pá 2. 12. 2011 09:23, prof. RNDr. Ivana Černá, CSc.

Práva

Právo číst
  • kdokoliv v Internetu
Právo vkládat
 
Právo spravovat
  • osoba doc. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D., učo 139914
  • osoba prof. RNDr. Ivana Černá, CSc., učo 1419
  • osoba RNDr. Nikola Beneš, Ph.D., učo 72525
Atributy
 

paper_51-1_hqkmdxut.pdf

Aplikace
Otevřít soubor.
Stáhnout soubor.
Adresa v ISu
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.pdf
Adresa ze světa
http://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.pdf
Typ souboru
PDF (application/pdf)
Velikost
357,1 KB
Hash md5
5aa177a40ffc12ab5438dcaf5a96024b
Vloženo
Pá 2. 12. 2011 09:23

paper_51-1_hqkmdxut.txt

Aplikace
Otevřít soubor.
Stáhnout soubor.
Adresa v ISu
https://is.muni.cz/auth/publication/950140/paper_51-1_hqkmdxut.txt
Adresa ze světa
http://is.muni.cz/publication/950140/paper_51-1_hqkmdxut.txt
Typ souboru
holý text (text/plain)
Velikost
40,3 KB
Hash md5
be9eb36c0cae331ec330d4e9644f5e4c
Vloženo
Pá 2. 12. 2011 09:26
Vytisknout
Nahlásit neoprávněně vložený soubor Zobrazeno: 30. 6. 2022 15:41