Galois Connections for Flow Algebras

Piotr Filipiuk; Michal Tomasz Terepeta; Hanne Riis Nielson; Flemming Nielson

doi:10.1007/978-3-642-21461-5

Galois Connections for Flow Algebras

Piotr Filipiuk
, Michal Tomasz Terepeta
, Hanne Riis Nielson
, Flemming Nielson

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

We generalise Galois connections from complete lattices to flow algebras. Flow algebras are algebraic structures that are less restrictive than idempotent semirings in that they replace distributivity with monotonicity and dispense with the annihilation property; therefore they are closer to the approach taken by Monotone Frameworks and other classical analyses. We present a generic framework for static analysis based on flow algebras and program graphs. Program graphs are often used in Model Checking to model concurrent and distributed systems. The framework allows to induce new flow algebras using Galois connections such that correctness of the analyses is preserved. The approach is illustrated for a mutual exclusion algorithm.

Original language	English
Title of host publication	Formal Techniques for Distributed Systems : Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011 Reykjavik, Iceland, June 6-9, 2011 Proceedings
Publisher	Springer
Publication date	2011
Pages	138-152
ISBN (Print)	978-3-642-21460-8
ISBN (Electronic)	978-3-642-21461-5
DOIs	https://doi.org/10.1007/978-3-642-21461-5
Publication status	Published - 2011
Event	Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference - Reykjavik, Iceland Duration: 6 Jun 2011 → 9 Jun 2011 Conference number: 13 & 31

Conference

Conference	Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference
Number	13 & 31
Country/Territory	Iceland
City	Reykjavik
Period	06/06/2011 → 09/06/2011

Series	Lecture Notes in Computer Science
Number	6722
ISSN	0302-9743

Access to Document

10.1007/978-3-642-21461-5

OpenUrl availability

Check availability in DTU Findit

Cite this

Filipiuk, P., Terepeta, M. T., Nielson, H. R., & Nielson, F. (2011). Galois Connections for Flow Algebras. In Formal Techniques for Distributed Systems: Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011 Reykjavik, Iceland, June 6-9, 2011 Proceedings (pp. 138-152). Springer. https://doi.org/10.1007/978-3-642-21461-5

Filipiuk, Piotr ; Terepeta, Michal Tomasz ; Nielson, Hanne Riis et al. / Galois Connections for Flow Algebras. Formal Techniques for Distributed Systems: Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011 Reykjavik, Iceland, June 6-9, 2011 Proceedings. Springer, 2011. pp. 138-152 (Lecture Notes in Computer Science; No. 6722).

@inproceedings{c3fdfaa26e4542fa86c091d44370de88,

title = "Galois Connections for Flow Algebras",

abstract = "We generalise Galois connections from complete lattices to flow algebras. Flow algebras are algebraic structures that are less restrictive than idempotent semirings in that they replace distributivity with monotonicity and dispense with the annihilation property; therefore they are closer to the approach taken by Monotone Frameworks and other classical analyses. We present a generic framework for static analysis based on flow algebras and program graphs. Program graphs are often used in Model Checking to model concurrent and distributed systems. The framework allows to induce new flow algebras using Galois connections such that correctness of the analyses is preserved. The approach is illustrated for a mutual exclusion algorithm.",

author = "Piotr Filipiuk and Terepeta, \{Michal Tomasz\} and Nielson, \{Hanne Riis\} and Flemming Nielson",

year = "2011",

doi = "10.1007/978-3-642-21461-5",

language = "English",

isbn = "978-3-642-21460-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "6722",

pages = "138--152",

booktitle = "Formal Techniques for Distributed Systems",

note = "Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, FMOODS \& FORTE ; Conference date: 06-06-2011 Through 09-06-2011",

}

Filipiuk, P, Terepeta, MT, Nielson, HR & Nielson, F 2011, Galois Connections for Flow Algebras. in Formal Techniques for Distributed Systems: Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011 Reykjavik, Iceland, June 6-9, 2011 Proceedings. Springer, Lecture Notes in Computer Science, no. 6722, pp. 138-152, Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, Reykjavik, Iceland, 06/06/2011. https://doi.org/10.1007/978-3-642-21461-5

Galois Connections for Flow Algebras. / Filipiuk, Piotr; Terepeta, Michal Tomasz; Nielson, Hanne Riis et al.
Formal Techniques for Distributed Systems: Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011 Reykjavik, Iceland, June 6-9, 2011 Proceedings. Springer, 2011. p. 138-152 (Lecture Notes in Computer Science; No. 6722).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Galois Connections for Flow Algebras

AU - Filipiuk, Piotr

AU - Terepeta, Michal Tomasz

AU - Nielson, Hanne Riis

AU - Nielson, Flemming

N1 - Conference code: 13 & 31

PY - 2011

Y1 - 2011

N2 - We generalise Galois connections from complete lattices to flow algebras. Flow algebras are algebraic structures that are less restrictive than idempotent semirings in that they replace distributivity with monotonicity and dispense with the annihilation property; therefore they are closer to the approach taken by Monotone Frameworks and other classical analyses. We present a generic framework for static analysis based on flow algebras and program graphs. Program graphs are often used in Model Checking to model concurrent and distributed systems. The framework allows to induce new flow algebras using Galois connections such that correctness of the analyses is preserved. The approach is illustrated for a mutual exclusion algorithm.

AB - We generalise Galois connections from complete lattices to flow algebras. Flow algebras are algebraic structures that are less restrictive than idempotent semirings in that they replace distributivity with monotonicity and dispense with the annihilation property; therefore they are closer to the approach taken by Monotone Frameworks and other classical analyses. We present a generic framework for static analysis based on flow algebras and program graphs. Program graphs are often used in Model Checking to model concurrent and distributed systems. The framework allows to induce new flow algebras using Galois connections such that correctness of the analyses is preserved. The approach is illustrated for a mutual exclusion algorithm.

U2 - 10.1007/978-3-642-21461-5

DO - 10.1007/978-3-642-21461-5

M3 - Article in proceedings

SN - 978-3-642-21460-8

T3 - Lecture Notes in Computer Science

SP - 138

EP - 152

BT - Formal Techniques for Distributed Systems

PB - Springer

T2 - Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference

Y2 - 6 June 2011 through 9 June 2011

ER -

Filipiuk P, Terepeta MT, Nielson HR, Nielson F. Galois Connections for Flow Algebras. In Formal Techniques for Distributed Systems: Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011 and 30th IFIP WG 6.1 International Conference, FORTE 2011 Reykjavik, Iceland, June 6-9, 2011 Proceedings. Springer. 2011. p. 138-152. (Lecture Notes in Computer Science; No. 6722). doi: 10.1007/978-3-642-21461-5

Galois Connections for Flow Algebras

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this