Lattice-valued kripke structures based on complete residuated lattice

  • Haiyu Pan
  • , Min Zhang*
  • , Yixiang Chen
  • *Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations

Abstract

We introduce the lattice-valued Kripke structures, for the purpose of allowing imprecise or incomplete specifications to be expressed, by extending the traditional notion of Kripke structures in the context of complete residuated lattice. Moreover, we show how the traditional trace inclusion and equivalence, can be lifted to a setting of quantitative where their interpretations are given as elements of complete residuated lattices. We also present logical characterizations of our notions, given by a lattice-valued extension of LTL.

Original languageEnglish
Title of host publicationProceedings of the 2012 IEEE 6th International Conference on Software Security and Reliability Companion, SERE-C 2012
Pages137-143
Number of pages7
DOIs
StatePublished - 2012
Event2012 IEEE 6th International Conference on Software Security and Reliability Companion, SERE-C 2012 - Gaithersburg, MD, United States
Duration: 20 Jun 201222 Jun 2012

Publication series

NameProceedings of the 2012 IEEE 6th International Conference on Software Security and Reliability Companion, SERE-C 2012

Conference

Conference2012 IEEE 6th International Conference on Software Security and Reliability Companion, SERE-C 2012
Country/TerritoryUnited States
CityGaithersburg, MD
Period20/06/1222/06/12

Keywords

  • Kripke structure
  • Linear time temporal logic
  • Residuated lattice
  • Trace equivalence

Fingerprint

Dive into the research topics of 'Lattice-valued kripke structures based on complete residuated lattice'. Together they form a unique fingerprint.

Cite this