arXiv subjects

Marko Popovic

Publications and source records attributed to Marko Popovic.

14 recordsLinked to original sources

arXiv2025

Formal Verification of a Generic Algorithm for TDM Communication Over Inter Satellite Links

The Python Testbed for Federated Learning Algorithms is a simple FL framework targeting edge systems, which provides the three generic algorithms: the centralized federated learning, the decentralized federated learning, and the universal TDM communication in the current time slot. The first two were formally verified in a previous paper using the CSP process algebra, and in this paper, we use the same approach to formally verify the third one, in two phases. In the first phase, we construct the CSP model as a faithful representation of the real Python code. In the second phase, the model checker PAT automatically proves correctness of the third generic algorithm by proving its deadlock freeness (safety property) and successful termination (liveness property).

cs.DC↗

arXiv2025

Generic Algorithm for Universal TDM Communication Over Inter Satellite Links

The original Python Testbed for Federated Learning Algorithms is a light FL framework, which provides the three generic algorithms: the centralized federated learning, the decentralized federated learning, and the TDM communication (i.e., peer data exchange) in the current time slot. The limitation of the latter is that it allows communication only between pairs of network nodes. This paper presents the new generic algorithm for the universal TDM communication that overcomes this limitation, such that a node can communicate with an arbitrary number of peers (assuming the peers also want to communicate with it). The paper covers: (i) the algorithm's theoretical foundation, (ii) the system design, and (iii) the system validation. The main advantage of the new algorithm is that it supports real-world TDM communications over inter satellite links.

cs.DC↗

arXiv2025

Translating Federated Learning Algorithms in Python into CSP Processes Using ChatGPT

The Python Testbed for Federated Learning Algorithms is a simple Python FL framework that is easy to use by ML&AI developers who do not need to be professional programmers and is also amenable to LLMs. In the previous research, generic federated learning algorithms provided by this framework were manually translated into the CSP processes and algorithms' safety and liveness properties were automatically verified by the model checker PAT. In this paper, a simple translation process is introduced wherein the ChatGPT is used to automate the translation of the mentioned federated learning algorithms in Python into the corresponding CSP processes. Within the process, the minimality of the used context is estimated based on the feedback from ChatGPT. The proposed translation process was experimentally validated by successful translation (verified by the model checker PAT) of both generic centralized and decentralized federated learning algorithms.

cs.AI↗

arXiv2024

Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites

Python Testbed for Federated Learning Algorithms (PTB-FLA) is a simple FL framework targeting smart Internet of Things in edge systems that provides both generic centralized and decentralized FL algorithms, which implement the corresponding FL orchestration protocols that were formally verified using the process algebra CSP. This approach is appropriate for systems with stationary nodes but cannot be applied to systems with moving nodes. In this paper, we use celestial mechanics to model spacecraft movement, and timed automata (TA) to formalize and verify the centralized FL orchestration protocol, in two phases. In the first phase, we created a conventional TA model to prove traditional properties, namely deadlock freeness and termination. In the second phase, we created a stochastic TA model to prove timing correctness and to estimate termination probability.

cs.DC↗

arXiv2024

MicroPython Testbed for Federated Learning Algorithms

Recently, Python Testbed for Federated Learning Algorithms emerged as a low code and generative large language models amenable framework for developing decentralized and distributed applications, primarily targeting edge systems, by nonprofessional programmers with the help of emerging artificial intelligence tools. This light framework is written in pure Python to be easy to install and to fit into a small IoT memory. It supports formally verified generic centralized and decentralized federated learning algorithms, as well as the peer-to-peer data exchange used in time division multiplexing communication, and its current main limitation is that all the application instances can run only on a single PC. This paper presents the MicroPyton Testbed for Federated Learning Algorithms, the new framework that overcomes its predecessor's limitation such that individual application instances may run on different network nodes like PCs and IoTs, primarily in edge systems. The new framework carries on the pure Python ideal, is based on asynchronous I/O abstractions, and runs on MicroPython, and therefore is a great match for IoTs and devices in edge systems. The new framework was experimentally validated on a wireless network comprising PCs and Raspberry Pi Pico W boards, by using application examples originally developed for the predecessor framework.

