2006
On Symbolic Verification of Weakly Extended PAD
BOUAJJANI, Ahmed, Jan STREJČEK a Tayssir TOUILIZá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
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
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 18. 6. 2007 14:11, prof. RNDr. Jan Strejček, Ph.D.
V originále
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.
Č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ěr |
| ||
| 1M0545, projekt VaV |
|