DocumentCode :
3295994
Title :
Unique fixpoint induction for value-passing processes
Author :
Rathke, Julian
Author_Institution :
Dept. of Cognitive & Comput. Sci., Sussex Univ., Brighton, UK
fYear :
1997
fDate :
29 Jun-2 Jul 1997
Firstpage :
140
Lastpage :
148
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on
Conference_Location :
Warsaw
ISSN :
1043-6871
Print_ISBN :
0-8186-7925-5
Type :
conf
DOI :
10.1109/LICS.1997.614942
Filename :
614942
Link To Document :
بازگشت