cs.DC↗

arXiv2023

Developing Elementary Federated Learning Algorithms Leveraging the ChatGPT

The Python Testbed for Federated Learning Algorithms is a simple Python FL framework easy to use by ML&AI developers who do not need to be professional programmers, and this paper shows that it is also amenable to emerging AI tools. In this paper, we successfully developed three elementary FL algorithms using the following three steps process: (i) specify context, (ii) ask ChatGPT to complete server and clients' callback functions, and (iii) verify the generated code.

cs.DC↗

arXiv2023

A Federated Learning Algorithms Development Paradigm

At present many distributed and decentralized frameworks for federated learning algorithms are already available. However, development of such a framework targeting smart Internet of Things in edge systems is still an open challenge. A solution to that challenge named Python Testbed for Federated Learning Algorithms (PTB-FLA) appeared recently. This solution is written in pure Python, it supports both centralized and decentralized algorithms, and its usage was validated and illustrated by three simple algorithm examples. In this paper, we present the federated learning algorithms development paradigm based on PTB-FLA. The paradigm comprises the four phases named by the code they produce: (1) the sequential code, (2) the federated sequential code, (3) the federated sequential code with callbacks, and (4) the PTB-FLA code. The development paradigm is validated and illustrated in the case study on logistic regression, where both centralized and decentralized algorithms are developed.

cs.DC↗

arXiv2023

Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP

