Real-Time Verification Techniques for Untimed Systems

Xiaoqun Du, C. R. Ramakrishnan, Scott A. Smolka

Abstract:
We show that verification techniques for timed automata based on the Alur and Dill region-graph construction can be applied to much more general kinds of systems, including asynchronous untimed systems over unbounded integer variables. We follow this approach in proving that the problem of verifying the n-process Bakery algorithm is decidable, for any fixed n. We believe this is the first decidability proof for this problem to appear in the literature.

Bibtex Entry:

@inproceedings{DRS:MTCS00,
author = {Xiaoqun Du and  C. R. Ramakrishnan and  Scott A. Smolka},
title = {Real-Time Verification Techniques for Untimed Systems},
booktitle = {Workshop on Models for Time-Critical Systems ({MTCS})},
address = {State College, Pennsylvania},
month = {August},
series = {Electronic Notes in Theoretical Computer Science},
volume = {39},
publisher = {Elsevier Science Publishers},
note = {http://www.elsevier.nl/gej-ng/31/29/23/66/22/show/Products/notes/index.htt},
year = {2000}
}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan
(cram@cs.sunysb.edu)