Operations on Fixpoint Equation Systems

Thomas Neele; Jaco van de Pol

doi:10.46298/lmcs-20(3:5)2024

Operations on Fixpoint Equation Systems

Thomas Neele
, Jaco van de Pol

Algorithms and Logics for Verification

Research output: Contribution to journal › Article › Academic › peer-review

48 Downloads (Pure)

Abstract

We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.

Original language	English
Number of pages	32
Journal	Logical Methods in Computer Science
Volume	20
Issue number	3
DOIs	https://doi.org/10.46298/lmcs-20(3:5)2024
Publication status	Published - 10 Jul 2024

Keywords

complete lattice
fixpoint equation system

Access to Document

10.46298/lmcs-20(3:5)2024

pdfFinal published version, 454 KBLicence: CC BY

Cite this

@article{7a09a4fcbb924fd0a15ef4643795e363,

title = "Operations on Fixpoint Equation Systems",

abstract = "We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.",

keywords = "complete lattice, fixpoint equation system",

author = "Thomas Neele and \{van de Pol\}, Jaco",

year = "2024",

month = jul,

day = "10",

doi = "10.46298/lmcs-20(3:5)2024",

language = "English",

volume = "20",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "3",

}

TY - JOUR

T1 - Operations on Fixpoint Equation Systems

AU - Neele, Thomas

AU - van de Pol, Jaco

PY - 2024/7/10

Y1 - 2024/7/10

N2 - We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.

AB - We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.

KW - complete lattice

KW - fixpoint equation system

UR - https://www.scopus.com/pages/publications/85199909987

U2 - 10.46298/lmcs-20(3:5)2024

DO - 10.46298/lmcs-20(3:5)2024

M3 - Article

AN - SCOPUS:85199909987

SN - 1860-5974

VL - 20

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 3

ER -

Operations on Fixpoint Equation Systems

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this