TaRDIS-APIs/Artificial-Intelligence-and-Machine-Learning-APIs.md

@@ -2,7 +2,7 @@
 
 ### 1\. Python and MicroPython Test Beds for Federated Learning Algorithms APIs
 
-The Python Test Bed for Federated Learning Algorithms (PTB-FLA) API is provided by the `PtbFla` class in the `ptbfla` module, whereas the MicroPython Test Bed for Federated Learning Algorithms (MPT-FLA) API is provided by the `PtbFla` class in the `mp_async_ptbfla` module. (Note: both classes have the same name to lighten porting legacy applications from PTB-FLA to MPT-FLA.) Both APIs include a constructor, two generic Federated Learning Algorithms (FLAs), the TDM (Time Division Multiplexing) peer data exchange algorithm, and a destructor. The MPT-FLA API also includes the `start` method. (Note: all the MPT-FLA API methods, except the constructor and the destructor, are Python asyncio coroutines, so they should not be called as functions but must be awaited using the `await` keyword.) Below are the details of each component and their respective arguments.
+The Python Test Bed for Federated Learning Algorithms (PTB-FLA) API is provided by the `PtbFla` class in the `ptbfla` module, whereas the MicroPython Test Bed for Federated Learning Algorithms (MPT-FLA) API is provided by the `PtbFla` class in the `mp_async_ptbfla` module. (Note: both classes have the same name to lighten porting legacy applications from PTB-FLA to MPT-FLA.) Both APIs include a constructor, two generic Federated Learning Algorithms (FLAs), two generic algorithms for TDM (Time Division Multiplexing) communication i.e., peer data exchange, and a destructor. The MPT-FLA API also includes the `start` method. (Note: all the MPT-FLA API methods, except the constructor and the destructor, are Python asyncio coroutines, so they should not be called as functions but must be awaited using the `await` keyword.) Below are the details of each component and their respective arguments.
 
 #### Class and Methods in the `ptbfla` module (PTB-FLA API)
 
@@ -86,7 +86,7 @@ Data used by the two generic FLAs (`ldata` and `pdata`) is application-specific.
 
 #### Formalization and Verification
 
-Both generic FLAs (i.e., `fl_centralized` and `fl_decentralized` methods) have been formalized using CSP (Communicating Sequential Process) calculus and verified using the model checker PAT (Process Analysis Toolkit). Two key properties were checked:
+Both generic FLAs (i.e., fl_centralized and fl_decentralized methods) and both generic algorithms for TDM communication (i.e., get1Meas and getMeas) have been formalized using CSP (Communicating Sequential Process) calculus and verified using the model checker PAT (Process Analysis Toolkit). Two key properties were checked:
 
 - **Deadlock Freedom (Safety):** Ensures that the system will not reach a state where no progress is possible.
 - **Termination (Liveness):** Ensures that the system will eventually complete its tasks.