Theoroidal maps as algebraic simulations

Narciso Martí-Oliet, Jose Meseguer, Miguel Palomino

Research output: Contribution to journalConference article


Computational systems are often represented by means of Kripke structures, and related using simulations. We propose rewriting logic as a flexible and executable framework in which to formally specify these mathematical models, and introduce a particular and elegant way of representing simulations in it: theoroidal maps. A categorical viewpoint is very natural in the study of these structures and we show how to organize Kripke structures in categories that afterwards are lifted to the rewriting logic's level. We illustrate the use of theoroidal maps with two applications: predicate abstraction and the study of fairness constraints.

Original languageEnglish (US)
Pages (from-to)126-143
Number of pages18
JournalLecture Notes in Computer Science
StatePublished - Sep 14 2005
Event17th International Workshop, WADT 2004 - Barcelona, Spain
Duration: Mar 27 2004Mar 29 2004


ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Martí-Oliet, N., Meseguer, J., & Palomino, M. (2005). Theoroidal maps as algebraic simulations. Lecture Notes in Computer Science, 3423, 126-143.