Volitional Multiagent Atomic Transactions: Describing People and their Machines Andy Lewis-Pye1 & Ehud Shapiro1,2 # 1
London School of Economics, UK, and 2 Weizmann Institute of Science, Israel
Abstract
arXiv:2604.25596v1 [cs.DC] 28 Apr 2026
Formal models for concurrent and distributed systems describe machines; the people who operate them are either ignored or treated as external environment. Yet key distributed systems—notably grassroots platforms—include people operating their personal machines (smartphones), and their faithful description must include the states of both people and machines and how they jointly effect system behaviour. Here, we propose volitional multiagent atomic transactions—executed atomically by machines and guarded by their people’s volitions—as a novel mathematical foundation for specifying systems consisting of people operating machines. Each agent’s state consists of a volitional state and machine state; a transaction is enabled when the machine precondition holds and the guarding persons are willing. For example, befriending two people is guarded by both; unfriending, by either; voluntary swap of coins and bonds is guarded by both parties, while a payment is guarded by the payer. We develop the mathematical machinery to express safety and liveness of platforms specified in this framework, and provide example specifications of two grassroots platforms: social networks, and coins and bonds. These specifications are then used by AI to derive working implementations. We employ here a novel and simpler definition of ‘grassroots’ that better captures the informal notion—multiple instances can form and operate independently, yet may coalesce—and show that the platforms specified here, as well as those hitherto proven grassroots under the original definition, are grassroots under the new definition. 2012 ACM Subject Classification Theory of computation → Distributed computing models; Theory of computation → Concurrency; Theory of computation → Operational semantics; Computer systems organization → Peer-to-peer architectures Keywords and phrases Grassroots Protocols, Multiagent Transition Systems, Atomic Transactions, Liveness, Social Networks, Grassroots Coins and Bonds, GLP
1
Introduction
The gap. Formal models for concurrent and distributed systems describe machines; the people who operate them are either ignored or treated as external environment (see Section 5). Across all surveyed formal traditions—Turing’s choice machines [48], CSP [20], CCS [31], I/O automata [30], angelic/demonic nondeterminism [5], ATL [3], game semantics [1], ceremony analysis [16], electronic institutions [17]—the person is modelled as environment, opponent, error source, or unconstrained nondeterministic process, but always as an entity external to the agent, never as a formal component of the agent’s state. Proposal. Here, we propose volitional multiagent atomic transactions—executed atomically by machines and guarded by their people’s volitions—as a formal foundation for specifying systems consisting of people operating machines. Each agent’s state decomposes into a machine state and a volitional state; a transaction is enabled when the machine precondition holds and the guarding persons are willing. Example: Grassroots social graphs. Each agent p maintains a set of friends cp ⊆ P . The social graph evolves via befriending and unfriending, specified as volitional transactions:
2
Describing People and their Machines
1. Befriend: c′p := cp ∪ {q}, c′q := cq ∪ {p}, provided q ∈ / cp . Guarded by {p, q}. 2. Unfriend: c′p := cp \ {q}, c′q := cq \ {p}, provided q ∈ cp . Guarded by p or q. Befriending requires both persons to be willing; unfriending can be initiated by either. The guard determines which persons must be willing for a machine transaction to proceed. This distinction is the essence of volitional multiagent atomic transactions. Further examples— including child-safe social networking and coins and bonds—appear in Section 2.2. Motivating domain: grassroots platforms. Volitional multiagent atomic transactions are a general framework for systems of people operating machines. An example of a class of such systems, which motivated this work, is grassroots platforms [37, 38, 39, 45], which aim to offer an egalitarian alternative to global platforms, centralized and decentralized alike. Grassroots platforms consist of people operating their personal machines (smartphones), and can have multiple instances that emerge and operate independently of each other and of any global resource except the network, yet can interoperate and coalesce once interconnected. Key grassroots platforms include grassroots social networks [38, 26], grassroots coins [39, 25] and bonds [41], and grassroots democratic communities [18, 45, 21]. No platform that operates on a shared global resource—a replicated ledger (Blockchain [33]), a distributed data structure (IPFS [6], DHT [35]), or a distributed pub/sub system with a global directory [12, 13, 10])—is grassroots. BitTorrent [47] and Mastodon [34] are peer-to-peer among servers not people; Scuttlebutt [46, 22] is grassroots in design even if not formally proven as such. An earlier paper [42] introduced atomic transactions for grassroots platforms and presented transactions-based specifications of social graphs, cryptocurrencies, and democratic federations; that work did not address the role of people, transaction equivalence, or liveness, and employed the original definition of grassroots protocols. Framework overview. We develop the mathematical machinery needed to express volitional multiagent atomic transactions and the safety and liveness of grassroots platforms they specify. We introduce transaction equivalence classes, which provide a natural notion of “same action” across configurations, and define liveness in terms of such classes: a run is correct iff every enabled class is eventually taken. We demonstrate the framework with two grassroots platforms: 1. Grassroots social networks [38, 26] let people maintain their friendship connections through local storage and peer-to-peer relationships without central control, with the social graph evolving through befriending and unfriending. 2. Grassroots coins and bonds [39, 25, 41] let each person mint their own coins, backed by the goods and services they offer, and exchange them with others via atomic swaps; bonds extend coins with a maturity date, enabling interest-bearing credit, loans, and the full gamut of financial instruments. The specifications presented here have been used by AI to derive working implementations in GLP, a grassroots multiagent concurrent logic programming language [40], as reported in companion papers [43, 26, 41, 44]. We employ here a novel—simpler than the original [37, 42]— definition of grassroots protocols based on interleavings of correct runs, that better captures the informal notion of grassroots, and show that the platforms specified here, as well as those hitherto proven grassroots under the original definition, are grassroots under the new definition. We also prove that Bitcoin, distributed hash tables, and similar systems are not grassroots. Contributions. This paper provides: (i) a formal foundation for concurrent and distributed systems that encompasses both people and their machines, in which volitions are persistent, inspectable agent state rather than point-of-choice nondeterminism; (ii) safety and liveness
Lewis-Pye and Shapiro
machinery for grassroots platforms, demonstrated on two platforms with AI-derived implementations; and (iii) a simpler definition of grassroots that better captures the informal notion and excludes systems based on shared global data structures. Paper outline. Section 2 presents examples of grassroots platforms specified by guarded transactions, and introduces the formal framework: volitional multiagent atomic transactions, transaction equivalence, and liveness. Section 3 defines protocols and grassroots protocols via interleavings of correct runs, and proves that transactions-based protocols satisfying a natural condition are grassroots. Section 4 presents two grassroots platforms (social networks, coins and bonds), proves their safety properties, and proves that they are grassroots. Section 5 discusses related work. Section 6 concludes and discusses future work. The appendix contains proofs that Bitcoin, distributed hash tables, and IPFS are not grassroots (Appendix A), notes on implementation (Section B), and a detailed survey of formal models of persons in concurrent systems (Appendix C).
2
Volitional Multiagent Transition Systems
Earlier work introduced multiagent transition systems [36], grassroots protocols and platforms [37], and their definition via multiagent atomic transactions [42]—capturing the behaviour of machines but not of the people operating them. Here we develop the mathematical machinery to describe agents consisting of a person and a machine, and the volitional multiagent atomic transactions they execute. A volitional transaction is a “regular” multiagent atomic transaction—henceforth, a machine transaction—guarded by the volitions of some, all, or none of the people whose machines participate; a person’s volitional state is a set of equivalence classes of machine transactions they are willing their machine to participate in. The social graph illustrates the two extremes: befriending is guarded by both p and q (the class of the ‘befriend p and q’ machine transaction must be in both volitions), while unfriending is guarded by either. A person may freely change their volitional state via change-volition transactions; additionally, the framework discharges a class from every agent’s volitional state when any equivalent machine transaction is taken, fulfilling the will upon satisfaction. The definitions of volitional transactions and agent states are mutually-recursive: a volitional transaction is a machine transaction guarded by volitions, which are themselves sets of equivalence classes of machine transactions. We resolve this circularity bottom-up: first machine transactions, then their equivalence, then agent states (including volitional states), and finally volitional transactions.
2.1
Agents, People, Machines, Guarded and Volitional Transactions
We assume a potentially infinite set of agents Π, but consider only finite subsets of it, so when referring to a particular set of agents P ⊂ Π we assume P to be nonempty and finite. We use ⊂ to denote the strict subset relation and ⊆ when equality is also possible, and use p ̸= q ∈ P as a shorthand for p ∈ P ∧ q ∈ P ∧ p = ̸ q. As standard, we use S P to denote the set of all total functions from P to S, and if c ∈ S P we use cp (instead of c(p)) to denote the value of c at p ∈ P . ▶ Definition 2.1 (Machine State, Configuration, Transaction, Guarded Transaction). Given an arbitrary set S of machine states, with a designated initial state s0 ∈ S, and agents Q ⊂ Π, a machine configuration over Q is a member of S Q , and a machine transaction
3
4
Describing People and their Machines
over participants Q is a pair c → c′ ∈ (S Q )2 such that c = ̸ c′ . Given such a machine ′ transaction t, a guarded transaction over t is a pair (t, Q ) where Q′ ⊆ Q are its guards. Machine transactions are atomic and asynchronous [36]—they can be carried out by their participants at any time, regardless of the states of non-participants. Participants include both active agents (whose state changes) and stationary agents (whose state is a precondition but does not change). Guarded transactions are machine transactions that can be carried-out only if their guards Q′ ⊆ Q are willing. Guarded transactions do not distinguish between agents that initiate a transaction and those willing to participate in it. When we say a transaction is “guarded by {p, q},” both must be willing; when we say it is “guarded by either p or q,” we mean there are two guarded transactions over the same machine transaction, (t, {p}) and (t, {q}), so that either person’s volition suffices. Distinct machine transactions can represent “the same action” in different configurations; we capture this with an equivalence relation on machine transactions. ▶ Definition 2.2 (Transaction Equivalence). Given a set of machine transactions R, a transaction equivalence is an equivalence relation ∼ on R such that t ∼ t′ implies t and t′ have the same participants. We write [t] for the equivalence class of t under ∼. For example, all befriend(p, q) transactions—differing only in the configurations in which they occur—form an equivalence class. Further examples for each platform appear in Section 4. Next we provide the mathematical machinery allowing people to express their volitions regarding the classes of machine transactions their machines may participate in. ▶ Definition 2.3 (Agent State and Configuration). Given agents P , states S with initial state s0 , a set of machine transactions T each over its own participants Q ⊆ P and S, and equivalence ∼ on T , an agent state is a pair (V, m) ∈ A = (2T /∼ × S) where V is its volitional state and m ∈ S its machine state. The initial agent state is (∅, s0 ). An agent configuration c over P , S, T , and ∼ is a member c ∈ AP , in which case we write cvp for the volitional state and cm p for the machine state of agent p in c. ▶ Definition 2.4 (Volitional Multiagent Atomic Transaction). Given agents P , states S, machine transactions T over P and S, and equivalence ∼ on T : 1. A change-volition transaction of agent p ∈ P is a pair c → c′ of agent configurations ′m over {p}, S, T , and ∼ such that cvp ̸= c′vp ⊆ T / ∼ and cm p =c p . 2. A volitional machine transaction induced by a guarded machine transaction (t, Q′ ), for some t = (d → d′ ) ∈ T over Q′ ⊆ Q ⊆ P , is a pair c → c′ where c ̸= c′ are agent configurations over P , S, T , and ∼ such that [t] ∈ cvq for every q ∈ Q′ ; cm p = dp and ′ m ′m ′v v c′m = d for every p ∈ Q; c = c for every p ∈ P \ Q; and c = c \ {[t]} for every p p p p p p p ∈ P. 3. A volitional multiagent atomic transaction is a change-volition transaction or a volitional machine transaction. When a volitional machine transaction induced by (t, Q′ ) is taken, the class [t] is removed from every agent’s volitional state. Volitions are thus discharged upon satisfaction—a person wills a class of transactions, and once any equivalent transaction is taken, the will is fulfilled and the class is removed. A person may independently change their volitional state via change-volition transactions, which may add or remove classes; beyond these, the framework removes a class from cvp only upon fulfilment.
Lewis-Pye and Shapiro
2.2
Examples of Grassroots Platforms Specified by Guarded Atomic Transactions
A grassroots platform is specified by a set of guarded transactions over a local-states function; the formal machinery for deriving a transition system and proving it grassroots is introduced in this section. First, we present the guarded transactions that specify several grassroots platforms, illustrating the range of guard structures that arise in practice. Child-safe social networks [26]. A child-safe social network is a grassroots social network in which a child’s partaking in online activities is subject to parental consent. Each agent a maintains a set of friends ca ⊆ P . 1. Child befriend: c′r := cr ∪ {s}, c′s := cs ∪ {r}, provided q ∈ cp and s ∈ / cr . Guarded by {r, s, p, q}. 2. Child unfriend: c′r := cr \ {s}, c′s := cs \ {r}, provided s ∈ cr . Guarded by any one of {r, s, p, q}. Here r, s are children with respective parents p, q (where r, s, p, q are four distinct agents with the stated precondition). The precondition q ∈ cp requires the parents to be friends. Child befriending requires all four—both children and both parents—to be willing; child unfriending can be initiated by any one of the four. The parent–child assignment is fixed externally and not part of the agent state; the full formalisation appears in [26]. Grassroots coins [39]. Grassroots coins are units of personal debt: each person mints their own coins, backed by the goods and services they offer, and liquidity arises from mutual credit via coin exchange among persons that know and trust each other. Each agent p maintains a multiset of coins cp ; we write ¢r for a coin minted by r (a r-coin) and ¢kr for a multiset of k such coins. We write ∪ and \ for multiset union and difference throughout. 1. Mint: c′p := cp ∪ ¢kp , k > 0. Guarded by p. 2. Voluntary swap: c′p := (cp ∪ y) \ x, c′q := (cq ∪ x) \ y, provided x ⊆ cp , y ⊆ cq . Guarded by {p, q}. 3. Pay: c′p := cp \ x, c′q := cq ∪ x, where x is a set of q-coins, x ⊆ cp . Guarded by p. 4. Redeem: c′p := (cp ∪ y) \ x, c′q := (cq ∪ x) \ y, where x = ¢kq ⊆ cp , y ⊆ cq , |y| = k. Guarded by p. Minting is a personal decision; voluntary swaps require both parties to be willing; payments and redemptions are guarded by the payer/redeemer. In redemption, the redeemer chooses any k coins held by the issuer. Grassroots bonds [41] extend grassroots coins with maturity dates, enabling interest-bearing credit and loans; they are formally specified in Section 4. Summary. The guard captures the essential distinction between voluntary and obligatory transactions. Befriending and voluntary swaps are guarded by all participants—they require mutual willingness. Unfriending, payments, and redemptions are guarded by a single party— they are obligatory once initiated. Child befriending illustrates the most complex case: a quaternary guard requiring all four persons to be willing. Unguarded transactions (guard Q′ = ∅), such as group message delivery [26], are purely mechanical and require no volitions.
2.3
Volitional Multiagent Transition Systems
The following is a simplified variation, sufficient for the purpose of this work, on the foundations introduced in [36].
5
6
Describing People and their Machines
▶ Definition 2.5 (Transition system, Computation, Run). A transition system is a tuple T S = (S, s0 , T ), where: 1. S is an arbitrary non-empty set, referred to as the set of states. 2. Some s0 ∈ S is the designated initial state. 3. T ⊂ S 2 is a set of transitions over S, where each transition t ∈ T is a pair (s, s′ ) of non-identical states s ̸= s′ ∈ S, also written as t = s → s′ . A computation of T S is a (nonempty, potentially infinite) sequence of states r = s1 , s2 , · · · such that for every two consecutive states si , si+1 ∈ r, si → si+1 ∈ T . If s1 = s0 then the computation is called a run of T S. Given a computation r = s1 , s2 , . . ., we use r ⊆ T to mean (si → si+1 ) ∈ T for every (si → si+1 ) ∈ r. ▶ Definition 2.6 (Multiagent Transition System). Given agents P ⊂ Π and an arbitrary set S of states with a designated initial state s0 ∈ S, a multiagent transition system over P and S is a transition system T S = (C, c0 , T ) with configurations C := S P , initial configuration c0 := {s0 }P , and transitions T ⊆ C 2 a set of transactions over P and S. Unary multiagent transition systems were introduced in [36] and were employed to define the notion of grassroots protocols [37] and to provide unary specifications for various grassroots platforms [38, 39, 25]. Here, we employ k-ary transition systems, for any k ≤ |P |, in which several agents can change their state simultaneously. Rather than specifying a multiagent transition system over a set of agents P directly, we specify it via machine transactions (Definition 2.1). A machine transaction over Q ⊆ P defines a set of multiagent transitions over P in which all members of P \ Q are stationary: ▶ Definition 2.7 (Transaction Closure). Let P ⊂ Π, S a set of machine states, and C := S P . For any transition or transaction t = c → c′ , we write tq := cq → c′q and say p is stationary in t if cp = c′p . For a machine transaction t = (c → c′ ) over S with participants Q, the P -closure of t, t↑P , is the set of transitions over P and S defined by: ( {t′ ∈ C 2 : ∀q ∈ Q.(tq = t′q ) ∧ ∀p ∈ P \ Q.(p is stationary in t′ )} if Q ⊆ P t↑P := ∅ otherwise If R is a set of machine transactions, each t ∈ R over some Q and S, then the P -closure of R, R↑P , is the set of transitions over P and S defined by: [ R↑P := t↑P t∈R
Namely, the closure over P ⊇ Q of a machine transaction t over Q includes all transitions t′ over P in which members of Q do the same in t and in t′ , and the rest remain in their current (arbitrary) state. ▶ Lemma 2.8 (Compositionality of Closure). For sets of machine transactions R, R′ over S and any P ⊂ Π: (R ∪ R′ )↑P = R↑P ∪ R′ ↑P , and R ⊆ R′ implies R↑P ⊆ R′ ↑P . S Proof. Both are immediate from the definition R↑P := t∈R t↑P . ◀ A transaction and a transition are structurally identical—both are pairs of configurations— but differ in their role: a transaction is specified over its participants Q, the agents whose states are preconditions for the transaction to occur, and says nothing about agents outside
Lewis-Pye and Shapiro
Q; different transactions may have different sets of participants. A transition, by contrast, is over a fixed set of agents P , as it is a building block of a transition system over P that consists of transitions over P . Given a set of transactions, each over its own set of participants, the closure operator induces from them a set of transitions over a fixed P , in which non-participants remain stationary. A set of machine transactions R over S, each with participants Q ⊆ P , defines a multiagent transition system over S and P as follows: ▶ Definition 2.9 (Transactions-Based Multiagent Transition System). Given agents P ⊂ Π, states S with initial state s0 ∈ S, and a set of transactions R, each t ∈ R over some Q ⊆ P and S, the transactions-based multiagent transition system over P , S, and R is the multiagent transition system T S = (S P , {s0 }P , R↑P ) . In other words, one can fully specify a multiagent transition system over S and P simply by providing a set of transactions over S, each with participants Q ⊆ P . Similarly, a set R of guarded machine transactions with an equivalence ∼ on their underlying machine transactions induces a volitional multiagent transition system: ▶ Definition 2.10 (Volitional Multiagent Transition System). Given agents P ⊂ Π, machine states S with initial state s0 , a set R of guarded machine transactions such that every (t, Q′ ) ∈ R has the participants of t contained in P , and an equivalence ∼ on the set TR := {t : (t, Q′ ) ∈ R for some Q′ } of underlying machine transactions, the volitional multiagent transition system induced by (S, R, ∼) over P is the multiagent transition system (AP , c0 , TV ) where: 1. A := 2TR /∼ × S is the agent state space; 2. c0 ∈ AP is the initial agent configuration, with c0 vp = ∅ and c0 m p = s0 for every p ∈ P ; 3. TV consists of all transitions e → e′ ∈ (AP )2 of one of two forms: (i) a change-volition ′m ′ of some p ∈ P —evp ̸= e′vp ⊆ TR / ∼, em p = e p , and er = er for every r ∈ P \ {p}; or (ii) a volitional machine transaction induced by some guarded machine transaction (t, Q′ ) ∈ R per Definition 2.4(2). The set R of guarded machine transactions that specifies a platform thus determines the volitional machine transitions of the induced VMTS, while change-volition transitions are freely available to every agent independent of R.
2.4
Enablement and Liveness
We now define when a guarded transaction is enabled, combining the machine precondition with the volitions of the guards. ▶ Definition 2.11 (Enabled). Given a set of guarded machine transactions, each (t, Q′ ) with t = d → d′ a machine transaction over some Q′ ⊆ Q ⊆ P and S, and an equivalence ∼ on machine transactions: the guarded transaction (t, Q′ ) is enabled in agent configuration c v ′ over P if cm p = dp for every p ∈ Q, and [t] ∈ cq for every q ∈ Q . An equivalence class [t] is ′ ′ ′ enabled in c if some guarded (t , Q ) with t ∈ [t] is enabled in c. Note that the machine precondition depends on the machine states of all participants, while the volitional condition depends only on the guards. A guarded transaction with an empty guard (Q′ = ∅) requires no volitions and is enabled whenever the machine precondition is met. We can now define liveness. In the original framework [36], liveness required a designated set λ of “live” transitions. With volitional transactions, λ is no longer needed: volitions determine which transactions become enabled, and liveness requires machines to
7
8
Describing People and their Machines
execute what is enabled. Personal volitional transactions—free choices of people—carry no liveness obligation. ▶ Definition 2.12 (Correct Run). Given a set R of guarded machine transactions with equivalence ∼ on the underlying machine transactions TR = {t : (t, Q′ ) ∈ R for some Q′ }, a run r is correct if no class [t] ∈ TR /∼ is enabled in some suffix of r with no member of the class taken in the suffix.
3
Grassroots Protocols
Here we define what is a protocol; define when a protocol is grassroots, using the notion of interleaving of correct runs; show how to define a protocol via a set of transactions; prove that any transactions-based protocol is oblivious under a natural condition; and conclude that if it is also interactive, it is grassroots.
3.1
Protocols and Grassroots Protocols
A protocol is a family of multiagent transition systems, one for each set of agents P ⊂ Π, which share an underlying set of local machine states S with a designated initial state s0 . A local-states function maps every set of agents P ⊂ Π to an arbitrary set of local machine states S(P ) ⊂ S that includes s0 and satisfies P ⊂ P ′ ⊂ Π =⇒ S(P ) ⊂ S(P ′ ). ▶ Definition 3.1 (Protocol). A protocol F over a local-states function S is a family of multiagent transition systems that has exactly one transition system F(P ) = (C(P ), c0 (P ), T (P )) for every P ⊂ Π, with configurations C(P ) and initial configuration c0 (P ) ∈ C(P ) determined by the protocol, such that P ⊆ P ′ ⊂ Π implies C(P ) ⊆ C(P ′ ) and c0 (P )p = c0 (P ′ )p for every p ∈ P. Informally, in a grassroots protocol two disjoint groups of agents can each operate independently—their interleaved correct runs are correct runs of the combined system—yet the combined system offers genuinely new behaviours that neither group could produce on its own. To capture this notion formally, we first define the interleaving of runs of two disjoint groups. ▶ Definition 3.2 (Interleaving). Let P, P ′ ⊂ Π be disjoint nonempty sets of agents, r = c0 , c1 , . . . a run of F(P ), and r′ = d0 , d1 , . . . a run of F(P ′ ). An interleaving of r and r′ is a sequence e0 , e1 , . . . of configurations in C(P ∪ P ′ ) for which there exist non-decreasing sequences of indices (ik )k≥0 and (jk )k≥0 with i0 = j0 = 0 such that for every k ≥ 0: 1. (ek )p = (cik )p for every p ∈ P , 2. (ek )q = (djk )q for every q ∈ P ′ , 3. if ek+1 exists, then exactly one of: (i) ik+1 = ik + 1 and jk+1 = jk (a P -step), or (ii) ik+1 = ik and jk+1 = jk + 1 (a P ′ -step). Note that an interleaving is well-defined: by Definition 3.1, C(P ) ⊆ C(P ∪ P ′ ) and C(P ′ ) ⊆ C(P ∪ P ′ ), so each ek is a valid configuration in C(P ∪ P ′ ). Also, e0 = c0 (P ∪ P ′ ), since (e0 )p = (c0 )p = c0 (P ∪ P ′ )p for p ∈ P and (e0 )q = (d0 )q = c0 (P ∪ P ′ )q for q ∈ P ′ , by the agreement of initial configurations across F(P ), F(P ′ ), and F(P ∪ P ′ ). We can now define the key notion of this paper, a grassroots protocol. The following definition improves upon the original definition [37], which was formulated in terms of a subset relation (P ⊂ P ′ ) and conditions on the availability of transitions, and upon the definition of [42], which did not incorporate liveness. The new definition captures the informal
Lewis-Pye and Shapiro
notion of grassroots directly, using disjoint groups and the interleaving of their correct runs; the differences are discussed below. ▶ Definition 3.3 (Oblivious, Interactive, Grassroots). A protocol F is: 1. oblivious if for every disjoint nonempty P, P ′ ⊂ Π, every interleaving of a correct run of F(P ) and a correct run of F (P ′ ) is a correct run of F (P ∪ P ′ ). 2. interactive if for every disjoint nonempty P, P ′ ⊂ Π, there exists a correct run r̂ of F(P ∪ P ′ ) such that for every correct run r of F(P ), every correct run r′ of F(P ′ ), and every interleaving e of r and r′ , r̂ ̸= e. 3. grassroots if it is oblivious and interactive. Oblivious. Being oblivious means that two disjoint groups of agents, each running the protocol independently and correctly, do not interfere with each other: any interleaving of their independent correct runs is a correct run of the combined system. Each group can operate as if the other does not exist. Interactive. Being interactive means that two disjoint groups, when brought together, can do something genuinely new: there exists a correct run of the combined system that could not arise from the two groups operating independently. In an interleaving, each step changes the local states of agents in only one group; therefore, any transaction whose active participants span both groups yields a step that cannot occur in any interleaving. The substance of interactivity for a given protocol is thus the content of its cross-group transactions, which the platforms in Section 4 illustrate. Federated systems such as BitTorrent [47] and Mastodon [34] are oblivious, as servers in one group can ignore servers in the other, but are not interactive: a group of clients P without a server cannot do more when joined by another group of clients P ′ , also without a server. Any protocol that employs a shared global data structure—whether replicated (Blockchain [33]) or distributed (DHT [35], IPFS [6])—is not oblivious, and hence not grassroots. In Appendix A we prove that Bitcoin is not grassroots and show that the same argument applies to distributed hash tables and IPFS.
3.2
Transactions-Based Grassroots Protocols
We now show that any transactions-based protocol whose cross-group transactions are guarded is automatically oblivious, and hence grassroots provided it is also interactive. The argument proceeds in three steps. First, the Volitional Containment Lemma (Lemma 3.6) establishes that an agent’s volitional state, in any configuration of F(P ), never contains classes of transactions outside R(P ) (as defined below). Second, Proposition 3.7 uses this invariant to reduce obliviousness of a transactions-based protocol to a condition on equivalence classes in the interleaving. Third, Corollary 3.8 combines the two: when every cross-group transaction is guarded, the volitional condition fails at every guard, so the class is never enabled and obliviousness follows. This is the main technical result of the paper; Theorem 3.9 then names the consequence for grassroots. ▶ Definition 3.4 (Transactions Over a Local-State Function). Let S be a local-states function. A set of transactions R is over S if every transaction t ∈ R is a multiagent transition over Q and S(P ′ ) for some Q ⊆ P ′ ⊂ Π. Given such a set R and P ⊂ Π, R(P ) := {t ∈ R : t is over Q and S(P ′ ), Q ⊆ P ′ ⊆ P }. ▶ Definition 3.5 (Transactions-Based Protocol). Let S be a local-states function and R a set of guarded transactions over S with equivalence ∼. The protocol F over R, S, and ∼
9
10
Describing People and their Machines
assigns to each set of agents P ⊂ Π the volitional multiagent transition system F(P ) induced by (S(P ), R(P ), ∼) over P (Definition 2.10). In particular, C(P ) = A(P )P with agent state space A(P ) := 2TR(P ) /∼ × S(P ), and c0 (P ) has p-component (∅, s0 ) for every p ∈ P . By Definition 2.10, the transitions of F(P ∪ P ′ ) comprise change-volition transitions of the agents in P ∪ P ′ , together with volitional machine transactions induced by the guarded transactions in R(P ∪ P ′ ). The latter split as R(P ∪ P ′ ) = R(P ) ∪ R(P ′ ) ∪ Rcross (P, P ′ ), where Rcross (P, P ′ ) := R(P ∪ P ′ ) \ (R(P ) ∪ R(P ′ )) collects the guarded transactions whose participants span both P and P ′ . Interleavings of P -runs and P ′ -runs produce only changevolitions and volitional machine transactions induced by R(P ) ∪ R(P ′ ); those induced by Rcross (P, P ′ ) require both groups to act in a single step and cannot appear in an interleaving. Obliviousness is the requirement that, on any interleaving of correct runs, no class drawn from Rcross (P, P ′ )/ ∼ is enabled, while interactivity is the requirement that some correct run of the combined system uses a class from Rcross (P, P ′ )/ ∼. We first record the basic containment property of volitional state under the VMTS construction. ▶ Lemma 3.6 (Volitional Containment). Let F be a transactions-based protocol over a set of guarded transactions R with equivalence ∼. For every P ⊂ Π, every configuration c of F(P ), and every p ∈ P : cvp ⊆ TR(P ) / ∼, where TR(P ) := {t : (t, Q′ ) ∈ R(P ) for some Q′ }. Proof. By Definition 2.10, every configuration of F(P ) is in A(P )P with A(P ) = 2TR(P ) /∼ × S(P ), so cvp ⊆ TR(P ) / ∼ for every p ∈ P . ◀ Since liveness applies to all equivalence classes (Definition 2.12), any class [t] in R(P ∪ P )/ ∼ whose transactions have participants spanning both P and P ′ could obstruct obliviousness if enabled in an interleaving. The following proposition identifies the condition under which this does not occur. ′
▶ Proposition 3.7. A transactions-based protocol is oblivious provided that for every disjoint nonempty P, P ′ ⊂ Π, no equivalence class whose transactions have participants spanning both P and P ′ is ever enabled in any interleaving of correct runs of F(P ) and F(P ′ ). Proof. Let F be a transactions-based protocol over a set of guarded transactions R, localstates function S, and equivalence ∼. Let P, P ′ ⊂ Π be disjoint and nonempty, r = c0 , c1 , . . . a correct run of F(P ), r′ = d0 , d1 , . . . a correct run of F(P ′ ), and e = e0 , e1 , . . . an interleaving of r and r′ . Safety. We show that e is a run of F(P ∪ P ′ ). e0 = c0 (P ∪ P ′ ) as noted above. Consider a P -step ek → ek+1 ; the transition cik → cik+1 of F(P ) it lifts is, by Definition 2.10, either a change-volition of some p ∈ P or a volitional machine transaction induced by some (t, Q′ ) ∈ R(P ). Since R(P ) ⊆ R(P ∪ P ′ ), a change-volition of p ∈ P in F(P ) is also a change-volition of p ∈ P ∪ P ′ in F(P ∪ P ′ ), and ek → ek+1 lifts it trivially: no non-p agent changes, with P ′ -agents unchanged because it is a P -step. A volitional machine transaction induced by (t, Q′ ) ∈ R(P ), with t = d → d′ over Q ⊆ P , is likewise induced by (t, Q′ ) ∈ R(P ∪P ′ ) over P ∪P ′ : the machine and volitional preconditions of Definition 2.4(2) hold at ek because they hold at cik , and P ′ -agents are machine-stationary at ek → ek+1 (it is a P -step). The volitional postcondition ek+1 vp = ek vp \ {[t]} for every
Lewis-Pye and Shapiro
p ∈ P ∪ P ′ holds on P -agents by the F(P )-step; on P ′ -agents it holds vacuously, since by Lemma 3.6 applied to r′ , ek vp′ = (djk )vp′ ⊆ TR(P ′ ) / ∼, and t ∈ / R(P ′ ) (because Q ⊆ P ′ and Q ∩ P = ∅), so [t] ∈ / TR(P ′ ) / ∼ by well-formedness of ∼, hence [t] ∈ / ek vp′ . Therefore ′ ek → ek+1 is a transition of F(P ∪ P ). The case of a P ′ -step is symmetric. Liveness. We show that e is correct. Suppose for contradiction that some class [t] ∈ R(P ∪ P ′ )/ ∼ is enabled in some suffix of e with no member of [t] taken in the suffix. By the hypothesis of the Proposition, every representative of [t] enabled at any ek has participants contained in P or contained in P ′ . Consider a representative (t′ , Q′ ) enabled at some ek in the suffix; without loss of generality Q ⊆ P . Enablement at ek depends only on the states of agents in P , which in the interleaving match those of r at index ik . Since [t] is enabled throughout the suffix of e, the tail of r from ik onward has [t] enabled throughout; and since no member of [t] is taken in the e-suffix, no P -step in that suffix fires a member of [t], hence no member is taken in the r-tail either. This contradicts correctness of r. The P ′ case is symmetric. ◀ For transactions-based protocols whose cross-group transactions are guarded, the hypothesis of Proposition 3.7 can be discharged by a uniform argument about volitions, without invoking platform-specific machine preconditions. ▶ Corollary 3.8 (Guarded Obliviousness). A transactions-based protocol over a set of guarded transactions R is oblivious if, for every disjoint nonempty P, P ′ ⊂ Π, every machine transaction in R(P ∪ P ′ ) with participants spanning both P and P ′ has a nonempty guard in R(P ∪ P ′ ). Proof. We verify the hypothesis of Proposition 3.7. Let [t] be an equivalence class of R(P ∪ P ′ )/∼ and (t, Q′ ) a representative whose participants Q span both P and P ′ . By hypothesis Q′ ̸= ∅; pick q ∈ Q′ and, without loss of generality, q ∈ P . Since Q has a participant in P ′ , t ∈ / R(P ) by Definition 3.4; and by well-formedness of ∼ (Definition 2.2), every t′ ∼ t has the same participants as t, so no t′ ∼ t lies in R(P ) and [t] ∈ / TR(P ) / ∼. By Lemma 3.6 applied to the P -run, ek vq ⊆ TR(P ) / ∼ at every ek , so [t] ∈ / ek vq and the guard on q fails. Hence (t, Q′ ) is not enabled at any ek . ◀ Corollary 3.8 reduces obliviousness—for transactions-based protocols—to a syntactic check on guards. The two platforms of Section 4 apply it uniformly. Combining it with interactivity yields the grassroots property: ▶ Theorem 3.9. A transactions-based protocol that satisfies the condition of Proposition 3.7 and is interactive is grassroots. Proof. By Proposition 3.7, the protocol is oblivious. If it is also interactive, it is grassroots by Definition 3.3. ◀ Relation to the original grassroots definition. The original definition of grassroots protocols [37, 42] used a subset relation (P ⊂ P ′ ) and conditions on transition availability, without incorporating liveness. The new definition uses disjoint groups and interleavings of correct runs. The two definitions are not comparable in general—neither implies the other—but for the platforms considered here, both definitions agree.
11
12
Describing People and their Machines
4
Grassroots Platforms via Guarded Atomic Transactions
We now present two grassroots platforms: grassroots social networks and grassroots coins and bonds. For each platform, we specify its guarded transactions, define the induced volitional multiagent transition system, prove platform-specific invariants, and prove the platform is grassroots via Theorem 3.9. By invariants we mean properties preserved across all runs of the induced multiagent transition system; these are the platform-specific analogue of safety in the classical sense.
4.1
Grassroots Social Networks via Befriending and Unfriending
In a grassroots social network [38], the social graph is stored distributively under the control of the people themselves, with each person storing the local neighbourhood pertaining to them, and no third-party having access unless explicitly granted. The original definition [38] was via a unary multiagent transition system; here both actions are specified as binary transactions. Each agent p maintains, as its local state, a finite set cp ⊆ P recording the friends of p; initially cp = ∅. Befriending adds q to cp and p to cq ; unfriending removes them. Communication functions of a social network can be added, under the restriction that communication occurs only among friends [38]. A liveness theorem can be proven for this design [38], stating that if a person p that follows a person q is connected to q via a chain of mutual friends, each of them correct and follows q, then p will eventually receive every item on q’s feed. The specification of the grassroots social graph is the foundation for grassroots social networks with feeds, groups, messaging, explored elsewhere [38, 40, 26]. ▶ Definition 4.1 (Grassroots Social Graph). The grassroots social graph SG is the protocol over the befriend and unfriend guarded transactions of the Introduction, with local-states function S(P ) := 2P and equivalence ∼ that identifies all befriend(p, q) transactions with each other and all unfriend(p, q) transactions with each other, per Definition 3.5. Invariants. ▶ Lemma 4.2 (Mutuality). Given a run r of SG, a configuration c ∈ r, and agents p, q ∈ P , q ∈ cp ⇐⇒ p ∈ cq . Proof. By induction on the length of the run r = c0 , c1 , . . . , cn . In the initial configuration c0 = ∅P the biconditional holds vacuously. Assume the lemma holds for cn , and consider the transition cn → cn+1 . It can be either Befriend or Unfriend for some pair {p, q}; both modify cp and cq symmetrically—Befriend adds q to cp and p to cq , Unfriend removes them— preserving the biconditional. For all other pairs {r, s}, the local states are unchanged. ◀ We note that each configuration c in a run r of SG induces a graph with agents as vertices and an edge p ↔ q when q ∈ cp (equivalently, by Lemma 4.2, when p ∈ cq ), and that the graphs induced by two consecutive configurations in r differ by exactly one added or removed edge. Transaction equivalence. All befriend(p, q) transactions—differing in the configurations in which they occur—form an equivalence class. Similarly for unfriend(p, q). Liveness. Liveness applies to all equivalence classes (Definition 2.12). Unfriending is guarded by either p or q: once either person wills the class, the transaction becomes enabled and must eventually be taken. Befriending is guarded by both p and q: it becomes enabled only when both persons will the class, and must then eventually be taken.
Lewis-Pye and Shapiro
Grassroots. ▶ Corollary 4.3. The grassroots social graph SG is grassroots. Proof. Obliviousness: Both befriend and unfriend are guarded (by {p, q} and by p or q, respectively); in particular, every cross-group transaction has a nonempty guard. By Corollary 3.8, SG is oblivious. Interactivity: Let P, P ′ ⊂ Π be disjoint and nonempty. Let r̂ be a run of SG(P ∪ P ′ ) starting from c0 (P ∪ P ′ ) in which p ∈ P and q ∈ P ′ each will befriend and the befriend is then taken. The befriend step changes the local states of both p and q, and hence is neither a P -step nor a P ′ -step. The run r̂ is correct: the befriend fulfils [befriend(p, q)] in both volitions, and no class is enabled at the end of the run. Therefore SG is interactive, and by Theorem 3.9, grassroots. ◀
4.2
Grassroots Coins and Bonds
Grassroots coins [39, 25] are units of debt that can be issued and traded digitally by any person. Each person’s coins are backed by the goods and services they offer, priced in their own currency, with liquidity arising from mutual credit via coin exchange among persons that know and trust each other. Grassroots bonds [41] extend grassroots coins with a maturity date, reframing grassroots coins—cash—as mature grassroots bonds. Coin-for-bond redemption generalises coin-for-coin redemption, allowing the lending of liquid coins in exchange for interest-bearing future-maturity bonds. Digital social contracts—voluntary agreements among persons, specified, fulfilled, and enforced digitally—can express the full gamut of financial instruments as the voluntary swap of grassroots bonds, including credit lines, loans, sale of debt, forward contracts, options, and escrow-based instruments [41]. ▶ Definition 4.4 (Grassroots Bonds). A p-bond with maturity date d, denoted ¢p,d , is a unit of debt issued by p ∈ Π maturing at date d ∈ N. We let B(P ) = {¢p,d : p ∈ P, d ∈ N} denote the set of all grassroots bonds by agents P ⊂ Π. Each agent p maintains as its local state a pair (cp , d∗p ) where cp is a multiset of members of B(P ) (initially ∅) and d∗p ∈ N is the local current date (initially 0); p considers a bond ¢q,d to be mature, and refers to it as a q-coin (denoted ¢q ), iff d ≤ d∗p . There is no global date; agents may disagree on which bonds are mature. The grassroots bonds guarded atomic transactions are: 1. Mint: c′p := cp ∪ ¢kp,d , k > 0, d ∈ N; d∗p unchanged. Guarded by p. 2. Advance-date: d∗p ′ > d∗p ; cp unchanged. Unguarded. 3. Voluntary swap: c′p := (cp ∪ y) \ x, c′q := (cq ∪ x) \ y, provided x ⊆ cp , y ⊆ cq ; d∗p and d∗q unchanged. Guarded by {p, q}. 4. Pay: c′p := cp \ x, c′q := cq ∪ x, where x ⊆ cp is a set of q-coins (that is, bonds ¢q,d with d ≤ d∗p ); d∗p and d∗q unchanged. Guarded by p. 5. Redeem: c′p := (cp ∪ y) \ x, c′q := (cq ∪ x) \ y, where x = {¢q,d′ } ⊆ cp with d′ ≤ d∗p , y = {¢r,d } ⊆ cq , r ∈ P , d ∈ N; d∗p and d∗q unchanged. Guarded by p. Minting, paying, and redeeming are guarded by the initiator; voluntary swap requires both parties to be willing; Advance-date is unguarded, since local time advances mechanically. In redemption, the redeemer chooses any bond held by the coin’s issuer—regardless of who issued the bond—generalising coin-for-coin redemption [39] to coin-for-bond redemption [41].
13
14
Describing People and their Machines
▶ Definition 4.5 (Grassroots Coins and Bonds). The grassroots coins and bonds GCB is the protocol over the guarded transactions above with local-states function mapping each P ⊂ Π to the set of pairs (c, d) where c is a multiset of members of B(P ) and d ∈ N, and equivalence ∼ identifying Mint transactions at the same agent with the same k and d, Advance-date transactions at the same agent, and Swap transactions between the same pair exchanging the same multisets, per Definition 3.5. Invariants. ▶ Lemma 4.6 (Conservation of Money). In any run r of GCB, the p-bonds in any configuration c ∈ r are exactly the p-bonds minted by p in the prefix of the run ending in c. Proof. Mint adds new p-bonds to p’s holdings. Voluntary swap, Pay, and Redeem transfer bonds between two agents without creating or destroying them: x moves from p to q and y from q to p, preserving the total multiset of bonds. Advance-date changes only d∗p and leaves bonds unchanged. Hence the multiset of p-bonds across all agents equals the multiset minted by p. ◀ Transaction equivalence. All Mint transactions at the same agent with the same k and d (differing only in the configurations in which they occur) form an equivalence class. All Advance-date transactions at the same agent form an equivalence class. All Swap transactions between the same pair {p, q} exchanging the same multisets x and y form an equivalence class. Liveness. Mint is guarded by the minting agent; it becomes enabled when the agent wills the class, and must then eventually be taken. Pay and Redeem are guarded by the initiator; once enabled, they must eventually be taken. Voluntary swap is guarded by both participants; it becomes enabled only when both persons will the class, and must then eventually be taken. Advance-date is unguarded and always enabled (since d∗p can always grow); hence in every correct run it is taken infinitely often for every agent, and d∗p grows without bound. Grassroots. ▶ Corollary 4.7. Grassroots Coins and Bonds are grassroots. Proof. Obliviousness: Mint, Voluntary swap, Pay, and Redeem are all guarded (by p; by {p, q}; by p; and by p, respectively); Advance-date is unary at a single agent, so its participants lie in either P or P ′ but never span both. In particular, every cross-group transaction has a nonempty guard. By Corollary 3.8, GCB is oblivious. Interactivity: Let P, P ′ ⊂ Π be disjoint and nonempty. Construct an infinite run r̂ of GCB(P ∪ P ′ ) whose prefix has some p ∈ P will Mint and mint p-coins, some q ∈ P ′ will Mint and mint q-coins, p and q both will Voluntary swap and execute it (exchanging p-coins for q-coins), and whose tail interleaves Advance-date transactions of every agent in P ∪ P ′ so that each is taken infinitely often. The swap step changes the local states of both p and q, and hence is neither a P -step nor a P ′ -step. The run r̂ is correct: the Mint and Voluntary swap classes are fulfilled upon execution and never re-willed thereafter, so they are not enabled in the tail; Advance-date is always enabled but taken infinitely often for every agent, satisfying liveness. Therefore GCB is interactive, and by Theorem 3.9, grassroots. ◀
5
Related Work
Atomic transactions. This work extends the notion of multiagent atomic transactions of [42] with volitions. Atomic transactions have been investigated early in distributed
Lewis-Pye and Shapiro
computing, mostly in the context of database systems [24, 29, 27]. Most research since and until today focuses on their efficient and robust implementation [9, 11]. The integration of atomic transactions in programming languages has also been explored [8]. In terms of formal models of concurrency, the extension of CCS with atomic transactions has been investigated in the past [2, 14, 15], but without follow-on research, so it seems. While transition systems have been the bedrock of abstract models of computation since the Turing machine, we are not aware of previous attempts to explore atomic transactions within their context. Formal models of persons in concurrent systems. The formal methods tradition has a long lineage of modeling human agents as sources of nondeterminism alongside deterministic machines, but—to the best of our knowledge—without decomposing an agent into person and machine as components of its state. A detailed survey appears in Appendix C; we summarise the key points here. Turing’s choice machines [48] introduced the person as an external operator making free choices at designated states. Hoare’s CSP [20] provides process-algebraic encoding via external choice (□), but models what the person does, not what the person is willing to do. Lynch and Tuttle’s I/O automata [30] model the environment (potentially human) via input-enabling. Back and von Wright’s angelic/demonic nondeterminism [5] is the closest precursor to the volition/obligation distinction: angelic choices model cooperative behaviour, demonic choices model adversarial behaviour. The distinction from the present work is that angelic nondeterminism is a point-of-choice semantics—a choice is resolved locally at each transition—whereas volitions are persistent, inspectable state, so a guard condition reads the agent’s current willing, not a single local resolution. Game structures [3, 23, 1], ceremony analysis [16], and electronic institutions [17, 4] treat agents as symmetric players or norm-governed entities, but none decompose an agent into person and machine components. Across all traditions, the person is modeled as environment, opponent, error source, or unconstrained nondeterministic process—but always as an entity external to the agent, never as a formal component of the agent’s state. The present work, to the best of our knowledge, is the first to decompose each agent’s state into a machine state and a volitional state within a multiagent transition system, with machine transactions conditioned on the volitions of the agents’ persons, and with liveness arising from the interplay of personal volitions and machine obligations rather than from a designated set of live transitions.
6
Conclusion and Future Work
We have presented volitional multiagent atomic transactions—a formal foundation for describing systems consisting of people operating machines—in which each agent’s state decomposes into a machine state and a volitional state, and machine transactions are guarded by their people’s volitions. We have developed the mathematical machinery needed to express the safety and liveness of grassroots platforms thus specified, and demonstrated the framework on two grassroots platforms: social networks and coins and bonds. We have provided a simpler definition of grassroots that better captures the informal notion and excludes systems based on shared global data structures. The framework extends naturally to platforms with richer guard structures—such as grassroots federations, in which transactions are guarded by supermajorities or assemblies of community members rather than by all participants—deferred to future work. The original framework [36] also considered faulty computations and fault-tolerant implementations. These could be re-introduced in follow-on work that considers fault-tolerant implementations of the specifications presented here.
15
16
Describing People and their Machines
References 1 2 3 4 5 6 7
8
9 10
11 12
13
14 15
16 17
18 19 20 21 22
Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409–470, 2000. Lucia Acciai, Michele Boreale, and Silvano Dal Zilio. A concurrent calculus with atomic transactions. In European Symposium on Programming, pages 48–63. Springer, 2007. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672–713, 2002. Alexander Artikis, Marek Sergot, and Jeremy Pitt. Specifying norm-governed computational societies. ACM Transactions on Computational Logic, 10(1):1–42, 2009. Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998. Juan Benet. Ipfs-content addressed, versioned, p2p file system. arXiv preprint arXiv:1407.3561, 2014. Matthew L. Bolton, Ellen J. Bass, and Radu I. Siminiceanu. Using formal verification to evaluate human-automation interaction: A review. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 43(3):488–503, 2013. Johannes Borgström, Karthikeyan Bhargavan, and Andrew D Gordon. A compositional theory for stm haskell. In Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, pages 69–80, 2009. Manuel Bravo and Alexey Gotsman. Reconfigurable atomic transaction commit. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, pages 399–408, 2019. Sonja Buchegger, Doris Schiöberg, Le-Hung Vu, and Anwitaman Datta. Peerson: P2p social networking: early experiences and insights. In Proceedings of the Second ACM EuroSys Workshop on Social Network Systems, pages 46–52, 2009. Gregory Chockler and Alexey Gotsman. Multi-shot distributed transaction commit. Distributed Computing, 34:301–318, 2021. Gregory Chockler, Roie Melamed, Yoav Tock, and Roman Vitenberg. Constructing scalable overlays for pub-sub with many topics. In Proceedings of the twenty-sixth annual ACM symposium on Principles of distributed computing, pages 109–118, 2007. Gregory Chockler, Roie Melamed, Yoav Tock, and Roman Vitenberg. Spidercast: a scalable interest-aware overlay for topic-based pub/sub communication. In Proceedings of the 2007 inaugural international conference on Distributed event-based systems, pages 14–25, 2007. Edsko de Vries, Vasileios Koutavas, and Matthew Hennessy. Communicating transactions. In International Conference on Concurrency Theory, pages 569–583. Springer, 2010. Edsko De Vries, Vasileios Koutavas, and Matthew Hennessy. Liveness of communicating transactions. In Asian Symposium on Programming Languages and Systems, pages 392–407. Springer, 2010. Carl Ellison. Ceremony design and analysis. Technical Report 2007/399, IACR, 2007. Marc Esteva, Juan A. Rodríguez-Aguilar, Carles Sierra, Pere Garcia, and Josep Lluís Arcos. On the formal specification of electronic institutions. In Agent-Mediated Electronic Commerce (AMEC), volume 1991 of LNCS, pages 126–147. Springer, 2001. Daniel Halpern, Ariel D Procaccia, Ehud Shapiro, and Nimrod Talmon. Federated assemblies. Proc AAAI 2025; arXiv preprint arXiv:2405.19129, 2024. David Harel and Amir Pnueli. On the development of reactive systems. In Logics and Models of Concurrent Systems, volume 13 of NATO ASI Series, pages 477–498. Springer, 1985. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Idit Keidar, Andrew Lewis-Pye, and Ehud Shapiro. Constitutional consensus. arXiv preprint arXiv:2505.19216, 2025. Anne-Marie Kermarrec, Erick Lavoie, and Christian Tschudin. Gossiping with append-only logs in secure-scuttlebutt. In Proceedings of the 1st international workshop on distributed infrastructure for common good, pages 19–24, 2020.
Lewis-Pye and Shapiro
23 24 25 26 27
28 29 30 31 32 33 34
35
36 37
38
39 40 41 42
43 44 45
Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module checking. Information and Computation, 164(2):322–344, 2001. Butler W Lampson. Chapter 11. atomic transactions. In Distributed Systems—Architecture and Implementation: an Advanced Course, pages 246–265. Springer, 1981. Andrew Lewis-Pye, Oded Naor, and Ehud Shapiro. Grassroots flash: A payment system for grassroots cryptocurrencies. arXiv preprint arXiv:2309.13191, 2023. Andy Lewis-Pye and Ehud Shapiro. Volitional multiagent atomic transactions: Describing people and their machines. 2026. Submitted, arXiv XXXX.XXXXX. Nancy Lynch, Michael Merritt, William Weihl, and Alan Fekete. A theory of atomic transactions. In ICDT’88: 2nd International Conference on Database Theory Bruges, Belgium, August 31–September 2, 1988 Proceedings 2, pages 41–71. Springer, 1988. Nancy Lynch, Roberto Segala, and Frits Vaandrager. Hybrid I/O automata. Information and Computation, 185(1):105–157, 2003. Nancy A Lynch and Michael Merritt. Atomic transactions: in concurrent and distributed systems. Morgan Kaufmann Publishers Inc., 1993. Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. Technical Report MIT/LCS/TM-373, MIT Laboratory for Computer Science, 1989. Robin Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980. Robin Milner. The Space and Motion of Communicating Agents. Cambridge University Press, 2009. Satoshi Nakamoto and A Bitcoin. A peer-to-peer electronic cash system, 2008. Aravindh Raman, Sagar Joglekar, Emiliano De Cristofaro, Nishanth Sastry, and Gareth Tyson. Challenges in the decentralised web: The mastodon case. In Proceedings of the internet measurement conference, pages 217–229, 2019. Sean Rhea, Brighten Godfrey, Brad Karp, John Kubiatowicz, Sylvia Ratnasamy, Scott Shenker, Ion Stoica, and Harlan Yu. Opendht: a public dht service and its uses. In Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications, pages 73–84, 2005. Ehud Shapiro. Multiagent transition systems: Protocol-stack mathematics for distributed computing. arXiv preprint arXiv:2112.13650, 2021. Ehud Shapiro. Grassroots distributed systems: Concept, examples, implementation and applications (brief announcement). In 37th International Symposium on Distributed Computing (DISC 2023). (Extended version: arXiv:2301.04391), pages 47:1, 47:7, Italy, 2023. LIPICS. Ehud Shapiro. Grassroots social networking: Serverless, permissionless protocols for twitter/linkedin/whatsapp. In OASIS ’23. Association for Computing Machinery, 2023. doi:10.1145/3599696.3612898. Ehud Shapiro. Grassroots currencies: Foundations for grassroots digital economies. arXiv preprint arXiv:2202.05619, 2024. Ehud Shapiro. Glp: A grassroots, multiagent, concurrent, logic programming language. arXiv preprint arXiv:2510.15747, 2025. Ehud Shapiro. Grassroots bonds: A grassroots foundation for market liquidity. arXiv preprint arXiv:2603.13671, 2026. Ehud Shapiro. Grassroots platforms with atomic transactions: Social graphs, cryptocurrencies, and democratic federations. In Proceedings of the 27th International Conference on Distributed Computing and Networking, pages 71–81, 2026. arXiv preprint arXiv:2502.11299. doi: 10.1145/3772290.3772309. Ehud Shapiro. Implementing grassroots logic programs with multiagent transition systems and ai. arXiv preprint arXiv:2602.06934, 2026. Ehud Shapiro. Types for grassroots logic programs. arXiv preprint arXiv:2601.17957, 2026. Ehud Shapiro and Nimrod Talmon. Grassroots federation: Fair governance of largescale, decentralized, sovereign digital communities. Proc. of AAMAS’26; arXiv preprint arXiv:2505.02208, 2025.
17
18
Describing People and their Machines
46
47
48 49
Dominic Tarr, Erick Lavoie, Aljoscha Meyer, and Christian Tschudin. Secure scuttlebutt: An identity-centric protocol for subjective and decentralized applications. In Proceedings of the 6th ACM conference on information-centric networking, pages 1–11, 2019. TorrentFreak. BitTorrent Turns 20: The File-Sharing Revolution Revisited, 7 2021. Contains Bram Cohen’s original statement: "BitTorrent’s customer is etree. Etree is a loose-knit community of people who distribute live concert recordings online". URL: https://torrentfreak. com/bittorrent-turns-20-the-file-sharing-revolution-revisited-210702/. Alan M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1):230–265, 1936. Alan M. Turing. Systems of logic based on ordinals. Proceedings of the London Mathematical Society, s2-45(1):161–228, 1939.
Acknowledgements. We thank Idit Keidar and Nimrod Talmon for our discussions and their feedback on this and related topics.
A
Systems Based on Shared Global Data Structures Are Not Grassroots
▶ Proposition A.1. Bitcoin is not grassroots. Proof. We argue that Bitcoin is not oblivious. The Bitcoin protocol specifies a set of bootnodes B, which know of and communicate with each other, each holding an initial chain consisting of the genesis block, and its liveness condition requires that blocks mined by correct agents are eventually propagated to all correct agents. Consider disjoint P, P ′ ⊂ Π such that P and P ′ have disjoint members of B, say q ∈ P and q ′ ∈ P ′ . In an interleaving of a correct run of P and a correct run of P ′ , each step is either a P -step or a P ′ -step, so q and q ′ develop independent chains and no block propagation between them ever occurs. Once q mines a block, the propagation-to-q ′ class becomes enabled and remains so indefinitely, violating the liveness condition of the combined system P ∪ P ′ . Hence the interleaving is not a correct run of P ∪ P ′ , and Bitcoin is not oblivious. ◀ Distributed Hash Tables and IPFS. The same argument applies to systems based on distributed hash tables [35] and distributed file systems such as IPFS [6]. In a DHT, a lookup by a member of P may require routing through a member of P ′ , so that a lookup transition that succeeds when P runs alone does not correspond to a valid transition in the combined system where routing tables reflect both groups. More precisely: in an interleaving of correct runs of P and P ′ , each group builds its own routing table over its own members. A lookup in the combined system P ∪ P ′ must route through the combined table, but in the interleaving no routing entry connecting the two groups is ever established, so lookups that should succeed in P ∪ P ′ (by routing through P ′ ) instead fail or route incorrectly. The liveness condition requiring that lookups for keys stored by correct agents eventually succeed is thus violated. The argument for IPFS is analogous, as it relies on a DHT (specifically, a Kademlia-based DHT) for content discovery.
B
Implementation
The specifications presented here provide the formal foundation for grassroots platforms. Here, we discuss how these platforms can be implemented, focusing on the role of GLP as the implementation language.
Lewis-Pye and Shapiro
GLP as implementation language. Grassroots Logic Programs (GLP) [40] is designed for implementing grassroots platforms on networked smartphones. A correct multiagent implementation of GLP (madGLP) [43] has been developed and proven to correctly implement maGLP, with the additional result that correct and complete implementations preserve the grassroots property. Thus, any grassroots platform that can be specified and proven grassroots at the transaction level, and correctly implemented in GLP, is guaranteed to remain grassroots at the implementation level. AI-derived implementations. The mathematical foundations presented here and in companion papers have been used by AI to derive working implementations: (i) a workstationbased implementation of concurrent GLP and a smartphone-based multiagent implementation of GLP, both in Dart, derived from the formal operational semantics [43]; (ii) a GLP implementation of the grassroots social graph, child-safe social networking with parentalconsent-based befriending and group membership [26]; (iii) a GLP implementation of grassroots bonds, including a running six-agent village market scenario exercising symmetric and asymmetric credit, payments, redemption, escrow, and sale of debt [41]; and (iv) a moded type system for GLP, implemented in Dart from a mathematical specification [44]. Enforcement. Enforcement of the digital social contract—ensuring that participants cannot deviate from the protocol as programmed—is achieved via mutual attestation among the participants’ machines, as described in companion work on secure GLP. Binary transactions. A standard way to realize binary transactions using unary transition systems is for one agent, say p, to offer the transaction to q, who may respond with accept, upon which p may respond with commit, upon which the offered transaction is deemed to have been executed, or abort. Agent p may also issue abort before or after receiving any response from q to its offer, provided p has not previously issued commit. A challenge in this implementation is that a faulty p may fail to either commit or abort following an accept by q, leaving q in limbo, at least in regards to this transaction. Solutions to this are a subject of future work. For now, we note that, worst case, a friendship offer by p accepted by q would remain in limbo. If it is committed by p at some later point, which is not convenient to q, then q can promptly unfriend p, with little or no harm done. In the case of grassroots bonds, a swap transaction in limbo may tie bonds offered by q, which may or may not be harmful to q (not harmful if these are q-bonds, which q may mint as it pleases; or p-bonds that q tries to redeem, and if p is non-responsive it might indicate that p-bonds are not worth much anyhow).
C
Formal Models of Persons in Concurrent Systems
The formal methods tradition has a long lineage of modeling human agents as sources of nondeterminism alongside deterministic machines, but—to the best of our knowledge— without decomposing an agent into person and machine as components of its state. Turing’s choice machines. Before defining what we now call Turing machines (automatic machines, or a-machines), Turing [48] introduced choice machines (c-machines), “whose motion is only partially determined by the configuration”—at designated states, the machine “cannot go on until some arbitrary choice has been made by an external operator.” The external operator is a person who freely chooses between alternatives; the sequence of choices determines which computation unfolds. Turing immediately set c-machines aside, showing that any c-machine computation can be enumerated by an a-machine. His 1939 oracle machines [49] extend this further: the oracle “cannot be a machine” and provides answers
19
20
Describing People and their Machines
the computation cannot derive internally. Both formalisms model the person as external to the machine, providing input at designated points. Process algebras. Hoare’s CSP [20] provides the cleanest process-algebraic encoding of human choice. External choice (□) offers the environment—potentially a person—a selection among initial events, while internal choice (⊓) is resolved by the system. However, the person remains outside the system boundary: CSP models what the person does, not what the person is willing to do. Milner’s CCS [31] uses a single summation operator without formally separating internal from external nondeterminism at the syntactic level. In his later work on bigraphs [32], Milner makes the scope explicit: agents “can be artificial, as in computing systems. . . or they can be natural, e.g. communicating humans.” Both CSP and CCS model agents uniformly—there is no formal distinction between a person and a machine within the same agent. I/O automata and reactive systems. Lynch and Tuttle’s I/O automata [30] partition actions into input (environment-controlled), output (automaton-controlled), and internal actions. The key property is input-enabling: an automaton cannot block input actions, so the environment—potentially a human operator—can act at any moment. The Hybrid I/O Automata extension [28] explicitly states that HIOAs are “intended to model all components of hybrid systems, including. . . humans.” The person, however, is part of the environment, not a component of the automaton’s state. Harel and Pnueli’s reactive systems paradigm [19] draws the foundational dichotomy between transformational systems (batch, terminating) and reactive systems (ongoing interaction with environment). The system is deterministic; all nondeterminism is attributed to the environment. This paradigm was explicitly motivated by human-machine interaction, yet the formalism treats the human as environment rather than as a component of the system. Angelic and demonic nondeterminism. The distinction between angelic and demonic nondeterminism, developed by Back and von Wright [5] in the refinement calculus, provides a semantic treatment relevant to the person/machine boundary. Demonic nondeterminism models adversarial environments (the worst-case choice is made); angelic nondeterminism models cooperative choices (the best-case choice is made). This duality is the closest precursor to the volition/obligation distinction in the present work: a volitional transaction guarded by both parties (both must be willing) versus one guarded by either party (either can force it). Two distinctions separate the frameworks. First, the refinement calculus operates within a sequential program framework, not a multiagent transition system. Second, angelic nondeterminism is a point-of-choice semantics: a choice is resolved locally at each transition, with no residue carried forward. Volitions, in contrast, are persistent, inspectable state that accumulates across transitions; a guard condition reads an agent’s record of willing over the history of the run, not a single local resolution. This shift—from choice as a point-semantic primitive to choice as state—is what lets volitions be shared, compared, and reasoned about within the transition system, rather than external to it. Game structures and alternating-time temporal logic. Module checking [23] models open systems with the environment fully adversarial. Alternating-time temporal logic (ATL) [3] interprets formulas over concurrent game structures where multiple agents simultaneously choose actions. Game semantics [1] models computation as dialogue between Proponent (program, following a deterministic strategy) and Opponent (environment, making free moves). These frameworks treat agents as symmetric players but do not decompose a single agent into person and machine components. Ceremony analysis and human-interactive verification. Ellison’s ceremony analysis [16] extends security protocol analysis to include human participants as protocol nodes.
Lewis-Pye and Shapiro
Bolton’s Enhanced Operator Function Model (EOFM) [7] translates hierarchical human task models into state machines for model checking, with the human as the sole source of nondeterminism. Both treat human nondeterminism as a source of error to be verified against, rather than as a source of legitimate volition to be formally recorded. Normative multiagent systems and electronic institutions. Electronic institutions [17] model multiagent interaction as dialogical frameworks where human and software agents are treated uniformly as role-playing entities. Normative multiagent systems [4] use Event Calculus to specify societies where agents “may fail to, or even choose not to, conform to the specifications.” These approaches model norms that constrain agents, but do not decompose an agent’s state into machine and volitional components, nor do they formalise the distinction between transactions requiring all parties to be willing and those that are obligatory once initiated.
21