Paper: Normal process representatives (at LICS 1990)

Authors: Vijay Gehlot Carl A. Gunter

Abstract

The relevance of a form of cut elimination theorem for linear logic tensor theories to the concept of a process on a Petri net is discussed. The discussion is based on two definitions of processes given by E. Best and R. Devillers (1987). Their notions of process correspond to equivalence relations on linear logic proofs. It is noted that the cut reduced proofs form a process under the finer of these definitions. Using a strongly normalizing rewrite system and a weak Church-Rosser theorem, it is shown that each class of the coarser process definition contains exactly one of these finer classes which can therefore be viewed as a canonical or normal process representative. The relevance of these rewrite rules to the categorical approach of P. Degano et al. (1989) is also discussed

BibTeX

  @InProceedings{GehlotGunter-Normalprocessrepres,
    author = 	 {Vijay Gehlot and Carl A. Gunter},
    title = 	 {Normal process representatives},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {200--207},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }