Executive Summary : | Graph-based models are commonly used to capture the behavior of complex software and hardware systems with stochastic behavior. These models can be categorized into action-labelled continuous-time Markov chains (ACTMCs) and state-labeled continuous-time Markov chains (SCTMCs). ACTMCs are used for various applications such as stochastic activity networks, Petri nets, and stochastic process algebras. However, model checking of ACTMC models is challenging due to the absence of expressive property specification formalisms in the action-labeled setting and fixed-point operators.
This project aims to propose a theoretical framework for model and logic transformation functions between state-labeled and action-labeled stochastic systems. The project will define model transformation functions that enable the construction of SCTMCs from ACTMC models and vice versa. The project will also provide definitions of the invertibility criterion and left inverse of these transformation functions. Another goal is to define logic transformation functions between state and action-based stochastic logics. The project will define the syntax and semantics of an intuitive action-based stochastic logic called action-based continuous stochastic logic (aCSL), which is sensitive to invisible actions. The project will propose logic transformation functions between CSL and aCSL.
The approach will help establish a detailed understanding of the connections between different classes of models and logics, enabling efficient minimization and verification of ADTMC models that cannot be verified in the stochastic process algebraic setting. |