Dexter Kozen ; Nicholas Ruozzi - Applications of Metric Coinduction

lmcs:1168 - Logical Methods in Computer Science, September 16, 2009, Volume 5, Issue 3 -
Applications of Metric Coinduction

Authors: Dexter Kozen ; Nicholas Ruozzi

    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.

    Volume: Volume 5, Issue 3
    Published on: September 16, 2009
    Imported on: December 20, 2007
    Keywords: Computer Science - Logic in Computer Science,F.4.1,F.3.1,I.1.3,I.2.3
    Financement :
      Source : OpenAIRE Graph
    • Specialized Logics for Applications in Computer Science; Funder: National Science Foundation; Code: 0635028

    7 Documents citing this article

    Consultation statistics

    This page has been seen 619 times.
    This article's PDF has been downloaded 206 times.