Bisimulation for lattice-valued transition systems

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

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

3 Scopus citations

Abstract

In this paper, we define lattice-valued labeled transition systems (LLTS) as a general framework for allowing imprecise or incomplete specifications to be expressed. We introduce a lattice-valued bisimulation between LLTSs that measures the degree of closeness of two systems as elements of residuated lattice, in contrast to the traditional boolean yes/no to bisimulation. Also, we show that our bisimulation is compositional for a synchronous composition operator. Moreover, we also consider lattice-valued extension of Kripke structures, define a lattice valued bisimulation between lattice-valued Kripke structures (LKSs), and establish the correspondence between lattice-valued bisimulation in LLTS and lattice-valued bisimulation in LKS.

Original languageEnglish
Title of host publicationProceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
Pages279-282
Number of pages4
DOIs
StatePublished - 2012
EventIEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012 - Beijing, China
Duration: 4 Jul 20126 Jul 2012

Publication series

NameProceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012

Conference

ConferenceIEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012
Country/TerritoryChina
CityBeijing
Period4/07/126/07/12

Keywords

  • Kripke structure
  • bisimulation
  • labeled transition system
  • residuated lattice

Fingerprint

Dive into the research topics of 'Bisimulation for lattice-valued transition systems'. Together they form a unique fingerprint.

Cite this