A Topological Framework for Finite Behavioural Observations and Verification

Antonis Achilleos; Vasiliki Kyriakou

arxiv: 2606.23975 · v1 · pith:A43ZNTI2new · submitted 2026-06-22 · 💻 cs.LO

A Topological Framework for Finite Behavioural Observations and Verification

Antonis Achilleos , Vasiliki Kyriakou This is my paper

Pith reviewed 2026-06-26 05:54 UTC · model grok-4.3

classification 💻 cs.LO

keywords topological frameworkfinite observationsverificationmonitorabilitytrace topologysimulation topologyprocess semanticsbehavioural observations

0 comments

The pith

For any topology generated by finite observations, open sets are exactly the verifiable properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that topologies arising from finite behavioral observations on processes have a direct correspondence to verification: a property is open precisely when it can be confirmed using only the finite observations that generate the topology. Trace observations on infinite words produce the Cantor topology, while simulation relations produce a strictly finer one called τ_sim. A general theorem then equates openness in any such observation topology with monitorability under those observations, and the authors instantiate it for both trace and simulation cases. Stronger relations such as finite-depth bisimulation induce still different topologies.

Core claim

The central claim is that for any topology generated by finite observations, the open sets are exactly the properties verifiable by those observations. The authors first establish that finite traces on Σ^ω yield the Cantor topology while full trace inclusion yields the discrete topology, then define τ_O from finite traces on arbitrary process spaces and show that simulation observations generate the strictly finer τ_sim. The general verification theorem is proved for any observation-generated topology, after which it is applied to obtain multi-trace monitorability for τ_O and simulation monitorability for τ_sim.

What carries the argument

The general verification theorem equating open sets in an observation-generated topology with properties verifiable by the generating finite observations.

If this is right

Finite trace observations on infinite words induce the Cantor topology.
Simulation observations generate a strictly finer topology than trace observations.
Multi-trace monitorability and simulation monitorability follow directly as instances of the general theorem.
Replacing simulation by finite-depth bisimulation produces a genuinely different topology.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The framework allows direct comparison of different observation mechanisms by the topologies they induce.
Results may extend to other process models such as timed or probabilistic systems by defining suitable finite observations.
Monitorability questions in new settings can be reduced to checking whether candidate properties are open in the induced topology.

Load-bearing premise

The topologies τ_O and τ_sim are generated exactly by the stated finite observations in the standard topological sense, without extra structure on the process space.

What would settle it

A concrete property that is open in τ_O (or τ_sim) yet cannot be verified by any finite collection of the corresponding observations, or a property verifiable by finite observations that fails to be open.

Figures

Figures reproduced from arXiv: 2606.23975 by Antonis Achilleos, Vasiliki Kyriakou.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper sets up trace and simulation topologies on processes and links monitorability to openness, but the general theorem is the standard basis definition rather than a new insight.

read the letter

The main takeaway is that this work organizes monitorability results by defining two topologies on process spaces and showing they capture what finite observations can verify. τ_O comes from finite traces and τ_sim from simulations, with the latter strictly finer. They also note that finite-depth bisimulation produces yet another topology. The general verification theorem then says open sets match the verifiable properties for any such observation-generated topology.

The concrete constructions and the comparison between τ_O, τ_sim, and bisimulation are the parts that feel fresh. The paper does a clean job of instantiating the result to recover multi-trace and simulation monitorability as special cases, and the Cantor versus discrete topology distinction on infinite words is a useful starting point.

The soft spot is the general theorem itself. It amounts to the usual fact that a set is open precisely when every point has a basis element inside it, and here the basis elements are the finite observations. The stress-test note is right that nothing in the setup breaks this correspondence, so the theorem follows directly once the topologies are defined. That does not make the work wrong, but it means the contribution sits more in the process-algebra applications than in a surprising topological result.

This is for people already working in concurrency theory or formal verification who want a topological language for monitorability questions. The math looks internally consistent and the citations are appropriate for the subfield. I would send it to peer review in a specialized venue because the constructions are explicit and the distinctions they draw are checkable, even if the core equivalence is expected.

Referee Report

0 major / 2 minor

Summary. The paper develops a topological framework linking finite behavioural observations to verification in process spaces. It shows that finite traces on Σ^ω generate the Cantor topology while full trace inclusion yields the discrete topology; defines τ_O from finite traces and the strictly finer τ_sim from simulation observations on general process spaces; proves a general theorem equating open sets in any observation-generated topology with properties verifiable from those finite observations; instantiates the result to obtain multi-trace and simulation monitorability; and shows that finite-depth bisimulation produces a distinct topology.

Significance. If the general verification theorem and the constructions of τ_O and τ_sim hold, the work supplies a clean topological unification of monitorability concepts, directly equating openness with finite verifiability. This could serve as a reusable foundation for comparing observation bases (traces, simulations, bisimulations) in concurrency theory and runtime verification.

minor comments (2)

[Abstract] Abstract: the statement of the general verification theorem is described at a high level but not formulated; adding a one-sentence version of the theorem would improve readability.
[Section on bisimulation topologies] The paper distinguishes τ_sim from finite-depth bisimulation topologies but does not quantify the separation (e.g., via an explicit example process pair that is separated in one but not the other); a concrete counter-example in § on bisimulation would strengthen the claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper and for recommending minor revision. No specific major comments appear in the report, so we have no points to address point-by-point at this stage. We will prepare a revised version incorporating any minor suggestions that may arise from further review.

Circularity Check

1 steps flagged

General verification theorem reduces to standard definition of openness

specific steps

self definitional [Abstract]
"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 τ_O and τ_sim, obtaining multi-trace and simulation monitorability as concrete cases."

The topology generated by finite observations is defined so that its open sets are exactly those for which membership can be confirmed by a finite observation forcing all compatible processes into the set. The claimed theorem therefore restates this definitional property rather than deriving it from separate principles; the instantiations for τ_O and τ_sim inherit the same reduction.

full rationale

The paper's central result equates openness in any topology generated by finite observations with verifiability by those observations. This equivalence holds by the definition of the topology generated by a basis (or subbasis) of observations: a set is open precisely when every point in it has a basis element contained in the set. The constructions of τ_O and τ_sim are presented as instances of this standard generation process on process spaces, making the 'theorem' and its instantiations true by construction of the topologies rather than independent derivation. No equations, fitted parameters, or self-citation chains are involved, but the load-bearing claim reduces directly to the setup.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Based solely on the abstract, the paper relies on standard mathematical definitions of topology and domain-specific notions from process algebra; no free parameters, invented entities, or ad-hoc axioms are mentioned.

axioms (2)

standard math Standard definition of the Cantor topology on Σ^ω
Invoked when stating that finite trace observations induce the Cantor topology.
domain assumption Standard definitions of trace inclusion and simulation relations on process spaces
Used to define τ_O and the finer τ_sim.

pith-pipeline@v0.9.1-grok · 5695 in / 1205 out tokens · 22337 ms · 2026-06-26T05:54:22.449119+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

32 extracted references · 20 canonical work pages · 1 internal anchor

[1]

arXiv:1112.0347

Samson Abramsky (2011):Domain Theory and the Logic of Observable Properties. arXiv:1112.0347

Pith/arXiv arXiv 2011
[2]

Samson Abramsky & Steven Vickers (1993):Quantales, Observational Logic and Process Semantics.Math. Struct. Comput. Sci.3(2), pp. 161–227, doi:10.1017/S0960129500000189

work page doi:10.1017/s0960129500000189 1993
[3]

In:International Conference on Foundations of Software Science and Computation Structures, Springer, pp

Luca Aceto, Antonis Achilleos, Adrian Francalanza & Anna Ingólfsdóttir (2018):A framework for param- eterized monitorability. In:International Conference on Foundations of Software Science and Computation Structures, Springer, pp. 203–220

2018
[4]

ACM Program

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir & Karoliina Lehtinen (2019):Adven- tures in monitorability: from branching to linear time and back again.Proc. ACM Program. Lang.3(POPL), doi:10.1145/3290365. Available athttps://doi.org/10.1145/3290365

