Paper: Reasoning with Many Processes (at LICS 1987)

Authors: A. Prasad Sistla Steven M. German

Abstract

We consider the problem of automatically verifying temporal properties of concurrent systems with an arbitrary number of identical finite state CCS processes. We consider two models of concurrent systems. In the first model all processes are identical. For this model we present an efficient decision procedure that checks if every execution of a process satisfies a given specification. This algorithm runs in the time polynomial in the size of a process. The second model consists of a unique control process and an arbitrary number of identical user processes. For this model we give a decision procedure to check if all the executions of a process satisfy the given specification. This algorithm runs in time double exponential in the size of the control process and the user process. We also prove that the problem of checking if all the fair executions of a process satisfy a given specification, is decidable. Finally, we show how these decision procedures can be used to reason about certain algorithms on networks of processes.

BibTeX

  @InProceedings{SistlaGerman-ReasoningwithManyPr,
    author = 	 {A. Prasad Sistla and Steven M. German},
    title = 	 {Reasoning with Many Processes},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {138--152},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }