On Symbolic Verification of Weakly Extended PAD
| Název česky | Symbolicka verifikace slabe rozsirenych PAD |
|---|---|
| Autoři | |
| 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 | |
| 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: |