Anonymous distributed consensus regarding the verification of protocols

Abstract

Techniques to perform mathematically and logically rigorous validations for decentralized applications (DApp) communicatively coupled to a distributed ledger are disclosed. A protocol for a business or enterprise process is encoded as a workflow on a labeled transition system as part of a DApp. Transitions are coded via an asynchronous Pi Calculus or other process calculi. A rules engine validates transitions using process calculi operations, or alternatively performing mathematical and logical analyses on the labeled transition system. Validations are disclosed for both development time and run time. In some embodiments, the logic behind the DApp is composed of a predetermined set of components representing processes. In one specific embodiment, the predetermined set of components is solely of an input component and an output component when composed perform a transaction where either both components received artifact representations from the other component or neither do.

What is claimed is: 
     
         1 . A method to perform workflow transition validations, comprising:
 receiving, at a server, a specification of a workflow, the specification comprising of actors, states, transitions between the states, and artifacts representing resources as assets to be exchanged in the transitions;   generating from a received workflow specification a directed graph (digraph) of the workflow comprised of a plurality of nodes representing the states and directed edges representing the transitions between the states, wherein each of the transitions is associated with at least one rule that includes a symmetric exchanging of the assets to verify the validity of the transitions between the states;   deploying, by the server, a validator application and a distributed ledger technology (DLT)-based application (decentralized application), wherein the validator application identifies the transitions and retrieves associated rules to offload processing off the decentralized application during a DLT runtime load on the workflow transition validations;   receiving, by the validator application, an input trigger that corresponds to a state transition in the digraph;   performing, by the validator application, a retrieved rule that is associated with the state transition in the digraph;   updating, by the validator application, the digraph based at least upon a verification of the state transition in the digraph, using at least the retrieved rule;   calling, by the validator application, the decentralized application to store an updated state of the digraph on a distributed ledger; and   storing, by the decentralized application, the updated state of the digraph on the distributed ledger.   
     
     
         2 . The method of  claim 1 , wherein the digraph comprises nodes representing the states and directed edges representing valid transitions between the states. 
     
     
         3 . The method of  claim 1 , wherein the transition in the digraph is encoded using expressions supporting formal methods, and the retrieved rule is encoded using a programmable language supporting formal method. 
     
     
         4 . The method of  claim 3 , wherein the programmable language supporting formal method includes an asynchronous pi calculus. 
     
     
         5 . The method of  claim 3 , wherein the digraph supports a bisimulation, a coinduction, or both and the retrieved rule includes an application of the bisimulation, the coinduction, or both. 
     
     
         6 . The method of  claim 3 , wherein the retrieved rule includes an application of a Hennessy-Milner logic. 
     
     
         7 . The method of  claim 1 , wherein the digraph includes a category theoretical representation of the received specification of the workflow. 
     
     
         8 . A method to perform workflow transition validations, comprising:
 receiving, at a server, a specification of a workflow, the specification comprising of actors, transitions, and artifacts that represent resources as assets to be exchanged in the transitions;   generating from a received workflow specification a labeled transition system (LTS), wherein each of the transitions in the LTS is associated with at least one rule that includes a symmetric exchanging of the assets to verify a validity of the transitions, and wherein a generated LTS is composed of a set of predetermined components communicatively coupled to a distributed ledger, the predetermined components representing processes;   deploying, by the server, a validator application and a distributed ledger technology (DLT)-based application (decentralized application), wherein the validator application identifies the transitions and retrieves associated rules to offload processing off the decentralized application during a DLT runtime load on the workflow transition validations;   receiving, by the validator application, an input trigger that corresponds to a state transition in a generated LTS, performing, by the validator application, a retrieved rule that is associated with the state transition in a directed graph (digraph);   updating, by the validator application, the digraph based at least upon a verification of the state transition in the LTS, using at least the retrieved rule; and   storing, by the decentralized application, an updated state of the digraph on the distributed ledger.   
     
     
         9 . The method of  claim 8 , wherein the predetermined components are atomic components. 
     
     
         10 . The method of  claim 8 , wherein the transition in the digraph is encoded using expressions supporting formal methods, and the retrieved rule is encoded using a programmable language supporting formal method. 
     
     
         11 . The method of  claim 10 , wherein the programmable language supporting formal method includes an asynchronous pi calculus. 
     
     
         12 . The method of  claim 10 , wherein the digraph supports a bisimulation, a coinduction, or both and the retrieved rule includes an application of the bisimulation, the coinduction, or both. 
     
     
         13 . The method of  claim 10 , wherein the retrieved rule includes an application of a Hennessy-Milner logic. 
     
     
         14 . The method of  claim 8  further comprising: calling, by the validator application, the decentralized application to store the updated digraph on the distributed ledger. 
     
     
         15 . The method of  claim 8 , wherein the predetermined components implement symmetrical exchange of artifacts. 
     
     
         16 . The method of  claim 8 , wherein the predetermined components are comprised of either symmetric asset exchange input atomic components, symmetric asset exchange output atomic components, or both. 
     
     
         17 . A system to automate a workflow, the system comprising:
 a processor;   a memory coupled to the processor, the memory includes a plurality of computer-executable components that are executable with the processor to perform a plurality of actions, the plurality of actions comprising:   receiving a specification of a workflow, the specification comprising transitions and artifacts representing resources as assets to be exchanged in the transitions;   generating from a received specification a directed graph (digraph) of the workflow, wherein each of the transitions in the digraph is associated with at least one rule that includes a symmetric exchanging of the assets to verify a validity of the transition;   deploying a validator application and a distributed ledger technology (DLT)-based application (decentralized application), wherein the validator identifies the transitions and retrieves associated rules to offload processing off the decentralized application during a DLT runtime load on workflow transition validations;   receiving an input trigger that corresponds to a state transition in the digraph;   performing a retrieved rule that is associated with the state transition in the digraph;   updating a state of the digraph, using at least the retrieved rule;   calling via the validator application the decentralized application to store an updated state of the digraph on a distributed ledger; and   storing the updated state of the digraph on the distributed ledger.   
     
     
         18 . The method of  claim 17 , wherein the transition in the digraph is encoded using expressions supporting formal methods, and the retrieved rule is encoded using a programmable language supporting formal method. 
     
     
         19 . The method of  claim 18 , wherein the programmable language supporting formal method includes an asynchronous pi calculus. 
     
     
         20 . The method of  claim 18 , wherein the digraph supports a bisimulation, a coinduction, or both and the retrieved rule includes an application of the bisimulation, the coinduction, or both.