So, how do we wrap up the first seventy pages of the book Temporal logics in computer science: finite-state systems or the first 90+ pages of the Principles of Model Checking 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]
- I/O actions have the form 𝑁(𝑥, 𝑟) for an action name 𝑁, an output 𝑥 forwarded to the environment, and an input 𝑟 obtained from the environment.
- 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. 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!
… and there are short versions out there, e.g., this slide deck ↩︎
see this paper for details, in §3 ↩︎
It turns out that traces can also be infinite, but that’s for another day’s post. ↩︎
It turns out, there’s hardly a canonical way to equate to systems The linear time — Branching time spectrum II | SpringerLink ↩︎
see also these slides ↩︎