Business Process Analysis with Model Checking

U ovom radu opisan je način na koji su se prikupili podaci, kako je napravljen sentiment nad njima te u konačnici model, tj. automat koji analizira i opisuje rast i pad cijene Bitcoin-a. Koriste se dvije vrste podataka, objave s društvene mreže Twitter nad kojima se vrši analiza sentimenta, te cijene Bitcoin-a. Nakon što se analiziraju sentimenti, oni se zajedno s cijenama prikazuju na dva odvojena grafa. Promatranjem međuovisnosti između cijene te pozitivnog i negativnog sentimenta dolazi se do formula linearne vremenske logike koje opisuju u jednom slučaju rast cijene te njenu promjenu u stanje u kojem pada, te u drugom slučaju pad cijene te nakon toga njezin rast. Obje formule se mogu prikazati pomoću nedeterminističkog Büchi automata. Spajanjem dva nedeterministička automata dobiva se deterministički Büchi automat koji u cijelosti opisuje rast i pad cijene u međuovisnosti s pozitivnim i negativnim sentimentom. Rad je koncipiran u nekoliko cjelina, pri čemu se u uvodnom dijelu opisuju teorijska pozadina koja se nalazi iza zadanog zadatka. U središnjem dijelu se opisuje prikupljanje i obrada podataka, te u konačnici se opisuje način dobivanja automata kojim se dalje može analizirati proces.This paper describes the way data was collected, how sentiment was made and ultimately the model i.e., the automaton that analyses and describes the rise and fall of the Bitcoin price. Two types of data are used, post from social network Twitter on which sentiment is analysed, and price of the Bitcoin. After the sentiments are analysed, they are displayed along with the prices on two separate graphs. Observing the interdependence between price and positive and negative sentiment, we come to the formulas of linear temporal logic that describe in one case the rise of price and its changes in the state in which it falls, and in other case the fall in price and then its growth. Both formulas can be represented by nondeterministic Büchi automaton. Merging two nondeterministic automata a deterministic Büchi automata is obtained, which fully describe the rise and fall of Bitcoin price in interdependence with positive and negative sentiment. The paper is conceived in several parts, with the introductory part describing the theoretical background of given task. The central part describes the collection and processing of data, and last part describes the method of obtaining automata that can further analyse the process