Abstract

Probabilistic model checking is frequently used to examine stochastic behavior. Model-checking is important for examining before extensive simulations, in differing fields, including computer communications, networks, security, and biology. In this work performance of histogram-based fuzzy image enhancement (HFIE Algorithm). The fuzzy contrast enhancement algorithm based on histograms is used to improve low contrast colored photographs. K is the contrast intensification parameter calculated from the histogram. The RGB image is transformed into HSV to preserve the chromatic information in the original image. To improve the image, only the V component is stretched using the M and K parameters. HFIE Algorithm is analyzed by developing its Discrete-time Markov Chain (DTMC) model in the Probabilistic Symbolic Model Checker (PRISM). First, a labeled transition diagram showing the functionality of HFIE Algorithm is constructed, then the HFIE Algorithm model using the PRISM tool is developed. The expected time to convert RGB image to HSV, probability of achieving enhanced RGB image, and expected SNR are measured with the help of properties.

Keywords: PRISM, MTBDD, DTMC, CTMC, MDP, PCTL, HFIEA, RGB, HSV, SNR.

Received: 26 October 2021 / Revised: 3 January 2022 / Accepted: 14 January 2022/ Published: 19 January 2020

Contribution/ Originality

This research is use to perform probabilistic model of Histogram based fuzzy image enhancement Algorithm.

1. INTRODUCTION

Model-checking is a technique used for specifying quantitative aspects of a system's stochastic behavior. the Probabilistic model checking refers to the construction and evaluation of a probabilistic model based on a high-level description of a system's behavior. The model is examined by expressing one or more quantitative properties in temporal logic. These elements enable us to develop a better understanding of the system's accuracy, as well as its reliability and performance. The Probabilistic Model Checking is an essential and extensively used verification way of measuring accuracy evaluations that would be very difficult and time expensive to achieve using simulations today. Due to extensive simulations, this approach has been successfully applied in all fields, including networks, computer communications, security, and biology [1]. Many researchers have used probabilistic and hybrid model checking techniques with success, such as Slede [2] PRISM CaVI, and APMC. However, in this paper, the Contrast enhancement will be discussed that improves an image's apparent visual quality [3]. The fast and efficient HFIE used for low contrast color images are described here, which improves the visual quality of the image and helps in the extraction of spatial information contained within the image in comparison to other powerful enhancement methods. When compared to previous approaches, such as a Fuzzy Enhancement can be defined as a fuzzy set is created by modifying the grey tone with a membership function. Using the fuzzy logic method, different experts used different membership values to refine the quality and steep of contrast enhancement. The image is usually consisting of a set of fuzzy singletons, each with its membership value. The membership value corresponds to the range's degree of image property [4].

Histogram enhancement (HE) is the most widely used method. This technique is used to change the intensities of an image to improve the contrast and confirm that the image has the intensities from 0 to 255, which represents the number of depth possible values [4]. It also assumes that the evenly spaced grayscale histograms have the best visual contrast. On the other hand, another advanced histogram-based extension (AHE) tends to change the noise and bi-histogram equalization in relatively uniform areas of the image [3]. The Leningrad value of the image is calculated from the gradient (x, y) at each pixel (x, y) and its partial derivative is obtained with a high pass filter. The Contrast Enhancement Index is the ratio of the results of the contrast enhancement method, contrast enhancement, and calculation time. In various areas of image processing, fuzzy logic is being used effectively. Fuzzy-based image enhancement algorithms with superior performance to conventional and other advanced techniques like GLG have been developed. Image fuzzification, changing membership values, and, if necessary, de-fuzzing images are the three main stages of fuzzy image processing. The main strength of fuzzy image processing lies in the intermediate steps (changing membership values). After the image data is converted from the grayscale area to the fuzzy membership area (fuzzification), the membership value will be changed using the appropriate fuzzy technology [4]. HFIE Algorithm is based on low contrast color images, the intercomparison of various techniques was conducted out. According to the performance evaluation, this method is computationally efficient. This technique is fundamentally based on two key attributes the image's average intensity M and the contrast intensification component K [3]. The proposed method is applied to the HSV color space so that only the V component is stretched while the color information is retained (S and H) [3].

Probabilistic analysis has been applied successfully for a diverse range of applications to examine the real-time attribute likewise, performance and reliability, power management, biological process modeling, Communication, network, and multimedia protocols, security protocols, game theory and, many others but it is not applied in the domain of fuzzy image enhancement algorithm. The contribution of this work is to present the working steps of the HFIE Algorithm in the terms of states and transitions by applying the probabilistic model checking approach.

The related work is discussed in this section2. Section3 discusses the working of HFIE Algorithm. Section4 gives the introduction of the PRISM model checker and the models that support it and also mentions the implementation of HBFIA.Section5 discusses the results.Finally, in Section6 conclusion of the paper is depicted.

2. RELATED

2.1. Work

This section is consisting of two parts. The first part highlights the successful image enhancement techniques, and the second part discusses the application of probabilistic modeling in a variety of applications. In the field of digital image enhancement and simulation of HFIE Algorithm lot of work is done and researchers have used different tools and techniques for measuring different parameters of the numerous types of images. Performance Evaluation of Fuzzy and Histogram Based Color Image Enhancement [4] Optimized Adaptive Fuzzy based Image Enhancement Techniques [5] FLBSMF [6] CLAHE [7] Underwater enhancement with HSV and HE image [8] are discussed in this section.

The enhancement based on fuzzy and histograms [4] the (HFIE Algorithm) proved effectively enhances the contrast of digital images. Fuzzy and histogram-based enhancements were designed and implemented in MATLAB using image processing. The efficiency of histogram and fuzzy-based image enhancement for various types of images, such as underwater, remote sensing, and medical images, is being studied. The effectiveness of fuzzy-based enhancements over existing methods was measured the MSE and PSNR using a modified edge-preserving adaptive k-fuzzy-based enhancement algorithm for digital images. The value of k was also evaluated by several optimization techniques.

Enhancement of Underwater Images [8] The V transform algorithm and histogram equalization techniques To attempt, an underwater image is separated into its R (Red), G (Green), and B (Blue) components and converted from RGB to HSV color space. Second, the V element's extension is determined by the start and end of the interval. The color space is then transformed from HSV to RGB, and histogram equalization is achieved to each R, G, and B component. The R, G, and B components are then merged to provide a color image and the Gaussian low-pass filter is applied to the underwater image. They also assess to measure its performance based on MSER, SNR, PSNR, and entropy. However, the (HE) method is based on a grey-scale histogram with a uniform distribution.

Image enhancement techniques based on optimized adaptive fuzzy [5] are primarily used to analyze the quality of existing image enhancement techniques such as histogram correction, adaptive histogram correction, and fuzzy image enhancement. It was observed that the value of the contrast parameter "K" in the fuzzy method was statically assumed to be 128. To overcome this, a new optimized fuzzy method was proposed to make the contrast dynamic. Various optimization algorithms such as ACO, PSO, and ABC are used to optimize the contrast in this situation. It can effectively increase the contrast of digital images by using the HFIE Algorithm with optimized contrast values. This method was designed and implemented in MATLAB, and the method with the most optimized contrast values was preferred.

The analysis [6] was developed to improve the brightness and contrast of color images. The lightness component was employed during the FLBSMF algorithm utilizing the YIQ color model, but the color composition has not changed. The proposed algorithm was compared to other algorithms using other criteria such as B. Enhancement of fuzzy logic using membership function changes based on squared operations, histogram-based fuzzy logic, histogram equalization, and multi scale readjustment with color restoration. As a result of FLBSMF has entropy (7.44), mean square saturation error (2.2E08) and hue (8.11E07), natural image brightness order error (2.97), and natural image quality (2,97) (0.90) entropy. Other algorithms have been proposed that have high values but low values for the other four parameters (MSEH, MSES, NIQE, LOE).

The proposed method is employed to attain local image contrast preservation, dynamic range compression and contrast limited adaptive histogram equalization (CLAHE) is used. Local gain parameter at each pixel is used during the contrast enhancement based on the corresponding local gain parameter, which is calculated in line with the present pixel proximity edge density. The execution of the proposed method is assessed using various image quality measures. Experimental results show that the proposed method provides more information about the image details, which can help facilitate further image analysis [7].

This part of the related work section explains how PRISM is used to evaluate and verify several protocols from diverse areas. Probabilistic modeling deals with several case studies. PRISM has been successfully used for the probabilistic model checking to examine the efficiency of a wide range of systems, and the gossip protocols [9] are also important to consider. FTTP [1] Robot swarm behavior [10] and (PEADG) [11] are proposed and evaluated via PRISM in the literature. Using Probabilistic Model Checking Designing Human Assisted Wireless Sensor and Robot Networks [12] path optimization modeling of UAV based on probabilistic model checking [13] variable reordering, quartiles, and weak deterministic automata with PRISM Advances in probabilistic model checking [14] Robots deployed in extreme environments via probabilistic model checking [15] PRISM-games [16] ant-based position less swarming of probabilistic model checking [17] A Heuristics-Based Incremental at Run time by Probabilistic Model Checking [18] and for the probabilistic systems automated verification techniques [19].

The Purpose of this research [19] is used to present an introduction to the probabilistic model checking technique, which is used to automatically verify the quantitative properties of probabilistic systems. Authors are particularly interested in Markov decision processes (MDPs), which can represent both stochastic and non-deterministic behavior. Methods are described for analyzing a wide range of their properties. The techniques covered in this work can be used to analyze the performance and dependability of networked systems, communication protocols, and randomized distributed algorithms, and other algorithms. They also discuss techniques for compositional modeling and verification of multi-component probabilistic systems, which frequently comprise various components that operate in parallel. Finally, they describe three large case studies that show how the methods discussed in the study can be used in practice.

MDP is used to model the Gossip Protocol to determine the best and worst performers, as well as the overall performance of the protocol. The Gossip protocols are a type of communication protocol in which each system node distributes information to many peer nodes daily basis. Although the use of probabilistic model checking limits the size of the networks that can be analyzed, the small networks can still highlight interesting behavior that may also occur in more realistic network configurations. Because of the asynchronous behavior of individual node activities in distributed networks as well information loss, the average case can differ greatly from the extreme (best/worst) cases. The behavior of gossip protocols and the random selection of nodes for information sharing are both probabilistic and nondeterministic [9]. Clusters are formed in the first step of the FTTT protocol to store data related to member sensor nodes in the wireless sensor network based on the CTMC model. The FTTT protocol's second step is to locate redundant sensor nodes. The moving target information is sent to the base station after redundancy has been removed in the third step of the protocol. This is the protocol's fourth step, the cluster-based arrangement facilitates the management of failed cluster heads. The FTTT protocol's final step deals with failed sensor nodes while avoiding extra messages [1]. By occupying less memory of the symmetry reduction enables verification on models of many orders of magnitude larger PRISM-symm and GRIP are presented in the study [1].This swarm algorithm is described in the study [10] using propositional linear-time temporal logic. This temporal swarm algorithm specification was used to investigate methods for generating implementations from a formal specification. The symmetry reduction approach can be used to improve the efficiency of probabilistic model checking by allowing the verification of models with large MTBDD spaces. In an intriguing study utilizing probabilistic modeling to examine foraging swarm robot behavior [10]. PEADG's goal is to extend the life of wireless sensor networks that collect data. To avoid the problem of Probabilistic Automata (PAs) has been created as a result of the state space explosion and applied to the DTMC module first. The original method consists of many modules, whereas the improved method consists of one module that constructs a module with only reachable state space and no possible state space. As a result, the advanced technique can deal with 226 sensor nodes instead of the original approach's 26 sensor nodes. Significantly, the number of nodes evaluated during modeling is not clearly stated in the majority of protocols, although this is one of the necessary factors. It is questionable to aim at the difference between the protocols [11].

The application of wireless sensor networks (WSNs) in a broad variety of applications is discussed including(air pollution and fire detection), industrial operations (including machine surveillance), and precision agriculture [12]. However, operating the massive WSN is a difficult task because it requires constant monitoring to remain operational. In robots, WSNs are dependent upon one or more robots that are an integral part of the system and to keep the system operational, and improve the overall performance of the system. Thus, in the study [12] authors analyzed the performance of a robot-assisted WSN using probabilistic model checking before deploying robots and sensors in the field. They examined key parameters such as network size, the number of sensors necessary to maintain the network operational, and the time to service the farthest location based on specific application requirements. The MDP is used to capture uncertainties and flaws in human-robot interactions. This shows smart decision-making by a human operator whose performance is influenced by both external and internal factors.

