Automata for Formal Methods: Little Steps Towards Perfection /

Jako vhodná reprezentace jazyků nekonečných slov jsou ω-automaty hojně využívány ve formálních metodách. Obzvlášťe algoritmy, které analyzují systémy vykazující nekonečné chování, často spoléhají na ω-automaty. Díky efektivním algoritmům pro průnik, sjednocení a test prázdnosti reprezentovaných jazy...

Celý popis

Uloženo v:
Podrobná bibliografie
Hlavní autor: Blahoudek, František (Autor práce)
Další autoři: Strejček, Jan, 1977- (Vedoucí práce)
Typ dokumentu: VŠ práce nebo rukopis
Jazyk:Angličtina
Vydáno: 2018
Témata:
počítačové systémy
formální logika
algoritmy (programování)
computer systems
formal logic
computer algorithms
disertace
dissertations
On-line přístup:http://is.muni.cz/th/gwriw/
Obálka
LEADER 05465ctm a22008417i 4500
001 MUB01006421774
003 CZ BrMU
005 20240520153316.0
008 180705s2018 xr ||||| |||||||||||eng d
STA |a POSLANO DO SKCR  |b 2020-04-14 
035 |a (ISMU-VSKP)232535 
040 |a BOD114  |b cze  |d BOD018  |e rda 
072 7 |a 004.4/.6  |x Programování. Software  |2 Konspekt  |9 23 
080 |a 164  |2 MRF 
080 |a 004.421  |2 MRF 
080 |a 004.03  |2 MRF 
100 1 |a Blahoudek, František  |% UČO 208029  |* [absolvent FI MU]  |4 dis 
242 1 0 |a Automata for Formal Methods: Little Steps Towards Perfection  |y eng 
245 1 0 |a Automata for Formal Methods: Little Steps Towards Perfection /  |c František Blahoudek 
264 0 |c 2018 
300 |a 145 stran :  |b ilustrace 
336 |a text  |b txt  |2 rdacontent 
337 |a bez média  |b n  |2 rdamedia 
338 |a svazek  |b nc  |2 rdacarrier 
500 |a Vedoucí práce: Jan Strejček 
502 |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2018 
520 2 |a Jako vhodná reprezentace jazyků nekonečných slov jsou ω-automaty hojně využívány ve formálních metodách. Obzvlášťe algoritmy, které analyzují systémy vykazující nekonečné chování, často spoléhají na ω-automaty. Díky efektivním algoritmům pro průnik, sjednocení a test prázdnosti reprezentovaných jazyků pro různé třídy ω-automatů jsou tyto automaty vhodné pro metody ověřování modelu se specifikací zadanou pomocí automatu či formule (nejen) logiky LTL. Determinizace a komplementace ω-automatů jsou problémy známé svou komplikovaností. Proto je nasazení metod, které pro své správné fungování vyžadují deterministické automaty (například syntéza reaktivních systémů či ověřování modelu pro systémy s pravděpodobností) nebo komplementují ω-automaty (například analýza terminace v nástroji Ultimate Büchi Automizer), často považované za problematické. Předkládaná dizertace přistupuje k ω-automatům a jejich využití ve formálních metodách z různých směrů a prezentuje hned několik výsledků, které př  |% cze 
520 2 9 |a As ω-automata are a convenient representation of languages of infinite words, they are widespread in the area of formal methods; many algorithms that analyze systems with infinite behaviours rely on ω-automata. The efficient algorithms for the intersection, union, and emptiness checking for various classes of ω-automata made them appealing for model checking of properties expressed as ω-regular languages or as formulae in (not only) Linear Temporal Logic (LTL). On the contrary, determinization and complementation of ω-automata are notoriously difficult problems. This fact complicates usage of the automata-based methods that need deterministic automata (like model checking of probabilistic systems or synthesis of reactive systems) or inherently employ language difference or complementation of ω-automata (like termination analysis in the tool Ultimate Automizer). This dissertation approaches ω-automata and formal methods from various directions and presents several contributions toward  |9 eng 
650 0 7 |a počítačové systémy  |7 ph115866  |2 czenas 
650 0 7 |a formální logika  |7 ph120290  |2 czenas 
650 0 7 |a algoritmy (programování)  |7 ph131788  |2 czenas 
650 0 9 |a computer systems  |2 eczenas 
650 0 9 |a formal logic  |2 eczenas 
650 0 9 |a computer algorithms  |2 eczenas 
655 7 |a disertace  |7 fd132024  |2 czenas 
655 9 |a dissertations  |2 eczenas 
658 |a Informatika (čtyřleté)  |b Informatika  |c FI D-IN4 IN (IN)  |2 CZ-BrMU 
700 1 |a Strejček, Jan,  |d 1977-  |7 ola2011623112  |% UČO 3366  |4 ths 
710 2 |a Masarykova univerzita.  |b Katedra teorie programování  |4 dgg 
856 4 1 |u http://is.muni.cz/th/gwriw/ 
CAT |c 20180705  |l MUB01  |h 0421 
CAT |a POSPEL  |b 02  |c 20180710  |l MUB01  |h 0634 
CAT |a POSPEL  |b 02  |c 20180710  |l MUB01  |h 0635 
CAT |a HANAV  |b 02  |c 20180809  |l MUB01  |h 1822 
CAT |a POSPEL  |b 02  |c 20190213  |l MUB01  |h 0801 
CAT |a POSPEL  |b 02  |c 20190924  |l MUB01  |h 0745 
CAT |a VESELA  |b 02  |c 20200306  |l MUB01  |h 0955 
CAT |a VESELA  |b 02  |c 20200306  |l MUB01  |h 0955 
CAT |c 20200414  |l MUB01  |h 0942 
CAT |a POSPEL  |b 02  |c 20200510  |l MUB01  |h 2306 
CAT |a POSPEL  |b 02  |c 20201212  |l MUB01  |h 2150 
CAT |a POSPEL  |b 02  |c 20210122  |l MUB01  |h 0054 
CAT |a POSPEL  |b 02  |c 20210322  |l MUB01  |h 1142 
CAT |a POSPEL  |b 02  |c 20210327  |l MUB01  |h 0026 
CAT |c 20210614  |l MUB01  |h 1029 
CAT |c 20210614  |l MUB01  |h 2015 
CAT |a BATCH  |b 00  |c 20210724  |l MUB01  |h 1303 
CAT |a POSPEL  |b 02  |c 20210912  |l MUB01  |h 2336 
CAT |a POSPEL  |b 02  |c 20211010  |l MUB01  |h 2218 
CAT |a POSPEL  |b 02  |c 20220629  |l MUB01  |h 0104 
CAT |a POSPEL  |b 02  |c 20221019  |l MUB01  |h 2326 
CAT |a POSPEL  |b 02  |c 20221101  |l MUB01  |h 0840 
CAT |a POSPEL  |b 02  |c 20230324  |l MUB01  |h 0919 
CAT |a POSPEL  |b 02  |c 20230629  |l MUB01  |h 0037 
CAT |a VASICEKX  |b 02  |c 20230713  |l MUB01  |h 1324 
CAT |a POSPEL  |b 02  |c 20240405  |l MUB01  |h 2124 
CAT |a VESELAX  |b 02  |c 20240520  |l MUB01  |h 1529 
CAT |a VESELAX  |b 02  |c 20240520  |l MUB01  |h 1529 
CAT |a VESELAX  |b 02  |c 20240520  |l MUB01  |h 1533 
LOW |a POSLANO DO SKCR  |b 2020-04-14 
994 - 1 |l MUB01  |l MUB01  |m VYSPR  |1 FI  |a Fakulta informatiky  |3 Diz. práce 2018  |5 42005D2695  |8 20200306  |f 72  |f Týdenní  |r 20200305 
AVA |a INF50  |b FI  |d Diz. práce 2018  |e available  |t K dispozici  |f 1  |g 0  |h N  |i 0 

Podobné jednotky