Title :
Unique fixpoint induction for value-passing processes
Author_Institution :
Dept. of Cognitive & Comput. Sci., Sussex Univ., Brighton, UK
fDate :
29 Jun-2 Jul 1997
Abstract :
We investigate the use of unique fixpoint induction as a proof method for value-passing process languages with recursion. An intuitive generalisation of unique fixpoint induction based on loop invariants for symbolic graphs yields strong completeness results; we give an axiomatic characterisation 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
Keywords :
inference mechanisms; process algebra; fixpoint induction; intuitive generalisation; loop invariants; process languages; recursion; symbolic graphs; value-passing calculi; Carbon capture and storage; Telephony;
Conference_Titel :
Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on
Conference_Location :
Warsaw
Print_ISBN :
0-8186-7925-5
DOI :
10.1109/LICS.1997.614942