TY - JOUR
T1 - Topology, monitorable properties and runtime verification
AU - Diekert, Volker
AU - Leucker, Martin
PY - 2014/6/5
Y1 - 2014/6/5
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84926689147&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2014.02.052
DO - 10.1016/j.tcs.2014.02.052
M3 - Journal articles
AN - SCOPUS:84926689147
SN - 0304-3975
VL - 537
SP - 29
EP - 41
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - C
ER -
