In case anyone is interested, I recently posted on my recent papers page a study of the equational theory of BPA with the interrupt operator. (See Luca Aceto, Silvio Capobianco and Anna Ingolfsdottir. On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt. ) This is the same language Anna and I studied in a very pleasant collaboration with Wan Fokkink and Sumit Nain that eventually led to a TCS publication. In that paper we showed that, modulo bisimilarity, there is no finite collection of sound equations that can prove all of the valid closed equations. This holds true even in the presence of a single action.
In the present paper we show that, unlike bisimilarity, complete trace equivalence affords a finite, ground-complete axiomatization, provided that the set of actions is finite. Moreover, we show that, when the set of actions is a singleton, the interrupt operator is a derived BPA-operator, and that complete trace equivalence affords a finite complete axiomatization over BPA with interrupt.
In the presence of at least two distinct actions, we isolate a collection of valid equations. A proof of their (in)completeness has so far escaped us. Feel free to get in touch with me if you have any idea on how to prove this!
No comments:
Post a Comment