-
C. Bannister, P. Höfner, G. Struth:
Effect Algebras, Girard Quantales and Complementation in Separation Logic. In U. Fahrenberg, M. Gehrke, L. Santocanale, M. Winter (eds.), elational and Algebraic Methods in Computer Science (RAMiCS 2021). Lecture Notes in Computer Science 13027, pp. 37-53, Springer, 2021.
doi: 10.1007/978-3-030-88701-8_3
abstract | pdf | bibtex
Abstract:
We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. It follows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.
@InProceedings{Hoefner2021-5,
Author = {Bannister, C. and H{\"o}fner, P. and Struth, G.},
Title = {Effect Algebras, Girard Quantales and Complementation in Separation Logic},
BookTitle = {elational and Algebraic Methods in Computer Science (RAMiCS 2021)},
Editor = {Fahrenberg, U. and Gehrke, M. and Santocanale, L. and Winter, M.},
Series = {Lecture Notes in Computer Science},
Volume = {13027},
Pages = {37-53},
Year = {2021},
Publisher = {Springer},
Doi = {10.1007/978-3-030-88701-8_3}
}
-
R.J. van Glabbeek, P. Höfner, W. Wang:
Enabling Preserving Bisimulation Equivalence. In Concurrency Theory (CONCUR 2021). LIPIcs 203, pp. 33:1-33:20, Schloss Dagstuhl -- Leibniz-Zentrum für Informatik, 2021.
arXiv: CoRR abs/2108.00142 | doi: 10.4230/LIPIcs.CONCUR.2021.33
abstract | pdf | bibtex
Abstract:
Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.
@InProceedings{Hoefner2021-4,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Wang, W.},
Title = {Enabling Preserving Bisimulation Equivalence},
BookTitle = {Concurrency Theory (CONCUR 2021)},
Editor = {},
Series = {LIPIcs},
Volume = {203},
Pages = {33:1-33:20},
Year = {2021},
Publisher = {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
Doi = {10.4230/LIPIcs.CONCUR.2021.33}
}
-
R.J. van Glabbeek, P. Höfner, R. Horne:
Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom. In Logic in Computer Science (LICS 2021). pp. 1-13, IEEE, 2021.
arXiv: CoRR abs/2104.14226 | doi: 10.1109/LICS52264.2021.9470531
abstract | pdf | bibtex
Abstract:
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.
@InProceedings{Hoefner2021-3,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Horne, R.},
Title = {Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom},
BookTitle = {Logic in Computer Science (LICS 2021)},
Editor = {},
Series = {},
Volume = {0},
Pages = {1-13},
Year = {2021},
Publisher = {IEEE},
Doi = {10.1109/LICS52264.2021.9470531}
}
-
R. Berghammer, H. Hitoshi, W. Guttmann, P. Höfner:
Relational Characterisations of Paths. In Journal of Logic and Algebraic Methods in Programming 117, Elsevier, 2020.
arXiv: CoRR abs/1801.04026 | doi: 10.1016/j.jlamp.2020.100590
abstract | pdf | bibtex
Abstract:
Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in relation algebras. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms. All results of this paper are formally verified using Isabelle/HOL.
@article{Hoefner2020-3,
Author = {Berghammer, R. and Hitoshi, H. and Guttmann, W. and H{\"o}fner, P.},
Title = {Relational Characterisations of Paths},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Volume = {117},
Year = {2020},
Publisher = {Elsevier},
Doi = {10.1016/j.jlamp.2020.100590}
}
-
J. Drury, P. Höfner, W. Wang:
Formal Models of the OSPF Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 72-120, Open Publishing Association, 2020.
doi: 10.4204/EPTCS.316.4
abstract | pdf | bibtex
Abstract:
We present three formal models of the OSPF routing protocol. The first two are formalised in the timed process algebra T-AWN, which is not only tailored for routing protocols, but also specifies protocols in pseudo-code that is easily readable. The difference between the two models lies in the level of detail (level of abstraction). From the more abstract model we then generate the third model. It is based on networks of timed automata and can be executed in the model checker Uppaal.
@InProceedings{Hoefner2020-2,
Author = {Drury, J. and H{\"o}fner, P. and Wang, W.},
Title = {Formal Models of the {OSPF} Routing Protocol},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
Editor = {Fehnker, A. and Garaval, H.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {316},
Pages = {72-120},
Year = {2020},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.316.4}
}
