Parameter Synthesis for Systems with Real Time /

Časové automaty se staly standardem pro modelování systémů s časem. Parametrické časové automaty rozšiřují časové automaty o možnost použití parametrů ve strážích a invariantech automatu. Zatímco problém dosažitelnosti hledá valuace parametrů, pro které je daná lokace automatu dosažitelná, problém s...

Celý popis

Uloženo v:
Podrobná bibliografie
Hlavní autor: Bezděk, Peter (Autor práce)
Další autoři: Černá, Ivana, 1963- (Vedoucí práce)
Typ dokumentu: VŠ práce nebo rukopis
Jazyk:Angličtina
Vydáno: 2018
Témata:
počítačové modelování
lineární programování
parametrické modelování
computer modeling
linear programming
parametric modeling
disertace
dissertations
On-line přístup:http://is.muni.cz/th/i4kyb/
Obálka
LEADER 05402ctm a22008297i 4500
001 MUB01006412809
003 CZ BrMU
005 20240517144452.0
008 180310s2018 xr ||||| |||||||||||eng d
STA |a POSLANO DO SKCR  |b 2018-05-14 
035 |a (ISMU-VSKP)238702 
040 |a BOD114  |b cze  |d BOD018  |e rda 
072 7 |a 004.9  |x Speciální počítačové metody. Počítačová grafika  |2 Konspekt  |9 23 
080 |a 004.94  |2 MRF 
080 |a 519.852  |2 MRF 
080 |a 004.925.8  |2 MRF 
100 1 |a Bezděk, Peter  |% UČO 72532  |* [absolvent FI MU]  |4 dis 
242 1 0 |a Parameter Synthesis for Systems with Real Time  |y eng 
245 1 0 |a Parameter Synthesis for Systems with Real Time /  |c Peter Bezděk 
264 0 |c 2018 
300 |a 120 stran 
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: Ivana Černá 
502 |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2018 
520 2 |a Časové automaty se staly standardem pro modelování systémů s časem. Parametrické časové automaty rozšiřují časové automaty o možnost použití parametrů ve strážích a invariantech automatu. Zatímco problém dosažitelnosti hledá valuace parametrů, pro které je daná lokace automatu dosažitelná, problém syntézy parametrů hledá valuace parametrů, pro které je splněna obecnější specifikace parametrického časového automatu, například formule lineární temporální logiky (LTL). V této práci představíme nové výsledky rozhodnutelnosti pro problém dosažitelnosti, zavedeme novou lineární temporální logiku vyjadřující se o hodinách (CA-LTL), a taktéž vyřešíme problém syntézy ohraničených celočíselných parametrů pro LTL a CA-LTL vlastnosti a parametrické časové automaty. Pro parametry s reálnými hodnotami je problém dosažitelnosti nerozhodnutelný. Proto se v práci zaměříme na celočíselné parametry, zatímco čas zůstane spojitý. Dokážeme, že problém dosažitelnosti zůstává nerozhodnutelný pro parametrické  |% cze 
520 2 9 |a For modelling of behaviour with time aspects the timed extension of nondeterministic finite automata called timed automata became the standard. Parametric timed automata extend the timed automata with the possibility to use parameters in the clock constraints. While the reachability problem for parametric timed automata computes parameter valuations for which certain locations are reachable, the parameter synthesis problem computes parameter valuations for which a more general type of specification is satisfied, e.g. linear temporal logic (LTL) formula. In the thesis we provide new decidability results for the reachability problem, we introduce new clock-aware linear temporal logic (CA-LTL) as an extension of LTL, and we solve the parameter synthesis problem for CA-LTL properties and restricted parameters. In general, if the parameters are real-valued, the reachability problem for parametric timed automata is undecidable even for various restricted subclasses. We thus focus on the cas  |9 eng 
650 0 7 |a počítačové modelování  |7 ph124513  |2 czenas 
650 0 7 |a lineární programování  |7 ph122356  |2 czenas 
650 0 7 |a parametrické modelování  |7 ph156637  |2 czenas 
650 0 9 |a computer modeling  |2 eczenas 
650 0 9 |a linear programming  |2 eczenas 
650 0 9 |a parametric modeling  |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 Černá, Ivana,  |d 1963-  |7 mub2011658599  |% UČO 1419  |4 ths 
710 2 |a Masarykova univerzita.  |b Katedra teorie programování  |4 dgg 
856 4 1 |u http://is.muni.cz/th/i4kyb/ 
CAT |c 20180310  |l MUB01  |h 0420 
CAT |a POSPEL  |b 02  |c 20180314  |l MUB01  |h 0814 
CAT |a POSPEL  |b 02  |c 20180314  |l MUB01  |h 0814 
CAT |a HANAV  |b 02  |c 20180322  |l MUB01  |h 2124 
CAT |a VESELA  |b 02  |c 20180427  |l MUB01  |h 0930 
CAT |a POSPEL  |b 02  |c 20180503  |l MUB01  |h 0729 
CAT |c 20180514  |l MUB01  |h 1105 
CAT |a POSPEL  |b 02  |c 20180710  |l MUB01  |h 0635 
CAT |a POSPEL  |b 02  |c 20190213  |l MUB01  |h 0800 
CAT |a POSPEL  |b 02  |c 20190924  |l MUB01  |h 0745 
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 1027 
CAT |c 20210614  |l MUB01  |h 2014 
CAT |a BATCH  |b 00  |c 20210724  |l MUB01  |h 1300 
CAT |a POSPEL  |b 02  |c 20210912  |l MUB01  |h 2336 
CAT |a POSPEL  |b 02  |c 20211010  |l MUB01  |h 2218 
CAT |a HANAV  |b 02  |c 20211116  |l MUB01  |h 0031 
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 20230629  |l MUB01  |h 0037 
CAT |a POSPEL  |b 02  |c 20240405  |l MUB01  |h 2124 
CAT |a VESELAX  |b 02  |c 20240517  |l MUB01  |h 1444 
CAT |a VESELAX  |b 02  |c 20240517  |l MUB01  |h 1444 
LOW |a POSLANO DO SKCR  |b 2018-05-14 
994 - 1 |l MUB01  |l MUB01  |m VYSPR  |1 FI  |a Fakulta informatiky  |3 Diz. práce 2017  |5 42005D2688  |8 20180427  |f 72  |f Týdenní  |r 20180427 
AVA |a INF50  |b FI  |d Diz. práce 2017  |e available  |t K dispozici  |f 1  |g 0  |h N  |i 0 

Podobné jednotky