Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: Bisimulation is not finitely (first order) equationally axiomatisable (at LICS 1994)

Authors: Peter Sewell

Abstract

This paper considers the existence of finite equational axiomatisations of bisimulation over a calculus of finite state processes. To express even simple properties such as μXE=μXE[E/X] equationally it is necessary to use some notation for substitutions. Accordingly the calculus is embedded in a simply typed lambda calculus, allowing axioms such as the above to be written as equations of higher type rather than as equation schemes. Notions of higher order transition system and bisimulation are then defined and using them the nonexistence of finite axiomatisations containing at most first order variables is shown

BibTeX

  @InProceedings{Sewell-Bisimulationisnotfi,
    author = 	 {Peter Sewell},
    title = 	 {Bisimulation is not finitely (first order) equationally axiomatisable },
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {62--70},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski