On Symbolic Verification of Weakly Extended PAD

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Symbolicka verifikace slabe rozsirenych PAD
Autoři

BOUAJJANI Ahmed STREJČEK Jan TOUILI Tayssir

Rok publikování 2007
Druh Článek ve sborníku
Konference Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://dx.doi.org/10.1016/j.entcs.2006.10.053
Obor Informatika
Klíčová slova rewrite systems; infinite-state systems; symbolic reachability analysis; model checking
Popis 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ů.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.