# Probabilistic Model Checking GitHub Repositories for Software Project Analysis
## 2 Background  
### Discrete-Time Markov Chain  
DTMC is a probabilistic model used to analyze the stochastic transitions between different states or events [13; 16]. Particularly useful for capturing and studying the dynamics of systems where transitions occur in discrete time steps, DTMC models the system's behavior as a series of states with transitions occurring at specific intervals. The Markov property, indicating that the probability of transitioning to a future state depends only on the current state and is independent of past states, allows for simplified modeling and analysis of systems with stochastic behavior. DTMC can be defined in 4-tuple: \(M=(S,P,L,AP)\)  
* \(S\) represents the state space, which is the set of all possible states the system can be in.
* \(P:S\times S\rightarrow[0,\,1]\) denotes the state transition probability matrix of the state space \(S\).
* \(L:S\to 2^{AP}\) is a labeling function that maps each state to its respective labels.
* \(AP\) is a finite set of atomic propositions.  
In more detail, for DTMC with \(n\) states, the state space \(S\) is defined as \(S=\{s_{1},s_{2},\ldots,s_{n}\}\), and the transition matrix \(P\) is an \(n\times n\) matrix, where \(P_{ij}\) represents the probability of transitioning from state \(s_{i}\) to state \(s_{j}\). The labeling function \(L\) provides a means to label states with specific properties or characteristics, enhancing the representation of system behavior.  
DTMC finds applications in studying various aspects related to social interactions, communication patterns, or behavioral dynamics within the context of interpersonal relationships. In [17; 18], DTMC is employed to model dialogue acts, emotions, decision making, and action information in conversations among project participants with assigned roles. Model checking is performed using probabilistic Computation Tree Logic (pCTL), allowing the analysis of relationships and interactions among participants over short or long periods and providing diverse quantitative metrics for analyzing interactions during meetings. In the context of continuous system behavior, Markov modeling is used to specify safety-related properties, and model checking verifies safety. Ref. [19] introduces a method for verifying the safety of human-robot interaction systems using probabilistic model checking. DTMC models the continuous states of robots and humans, and safety properties are specified and verified using probabilistic reward computation tree logic. Ref. [20] models the Automated Airspace Concept system for air traffic control using DTMC to ensure safety. Separation assurance algorithms defined over specific time intervals are modeled, safety requirements are specified using pCTL, and model checking calculates the likelihood of conflicts, evaluating various design options and providing quantitative measurement methods.  
Our choice to use DTMC and model-checking techniques in this research is motivated by the need to comprehensively analyze the temporal dynamics of contributions and collaboration patterns within GitHub repositories. By modeling essential GitHub actions through DTMC and employing model checking, we can quantitatively assess various aspects, such as repository characteristics, branch management, and participant analysis. This approach enables us to gain insights into the evolving behavior and interaction patterns of contributors over time, contributing to a more holistic understanding of GitHub project dynamics.