The main purpose of the literature [13] is to provide the overview that the unmanned aerial vehicle (UAV) flight path optimization to progress effectiveness and safety, UAV path optimization modeling built on probabilistic model checking considers the UAV's repeated round-trip flight and arbitrary angle selection. When the UAV interrelates with the on-duty operator, the impact of the operator's characteristics is correctly considered after receiving the image from the UAV, the operator on duty defines whether the image is fit to monitoring and non-monitoring regions. Moreover, the UAV's unsafe area is evaded, and the initial node's repetitive flight in the UAV's flight strategy is restricted. Finally, the target monitoring scene extends the MDP model to specify the formal model for UAV, and the PRISM model checking verifies multi-objective attributes for UAV. Formal verification results show that the operator's workload is reduced, as is the operator's efficiency and the UAV's improved.

Probabilistic model checking has been significantly utilized to investigate quantitative properties of systems in an exceedingly broad selection of applications, including robotic systems which are accustomed to accomplishing serious missions in hazardous environments for individuals. Such robots use the model to validate the security and reliability requirements of such robots, both before the mission and during runtime. To learn the unknown transition parameters from operational data, two novel estimators based on conservative Bayesian inference and an imprecise probability model with sets of priors are introduced. They showed how their approach works by using data from a real-world deployment of unmanned underwater vehicles in harsh environments [14].

PRISM enhancements and demonstrated a significant reduction in both time and memory consumption gained through the implementation of automated variable reordering are presented in Klein, et al. [15]. Its support for more fine-grained user influence on the order to implementation of quantile computations for reward bounded reachability properties in MDPs for the MTBDDs, Hybrid, and Sparse engines complements. In addition, support for computing quantile approximations in CTMCs for time-bounded properties has been implemented. Transformation to poorly deterministic automata for the syntactic obligation fragment of LTL guarantees the minimal size of the obtained deterministic automata and yields the basis for obtaining deterministic finite automata to be used in the computation of (external) accumulated rewards for co-safe LTL path formulas.

A comprehensive overview of the PRISM-games tool, including its modeling and property specification formalisms, as well as its underlying architecture, implementation is presented in Kwiatkowska, et al. [16]. They also discussed some key features, which are multi-objective and compositional approaches to verification, as well as strategy synthesis. In addition, the tool's scalability and efficiency, an overview of some case studies, and several extensions. To begin with, it is in the process of supporting a broader range of temporal properties as specified in linear temporal logic (LTL). Second, symbolic model checking implementations will be added to supplement the current explicit-state version. Initially, this builds on the existing symbolic techniques in PRISM for other probabilistic models, such as binary decision diagrams (BDDs) and multi-terminal BDDs.

A formal analysis of an algorithm inspired by ant-aging behavior, in which a swarm of flying vehicles searches for a target in an unknown location is discussed in Gainer, et al. [17]. They demonstrate how to check reward-based properties using both exhaustive and statistical model checking, where the calculated values could be used to plan the deployment of a swarm of MAVs where contact with a user must be guaranteed. Battery life has a significant impact on the flight duration of MAVs. The a priori calculation of the swarm's total expected flight time, or total expected distance traveled, would ensure that sufficient resources are made available to confirm that it achieves its objectives.

Uses of heuristics-based incremental probabilistic model checking at runtime are discussed in this research [18].The main work of the paper is to examine the principles of existing runtime probabilistic model checking and summarize the limitations of some verification methods, and then to develop the concept of incremental verification to the process of probabilistic model checking. Second, during the incremental probabilistic model checking process, they develop a heuristic method. It focuses on the DTMC model and reachability, which includes the Crowds (Crowds Protocol) and BRP (Bounded Retransmission Protocol) models. PCTL can be used to translate the properties. Due to the heuristic-based approach, the system verification time of standard runtime probabilistic model checking is reduced by more than 40%. When the system model changes at runtime, this significantly improves the performance of the runtime probabilistic model checking. Finally, in PRISM, the authors test the efficacy of the proposed method using two types of benchmark case studies. The current study is primarily concerned with the DTMC model.

3. WORKING OF HFIE ALGORITHM

