Skip to main content

2001 | OriginalPaper | Buchkapitel

Efficient Multiple-Valued Model-Checking Using Lattice Representations

verfasst von : Marsha Chechik, Benet Devereux, Steve Easterbrook, Albert Y. C. Lai, Victor Petrovykh

Erschienen in: CONCUR 2001 — Concurrency Theory

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Multiple-valued logics can be effectively used to reason about incomplete and/or inconsistent systems, e.g. during early software requirements or as the systems evolve. We specify multiple-valued logics using finite lattices. In this paper, we use lattice representation theory to cast the multiple-valued modelchecking problem in terms of symbolic operations on classical sets of states, provided the lattices are distributive. This allows us to partially reuse existing symbolic model-checking technology and improve efficiency over previous implementations that were based on multiple-valued decision diagrams.

Metadaten
Titel
Efficient Multiple-Valued Model-Checking Using Lattice Representations
verfasst von
Marsha Chechik
Benet Devereux
Steve Easterbrook
Albert Y. C. Lai
Victor Petrovykh
Copyright-Jahr
2001
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-44685-0_30

Neuer Inhalt