@inbook{6a6bcff1bf69462b83a05c41c53afa53,
title = "On two-sided approximate model-checking: problem formulation and solution via finite topologies",
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.",
author = "Davoren, {Jennifer M.} and Thomas Moor and Gor{\'e}, {R. P.} and Vaughan Coulthard and Anil Nerode",
year = "2004",
doi = "10.1007/978-3-540-30206-3_6",
language = "English",
isbn = "3540231676",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "52--67",
editor = "Yassine Lakhnech and Sergio Yovine",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "Germany",
}