Deterministic computations whose history is independent of the order of asynchronous updating
Peter Gacs

TL;DR
This paper investigates the conditions under which the history of state updates in asynchronous networks remains consistent regardless of update order, introducing the concept of commutativity as a sufficient condition for invariant histories.
Contribution
It establishes that invariant histories are generally undecidable but provides a simple, practical sufficient condition called commutativity for ensuring order-independent outcomes.
Findings
Invariant histories are typically undecidable.
Commutativity guarantees order-independent update results.
Provides a practical criterion for designing asynchronous systems.
Abstract
Consider a network of processors (sites) in which each site x has a finite set N(x) of neighbors. There is a transition function f that for each site x computes the next state \xi(x) from the states in N(x). But these transitions (updates) are applied in arbitrary order, one or many at a time. If the state of site x at time t is \eta(x,t) then let us define the sequence \zeta(x,0), \zeta(x,1), ... by taking the sequence \eta(x,0), \eta(x,1), ..., and deleting repetitions. The function f is said to have invariant histories if the sequence \zeta(x,i), (while it lasts, in case it is finite) depends only on the initial configuration, not on the order of updates. This paper shows that though the invariant history property is typically undecidable, there is a useful simple sufficient condition, called commutativity: For any configuration, for any pair x,y of neighbors, if the updating would…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Petri Nets in System Modeling
