BOUAJJANI, Ahmed, Jan STREJČEK and 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. p. 29-41, 13 pp.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name On Symbolic Verification of Weakly Extended PAD
Name in Czech Symbolicka verifikace slabe rozsirenych PAD
Authors BOUAJJANI, Ahmed (504 Morocco), Jan STREJČEK (203 Czech Republic, guarantor) and Tayssir TOUILI (788 Tunisia).
Edition London, Preliminary Proceedings - 13th International Workshow on Expressiveness in Concurrency - EXPRESS'06, p. 29-41, 13 pp. 2006.
Publisher Imperial College London
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/06:00018747
Organization unit Faculty of Informatics
Keywords in English rewrite systems; infinite-state systems; symbolic reachability analysis; model checking
Tags infinite-state systems, Model checking, rewrite systems, symbolic reachability analysis
Tags International impact, Reviewed
Changed by Changed by: doc. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 18/6/2007 14:11.
Abstract
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.
Abstract (in Czech)
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ů.
Links
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Research Centres (National Research Programme)
PrintDisplayed: 6/4/2020 14:54