Pemodelan dan Verifikasi Formal Pergerakan Return Saham Menggunakan Rantai Markov Waktu Diskrit dan Probabilistic Computation Tree Logic

Rohim, Bintang Nur (2025) Pemodelan dan Verifikasi Formal Pergerakan Return Saham Menggunakan Rantai Markov Waktu Diskrit dan Probabilistic Computation Tree Logic. Other thesis, Institut Teknologi Sepuluh Nopember.

Text 5002211013-Undergraduate_Thesis.pdf Restricted to Repository staff only Download (5MB) | Request a copy

Abstract

Pasar saham Indonesia semakin diminati karena potensi imbal hasil (return) tinggi, tetapi fluktuasi harga menciptakan ketidakpastian dalam pengambilan keputusan investasi. Penelitian ini mengembangkan model rantai Markov waktu diskrit (RMWD) yang diverifikasi secara formal menggunakan probabilistic model checking berbasis probabilistic computation tree logic (PCTL) untuk menganalisis perilaku stokastik pergerakan return saham. Data yang digunakan berupa harga penutupan harian lima saham sektor perbankan Indonesia periode 2015-2025. Model dibentuk melalui proses diskretisasi return dan pembentukan matriks probabilitas transisi, kemudian diverifikasi dengan PRISM melalui lima properti temporal PCTL menggunakan operator next (X), eventually (F), globally (G), dan until (U). Hasil verifikasi menunjukkan bahwa pergerakan return saham mengikuti pola probabilistik yang dapat dimanfaatkan dalam strategi investasi. Pendekatan ini terbukti mampu merepresentasikan dinamika historis secara kuantitatif dan diharapkan dapat memberikan panduan informatif bagi investor untuk meminimalkan risiko dalam jangka pendek hingga menengah.
===================================================================================================================================
The Indonesian stock market has become increasingly attractive due to its high return potential; however, price fluctuation pose significant uncertainty in investment decision-making. This study develops a discrete-time Markov chain (DTMC) model, formally verified through probabilistic model checking based on probabilistic computation tree logic (PCTL), to analyze the stochastic behavior of stock return movements. The data consist of daily closing prices form five banking sector stocks in Indonesia over the period 2015-2025. The model is constructed by discretizing returns and forming a transition probability matrix, followed by formal verification in PRISM using five temporal PCTL properties involving the next (X), eventually (F), globally (G), and until (U) operators. The verification results indicate that stock return movements follow probabilistic patterns that can be leveraged for investment strategies. This approach effectively quantitatively captures historical dynamics and is expected to provide informative guidance for investors seeking to minimize risk in the short to medium term.

Item Type:	Thesis (Other)
Uncontrolled Keywords:	Return Saham, Rantai Markov Waktu Diskrit, Probabilistic Computation Tree Logic, Pemodelan dan Verifikasi Formal ============================================================ Stock Return, Discrete-Time Markov Chain, Probabilistic Computation Tree Logic, Formal Modeling and Verification
Subjects:	H Social Sciences > HG Finance H Social Sciences > HG Finance > HG4012 Mathematical models H Social Sciences > HG Finance > HG4529.5 Portfolio management Q Science Q Science > QA Mathematics Q Science > QA Mathematics > QA274.2 Stochastic analysis Q Science > QA Mathematics > QA274.7 Markov processes--Mathematical models. Q Science > QA Mathematics > QA276 Mathematical statistics. Time-series analysis. Failure time data analysis. Survival analysis (Biometry)
Divisions:	Faculty of Science and Data Analytics (SCIENTICS) > Mathematics > 44201-(S1) Undergraduate Thesis
Depositing User:	Bintang Nur Rohim
Date Deposited:	23 Jul 2025 00:43
Last Modified:	23 Jul 2025 00:43
URI:	http://repository.its.ac.id/id/eprint/120515

Actions (login required)

View Item