Lics

IEEE Symposium on Logic in Computer Science

Paper: Unique Fixpoint Induction for Value-Passing Processes (at LICS 1997)

Abstract

We investigate the use of unique fixpoint induction as a proof method for value-passing process languages with recursion. An intuitive generalization of unique fixpoint induction based on loop invariants for symbolic graphs yields strong completeness results; we give an axiomatic characterization of both late and early observational congruence for a class of fully parameterised processes. This new, generalised, rule is shown to be derivable from existing formulations of unique fixpoint induction for value-passing calculi, thereby providing original completeness results. An example of the use of this new rule is presented in detail.

BibTeX

 @InProceedings{Rathke-UniqueFixpointInduc,
 author = 	 {Julian Rathke},
 title = 	 {Unique Fixpoint Induction for Value-Passing Processes},
 booktitle = {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)},
 year =	 {1997},
 month =	 {June}, 
 pages = {140--148},
 location = {Warsaw, Poland}, 
 publisher =	 {IEEE Computer Society Press}
 }