Abstract:Formal verification and monitorability are based on finite observations, which allow properties to be verified from finite information about system behaviour. We study such observations through the topologies they generate on spaces of processes. We first consider trace-based topologies and show that finite trace observations on $\Sigma^\omega$ induce the Cantor topology, while the topology corresponding to full trace inclusion is the discrete one. We then move to arbitrary process spaces, where finite trace observations define the topology $\tau_O$, and show that simulation observations generate a strictly finer topology $\tau_{\mathrm{sim}}$. Next, we prove a general verification theorem showing that, for any topology generated by finite observations, open sets are exactly the properties verifiable by those observations. We instantiate this result for $\tau_O$ and $\tau_{\mathrm{sim}}$, obtaining multi-trace and simulation monitorability as concrete cases. Finally, we examine the effect of replacing simulation with stronger relations, showing that finite-depth bisimulation yields a genuinely different topology.
From: Vasiliki Kyriakou [view email]
[v1]
Mon, 22 Jun 2026 22:04:54 UTC (58 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。