BOUAJJANI, Ahmed, Jan STREJČEK a Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In Preliminary Proceedings - 13th International Workshow on Expressiveness in Concurrency - EXPRESS'06. London: Imperial College London, 2006. s. 29-41, 13 s.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název On Symbolic Verification of Weakly Extended PAD
Název česky Symbolicka verifikace slabe rozsirenych PAD
Autoři BOUAJJANI, Ahmed (504 Maroko), Jan STREJČEK (203 Česká republika, garant) a Tayssir TOUILI (788 Tunisko).
Vydání London, Preliminary Proceedings - 13th International Workshow on Expressiveness in Concurrency - EXPRESS'06, od s. 29-41, 13 s. 2006.
Nakladatel Imperial College London
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í
Kód RIV RIV/00216224:14330/06:00018747
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky rewrite systems; infinite-state systems; symbolic reachability analysis; model checking
Štítky infinite-state systems, Model checking, rewrite systems, symbolic reachability analysis
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 18. 6. 2007 14:11.
Anotace
We consider the verification problem of a class of infinite-state systems called wPAD. These systems can be used to model programs with (possibly recursive) procedure calls and dynamic creation of parallel processes. They correspond to PAD models extended with an acyclic finite-state control unit, where PAD models can be seen as combinations of prefix rewrite systems (pushdown systems) with context-free multiset rewrite systems (synchronization-free Petri nets). Recently, we have presented symbolic reachability techniques for the class of PAD based on the use of a class of unranked tree automata. In this paper, we generalize our previous work to the class wPAD which is strictly larger than PAD. This generalization brings a positive answer to an open question on decidability of the model checking problem for wPAD against EF logic. Moreover, we show how symbolic reachability analysis of wPAD can be used in (under) approximate analysis of Synchronized PAD.
Anotace česky
Studujeme otázky verifikace třídy nekonečně stavových systémů známé jako wPAD. Tyto systémy slouží k modelování programů s (rekurzivním) voláním procedur a dynamickým vytvářením paralelních procesů. wPAD systémy odpovídají PAD systémům rozšířeným o acyklickou konečnou řídící jednotku. PAD systemy jsou pak kombinací prefixových přepisovacích systémů (zasobníkové systémy) a bezkontextových paralelních přepisovacích systémů (nesynchronizované Petriho sítě). Nedávno jsme představili symbolický algoritmus pro dosažitelnost v PAD systémech zalozený na stromových automatech s neomezeným větvením. V tomto článku zobecníme naše předchozí výsledky na třídu wPAD, která je striktně větší než PAD. Zmíněné zobecnění přináší kladnou odpověď na otevřenou otázku rozhodnutelnosti ověřování modelů pro wPAD a EF logiku. Také ukážeme, jak může být zmíněný symbolický algoritmus pro dosažitelnost použit k přibližné analýze synchronních PAD systémů.
Návaznosti
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
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: 27. 2. 2020 15:58