FORMATS-FTRTFT 2004 START ConferenceManager    

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

J.M.Davoren, T.Moor, R.P.Gore, V.Coulthard, A.Nerode

Presented at Formal Modelling and Analysis of Timed Systems - Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT 2004), Grenoble, France, September 22-24, 2004


We present 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. Technically, our discussion is set within modal mu-calculus, and, hence, includes standard linear and branching temporal logics over transition systems like LTL, CTL and CTL*. The state-space discretization via an A/D-map and the induced Alexandroff topology are established as the constructive basis for a topological approximation scheme, for which we provide classical as well as intuitionistic topological semantics. Finally, we show that under natural coherence conditions any approximation can be refined to a topological one.

START Conference Manager (V2.47.2)