Applications of Metric Coinduction

Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step showing that some property is preserved by one step of the approximation process, then automatically infer by the coinduct...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2009-09, Vol.5, Issue 3
Main Authors: Kozen, Dexter, Ruozzi, Nicholas
Format: Article
Language:English
Subjects:
computer science - logic in computer science
f.3.1
f.4.1
i.1.3
i.2.3
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step showing that some property is preserved by one step of the approximation process, then automatically infer by the coinduction principle that the property holds of the limit object. This can often be used to avoid complicated analytic arguments involving limits and convergence, replacing them with simpler algebraic arguments. This paper examines the application of this principle in a variety of areas, including infinite streams, Markov chains, Markov decision processes, and non-well-founded sets. These results point to the usefulness of coinduction as a general proof technique.
ISSN:1860-5974
1860-5974
DOI:10.2168/LMCS-5(3:10)2009