work page doi:10.1145/3290365 2019
[5]

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir & Karoliina Lehtinen (2021):An operational guide to monitorability with applications to regular properties.Software and Systems Modeling 20, pp. 335–361. DOI:https://doi.org/10.1007/s10270-020-00860-z

work page doi:10.1007/s10270-020-00860-z 2021
[6]

Luca Aceto, Dario Della Monica, Ignacio Fábregas & Anna Ingólfsdóttir (2019):When Are Prime Formulae Characteristic?Theor. Comput. Sci.777, pp. 3–31, doi:10.1016/J.TCS.2018.12.004

work page doi:10.1016/j.tcs.2018.12.004 2019
[7]

Technical Report 59, BRICS, De- partment of Computer Science, Aarhus University, doi:10.7146/brics.v2i59.19960

Luca Aceto & Anna Ingolfsdottir (1995):On the Finitary Bisimulation. Technical Report 59, BRICS, De- partment of Computer Science, Aarhus University, doi:10.7146/brics.v2i59.19960. Available athttps: //doi.org/10.7146/brics.v2i59.19960

work page doi:10.7146/brics.v2i59.19960 1995
[8]

Cambridge University Press, doi:10.1017/CBO9780511814105

Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen & Jiri Srba (2007):Reactive systems: modelling, specification and verification. Cambridge University Press, doi:10.1017/CBO9780511814105

work page doi:10.1017/cbo9780511814105 2007
[9]

Luca Aceto, Anna Ingólfsdóttir, Paul Blain Levy & Joshua Sack (2012):Characteristic formulae for fixed-point semantics: a general framework.Math. Struct. Comput. Sci.22(2), pp. 125–173, doi:10.1017/S0960129511000375

work page doi:10.1017/s0960129511000375 2012
[10]

127–134, doi:https://doi.org/10.1016/S0020-0190(97)00163-4

Luca Aceto & Anna Ingólfsdóttir (1997):A characterization of finitary bisimulation.Information Processing Letters64(3), pp. 127–134, doi:https://doi.org/10.1016/S0020-0190(97)00163-4. Available athttps:// www.sciencedirect.com/science/article/pii/S0020019097001634

work page doi:10.1016/s0020-0190(97)00163-4 1997
[11]

In:Lectures on Runtime Verification: Introductory and Advanced Topics, Springer, pp

Ezio Bartocci, Yliès Falcone, Adrian Francalanza & Giles Reger (2018):Introduction to runtime verification. In:Lectures on Runtime Verification: Introductory and Advanced Topics, Springer, pp. 1–33

2018
[12]

Berlin (1938):Verification.Proceedings of the Aristotelian Society39, pp

I. Berlin (1938):Verification.Proceedings of the Aristotelian Society39, pp. 225–248. Available athttp: //www.jstor.org/stable/4544328

arXiv 1938
[13]

The complexity of being monitorable

Riccardo Camerlo & Francesco Dagnino (2026):The Complexity of Being Monitorable.https://doi. org/10.48550/arXiv.2601.04256

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2601.04256 2026
[14]

In Irène Guessarian, editor:Semantics of Systems of Concurrent Processes, Springer Berlin Heidelberg, Berlin, Heidelberg, pp

Rocco De Nicola & Frits Vaandrager (1990):Action versus state based logics for transition systems. In Irène Guessarian, editor:Semantics of Systems of Concurrent Processes, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 407–419

1990
[15]

Theoretical Computer Science537, pp

V olker Diekert & Martin Leucker (2014):Topology, monitorable properties and runtime verification. Theoretical Computer Science537, pp. 29–41. Theoretical Aspects of Computing (ICTAC 2011). DOI: 10.1016/j.tcs.2014.02.052

work page doi:10.1016/j.tcs.2014.02.052 2014
[16]

Kit Fine (1975):Normal forms in modal logic.Notre Dame journal of formal logic16(2), pp. 229–237

1975
[17]

van Glabbeek (2001):The Linear Time–Branching Time Spectrum I

