|Process algebras have non-observable (\tau) actions that are discarded by weak bisimulation etc., couldn't these be seen as playing a similar role as stuttering steps in TLA? The analogy is imperfect due to the linear-vs.-branching view of system behaviors, however.|
Unlike process algebras, TLA has no program / process structure (and in particular no recursive definitions of process behavior) but represents systems as state machines: all recursion is embodied by the  operator of temporal logic.--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/408955CA-B884-42D0-B708-287487FE11F6%40gmail.com.