Galois Connections for Flow Algebras

International audience 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 the...

Full description

Bibliographic Details
Main Authors: Filipiuk, Piotr, Terepeta, Michał, Nielson, Hanne, Nielson, Flemming
Other Authors: Technical University of Denmark Lyngby (DTU), Roberto Bruni, Juergen Dingel, TC 6, WG 6.1
Format: Conference Object
Language:English
Published: HAL CCSD 2011
Subjects:
[INFO]Computer Science [cs]
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI]
Iceland
Online Access:https://hal.inria.fr/hal-01583315
https://hal.inria.fr/hal-01583315/document
https://hal.inria.fr/hal-01583315/file/978-3-642-21461-5_9_Chapter.pdf
https://doi.org/10.1007/978-3-642-21461-5_9
Description
Summary:International audience 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.

Similar Items