Rob J. van Glabbeek (2001):The Linear Time–Branching Time Spectrum I. In Jan A. Bergstra, Alban Ponse & Scott A. Smolka, editors:Handbook of Process Algebra, North-Holland / Elsevier, pp. 3–99, doi:10.1016/B978-044482830-9/50019-9

work page doi:10.1016/b978-044482830-9/50019-9 2001
[18]

Control.68(1-3), pp

Susanne Graf & Joseph Sifakis (1986):A Modal Characterization of Observational Congruence on Finite Terms of CCS.Inf. Control.68(1-3), pp. 125–145, doi:10.1016/S0019-9958(86)80031-6

work page doi:10.1016/s0019-9958(86)80031-6 1986
[19]

Vaandrager (1992):Structured Operational Semantics and Bisimulation as a Congruence.Inf

Jan Friso Groote & Frits W. Vaandrager (1992):Structured Operational Semantics and Bisimulation as a Congruence.Inf. Comput.100(2), pp. 202–260, doi:10.1016/0890-5401(92)90013-6. 16Topological Verification

work page doi:10.1016/0890-5401(92)90013-6 1992
[20]

Harel & A

D. Harel & A. Pnueli (1985):On the Development of Reactive Systems. In Krzysztof R. Apt, editor: Logics and Models of Concurrent Systems, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 477–498, doi:10.1007/978-3-642-82453-1_17

work page doi:10.1007/978-3-642-82453-1_17 1985
[21]

ACM 32(1), pp

Matthew Hennessy & Robin Milner (1985):Algebraic Laws for Nondeterminism and Concurrency.J. ACM 32(1), pp. 137–161, doi:10.1145/2455.2460

work page doi:10.1145/2455.2460 1985
[22]

A. S. Kechris (1995):Classical Descriptive Set Theory. Springer-Verlag, New York

1995
[23]

Kleijnen (1995):Verification and validation of simulation models.European Journal of Operational Research82(1), pp

Jack P.C. Kleijnen (1995):Verification and validation of simulation models.European Journal of Operational Research82(1), pp. 145–162, doi:https://doi.org/10.1016/0377-2217(94)00016-6. Available athttps:// www.sciencedirect.com/science/article/pii/0377221794000166

work page doi:10.1016/0377-2217(94)00016-6 1995
[24]

A brief account of runtime verification.Journal of Logic and Algebraic Programming, 78(5):293–303, 2009

Martin Leucker & Christian Schallhart (2009):A brief account of runtime verification.The Journal of Logic and Algebraic Programming78(5), pp. 293–303, doi:https://doi.org/10.1016/j.jlap.2008.08.004. Available at https://www.sciencedirect.com/science/article/pii/S1567832608000775. The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Softw...

work page doi:10.1016/j.jlap.2008.08.004 2009
[25]

Milner (1989):Communication and Concurrency

R. Milner (1989):Communication and Concurrency. Prentice-Hall, Inc

1989
[26]

Y . N. Moschovakis (2009):Descriptive Set Theory, second edition.Mathematical Surveys and Monographs 155, American Mathematical Society

2009
[27]

In Kim G

Ji ˇrí Srba (2001):On the Power of Labels in Transition Systems. In Kim G. Larsen & Mogens Nielsen, editors: CONCUR 2001 — Concurrency Theory, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 277–291

2001
[28]

Comput.110(1), pp

Bernhard Steffen & Anna Ingólfsdóttir (1994):Characteristic Formulae for Processes with Divergence.Inf. Comput.110(1), pp. 149–163, doi:10.1006/INCO.1994.1028

work page doi:10.1006/inco.1994.1028 1994
[29]

Technical Report, Los Alamos National Lab., Los Alamos, NM (US), doi:10.2172/835920

B H Thacker, S W Doebling, F M Hemez, M C Anderson, J E Pepin & E A Rodriguez (2004):Concepts of Model Verification and Validation. Technical Report, Los Alamos National Lab., Los Alamos, NM (US), doi:10.2172/835920. Available athttps://www.osti.gov/biblio/835920

work page doi:10.2172/835920 2004
[30]

In Robert M

