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

@article{2668139528f54ec8bb44ee2c6b93d6e2,
title = "Multi-valued simulation and abstraction using lattice operations",
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.",
keywords = "Bilattices, Kripke models, Mixed simulation, Multi-valued logics",
author = "Stefan Vijzelaar and W.J. Fokkink",
year = "2017",
month = "1",
day = "1",
doi = "10.1145/3012282",
language = "English",
volume = "16",
journal = "ACM Transactions on Embedded Computing Systems",
issn = "1539-9087",
publisher = "Association for Computing Machinery (ACM)",
number = "2",

}

Multi-valued simulation and abstraction using lattice operations. / Vijzelaar, Stefan; Fokkink, W.J.

In: ACM Transactions on Embedded Computing Systems, Vol. 16, No. 2, 42, 01.01.2017.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Multi-valued simulation and abstraction using lattice operations

AU - Vijzelaar, Stefan

AU - Fokkink, W.J.

PY - 2017/1/1

Y1 - 2017/1/1

N2 - 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.

AB - 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.

KW - Bilattices

KW - Kripke models

KW - Mixed simulation

KW - Multi-valued logics

UR - http://www.scopus.com/inward/record.url?scp=85008881153&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85008881153&partnerID=8YFLogxK

U2 - 10.1145/3012282

DO - 10.1145/3012282

M3 - Article

VL - 16

JO - ACM Transactions on Embedded Computing Systems

JF - ACM Transactions on Embedded Computing Systems

SN - 1539-9087

IS - 2

M1 - 42

ER -