Zettelkasten/Permanent Notes/20250818165010-liveness-properties.md

id	title	type	created	modified	tags
20250818165010	Liveness Properties	permanent	2025-08-18T20:50:10Z	2025-08-18T20:54:38Z

Liveness Properties

Liveness properties are kinda the dual of safety-properties, but instead they say that something good will eventually happen.

Here's an example:

If there's someone waiting, the light will eventually turn green:

G(request \rightarrow F\, green)