Jan Tretmans (2008):Model Based Testing with Labelled Transition Systems. In Robert M. Hi- erons, Jonathan P. Bowen & Mark Harman, editors:Formal Methods and Testing: An Outcome of the FORTEST Network, Revised Selected Papers, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 1–38, doi:10.1007/978-3-540-78917-8_1. Available athttps://doi.org/10.1007/978...

work page doi:10.1007/978-3-540-78917-8_1 2008
[31]

Antonis Achilleos and Vasiliki Kyriakou17 A Appendix A.1 Proofs on Trace-Based Topologies Proof of Lemma 3.3

Steven Vickers (1988):Topology via Logic.Cambridge Tracts in Theoretical Computer Science5, Cambridge University Press. Antonis Achilleos and Vasiliki Kyriakou17 A Appendix A.1 Proofs on Trace-Based Topologies Proof of Lemma 3.3. (i)(∅,Proc∈τ(⊑ T ).) Both∅and Proc are upward-closed. Indeed,∅is upward- closed , since it has no elements. Moreover, Proc is u...

1988
[32]

For the case of⊑ f in T andL T , observe that Trc(p)is finite

and [18] (but see also [16]) can also be adapted to the rest of the cases of the theorem, but for completeness, we prove these in the following. For the case of⊑ f in T andL T , observe that Trc(p)is finite. Then, we can defineϕ= V s∈Trc(p) ϕ(s). The theorem follows from Lemma A.2. For the remaining case of∼ k, we use induction onk. Fork=0, observe thatp∼...

[1] [1]

arXiv:1112.0347

Samson Abramsky (2011):Domain Theory and the Logic of Observable Properties. arXiv:1112.0347

Pith/arXiv arXiv 2011

[2] [2]

Samson Abramsky & Steven Vickers (1993):Quantales, Observational Logic and Process Semantics.Math. Struct. Comput. Sci.3(2), pp. 161–227, doi:10.1017/S0960129500000189

work page doi:10.1017/s0960129500000189 1993

[3] [3]

In:International Conference on Foundations of Software Science and Computation Structures, Springer, pp

Luca Aceto, Antonis Achilleos, Adrian Francalanza & Anna Ingólfsdóttir (2018):A framework for param- eterized monitorability. In:International Conference on Foundations of Software Science and Computation Structures, Springer, pp. 203–220

2018

[4] [4]

ACM Program

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir & Karoliina Lehtinen (2019):Adven- tures in monitorability: from branching to linear time and back again.Proc. ACM Program. Lang.3(POPL), doi:10.1145/3290365. Available athttps://doi.org/10.1145/3290365

work page doi:10.1145/3290365 2019

[5] [5]

Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir & Karoliina Lehtinen (2021):An operational guide to monitorability with applications to regular properties.Software and Systems Modeling 20, pp. 335–361. DOI:https://doi.org/10.1007/s10270-020-00860-z

work page doi:10.1007/s10270-020-00860-z 2021

[6] [6]

Luca Aceto, Dario Della Monica, Ignacio Fábregas & Anna Ingólfsdóttir (2019):When Are Prime Formulae Characteristic?Theor. Comput. Sci.777, pp. 3–31, doi:10.1016/J.TCS.2018.12.004

work page doi:10.1016/j.tcs.2018.12.004 2019

[7] [7]

Technical Report 59, BRICS, De- partment of Computer Science, Aarhus University, doi:10.7146/brics.v2i59.19960

Luca Aceto & Anna Ingolfsdottir (1995):On the Finitary Bisimulation. Technical Report 59, BRICS, De- partment of Computer Science, Aarhus University, doi:10.7146/brics.v2i59.19960. Available athttps: //doi.org/10.7146/brics.v2i59.19960

work page doi:10.7146/brics.v2i59.19960 1995

[8] [8]

Cambridge University Press, doi:10.1017/CBO9780511814105

Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen & Jiri Srba (2007):Reactive systems: modelling, specification and verification. Cambridge University Press, doi:10.1017/CBO9780511814105

work page doi:10.1017/cbo9780511814105 2007

[9] [9]

Luca Aceto, Anna Ingólfsdóttir, Paul Blain Levy & Joshua Sack (2012):Characteristic formulae for fixed-point semantics: a general framework.Math. Struct. Comput. Sci.22(2), pp. 125–173, doi:10.1017/S0960129511000375

work page doi:10.1017/s0960129511000375 2012

[10] [10]

127–134, doi:https://doi.org/10.1016/S0020-0190(97)00163-4

Luca Aceto & Anna Ingólfsdóttir (1997):A characterization of finitary bisimulation.Information Processing Letters64(3), pp. 127–134, doi:https://doi.org/10.1016/S0020-0190(97)00163-4. Available athttps:// www.sciencedirect.com/science/article/pii/S0020019097001634

work page doi:10.1016/s0020-0190(97)00163-4 1997

[11] [11]

In:Lectures on Runtime Verification: Introductory and Advanced Topics, Springer, pp

Ezio Bartocci, Yliès Falcone, Adrian Francalanza & Giles Reger (2018):Introduction to runtime verification. In:Lectures on Runtime Verification: Introductory and Advanced Topics, Springer, pp. 1–33

2018

[12] [12]

Berlin (1938):Verification.Proceedings of the Aristotelian Society39, pp

I. Berlin (1938):Verification.Proceedings of the Aristotelian Society39, pp. 225–248. Available athttp: //www.jstor.org/stable/4544328

arXiv 1938

[13] [13]

The complexity of being monitorable

Riccardo Camerlo & Francesco Dagnino (2026):The Complexity of Being Monitorable.https://doi. org/10.48550/arXiv.2601.04256

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2601.04256 2026

[14] [14]

In Irène Guessarian, editor:Semantics of Systems of Concurrent Processes, Springer Berlin Heidelberg, Berlin, Heidelberg, pp

Rocco De Nicola & Frits Vaandrager (1990):Action versus state based logics for transition systems. In Irène Guessarian, editor:Semantics of Systems of Concurrent Processes, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 407–419

1990

[15] [15]

Theoretical Computer Science537, pp

V olker Diekert & Martin Leucker (2014):Topology, monitorable properties and runtime verification. Theoretical Computer Science537, pp. 29–41. Theoretical Aspects of Computing (ICTAC 2011). DOI: 10.1016/j.tcs.2014.02.052

work page doi:10.1016/j.tcs.2014.02.052 2014

[16] [16]

Kit Fine (1975):Normal forms in modal logic.Notre Dame journal of formal logic16(2), pp. 229–237

1975

[17] [17]

van Glabbeek (2001):The Linear Time–Branching Time Spectrum I

Rob J. van Glabbeek (2001):The Linear Time–Branching Time Spectrum I. In Jan A. Bergstra, Alban Ponse & Scott A. Smolka, editors:Handbook of Process Algebra, North-Holland / Elsevier, pp. 3–99, doi:10.1016/B978-044482830-9/50019-9

work page doi:10.1016/b978-044482830-9/50019-9 2001

[18] [18]

Control.68(1-3), pp

Susanne Graf & Joseph Sifakis (1986):A Modal Characterization of Observational Congruence on Finite Terms of CCS.Inf. Control.68(1-3), pp. 125–145, doi:10.1016/S0019-9958(86)80031-6

work page doi:10.1016/s0019-9958(86)80031-6 1986

[19] [19]

Vaandrager (1992):Structured Operational Semantics and Bisimulation as a Congruence.Inf

Jan Friso Groote & Frits W. Vaandrager (1992):Structured Operational Semantics and Bisimulation as a Congruence.Inf. Comput.100(2), pp. 202–260, doi:10.1016/0890-5401(92)90013-6. 16Topological Verification

work page doi:10.1016/0890-5401(92)90013-6 1992

[20] [20]

Harel & A

D. Harel & A. Pnueli (1985):On the Development of Reactive Systems. In Krzysztof R. Apt, editor: Logics and Models of Concurrent Systems, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 477–498, doi:10.1007/978-3-642-82453-1_17

work page doi:10.1007/978-3-642-82453-1_17 1985

[21] [21]

ACM 32(1), pp

Matthew Hennessy & Robin Milner (1985):Algebraic Laws for Nondeterminism and Concurrency.J. ACM 32(1), pp. 137–161, doi:10.1145/2455.2460

