Multi-valued simulation and abstraction using lattice operations

Stefan Vijzelaar, W.J. Fokkink

Research output: Contribution to JournalArticleAcademicpeer-review


Abstractions can cause spurious results, which need to be verified in the concrete system to gain conclusive results. Verification based on a multi-valued logic can distinguish between conclusive and inconclusive results, provides increased precision, and allows for encoding additional information into the model. To ensure a correct abstraction, one can use a mixed simulation [Meller et al. 2009]. We extend mixed simulation to include inconsistent values, thereby resolving an asymmetry and allowing for abstractions with increased precision when inconsistent values are available. In addition, we present a set of abstraction rules, compatible with the extended notion, for constructing abstract models.

Original languageEnglish
Article number42
JournalACM Transactions on Embedded Computing Systems
Issue number2
Publication statusPublished - 1 Jan 2017


  • Bilattices
  • Kripke models
  • Mixed simulation
  • Multi-valued logics


Dive into the research topics of 'Multi-valued simulation and abstraction using lattice operations'. Together they form a unique fingerprint.

Cite this