Fixed-Points for Quantitative Equational Logics

Radu Mardare; Prakash Panangaden; Gordon D Plotkin

doi:10.1109/LICS52264.2021.9470662

Fixed-Points for Quantitative Equational Logics

Radu Mardare, Prakash Panangaden, Gordon D Plotkin

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Proceedings of the 36th Annual Symposium on Logic in Computer Science
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Number of pages	13
ISBN (Electronic)	978-1-6654-4895-6
ISBN (Print)	978-1-6654-4896-3
DOIs	https://doi.org/10.1109/LICS52264.2021.9470662
Publication status	Published - 9 Jul 2021
Event	36th Annual ACM/IEEE Symposium on Logic in Computer Science - Online Duration: 29 Jun 2021 → 2 Jul 2021 http://easyconferences.eu/lics2021/

Symposium

Symposium	36th Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2021
Period	29/06/21 → 2/07/21
Internet address	http://easyconferences.eu/lics2021/

Access to Document

10.1109/LICS52264.2021.9470662Licence: All Rights Reserved

Fixed-Points for Quantitative_MARDARE_DOA31032121_AFVAccepted author manuscript, 274 KBLicence: All Rights Reserved

https://ieeexplore.ieee.org/document/9470662Licence: All Rights Reserved

Cite this

@inproceedings{e9a2693e3f104110abf72dbee2e9d991,

title = "Fixed-Points for Quantitative Equational Logics",

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.",

author = "Radu Mardare and Prakash Panangaden and Plotkin, {Gordon D}",

year = "2021",

month = jul,

day = "9",

doi = "10.1109/LICS52264.2021.9470662",

language = "English",

isbn = "978-1-6654-4896-3",

booktitle = "Proceedings of the 36th Annual Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

note = "36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 ; Conference date: 29-06-2021 Through 02-07-2021",

url = "http://easyconferences.eu/lics2021/",

}

TY - GEN

T1 - Fixed-Points for Quantitative Equational Logics

AU - Mardare, Radu

AU - Panangaden, Prakash

AU - Plotkin, Gordon D

PY - 2021/7/9

Y1 - 2021/7/9

N2 - 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.

AB - 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.

U2 - 10.1109/LICS52264.2021.9470662

DO - 10.1109/LICS52264.2021.9470662

M3 - Conference contribution

SN - 978-1-6654-4896-3

BT - Proceedings of the 36th Annual Symposium on Logic in Computer Science

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 29 June 2021 through 2 July 2021

ER -

Fixed-Points for Quantitative Equational Logics

Abstract

Symposium

Access to Document

Fingerprint

Cite this