Topology, monitorable properties and runtime verification

We review concepts like safety, liveness, and monitorability from a rigorous topological viewpoint. Thus, monitorability of an ω-language means that the boundary in the Cantor topology has an empty interior. We show that all ω-regular languages which are deterministic and co-deterministic are monitorable, but certain deterministic liveness properties like “infinitely many a  's” cannot be written as a countable union of monitorable languages. We briefly discuss model checking with LTL, its three-valued variant LTL3LTL3 and monitor constructions based upon LTL3LTL3.