License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2010.216
URN: urn:nbn:de:0030-drops-28653
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2865/
Go to the corresponding LIPIcs Volume Portal

Atig, Mohamed Faouzi

Global Model Checking of Ordered Multi-Pushdown Systems

pdf-format:
19.pdf (0.4 MB)

Abstract

In this paper, we address the verification problem of ordered multi-pushdown systems: A multi-stack extension of pushdown systems that comes with a constraint on stack operations such that a pop can only be performed on the first non-empty stack. First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given $w$-regular property (expressible in linear-time temporal logics or the linear-time $\mu$-calculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of $w$-regular properties for ordered multi-pushdown systems (matching its lower-bound).

BibTeX - Entry

@InProceedings{atig:LIPIcs:2010:2865,
  author =	{Mohamed Faouzi Atig},
  title =	{{Global  Model Checking of Ordered Multi-Pushdown Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{216--227},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Kamal Lodaya and Meena Mahajan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2865},
  URN =		{urn:nbn:de:0030-drops-28653},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.216},
  annote =	{Keywords: Concurrent Programs, Pushdown Systems, Global Model-Checking}
}

Keywords: Concurrent Programs, Pushdown Systems, Global Model-Checking
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Issue Date: 2010
Date of publication: 14.12.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI