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
Link To Document :
بازگشت