The purpose of HFIE Algorithm [4] is to select the RGB image and in the image, each pixel value is composed of from [0..255] then it is converted into HSV. This method is primarily characterized by two main parameters the image's average intensity value which is M and the contrast intensification parameter is K. Set the control parameter K whose value is fixed K=128 because it provides the better contrast enhancement value and M to their initial values. Calculate the histogram from V component. Divide the pixel value range into two classes a1 [0, M-1] and a2 [M, 255]. Then calculate the fuzzy membership values Cu1 is from class a1, and Cu2 from class a2. Further improved intensity values Xe for the Cu1 and Cu2 classes are determined. To obtain an improved Ve component, to improve the pixel values V component using Xe. To obtain the enhanced HSVe image, combine the (H) and (S) to HSV image Ve components. Finally, an enhanced RGBe image is obtained when HSVe is completely changed into an RGB model. Table 1 describes all the variables used in labeled transition diagram of HFIE Algorithm.

Table 1. List variables.

Names of states	Descriptions
H	Hue is the angle of color
S	Saturation
V	Value
M	Value of intensity
K	Intensification parameter
X	Value of current intensity
Xe	Value of improved intensity
H(x)	Histogram
a1 class	Class 1
a2 class	Class 2
Cu1	Membership function for a1 class
Cu2	Membership function for a2 class

4. MODEL CONSTRUCTION OF HFIE ALGORITHM AND ANALYSIS VIA PRISM

4.1. Overview of PRISM model Checker

The PRISM model is a Probabilistic Model for formal modeling and analysis of systems with random or probabilistic behavior [11]. The PRISM model is a Probabilistic Symbolic Model developed by the University of Oxford. The PRISM website it is open source and ability to operate on a variety of operating systems it provide multiple case studies. PRISM tool supports a variety of probabilistic models, such as (DTMCs), (CTMCs), (MDPs) and (PTAs). In the PRISM modules and variables are the fundamental components of the PRISM model. A model's modules communicate with one another. A module contains many local variables, the values of which define the module's state. A model's global state is determined by the local states of all its modules [11]. The system models are constructed in a high-level language that uses guarded command generation and is based on the reactive modules formalism. The properties of these models written in specification language are based on temporal logic and can execute properties via PCTL, CSL. The cost and reward concepts are also supported by property language. Both logic and actual values are related to certain model states or transitions. The system specification is divided into two parts: model and property. The PRISM displays the results in log window and graph form. In PRISM, a data structure known as a multi-terminal binary decision diagram (MTBDD) is employed to represent vectors and metrics for efficient storage. storage MTBDD-based model checker is partially integrated with PRISM and it natively supports the probability value. In each state, the number of non-deterministic options is finite and bounded. Parallel composition determines the maximum number of non-deterministic choices for all states [1, 9].

4.2. HFIE Algorithm Model Construction

The HFIE Algorithm is used to improve low-contrast and low-brightness color pictures. This method is computationally efficient and effective. The DTMC model of HFIE Algorithm is constructed in PRISM. The model is consisting of global variables, formulas for RGB to HSV conversion, formulas for HSV to RGB conversion, formulas for a1, a2 class, cu1 and cu2. The DTMC model is consisting of three modules which are RGB-HSV, HFIE Algorithm, and HSVe-RGB. In this method, RGB is used with each color value consisting of [0..255] =2^8 colored image and converted into HSV, where H stands for hue, it is the angle of color it produces with various colors at different angles stands for saturation. its value from [0..100] which shows at 0 value dark and 100 value brighter and V is the value. Only the V component can stretch under the control parameters M&K, where M stands for average intensity and K is intensification parameter and calculates the Histogram from HSV. Here M is divided into two classes a1 = [0-M] and a2 = [M-255] and calculate Cu1 and Cu2 from the classes a1 and a2 respectively. In this way the HSV-enhanced is achieved then it is changed into RGB then finally, RGB-enhanced is received. The initial stage in HFIE Algorithm is to transform an RGB picture into an HSV image [3, 4]. However HFIE Algorithm analysis is done by applying fourth properties. Table 2 shows the statistics values of HFIE Algorithm.

Table 2. Statistics values of HFIE Algorithm.

