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

Fadlina, Agfa Syalsa (2024) Pemodelan dan Verifikasi Formal Pergerakan Harga Saham Menggunakan Rantai Markov Waktu Diskrit dan Probabilistic Computation Tree Logic. Other thesis, Institut Teknologi Sepuluh Nopember.

Text 5002201128-Undergraduate_Thesis.pdf - Accepted Version Restricted to Repository staff only until 1 October 2026. Download (7MB) | Request a copy

Abstract

Saham memiliki popularitas sebagai salah satu instrumen investasi dan sumber pemasukan sekunder. Akan tetapi, harga saham memiliki perubahan yang sangat cepat dan tidak teratur sehingga menyulitkan investor untuk memprediksi tren di masa mendatang. Oleh sebab itu, pemodelan saham akan membantu bagi para investor untuk memprediksi tren yang akan terjadi. Sedangkan kebenaran dari suatu model dapat menjadi indikator untuk mengetahui keakuratan prediksi oleh model. Pada Tugas Akhir ini, dilakukan pemodelan harga saham menggunakan rantai Markov waktu diskrit dengan banyak state 5, 10, dan 15 untuk selanjutnya diverifikasi. Spesifikasi yang digunakan dalam verifikasi adalah spesifikasi dengan logic PCTL menggunakan operator ”until” dan ”eventually”. Tugas Akhir ini memodelkan lima saham farmasi di Indonesia, yaitu DVLA.JK, INAF.JK, KAEF.JK, TSPC.JK, dan KLBF.JK. Diperoleh bahwa perbedaan banyak state berpengaruh pada penyajian informasi yang lebih detil mengenai kenaikan probabilitas. Hasil verifikasi menunjukkan bahwa state yang memiliki jarak dekat dengan state awal memiliki probabilitas pergerakan yang lebih tinggi daripada state yang berjarak jauh dari state awal.
===========================================================
Stocks are popular as one of the investment instruments and sources of secondary income. However, stock prices change very rapidly and irregularly, making it difficult for investors to predict future trends. Therefore, stock modeling will help investors to predict upcoming trends. The accuracy of a model can serve as an indicator of the model’s prediction accuracy. In this thesis, stock price modeling is carried out using discrete-time Markov chains with 5, 10, and 15 states, which are then verified. The specification used in the verification is a PCTL logic specification using the ”until” and ”eventually” operators. This thesis models five pharmaceutical stocks in Indonesia, namely DVLA.JK, INAF.JK, KAEF.JK, TSPC.JK, and KLBF.JK. It was found that the difference in the number of states affects the presentation of more detailed information regarding the increase in probability. Verification results show that states that are closer to the initial state have a higher probability of movement than states that are farther from the initial state.

Item Type:	Thesis (Other)
Uncontrolled Keywords:	Saham, Rantai Markov, Verifikasi Formal. Stocks, Markov Chains, Formal Verification
Subjects:	Q Science > QA Mathematics > QA274.7 Markov processes--Mathematical models. T Technology > T Technology (General)
Divisions:	Faculty of Mathematics, Computation, and Data Science > Mathematics > 44201-(S1) Undergraduate Thesis
Depositing User:	Agfa Syalsa Fadlina
Date Deposited:	06 Aug 2024 07:12
Last Modified:	06 Aug 2024 07:12
URI:	http://repository.its.ac.id/id/eprint/111775

Actions (login required)

View Item