Modal Transition Systems: Extensions and Analysis
Tato dizertační práce studuje specifikační formalizmus zvaný modální přechodové systémy (MTS). Zavádíme několik rozšíření MTS a rozebíráme jejich vzájemné vztahy a modelovací sílu. Zaprvé rozšiřujeme modality MTS, zadruhé uvažujeme rozšíření s prvky času a ceny a zatřetí zavádíme různé třídy MTS s n...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2014
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/139914/fi_d/ |
| LEADER | 05919ctm a22009857a 4500 | ||
|---|---|---|---|
| 001 | MUB01001009932 | ||
| 003 | CZ BrMU | ||
| 005 | 20240514135346.0 | ||
| 008 | 140920s2014 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2021-02-08 | ||
| 035 | |a (ISMU-VSKP)177839 | ||
| 040 | |a BOD114 |b cze |d BOD018 | ||
| 072 | 7 | |a 004.4/.6 |x Programování. Software |2 Konspekt |9 23 | |
| 080 | |a 004.03 |2 MRF | ||
| 080 | |a 004.9:794 |2 MRF | ||
| 080 | |a (0.034.2)004.4 |2 MRF | ||
| 100 | 1 | |a Křetínský, Jan, |d 1984- |7 mub2013777259 |% UČO 139914 |4 dis | |
| 242 | 1 | 0 | |a Modal Transition Systems: Extensions and Analysis |y eng |
| 245 | 1 | 0 | |a Modal Transition Systems: Extensions and Analysis |h [rukopis] / |c Jan Křetínský |
| 260 | |c 2014 | ||
| 300 | |a xiii, 227 s. | ||
| 500 | |a Vedoucí práce: Antonín Kučera | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2014 | ||
| 520 | 2 | |a Tato dizertační práce studuje specifikační formalizmus zvaný modální přechodové systémy (MTS). Zavádíme několik rozšíření MTS a rozebíráme jejich vzájemné vztahy a modelovací sílu. Zaprvé rozšiřujeme modality MTS, zadruhé uvažujeme rozšíření s prvky času a ceny a zatřetí zavádíme různé třídy MTS s nekonečně mnoha stavy. Rovněž tato rozšíření MTS srovnáváme jako formalizmy automatové s formalizmy logickými. Těžiště práce se nachází v oblasti algoritmické analýzy a verifikace uvedených systémů. Zajímá nás především kontrola zjemňování, ověřování modelu, obvyklé logické a strukturální operace používané v kontextu specifikačních teorií, automatická tvorba implementací splňujících danou logickou formuli či optimalitu vzhledem k danému cenovému schématu. Věnujeme se jak teroretickým otázkám, zejména složitosti zkoumaných problémů, tak i praktickým aspektům, zejména heuristikám a softwarovému nástroji pro podporu práce s MTS. |% cze | |
| 520 | 2 | 9 | |a In this thesis, we deal with the specification formalism of modal transition systems (MTS). We introduce several extensions thereof and discuss their relationships and modelling capabilities. Apart from extending the modalities of MTS, we consider timed and priced extensions as well as systems with infinite state space. We also compare the behavioural framework of MTS and its extensions to logical frameworks. The main focus of the thesis lies on algorithms for verification and analysis of the introduced MTS extensions. We cover refinement checking, model checking, standard logical and structural operations as used in specification theories as well as synthesis of implementations satisfying given logical formulae or optimality with respect to a given price scheme. Beside theoretical aspects such as establishing complexity of investigated problems, we also deal with practical issues such as heuristics and tool support. |9 eng |
| 650 | 0 | 7 | |a algoritmy (programování) |7 ph131788 |2 czenas |
| 650 | 0 | 7 | |a počítačové systémy |7 ph115866 |2 czenas |
| 650 | 0 | 7 | |a software |7 ph125823 |2 czenas |
| 650 | 0 | 9 | |a computer algorithms |2 eczenas |
| 650 | 0 | 9 | |a computer systems |2 eczenas |
| 650 | 0 | 9 | |a software |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 Kučera, Antonín, |d 1971- |7 mub2012683133 |% UČO 2508 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Katedra teorie programování |4 dgg | |
| 856 | 4 | 1 | |u http://is.muni.cz/th/139914/fi_d/ |
| CAT | |c 20140920 |l MUB01 |h 0422 | ||
| CAT | |a HANAV |b 02 |c 20140922 |l MUB01 |h 2208 | ||
| CAT | |a HANAV |b 02 |c 20140922 |l MUB01 |h 2211 | ||
| CAT | |a VESELA |b 02 |c 20150108 |l MUB01 |h 1055 | ||
| CAT | |a POSPEL |b 02 |c 20150625 |l MUB01 |h 0751 | ||
| CAT | |c 20150703 |l MUB01 |h 1246 | ||
| CAT | |c 20150901 |l MUB01 |h 1452 | ||
| CAT | |c 20150921 |l MUB01 |h 1413 | ||
| CAT | |a VACOVAX |b 02 |c 20151012 |l MUB01 |h 1025 | ||
| CAT | |a POSPEL |b 02 |c 20151029 |l MUB01 |h 0733 | ||
| CAT | |a BATCH |b 00 |c 20151226 |l MUB01 |h 0516 | ||
| CAT | |a POSPEL |b 02 |c 20160914 |l MUB01 |h 1427 | ||
| CAT | |a POSPEL |b 02 |c 20160920 |l MUB01 |h 0817 | ||
| CAT | |a POSPEL |b 02 |c 20160927 |l MUB01 |h 0741 | ||
| CAT | |a POSPEL |b 02 |c 20170228 |l MUB01 |h 1036 | ||
| CAT | |a POSPEL |b 02 |c 20170302 |l MUB01 |h 0827 | ||
| CAT | |a POSPEL |b 02 |c 20180314 |l MUB01 |h 0814 | ||
| CAT | |a POSPEL |b 02 |c 20180503 |l MUB01 |h 0729 | ||
| CAT | |a HANAV |b 02 |c 20180503 |l MUB01 |h 1853 | ||
| 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 | |c 20210208 |l MUB01 |h 1140 | ||
| 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 1011 | ||
| CAT | |c 20210614 |l MUB01 |h 1958 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1232 | ||
| CAT | |a POSPEL |b 02 |c 20210912 |l MUB01 |h 2336 | ||
| CAT | |a POSPEL |b 02 |c 20211010 |l MUB01 |h 2218 | ||
| CAT | |a REPISOVA |b 02 |c 20211111 |l MUB01 |h 1525 | ||
| CAT | |c 20220114 |l MUB01 |h 1647 | ||
| 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 2123 | ||
| CAT | |a VESELAX |b 02 |c 20240514 |l MUB01 |h 1353 | ||
| CAT | |a VESELAX |b 02 |c 20240514 |l MUB01 |h 1353 | ||
| CAT | |a POSPEL |b 02 |c 20250808 |l MUB01 |h 1401 | ||
| CAT | |a POSPEL |b 02 |c 20251007 |l MUB01 |h 2008 | ||
| LOW | |a POSLANO DO SKCR |b 2021-02-08 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |2 SKLAD |b sklad |3 Diz. práce 2014 |5 42005D2644 |8 20150108 |f 72 |f Týdenní |r 20150108 |
| AVA | |a INF50 |b FI |c sklad |d Diz. práce 2014 |e available |t K dispozici |f 1 |g 0 |h N |i 0 |j SKLAD | ||