Multi-valued simulation and abstraction using lattice operations

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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
Volume16
Issue number2
DOIs
Publication statusPublished - 1 Jan 2017

Keywords

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

Cite this