arXiv Analytics

Sign in

arXiv:1811.03606 [cs.LO]AbstractReferencesReviewsResources

Bisimilarity of Open Terms in Stream GSOS

Filippo Bonchi, Tom van Bussel, Matias David Lee, Jurriaan Rot

Published 2018-11-08Version 1

Stream GSOS is a specification format for operations and calculi on infinite sequences. The notion of bisimilarity provides a canonical proof technique for equivalence of closed terms in such specifications. In this paper, we focus on open terms, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables. Our main contribution is to capture equivalence of open terms as bisimilarity on certain Mealy machines, providing a concrete proof technique. Moreover, we introduce an enhancement of this technique, called bisimulation up-to substitutions, and show how to combine it with other up-to techniques to obtain a powerful method for proving equivalence of open terms.

Related articles: Most relevant | Search more
arXiv:1804.10886 [cs.LO] (Published 2018-04-29)
Bisimilarity of diagrams
arXiv:1305.6115 [cs.LO] (Published 2013-05-27)
Bisimilarity and refinement for hybrid(ised) logics
arXiv:1303.0780 [cs.LO] (Published 2013-03-04)
Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes