Reference. Defining Liveness [alpern-schneider-1985]

October 7, 1985
Bowen Alpern, Fred B. Schneider
Information Processing Letters, Volume 21, Issue 4
10.1016/0020-0190(85)90056-0

Backlinks

Progress on linear-temporal properties research notes [loc-003Z]

April 12, 2026
Liam O'Connor

I have made significant additions to my research notes on Linear-time temporal properties. Now I have all the relevant content from Defining Liveness, and some of the definitions that will appear in the forthcoming journal paper from me and Rayhana Amjad. This paper finally got reviews back, and we have quite a few things to do but I'm confident we'll get there.

Begun Notes on Linear-time Temporal Properties [loc-0039]

February 15, 2026
Liam O'Connor

In my work with Rayhana Amjad and Rob van Glabbeek, I've been thinking a bit about the space of linear-time temporal properties $\Sigma ^\omega$ . There are a lot of results about this, some of which we're still working on proving. While the canonical account will be in our forthcoming journal paper and Rayhana's PhD thesis, I'm going to start writing a research notebook on this topic. I've decided to do this rather than blog about our results, because it's more in the spirit of Zettelkästen (Zettelkastengeist?) — the post I had in mind ended up ballooning in size because it needed so much context. Instead, I will just fill in the notebook including our current conjectures.

Currently, there isn't much there, just some basic definitions from Defining Liveness. But I will eventually hopefully have a fairly well-developed summary of a lot of the work in this area over there.

IFIP WG2.1 Meeting #83 [loc-001U]

September 16, 2025
Liam O'Connor

Last week I attended the meeting of IFIP Working Group 2.1: Algorithmic Languages and Calculi in Viana do Castelo, Portugal. I think all members and observers agreed that it was a good meeting, with (perhaps overly) abundant food and good company. Thanks in particular to José Nuno Oliveira for organising the meeting and to Peter Höfner for serving as chair of WG2.1 for the last six years.

Because this was my third meeting as an observer, I was eligible to be selected as an ongoing member of the group, and I'm happy to say that I was invited to become a member at the conclusion of this meeting.

I presented some new work my student Rayhana and I did with Rob van Glabbeek, classifying monitorability classes topologically.

Reference. Runtime monitoring via topology [oconnor-2025-wg21]

September 10, 2025
Liam O'Connor
IFIP Working Group 2.1: Algorithmic Languages and Calculi Meeting, Viana do Castelo, Portugal

The literature on runtime “verification” (the activity of monitoring a running process to ensure compliance with a given specification) offers many different definitions of “monitorability” for properties. In a linear-time temporal setting, properties take the form of sets of behaviours (infinite sequences of states). In this talk, I will arrange the various monitorability classes found in the literature into a hierarchy along with well-known classes of properties such as safety and guarantee properties. I then give each of these monitorability classes neat topological characterisations within the topology induced by the "guarantee kernel" interior operator. Lastly, I show that the metric space used by Alpern and Schneider coincides with our topology.

This was the sequel of sorts to my prior WG2.1 talk on LTL properties within finite time, which was in turn presenting work from our EXPRESS/SOS paper last year. The topological connection was realised thanks to Nicolas Wu, also a WG2.1 member, who pointed out in the Canberra meeting that the work I was presenting had distinct notes of domain theory. The topological connection was more that of Alpern and Schneider than Scott, but that was the spark that drove this later work, which will hopefully be included in our forthcoming Information and Computation paper.

Views of Spain from the Camarido Beach.

The excursion of the meeting included several stops, including two interesting Viana museums, an archaelogical site on the nearby mountaintop, and a memorable trip to Camarido Beach, at the northernmost tip of Portugal, with Spanish Galicia just to the north along the road from Portugal to Santiago de Compostela.

The climb and the Santuario church.

After the meeting had formally concluded, Oleg Kiselyov, Fritz Henglein, Matija Pretnar, Thomas Sewell, Ningning Xie and I climbed to Santuario de Santa Luzia. We took the arduous stairs rather than the funicular, as Matija's wife had forbidden him from Portuguese funiculars after the recent Ascensor da Glória derailment, which led to me overdoing it and nearly fainting, but in recompense Matija bought me a beer at the top of the mountain which made it (mostly) worth it!

Hopefully I can make it to the next meeting in Estonia next year!

Reference. Runtime monitoring via topology [oconnor-2025-wg21]

September 10, 2025
Liam O'Connor
IFIP Working Group 2.1: Algorithmic Languages and Calculi Meeting, Viana do Castelo, Portugal

The literature on runtime “verification” (the activity of monitoring a running process to ensure compliance with a given specification) offers many different definitions of “monitorability” for properties. In a linear-time temporal setting, properties take the form of sets of behaviours (infinite sequences of states). In this talk, I will arrange the various monitorability classes found in the literature into a hierarchy along with well-known classes of properties such as safety and guarantee properties. I then give each of these monitorability classes neat topological characterisations within the topology induced by the "guarantee kernel" interior operator. Lastly, I show that the metric space used by Alpern and Schneider coincides with our topology.

Construction. Behaviours as topology [ltp-0007]

(from Defining Liveness)

The space $\Sigma ^\omega {}$ forms a topology where safety properties are the closed sets and guarantee properties are the open sets. This follows from Theorem [ltp-000C], Theorem [ltp-000G], and Theorem [ltp-000F] (or, equivalently, from Theorem [ltp-000A], Theorem [ltp-0009] and Theorem [ltp-0008]).

Definition. Guarantee properties [ltp-0005]

Liam O'Connor

A guarantee (or cosafety) property is the complement of a safety property. A guarantee property says that a good thing happens eventually. As with safety properties, the "good thing" is some finite, observable event. In other words, guarantee properties are those properties whose satisfaction can be established by examining only a finite prefix of the behaviour.

For example, the guarantee property "The state $\mathtt {a}$ is eventually reached" is satisfied by any finite prefix containing the state $\mathtt {a}$ .

Leslie Lamport originally called these liveness properties, but we use the more popular definition of that term from Alpern and Schneider.

Theorem. Liveness properties are dense [ltp-000K]

(from Defining Liveness)

In the topology of properties, a property $P$ is a liveness property iff $P$ is dense. In other words, when the safety closure $\overline {P} = \Sigma ^\omega$ .

Proof.

If $\sigma \in \overline {P}$ that means no finite prefix of $\sigma$ can be used to rule out $P$ , i.e. every prefix of $\sigma$ can be extended in some way to a behaviour in $P$ . If $\overline {P} = \Sigma ^\omega$ , this means that every finite prefix can be extended to a behaviour in $P$ , which is exactly the definition of a liveness property.

Definition. Safety closure [ltp-000J]

(from Defining Liveness)

Given a property $P \subseteq \Sigma ^\omega$ , the safety closure of $P$ , written $\overline {P}$ , is the smallest superset of $P$ which is a safety property. It is the dual of the guarantee kernel, so $\underline {P^\complement } = \overline {P}^\complement$ . This means that the safety closure of $P$ contains all behaviours which cannot be shown to violate $P$ by a finite bad prefix.

It follows that $P$ is a safety property iff $\overline {P} = P$ .

This is a closure operator, so it is extensive ( $\overline {P} \supseteq P$ ), idempotent ( $\overline {\overline {P}} = \overline {P}$ ), and monotonic ( $P \subseteq R$ implies $\overline {P} \subseteq \overline {R}$ ).

Topologically speaking, the safety closure is the (limit-)closure.

Intuitively, the safety closure of $P$ is all behaviours for which any finite prefix extended in some way will get into $P$ .

Theorem. Safety-liveness decomposition [ltp-000L]

(from Defining Liveness)

Every property is the intersection of a safety and a liveness property.

Proof.

Let $P$ be a property. Then, let $L$ = $(\overline {P} \setminus P)^\complement$ . Then:

\begin {array}{lcl} L \cap \overline {P} & = & (\overline {P} \setminus P)^\complement \cap \overline {P} \\ & = & (\overline {P}^\complement \cup P) \cap \overline {P} \\ & = & (\overline {P}^\complement \cap \overline {P}) \cup (P \cap \overline {P}) \\ & = & \emptyset \cup (P \cap \overline {P}) \\ & = & P \end {array}

The set $\overline {P}$ is clearly closed and therefore a safety property. It remains to show that $L$ is dense (and therefore a liveness property).

Assume for contradiction that $A = (\overline {P}\setminus P)^\complement$ is not dense, so there exists $\sigma \in \Sigma ^\omega$ such that $\sigma \notin \overline {A}$ . By our definition of safety closure, some finite prefix $u$ of $\sigma$ is a bad prefix of $A$ , meaning no extension of $u$ lies in $A$ . Hence every extension of $u$ lies in $\overline {P} \setminus P$ , i.e. every extension of $u$ lies in $\overline {P}$ but not in $P$ . Because every extension of $u$ lies in $\overline {P}$ , $u$ cannot finitely refute $P$ , so every extension of $u$ must be extendable to some trace in $P$ , contradicting that no extension of $u$ lies in $P$ . Therefore no such $u$ exists, so every behaviour $\sigma$ is in $\overline {A}$ , and $A$ is dense.

Related

Journal. Information Processing Letters [ipl]

https://www.sciencedirect.com/journal/information-processing-letters

Information Processing Letters invites submission of original research articles that focus on fundamental aspects of information processing and computing. This naturally includes work in the broadly understood field of theoretical computer science; although papers in all areas of scientific inquiry will be given consideration, provided that they describe research contributions credibly motivated by applications to computing and involve rigorous methodology. High quality experimental papers that address topics of sufficiently broad interest may also be considered.

Since its inception in 1971, Information Processing Letters has served as a forum for timely dissemination of short, concise and focused research contributions. Continuing with this tradition, and to expedite the reviewing process, manuscripts are generally limited in length to nine pages when they appear in print.