Rewriting Systems over Nested Data Words Invariance checking for systems with dynamic control and data structures
Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu · 2009
We propose a generic framework for reasoning about innite state systems handling data like integers, booleans etc. and having com- plex control structures. We consider that congurations of such systems are represented by nested data words, i.e., words of ... words over a po- tentially innite data domain. We dene a logic called NDWL allowing to reason about nested data words, and we dene rewriting systems called NDW-RS over these nested structures. The rewriting systems are con- strained by formulas in the logic specifying the rewriting positions as well as structure/data transformations. We dene a fragment 2 of NDWL with a decidable satisability problem. Moreover, we show that the tran- sition relation dened by rewriting systems with 2 constraints can be eectively dened in the same fragment. These results can be used in the automatization of verication problems such as inductive invariance checking and bounded reachability analysis. Our framework allows to rea- son about a wide range of concurrent systems including multithreaded programs (with procedure calls, thread creation, global/local variables over innite data domains, locks, monitors, etc.), dynamic networks of timed systems, cache coherence/mutex/communication protocols, etc.