Robot, Marcellius Fernando (2026) Pemodelan Dan Verifikasi Formal Perubahan Temperatur Di Kota Surabaya Menggunakan Rantai Markov Waktu Diskrit Dan Probabilistic Computation Tree Logic. Other thesis, Institut Teknologi Sepuluh Nopember.
![[thumbnail of 50022221091-Undergraduate_Thesis.pdf]](http://repository.its.ac.id/style/images/fileicons/text.png) |
Text
50022221091-Undergraduate_Thesis.pdf - Accepted Version Restricted to Repository staff only Download (9MB) | Request a copy |
Abstract
Temperatur udara berpengaruh besar terhadap keberlangsungan hidup manusia, terutama pada era pemanasan global. Sejumlah penelitian telah menunjukkan bahwa perubahan temperatur dapat berdampak negatif dalam aspek ekonomis maupun nonekonomis. Penelitian ini melakukan pemodelan perubahan temperatur di Kota Surabaya menggunakan rantai Markov waktu diskrit dengan struktur imbalan dan melakukan verifikasi formal terhadap perilaku perubahan temperatur Kota Surabaya. Pemodelan dilakukan dengan diskritisasi data per jam temperatur Kota Surabaya periode 2015 – 2024 ke dalam beberapa keadaan diskrit. Selanjutnya, struktur imbalan untuk model Markov perubahan temperatur ditentukan untuk menguantifikasi keadaan panas di Kota Surabaya. Verifikasi formal dilakukan menggunakan PRISM terhadap properti dari model rantai Markov waktu diskrit yang dinyatakan dalam PCTL menggunakan operator "bounded eventually" dan imbalan kumulatif terbatas. Hasil verifikasi menunjukkan bahwa pemodelan perubahan dengan rantai Markov waktu diskrit dapat menangkap beberapa fenomena iklim yang terjadi selama periode 2015 – 2024. Selain itu, verifikasi formal juga menunjukkan bahwa ada peningkatan potensi risiko akibat temperatur udara secara drastis pasca-pandemi COVID-19 di Kota Surabaya.
=====================================================================================================================================
Air temperature has a substantial influence on human survival, particularly in the era of global warming. Numerous studies have shown that temperature changes can have negative impacts on both economic and non-economic aspects. This study models temperature changes in Surabaya using a discrete-time Markov chain with a reward structure and conducts formal verification of the behavior of temperature changes in Surabaya. The modeling is performed by discretizing hourly air temperature data for Surabaya over the period 2015 – 2024 into several discrete states. Subsequently, a reward structure for the Markov model of temperature change is defined to quantify hot condition in Surabaya. Formal verification is carried out using PRISM on properties of the discrete-time Markov chain expressed in PCTL, employing the bounded eventually operator and bounded cumulative rewards operator. The verification results indicate that discrete-time Markov chain modeling is capable of capturing several climatic phenomena occurring during the period 2015 – 2024. Furthermore, the formal verification also shows a significant increase in potential risk associated with air temperature in Surabaya in the post–COVID-19 pandemic period.
| Item Type: | Thesis (Other) |
|---|---|
| Uncontrolled Keywords: | Perubahan Temperatur, Rantai Markov Waktu Diskrit dengan Struktur Imbalan, Verifikasi Formal, Temperature Changes, Discrete-Time Markov Chain with Rewards Structure, Formal Verification |
| 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: | Marcellius Fernando Robot |
| Date Deposited: | 27 Jan 2026 06:27 |
| Last Modified: | 27 Jan 2026 06:27 |
| URI: | http://repository.its.ac.id/id/eprint/130423 |
Actions (login required)
 |
View Item |