Federated learning (FL) is a machine learning setting where clients keep the training data decentralised and collaboratively train a model either under the coordination of a central server (centralised FL) or in a peer-to-peer network (decentralised FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralised and a decentralised one, using the CSP process calculus and the PAT model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freeness (safety property) and successful termination (liveness property). The CSP models are constructed bottom-up by hand as a faithful representation of the real Python code and is automatically checked top-down by PAT.

cs.DC↗

arXiv2023

A Simple Python Testbed for Federated Learning Algorithms

Nowadays many researchers are developing various distributed and decentralized frameworks for federated learning algorithms. However, development of such a framework targeting smart Internet of Things in edge systems is still an open challenge. In this paper, we present our solution to that challenge called Python Testbed for Federated Learning Algorithms. The solution is written in pure Python, and it supports both centralized and decentralized algorithms. The usage of the presented solution is both validated and illustrated by three simple algorithm examples.

cs.DC↗

arXiv2023

PSTM Transaction Scheduler Verification Based on CSP and Testing

Many online transaction scheduler architectures and algorithms for various software transactional memories have been designed in order to maintain good system performance even for high concurrency workloads. Most of these algorithms were directly implemented in a target programming language, and experimentally evaluated, without theoretical proofs of correctness and analysis of their performance. Only a small number of these algorithms were modeled using formal methods, such as process algebra CSP, in order to verify that they satisfy properties such as deadlock-freeness and starvation-freeness. However, as this paper shows, using solely formal methods has its disadvantages, too. In this paper, we first analyze the previous CSP model of PSTM transaction scheduler by comparing the model checker PAT results with the manually derived expected results, for the given test workloads. Next, according to the results of this analysis, we correct and extend the CSP model. Finally, based on PAT results for the new CSP model, we analyze the performance of PSTM online transaction scheduling algorithms from the perspective of makespan, number of aborts, and throughput. Based on our findings, we may conclude that for the complete formal verification of trustworthy software, both formal verification and it's testing must be jointly used.

cs.DC↗

arXiv2019

Negentropy concept revisited: Standard thermodynamic properties of 16 bacteria, fungi and algae species

Standard molar and specific (per gram) enthalpy of formation, entropy and Gibbs free energy of formation of biomatter have been determined for 16 microorganism species, including Methylococcus capsulatus, Klebsiella aerogenes, Paracoccus denitrificans, Escherichia coli, Pseudomonas C12B, Aerobacter aerogenes, Magnetospirillum gryphiswaldense, Saccharomyces cerevisiae, Candida utilis, Chlorella, Chlorella a sp. MP-1, C. minutissima, C. pyrenoidosa and C. vulgaris. The average values of ${\Delta}_{f}H{\deg}$ are for bacteria -4.22 kJ/g, for fungi -5.03 kJ/g and for algae -4.40 kJ/g. The average values of S{\deg} are for bacteria 1.48 J/g K, for fungi 1.45 J/g K and for algae 1.48 J/g K. The average values of ${\Delta}_{f}G{\deg}$ are for bacteria -2.30 kJ/g, for fungi -3.15 kJ/g and for algae -2.48 kJ/g. Based on the results, an analysis was made of colony growth in time. In the first three phases, entropy change of microorganisms plated in a Petri dish is positive and entropy of the colony increases. In the fourth phase, due to limitation of nutrients, entropy remains constant. In the fifth phase, due to lack of nutrients, entropy of the colony decreases and microorganisms die-off. Based on the results, the negentropy concept is analyzed.

physics.bio-ph↗

arXiv2018

Wanted Dead or Alive Extraterrestrial Life Forms (Thermodynamic criterion for life is a growing open system that performs self-assembly processes)

For more than 100 years, humanity (both specialists and enthusiastic laics) has been searching for extraterrestrial life hoping we are not alone. The first step in the quest for extraterrestrial life is to define what and where exactly to look for. Thus, the basic definition of living matter is a conditio sine qua non for the quest. The diversity of species on Earth is so large that our quest for extraterrestrial life cannot be limited to forms and shapes present and known to us from our environment. However, there are two formal conditions that must be fulfilled in order for something to be assumed as living matter. First, it should represent a growing open thermodynamic system (in biological terms - a cell), and thus be a system out of equilibrium. Second, it must perform synthesis, self-assembly and accumulation processes (in biological terms to grow, maintain homeostasis, respond to environment, reproduce, exchange matter and energy, evolve). Populated planets are consisted of two components: biosphere and its environment (geosphere, hydrosphere and atmosphere). Living matter and its environment are out of equilibrium. Thus, the candidate planets are dynamic inhomogeneous systems for two reasons. First, a planet receives energy from its star, which leads to disequilibrium for external reasons. Animate matter contributes to disequilibrium for internal reasons: accumulation of matter and self-assembly. In practice, for a screening, an astrobiologist should search for increase in inhomogeneity on a candidate planet.

q-bio.OT↗

arXiv2018

Thermodynamic Mechanism of Life and Aging

Life is a complex biological phenomenon represented by numerous chemical, physical and biological processes performed by a biothermodynamic system/cell/organism. Both living organisms and inanimate objects are subject to aging, a biological and physicochemical process characterized by changes in biological and thermodynamic state. Thus, the same physical laws govern processes in both animate and inanimate matter. All life processes lead to change of an organism's state. The change of biological and thermodynamic state of an organism in time underlies all of three kinds of aging (chronological, biological and thermodynamic). Life and aging of an organism both start at the moment of fertilization and continue through entire lifespan. Fertilization represents formation of a new organism. The new organism represents a new thermodynamic system. From the very beginning, it changes its state by changing thermodynamic parameters. The change of thermodynamic parameters is observed as aging and can be related to change in entropy. Entropy is thus the parameter that is related to all others and describes aging in the best manner. In the beginning, entropy change appears as a consequence of accumulation of matter (growth). Later, decomposition and configurational changes dominate, as a consequence of various chemical reactions (free radical, decomposition, fragmentation, accumulation of lipofuscin-like substances...).

q-bio.OT↗

arXiv2017

Researchers in an Entropy Wonderland: A Review of the Entropy Concept

Entropy concept was introduced by Clausius 160 years ago, and has been continually enriched, developed and interpreted by the researchers in many different scientific disciplines ever since. Thermodynamics and other scientific disciplines face several simple but crucial questions concerning the entropy concept. Thus, it is frequently possible to notice a misuse of entropy. Sometimes unbelievable confusion in the literature is summarized by von Neumann's sentence: "No one knows what entropy really is." Four major questions stand before thermodynamics. (1) How many kinds of entropy are there? (2) What is the physical meaning of entropy? (3) Is entropy a subjective or an objective property? (4) Is entropy in any way related to information? This paper attempts to describe the roots, the conceptual history of this important concept and to describe the path of its development and application in different scientific disciplines. Through this we attempt to give some possible answers to the questions mentioned above.

physics.chem-ph↗