Verification by computing languages closures under rewriting systems

can be reduced to the problem of computing closures of the form $R^*(L)$
where $L$ is a word language and $R$ is a word rewriting system.
We discuss various classes of regular languages and rewriting systems
for which such closures are regular and effectively computable.
We show the applicability of such results in the verification
of FIFO lossy channel systems and parametrized networks of processes.
This talk is based on the papers:

1- A. Bouajjani, A. Muscholl, T. Touili. Permutation Rewriting and
Algorithmic Verification,
in Proc. 16th IEEE Symp. on Logic in Computer Science (LICS'01), June 2001.

2- P. Abdulla, L. Boasson, A. Bouajjani. Effective Lossy Queue Languages,
in Proc. 28th Intern. Coll. on Automata, Languages and Programming
(ICALP'01),
LNCS 2076, July 2001.

3- A. Bouajjani. Languages, Rewriting systems, and Verification of
Infinite-State Systems,
in Proc. 28th Intern. Coll. on Automata, Languages and Programming
(ICALP'01),
LNCS 2076, July 2001.