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/DROPS.MEMICS.2009.2356
URN: urn:nbn:de:0030-drops-23567
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2356/
Go to the corresponding OASIcs Volume Portal

Bouajjani, Ahmed ; Drăgoi, Cezara ; Jurski, Yan ; Sighireanu, Mihaela

Rewriting Systems over Nested Data Words

pdf-format:
09006.BoujjaniA.2356.pdf (0.4 MB)

Abstract

We propose a generic framework for reasoning about infinite state systems handling data like integers, booleans etc. and having complex control structures. We consider that configurations of such systems are represented by nested data words, i.e., words of ... words over a potentially infinite data domain. We define a logic called $\ndwl$ allowing to reason about nested data words, and we define rewriting systems called $\ndwrs$ over these nested structures. The rewriting systems are constrained by formulas in the logic specifying the rewriting positions as well as structure/data transformations. We define a fragment $\Sigma_2^*$ of $\ndwl$ with a decidable satisfiability problem. Moreover, we show that the transition relation defined by rewriting systems with $\Sigma_2^*$ constraints can be
effectively defined in the same fragment. These results can be used in the automatization of verification problems such as inductive invariance checking and bounded reachability analysis. Our framework allows to reason about a wide range of concurrent systems including multithreaded programs (with procedure calls, thread creation, global/local variables over infinite data domains, locks, monitors, etc.), dynamic networks of timed systems, cache coherence/mutex/communication protocols, etc.

BibTeX - Entry

@InProceedings{bouajjani_et_al:OASIcs:2009:2356,
  author =	{Ahmed Bouajjani and Cezara Drăgoi and Yan Jurski and Mihaela Sighireanu},
  title =	{{Rewriting Systems over Nested Data Words}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{70--77},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Petr Hlinen{\'y} and V{\'a}clav Maty{\'a}{\v{s}} and Tom{\'a}{\v{s}} Vojnar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2356},
  URN =		{urn:nbn:de:0030-drops-23567},
  doi =		{10.4230/DROPS.MEMICS.2009.2356},
  annote =	{Keywords: Nested data words, rewriting systems, program verification, dynamic and parametrized systems, invariance checking}
}

Keywords: Nested data words, rewriting systems, program verification, dynamic and parametrized systems, invariance checking
Collection: Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)
Issue Date: 2009
Date of publication: 15.12.2009

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