• DocumentCode
    2717094
  • Title

    Normal process representatives

  • Author

    Gehlot, Vijay ; Gunter, Carl

  • Author_Institution
    Dept. of Comput. & Inf. Sci., Pennsylvania Univ., Philadelphia, PA, USA
  • fYear
    1990
  • fDate
    4-7 Jun 1990
  • Firstpage
    200
  • Lastpage
    207
  • 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
  • Keywords
    Petri nets; formal logic; rewriting systems; theorem proving; Petri net; canonical; coarser process definition; cut elimination theorem; cut reduced proofs; equivalence relations; linear logic tensor theories; normal process representation; strongly normalizing rewrite system; weak Church-Rosser theorem;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
  • Conference_Location
    Philadelphia, PA
  • Print_ISBN
    0-8186-2073-0
  • Type

    conf

  • DOI
    10.1109/LICS.1990.113746
  • Filename
    113746