Multi-valued simulation and abstraction using lattice operations

Stefan Vijzelaar, W.J. Fokkink

Research output: Contribution to JournalArticleAcademicpeer-review

6 Downloads (Pure)

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
Pages (from-to)1-26
Number of pages26
JournalACM Transactions on Embedded Computing Systems
Volume16
Issue number2
Early online date2 Jan 2017
DOIs
Publication statusPublished - May 2017

Keywords

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

Fingerprint

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

Cite this