The Approximate Correctness of Systems Based on δ -bisimulation | Zendy

Yanfang Ma | Zendy; Haiyu Pan | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

The Approximate Correctness of Systems Based on δ -bisimulation

Author(s) -

Yanfang Ma,

Haiyu Pan

Publication year - 2017

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2017.08.007

Subject(s) - bisimulation , correctness , limit (mathematics) , modular design , computer science , mathematics , implementation , algebra over a field , theoretical computer science , algorithm , pure mathematics , programming language , mathematical analysis

The correctness of system is an important attribute to quantify the quality. δ -bisimulation based on complete lattices have been proposed to generalize the classical bisimulation. To analyze the implementations of system approximates its specification step by step, the infinite evolution mechanism of δ -bisimulation is established. Firstly, the relations between the implementations and specification under δ -bisimulation are analyzed, δ -limit bisimulation is defined and some examples of δ -limit bisimulations are given. Then, δ -bisimulation limit is proposed to state the specification is the limit of implementations. Some algebraical properties of δ -bisimulation limit are proved. Finally, in order to use the flexible hierarchic development and modular design methods to archive the limit, the continuous of δ -bisimulation limit under various combinators are showed.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research