REVIEW 5 cited by
Multiagent Transition Systems for Composing Fault-Resilient Protocol Stacks
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
We present a novel mathematical framework for the specification and analysis of fault-resilient distributed protocols and their implementations, with the following components: 1. Transition systems that allow the specification and analysis of computations with safety and liveness faults and their fault resilience. 2. Notions of safe, live and complete implementations among transition systems and their composition, with which the correctness (safety and liveness) and completeness of a protocol stack as a whole follows from each protocol implementing correctly and completely the protocol above it in the stack. 3. Applying the notion of monotonicity, pertinent to histories of distributed computing systems, to ease the specification and proof of correctness of implementations among distributed computing systems. 4. Multiagent transition systems, further characterized as centralized/distributed and synchronous/asynchronous; safety and liveness fault-resilience of implementations among them and their composition. The framework is being employed in the specification of a grassroots ordering consensus protocol stack, with a grassroots dissemination protocol and its implementation of grassroots social networking and of sovereign cryptocurrencies, and an efficient Byzantine atomic broadcast protocols as initial applications.
Forward citations
Cited by 5 Pith papers
-
Volition-Guarded Multiagent Atomic Transactions: Describing People and their Machines
Volition-guarded multiagent atomic transactions decompose agents into person volitions plus machine state, enabling formal specs and proofs that social networks and coins/bonds are volitionally grassroots under a new ...
-
Volition Elicitation: Operational Semantics for People and Their Machines
vGLP extends GLP so that program reductions can be guarded by a person's expressed volition, with the UI derived from the semantics and correctness proofs for soundness, liveness, and compilation.
-
Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI (Full Version)
dGLP and madGLP are deterministic, implementation-ready semantics for Grassroots Logic Programs, proved correct against the abstract nondeterministic semantics.
-
GLP: A Grassroots, Multiagent, Concurrent, Logic Programming Language for AI (Full Version)
GLP is a logic programming language whose single-reader/single-writer variables give secure channels, with proofs that multiagent GLP computations are deductions and that multiagent GLP is a grassroots protocol.
-
GLP: A Grassroots, Multiagent, Concurrent, Logic Programming Language for AI
GLP is a single-assignment concurrent logic language whose multiagent semantics is claimed to guarantee that any program using cold-calls yields a grassroots platform, with the proof deferred to the full paper.
Discussion (0). Sign in to comment.