Characterizing contextual equivalence in calculi with passivation

• Published in: Information and computation 2011-11, Vol.209 (11), p.1390-1433
• Main Authors: Lenglet, Sergueï, Schmitt, Alan, Stefani, Jean-Bernard
• Format: Article
• Language: English
• Subjects: Applied sciences; Computer Science; Computer science; control theory; systems; Exact sciences and technology; Formal Languages and Automata Theory; Language theory and syntactical analysis; Miscellaneous; Theoretical computing
• ISSN: 0890-5401; 1090-2651
• DOI: 10.1016/j.ic.2011.08.002

We study the problem of characterizing contextual equivalence in higher-order languages with passivation. To overcome the difficulties arising in the proof of congruence of candidate bisimilarities, we introduce a new form of labeled transition semantics together with its associated notion of bisimulation, which we call complementary semantics. Complementary semantics allows to apply the well-known Howeʼs method for proving the congruence of bisimilarities in a higher-order setting, even in the presence of an early form of bisimulation. We use complementary semantics to provide a coinductive characterization of contextual equivalence in the HO πP calculus, an extension of the higher-order π-calculus with passivation, obtaining the first result of this kind. We then study the problem of defining a more effective variant of bisimilarity that still characterizes contextual equivalence, along the lines of Sangiorgiʼs notion of normal bisimilarity. We provide partial results on this difficult problem: we show that a large class of test processes cannot be used to derive a normal bisimilarity in HO πP, but we show that a form of normal bisimilarity can be defined for HO πP without restriction.