Multi-valued simulation and abstraction using lattice operations

S.J.J. Vijzelaar, W. Fokkink

Research output: Contribution to journalArticleAcademicpeer-review

1 Citation (Scopus)

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
Number of pages26
JournalACM Transactions on Embedded Computing Systems
Volume16
Issue number2
DOIs
Publication statusPublished - Apr 2017
Externally publishedYes

Keywords

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

Cite this