# What's a trace property anyway? **URL:** \ **Category:** Information flow properties\ **Created:** [October 16, 2025, 1:13pm UTC](https://forum.anoma.net/t/whats-a-trace-property-anyway/2384 "2025-10-16T13:13:08Z")\ **Posts on this page:** 1\ **Page:** 1
**Author:** ![graphomath](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/graphomath/32/9_2.png) [@graphomath](https://forum.anoma.net/u/graphomath)\ **Post date:** [October 16, 2025, 1:13pm UTC](https://forum.anoma.net/t/whats-a-trace-property-anyway/2384/1 "2025-10-16T13:13:08Z")
So, how do we wrap up the first seventy pages of the book [Temporal logics in computer science: finite-state systems](https://books.google.com/books?hl=en&lr=&id=B7IkDQAAQBAJ&oi=fnd&pg=PA1&ots=Ho9oAQH_3g&sig=jp18L4B780zMGdHZ1F8buE7yPPE) or the first 90+ pages of the [Principles of Model Checking](https://is.ifmo.ru/books/_principles_of_model_checking.pdf) in a paragraph? Well, we don’t,\[1\] but we go one step back and ask _when are two systems observationally equivalent?_ If you are reminded of something like\[2\] > “looks like a duck, and swims like a duck, and quacks like a duck, then it is probably a duck” you are on the right track. Especially since objects are “just” a specific case of stream transformers, i.e., something that listens to receive messages and replies, … ok, but let’s get to the point! ## I/O behaviour The possible interactions of a program are its _I/O behaviour_, which we can define in two bullets:\[3\] 1. _I/O actions_ have the form 𝑁(𝑥, 𝑟) for an _action name_ 𝑁, an _output_ 𝑥 forwarded to the environment, and an _input_ 𝑟 obtained from the environment. 2. A program’s _I/O behavior_ is the set of traces of all partial program executions (if run on an object). Thus a _trace_ is roughly a string over an alphabet whose letters have the shape 𝑁(𝑥, 𝑟).\[4\] **TL;DR** _There’s a general trick!_ Abstract any system and just look at all possible ways in which it could interact with its environment. Traces is one way of capturing an interaction with the environment.\[5\] ## Trace properties Now, why is this relevant? Well, the answer is hinted at in the title: trace properties. A _trace property_ is just a set of traces. Finally, a system satisfies a property if its traces are _included_ in the property. Simple as that.\[6\] One fun fact about traces is that we can get an extremely succinct definition of a safety property as a set of “forbidden” prefixes of traces. So, if a safety property is violated by a system, there is one run whose prefix is forbidden. Last but not least, a liveness property is any property that is not a safety property. Now, we also can explain why liveness properties are so hard: we cannot tell by finite observation whether they are true or not. ## Why this post ?! Applications on the highest level of abstraction are interactions between the system and the environment, which may be hosting a finite set of observers. So, we have additional structure on the action alphabet: each action is performed by a player or is a response that is addressed to players of the game. Oh, yes, each dapp is to be thought of as a [vast multi-player game](http://erights.org/elib/capability/ode/overview.html). And the good news is that traces are still useful to describe the _possible_ plays (w/o the need to assign rewards). ## What’s next? Hyperproperties. Stay tuned! * * * 1. … _and_ there are short versions out there, e.g., [this slide deck](https://lmf.di.uminho.pt/ic-1819/slides/IeC1819-LTS2.pdf) 2. see e.g., [here](https://edbennett.github.io/python-oop-novice/06-duck/index.html) 3. see [this paper](https://doi.org/10.1145/3658644.3690303) for details, in §3 4. It turns out that traces can also be infinite, but that’s for another day’s post. 5. It turns out, there’s hardly a canonical way to equate to systems [The linear time — Branching time spectrum II | SpringerLink](https://link.springer.com/chapter/10.1007/3-540-57208-2_6) 6. see also [these slides](https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec3.pdf)