Pemodelan Dan Verifikasi Formal Perubahan Suhu Menggunakan Interval Markov Chain Dan Probabilistic Computation Tree Logic

Salim, Abdullah Harits (2026) Pemodelan Dan Verifikasi Formal Perubahan Suhu Menggunakan Interval Markov Chain Dan Probabilistic Computation Tree Logic. Other thesis, Insitut Teknologi Sepuluh Nopember.

Text 5002211083-Undergraduate_Thesis.pdf - Accepted Version Restricted to Repository staff only Download (1MB) | Request a copy

Abstract

Perubahan suhu udara merupakan salah satu indikator penting dalam kajian perubahan iklim yang bersifat stokastik dan mengandung ketidakpastian tinggi. Oleh karena itu, diperlukan pendekatan pemodelan yang mampu merepresentasikan dinamika perubahan suhu secara probabilistik sekaligus mempertimbangkan ketidakpastian pada data. Penelitian ini bertujuan untuk memodelkan perubahan suhu udara per jam menggunakan Interval Markov Chain (IMC) serta melakukan verifikasi formal terhadap model yang dibangun menggunakan Probabilistic Computation Tree Logic (PCTL). Data suhu yang digunakan merupakan data historis per jam dari tiga lokasi di wilayah Surabaya selama periode 1 Januari 2010 hingga 31 Desember 2024. Tahapan penelitian meliputi pengelompokan data suhu ke dalam beberapa interval state, pembentukan model Discrete-Time Markov Chain (DTMC) pada masing-masing lokasi, serta penggabungan model tersebut menjadi IMC dengan batas probabilitas minimum dan maksimum. Selanjutnya, model IMC diverifikasi secara formal menggunakan perangkat lunak PRISM dengan sejumlah spesifikasi PCTL yang merepresentasikan properti probabilistik perubahan suhu. Hasil penelitian menunjukkan bahwa model IMC mampu merepresentasikan dinamika perubahan suhu secara lebih fleksibel dibandingkan DTMC tunggal, serta verifikasi formal dapat memastikan terpenuhinya properti-properti probabilistik yang diharapkan. Dengan demikian, pendekatan IMC dan PCTL dapat menjadi alternatif yang andal dalam analisis perubahan suhu berbasis data historis yang mengandung ketidakpastian.
====================================================================================================================================
Temperature fluctuation is a crucial indicator in climate change studies and exhibits stochastic behavior with significant uncertainty. Therefore, a modeling approach that can capture probabilistic dynamics while accommodating uncertainty is required. This study aims to model hourly temperature variations using Interval Markov Chains (IMC) and to formally verify the constructed model using Probabilistic Computation Tree Logic (PCTL). The dataset consists of hourly historical temperature data collected from three locations in the Surabaya region over the period from January 1, 2010 to December 31, 2024. The research methodology includes partitioning temperature data into interval-based states, constructing Discrete-Time Markov Chain (DTMC) models for each location, and combining them into an IMC by determining lower and upper bounds of transition probabilities. Formal verification is then performed using the PRISM model checker by evaluating several PCTL specifications that represent probabilistic properties of temperature changes. The results demonstrate that the IMC model provides a more flexible representation of temperature dynamics compared to a single DTMC, and that formal verification ensures the satisfaction of the specified probabilistic properties. Hence, the proposed IMC and PCTL-based approach offers a reliable framework for analyzing temperature variations under uncertainty.

Item Type:	Thesis (Other)
Uncontrolled Keywords:	Pemodelan, Perubahan Suhu, Rantai Markov, PRISM, Verifikasi Formal, Formal Verification, Interval Markov Chain, Modeling, PRISM, Temperature Fluctuation
Subjects:	Q Science > QA Mathematics > QA274.7 Markov processes--Mathematical models.
Divisions:	Faculty of Science and Data Analytics (SCIENTICS) > Mathematics > 44201-(S1) Undergraduate Thesis
Depositing User:	Abdullah Harits Salim
Date Deposited:	03 Feb 2026 01:30
Last Modified:	03 Feb 2026 01:30
URI:	http://repository.its.ac.id/id/eprint/131789

Actions (login required)

View Item