On two-sided approximate model-checking: problem formulation and solution via finite topologies
Davoren, Jen; Moor, Thomas; Gore, Rajeev; Coulthard, Vaughan; Nerode, Anil
Description
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...[Show more]
Collections | ANU Research Publications |
---|---|
Date published: | 2004 |
Type: | Book chapter |
URI: | http://hdl.handle.net/1885/87364 |
Download
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 20 July 2017/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator