On two-sided approximate model-checking: problem formulation and solution via finite topologies

Jennifer M. Davoren, Thomas Moor, R. P. Goré, Vaughan Coulthard, Anil Nerode

    Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

    1 Citation (Scopus)

    Abstract

    We give a general formulation of approximate model- checking, in which both under- and over-approximations are propagated to give two-sided approximations of the denotation set of an arbitrarily complex formula. As our specification language, we use the modal μ-calculus, since it subsumes standard linear and branching temporal logics over transition systems like LTL, CTL and CTL*. We give a general construction of a topological finite approximation scheme for a Kripke model from a state-space discretization via an A/D-map and its induced finite topology. We further show that under natural coherence conditions, any finite approximation scheme can be refined by a topological one.

    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    EditorsYassine Lakhnech, Sergio Yovine
    PublisherSpringer Verlag
    Pages52-67
    Number of pages16
    ISBN (Print)3540231676, 9783540231677
    DOIs
    Publication statusPublished - 2004

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume3253
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Fingerprint

    Dive into the research topics of 'On two-sided approximate model-checking: problem formulation and solution via finite topologies'. Together they form a unique fingerprint.

    Cite this