Topology, monitorable properties and runtime verification

Volker Diekert, Martin Leucker*

*Corresponding author for this work
8 Citations (Scopus)


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 LTL3 and monitor constructions based upon LTL3.

Original languageEnglish
JournalTheoretical Computer Science
Issue numberC
Pages (from-to)29-41
Number of pages13
Publication statusPublished - 05.06.2014


Dive into the research topics of 'Topology, monitorable properties and runtime verification'. Together they form a unique fingerprint.

Cite this