Initial state	No of transitions	No of states	Time(s)	Itre.s
1	92928	18432	1.437	28

Following four properties are used for the analysis of the DTMC model of HFIE Algorithm:

R{"RGB_HSV"}=? [ C<=2 ]
R{"convert_into_HSV"}=? [ C<=T ]
P=? [ !Enh_RGB=9 U s =Z]
R{"SNR"}=? [ C<=Z ]

5. RESULT

The labeled transition diagram of the HFIE Algorithm shown in (Figure 1) which is created by following all the steps of HFIE Algorithm. It is consisting of ten states which are labeled from s=0 to s=9. In Figure 1, P shows the probability of transition from one state to next state. For example, there is fifty percent probability that RGB image is moved from s=0 to s=1.

5.1. R {"RGB_HSV"}=? [C<=2]

The first property is based on the reward which states the expected RGB_HSV model conversion concerning the probability of the number of pixel input. The intensity value of M is varied from 100 to 128.The x-axis in Figure 2 shows the number of pixels and the y-axis represents the expected probability of RGB to HSV conversion. It also depicts that probability increases with the increase in the number of pixels.

5.2. R{"convert_into_HSV"}=? [ C<=T ]

The 2nd reward property shows the expected time when the original RGB image changes into HSV. The image with three different numbers of pixels is 6000,2000and 4000 taken. The y-axis in Figure 3 shows the expected time in milli seconds and the x-axis shows the average intensity value. It also reveals that the RGB to HSV conversion time is directly propositional to the intensity value.

Figure 1. Label transition diagram

Figure 2. Expected RGB_HSV conversion model.

5.3. P=? [ !Enh_RGB=10 U s=Z ]

The 3rd property calculates the probability of reaching the Enhanced RGB at state 9 which is shown in Figure 4. It also shows the effect of the number of pixels on the probability of achieving an enhanced RGB image. The y-axis shows the probability, and the x-axis shows the average intensity value. The figure reveals the high probability of achieving an enhanced image with more pixels.

Figure 3. RGB image into HSV conversion expected time.

Figure 4. Probability of achieving enhanced image.

5.4. R{"SNR"}=? [ C<=Z ]

The fourth property is used to calculate the SNR when applied to images with a different number of pixels and different average intensity values. The y-axis in Figure 5 shows the expected SNR value and the x-axis shows the number of pixels. The SNR is directly proportional to the number of pixels and intensity value.

Figure 5. Calculate SNR.

6. CONCLUSION

The probabilistic Modeling checking has been applied successfully in various research areas. However, to the best of knowledge, for the first-time probabilistic analysis of the HFIE Algorithm has been performed in this research. For DTMC model development, initially labeled transition diagram is built, then the model is developed and finally it is analyzed by running the properties. In this paper we present model checking time and model building and also analysis the model storage and in this paper we select the image size 2^8 colored image and calculate the HFIE Algorithm which give the best result via in PRISM tool. We apply the for property in the HFIE Algorithm and also measure the Signal to the Noise ratio of the different image at different size with respect to time. One of the future directions is to apply more properties to the developed DTMC model.

Funding: This study received no specific financial support.

Competing Interests: The authors declare that they have no competing interests.

Authors’ Contributions: All authors contributed equally to the conception and design of the study.

REFERENCES

[1] S. Bhatti, M. Memon, and S. Memon, "Evaluating FTTT protocol via PRISM, PRISM-symm and GRIP," International Journal of Computer Theory and Engineering, vol. 9, pp. 162-166, 2017. Available at: https://doi.org/10.7763/ijcte.2017.v9.1131.

[2] Y. Hanna, R. Hridesh, and Z. Wensheng, "Slede: A domain-specific verification framework for sensor network security protocol implementations," in Proceedings of the First ACM Conference on Wireless Network Security, 2008, pp. 109-118.

[3] G. Raju and M. S. Nair, "A fast and efficient color image enhancement method based on fuzzy-logic and histogram," AEU-International Journal of Electronics and Communications, vol. 68, pp. 237-243, 2014. Available at: https://doi.org/10.1016/j.aeue.2013.08.015.

[4] T. Kaur and R. K. Sidhu, "Performance evaluation of fuzzy and histogram based color image enhancement," Procedia Computer Science, vol. 58, pp. 470-477, 2015. Available at: https://doi.org/10.1016/j.procs.2015.08.009.