work page doi:10.1145/2455.2460 1985

[22] [22]

A. S. Kechris (1995):Classical Descriptive Set Theory. Springer-Verlag, New York

1995

[23] [23]

Kleijnen (1995):Verification and validation of simulation models.European Journal of Operational Research82(1), pp

Jack P.C. Kleijnen (1995):Verification and validation of simulation models.European Journal of Operational Research82(1), pp. 145–162, doi:https://doi.org/10.1016/0377-2217(94)00016-6. Available athttps:// www.sciencedirect.com/science/article/pii/0377221794000166

work page doi:10.1016/0377-2217(94)00016-6 1995

[24] [24]

A brief account of runtime verification.Journal of Logic and Algebraic Programming, 78(5):293–303, 2009

Martin Leucker & Christian Schallhart (2009):A brief account of runtime verification.The Journal of Logic and Algebraic Programming78(5), pp. 293–303, doi:https://doi.org/10.1016/j.jlap.2008.08.004. Available at https://www.sciencedirect.com/science/article/pii/S1567832608000775. The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Softw...

work page doi:10.1016/j.jlap.2008.08.004 2009

[25] [25]

Milner (1989):Communication and Concurrency

R. Milner (1989):Communication and Concurrency. Prentice-Hall, Inc

1989

[26] [26]

Y . N. Moschovakis (2009):Descriptive Set Theory, second edition.Mathematical Surveys and Monographs 155, American Mathematical Society

2009

[27] [27]

In Kim G

Ji ˇrí Srba (2001):On the Power of Labels in Transition Systems. In Kim G. Larsen & Mogens Nielsen, editors: CONCUR 2001 — Concurrency Theory, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 277–291

2001

[28] [28]

Comput.110(1), pp

Bernhard Steffen & Anna Ingólfsdóttir (1994):Characteristic Formulae for Processes with Divergence.Inf. Comput.110(1), pp. 149–163, doi:10.1006/INCO.1994.1028

work page doi:10.1006/inco.1994.1028 1994

[29] [29]

Technical Report, Los Alamos National Lab., Los Alamos, NM (US), doi:10.2172/835920

B H Thacker, S W Doebling, F M Hemez, M C Anderson, J E Pepin & E A Rodriguez (2004):Concepts of Model Verification and Validation. Technical Report, Los Alamos National Lab., Los Alamos, NM (US), doi:10.2172/835920. Available athttps://www.osti.gov/biblio/835920

work page doi:10.2172/835920 2004

[30] [30]

In Robert M

Jan Tretmans (2008):Model Based Testing with Labelled Transition Systems. In Robert M. Hi- erons, Jonathan P. Bowen & Mark Harman, editors:Formal Methods and Testing: An Outcome of the FORTEST Network, Revised Selected Papers, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 1–38, doi:10.1007/978-3-540-78917-8_1. Available athttps://doi.org/10.1007/978...

work page doi:10.1007/978-3-540-78917-8_1 2008

[31] [31]

Antonis Achilleos and Vasiliki Kyriakou17 A Appendix A.1 Proofs on Trace-Based Topologies Proof of Lemma 3.3

Steven Vickers (1988):Topology via Logic.Cambridge Tracts in Theoretical Computer Science5, Cambridge University Press. Antonis Achilleos and Vasiliki Kyriakou17 A Appendix A.1 Proofs on Trace-Based Topologies Proof of Lemma 3.3. (i)(∅,Proc∈τ(⊑ T ).) Both∅and Proc are upward-closed. Indeed,∅is upward- closed , since it has no elements. Moreover, Proc is u...

1988

[32] [32]

For the case of⊑ f in T andL T , observe that Trc(p)is finite

and [18] (but see also [16]) can also be adapted to the rest of the cases of the theorem, but for completeness, we prove these in the following. For the case of⊑ f in T andL T , observe that Trc(p)is finite. Then, we can defineϕ= V s∈Trc(p) ϕ(s). The theorem follows from Lemma A.2. For the remaining case of∼ k, we use induction onk. Fork=0, observe thatp∼...