Logic in Computer Science (LICS 1996)

Paper: General decidability theorems for infinite-state systems (at LICS 1996)

Authors: Parosh Aziz Abdulla Karlis Cerans Bengt Jonsson Yih-Kuen Tsay

Abstract

Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems), which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a well-ordered and well-founded preorder such that the transition relation is "monotonic" (is a simulation) with respect to the preorder. We show that the following properties are decidable for well-structured systems: reachability; eventuality; and simulation. We also describe how these general principles subsume several decidability results from the literature about timed automata, relational automata, Petri nets, and lossy channel systems.

BibTeX

  @InProceedings{AbdullaCeransJonsso-Generaldecidability,
    author = 	 {Parosh Aziz Abdulla and Karlis Cerans and Bengt Jonsson and Yih-Kuen Tsay},
    title = 	 {General decidability theorems for infinite-state systems},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {313-321},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }