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.

翻译：并发与分布式系统的形式化模型通常描述机器；而操作机器的人要么被忽略，要么被当作外部环境处理。然而，关键分布式系统——尤其是草根平台——包含操作个人机器（如智能手机）的人，对其忠实描述必须涵盖人与机器的状态，以及二者如何共同影响系统行为。本文提出意志多智能体原子事务——由机器原子执行且受人的意志守护——作为描述由人操作机器所构成系统的新型数学基础。每个智能体的状态由意志状态和机器状态组成；事务在机器前置条件成立且守护人愿意时被启用。例如，建立两人好友关系需双方共同守护；解除好友关系则由任意一方守护；货币与债券的自愿交换需双方共同守护，而支付仅需支付方守护。我们构建了数学机制以表达该框架下平台的安全性与活跃性，并提供了两个草根平台的示例规约：社交网络以及货币与债券。这些规约随后被AI用于推导出可工作的实现。