Fixed-points for quantitative equational logics
Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon; (2021) Fixed-points for quantitative equational logics. In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. Proceedings - Symposium on Logic in Computer Science, 1 . IEEE, Piscataway, NJ, pp. 1-13. ISBN 9781665448956 (https://doi.org/10.1109/LICS52264.2021.9470662)
Preview |
Text.
Filename: Mardare_etal_LICS_2021_Fixed_points_for_quantitative_equational_logics.pdf
Accepted Author Manuscript Download (191kB)| Preview |
Abstract
We develop a fixed-point extension of quantitative equational logic and give semantics in one-bounded complete quantitative algebras. Unlike previous related work about fixed-points in metric spaces, we are working with the notion of approximate equality rather than exact equality. The result is a novel theory of fixed points which can not only provide solutions to the traditional fixed-point equations but we can also define the rate of convergence to the fixed point. We show that such a theory is the quantitative analogue of a Conway theory and also of an iteration theory; and it reflects the metric coinduction principle. We study the Bellman equation for a Markov decision process as an illustrative example.
-
-
Item type: Book Section ID code: 77763 Dates: DateEvent7 July 2021Published2 July 2021Published Online31 March 2021AcceptedNotes: © 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting /republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Subjects: Technology > Electrical engineering. Electronics Nuclear engineering Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 10 Sep 2021 09:10 Last modified: 11 Nov 2024 15:25 URI: https://strathprints.strath.ac.uk/id/eprint/77763