[5] T. Kaur and R. K. Sidhu, "Optimized adaptive fuzzy based image enhancement techniques," International Journal of Signal Processing, Image Processing and Pattern Recognition, vol. 9, pp. 11-20, 2016. Available at: https://doi.org/10.14257/ijsip.2016.9.1.02.

[6] H. G. Daway, E. G. Daway, and H. H. Kareem, "Colour image enhancement by fuzzy logic based on sigmoid membership function," International Journal of Intelligent Engineering and Systems, vol. 13, pp. 238-246, 2020. Available at: https://doi.org/10.22266/ijies2020.1031.21.

[7] J. Lee, S. R. Pant, and H.-S. Lee, "An adaptive histogram equalization based local technique for contrast preserving image enhancement," International Journal of Fuzzy Logic and Intelligent Systems, vol. 15, pp. 35-44, 2015.

[8] O. Deperlioglu, U. Kose, and G. E. Guraksin, "Underwater image enhancement with Hsv and histogram equalization," in Proceedings of the 7TH International Conference on Advanced Technologies, 2018, pp. 461-4, 2018.

[9] M. Kwiatkowska, G. Norman, and D. Parker, "Analysis of a gossip protocol in PRISM," ACM SIGMETRICS Performance Evaluation Review, vol. 36, pp. 17-22, 2008. Available at: https://doi.org/10.1145/1481506.1481511.

[10] S. Konur, C. Dixon, and M. Fisher, "Analysing robot swarm behaviour via probabilistic model checking," Robotics and Autonomous Systems, vol. 60, pp. 199-213, 2012. Available at: https://doi.org/10.1016/j.robot.2011.10.005.

[11] K. He, Y. Hongli, F. Yachao, L. Yuan, and Q. Zongyan, "Performance analysis of data gathering protocol using PRISM," presented at the 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, IEEE, 2012.

[12] S. Muhammad, N. Mohammad, A. Bashar, and M. A. Khan, "Designing human assisted wireless sensor and robot networks using probabilistic model checking," Journal of Intelligent & Robotic Systems, vol. 94, pp. 687-709, 2019. Available at: https://doi.org/10.1007/s10846-018-0901-x.

[13] X. Wang, X. Shao, and C. OuYang, "A method on path optimization modeling of UAV based on probabilistic model checking," Journal of Physics: Conference Series. IOP Publishing, vol. 1176, p. 022053, 2019.

[14] X. Zhao, V. Robu, D. Flynn, F. Dinmohammadi, M. Fisher, and M. Webster, "Probabilistic model checking of robots deployed in extreme environments," in Proceedings of the AAAI Conference on Artificial Intelligence, 2019, pp. 8066-8074.

[15] J. Klein, C. Baier, P. Chrszon, M. Daum, C. Dubslaff, S. Klüppelholz, and D. Müller, "Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata," International Journal on Software Tools for Technology Transfer, vol. 20, pp. 179-194, 2018. Available at: https://doi.org/10.1007/s10009-017-0456-3.

[16] M. Kwiatkowska, D. Parker, and C. Wiltsche, "PRISM-games: Verification and strategy synthesis for stochastic multi-player games with multiple objectives," International Journal on Software Tools for Technology Transfer, vol. 20, pp. 195-210, 2018. Available at: https://doi.org/10.1007/s10009-017-0476-z.

[17] P. Gainer, C. Dixon, and U. Hustadt, "Probabilistic model checking of ant-based positionless swarming," presented at the Annual Conference Towards Autonomous Robotic Systems. Springer, Cham, 2016.

[18] Y. Liu and C. He, "A heuristics-based incremental probabilistic model checking at runtime," presented at the 2020 IEEE 11th International Conference on Software Engineering and Service Science (ICSESS). IEEE, 2020.

[19] V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker, "Automated verification techniques for probabilistic systems. In International school on formal methods for the design of computer, communication and software systems," ed Berlin, Heidelberg: Springer, 2011, pp. 53-113.

Views and opinions expressed in this article are the views and opinions of the author(s), Review of Information Engineering and Applications shall not be responsible or answerable for any loss, damage or liability etc. caused in relation to/arising out of the use of the content.