Other formats:
BibTeX
LaTeX
RIS
@inproceedings{702264,
author = {Bouajjani, Ahmed and Strejček, Jan and Touili, Tayssir},
address = {Neuveden},
booktitle = {Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006)},
keywords = {rewrite systems; infinite-state systems; symbolic reachability analysis; model checking},
language = {eng},
location = {Neuveden},
pages = {47-64},
publisher = {Elsevier},
title = {On Symbolic Verification of Weakly Extended PAD},
url = {http://dx.doi.org/10.1016/j.entcs.2006.10.053},
year = {2007}
}
TY - JOUR
ID - 702264
AU - Bouajjani, Ahmed - Strejček, Jan - Touili, Tayssir
PY - 2007
TI - On Symbolic Verification of Weakly Extended PAD
PB - Elsevier
CY - Neuveden
KW - rewrite systems
KW - infinite-state systems
KW - symbolic reachability analysis
KW - model checking
UR - http://dx.doi.org/10.1016/j.entcs.2006.10.053
N2 - 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.
ER -
BOUAJJANI, Ahmed, Jan STREJČEK and Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In \textit{Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006)}. Neuveden: Elsevier. p.~47-64. ISSN~1571-0661. 2007.
|
