20.500.12556/DKUM-72041 Tvorjenje avtomatov linearnih končnih prič za formule ACTLW z orodjem EST Generating linear finite witness automata for ACTLW formulae with EST Magistrsko delo obravnava tvorjenje avtomatov linearnih končnih prič veljavnosti formul akcijske logike dreves izvajanj z operatorjem unless (ACTLW -- Action-based Computation Tree Logic with Unless operator) v modelih realnih sistemov, imenovanih označeni sistemi prehajanja stanj. Namen dela je tvorjenje avtomatov prič, ki kažejo, kako so v takem modelu prisotne lastnosti, opisane z veljavno formulo ACTLW. V prvem delu naloge so predstavljeni ključni elementi za tvorjenje avtomatov prič. Vpeljana sta pojma karakteristična funkcija in binarni odločitveni graf. Definirani so označeni sistemi prehajanja stanj, končni avtomati ter logika ACTLW. V drugem delu je na podlagi definicij razvit postopek in opisana implementacija tvorjenja avtomatov linearnih končnih prič z orodjem EST. Tvorjenje avtomatov je prikazano na primeru modela komunikacijskega protokola z omejenim številom ponovnih oddaj in biološkega sistema uravnavanja laktoznega operona. This master's thesis deals with the generation of linear finite witness automata witnessing the validity of ACTLW (Action-based Computation Tree Logic with Unless operator) formulae in models of real systems called labelled transition systems. The purpose of this thesis is to generate witness automata showing how in such a model, properties described by a valid ACTLW formula are present. In the first part of the thesis, key notions for the generation of witness automata are defined. Characteristic functions and binary decision diagrams are introduced, as well as labelled transition systems, finite automata and the ACTLW logic. In the second part, a procedure for generating witness automata is described, along with its implementation with the EST toolbox. The generation of automata is demonstrated on a model of the bounded retransmission protocol and on a model of the lactose operon regulatory system. formalne metode preverjanje modelov temporalna logika avtomati prič simbolične metode formal methods model checking temporal logic witness automata symbolic methods true true false R. Vogrin Slovenski jezik Angleški jezik Magistrsko delo/naloga 2018-09-07 13:28:04 2018-10-09 07:34:33 2022-08-01 21:53:56 2019-07-11 19:04:00 2018 0 [Maribor 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 004.8:621.395(043.2) 21776406 URN:SI:UM:DK:0WRUZOVQ MAG_Vogrin_Rok_2018.pdf MAG_Vogrin_Rok_2018.pdf 1 376D00DBEEE8CB1376DE075ED1ED5D06 1ab6eb3cbda5a9d92d1d8fdcf9ab8417fa59e30bdd8012649df949d364b80a99 483f2493-7c10-11eb-bb7a-00155d0001ca 20.500.12556/dkum/1c63a1be-c512-4325-a21e-022e7ed9e5b6 https://dk.um.si/Dokument.php?lang=slv&id=129013 Fakulteta za elektrotehniko, računalništvo in informatiko 0 0 0