Translation of Linear Temporal Logic to Omega-Automata /
Překlad logiky lineárního času (Linear Temporal Logic - LTL) na různé typy ɷ-automatů je intenzivně studovaná oblast, která má mnoho aplikací. Metoda LTL ověřovaní modelu (LTL model checking) je rozšířená a plně automatizovaná technika, která se používá k ověření, zda daný systém splňuje požadovanou...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2017
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/143254/fi_d/ |
| LEADER | 05727ctm a22008897i 4500 | ||
|---|---|---|---|
| 001 | MUB01006386064 | ||
| 003 | CZ BrMU | ||
| 005 | 20240517133906.0 | ||
| 008 | 170301s2017 xr ||||| |||||||||||eng d | ||
| STA | |a POSLANO DO SKCR |b 2018-05-14 | ||
| 035 | |a (ISMU-VSKP)188851 | ||
| 040 | |a BOD114 |b cze |d BOD018 |e rda | ||
| 072 | 7 | |a 004.4/.6 |x Programování. Software |2 Konspekt |9 23 | |
| 072 | 7 | |a 519.1/.8 |x Kombinatorika. Teorie grafů. Matematická statistika. Operační výzkum. Matematické modelování |2 Konspekt |9 13 | |
| 080 | |a 004.42.047 |2 MRF | ||
| 080 | |a 519.713:519.21 |2 MRF | ||
| 080 | |a 519.21 |2 MRF | ||
| 080 | |a 004.94 |2 MRF | ||
| 100 | 1 | |a Babiak, Tomáš |% UČO 143254 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Translation of Linear Temporal Logic to Omega-Automata |y eng |
| 245 | 1 | 0 | |a Translation of Linear Temporal Logic to Omega-Automata / |c Tomáš Babiak |
| 264 | 0 | |c 2017 | |
| 300 | |a vii, 152 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: Mojmír Křetínský | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2017 | ||
| 520 | 2 | |a Překlad logiky lineárního času (Linear Temporal Logic - LTL) na různé typy ɷ-automatů je intenzivně studovaná oblast, která má mnoho aplikací. Metoda LTL ověřovaní modelu (LTL model checking) je rozšířená a plně automatizovaná technika, která se používá k ověření, zda daný systém splňuje požadovanou specifikaci. Jedním z klíčových kroků je překlad logiky LTL na Büchiho automaty. Různé vlastnosti, jako velikost a determinismus použitého automatu, mohou mít velký vliv na celkový výkon a průběh metody ověřování modelu. Jiné typy automatů, například deterministické Rabinovy automaty, se používají při ověřování modelu pravděpodobnostních systémů. Překlad LTL na ɷ-automaty má kromě metody ověřovaní modelu využití i v jiných oblastech jako jsou kontrola správnosti (sanity checking), detekce prázdnosti (vacuity detection), syntéza kontrolérů (controller synthesis) a syntéza reaktivních modulů (synthesis of reactive modules). Zlepšení různých překladů LTL na ɷ-automaty se v minulosti věnovalo |% cze | |
| 520 | 2 | 9 | |a Translation of Linear Temporal Logic (LTL) into ɷ-automata of various types is a heavily studied area with wide range of applications. The translation of LTL formulae into Büchi automata represents one of the crucial steps for LTL model checking, a wide-spread fully-automated technique used to verify whether a given system satisfies a desired specification. Properties, such as size and determinism, of a produced automaton can have a significant impact on the overall performance of the model checking procedure. Other types of automata, such as deterministic Rabin automata, are employed in the context of model checking of probabilistic systems. Besides model checking, the LTL to ɷ-automata translation has its utilization also in areas like sanity checking, vacuity detection, controller synthesis, and synthesis of reactive modules. Much effort was already devoted to improve various LTL to ɷ-automata translations, however, there is still some space for further improvements and tuning. In |9 eng |
| 650 | 0 | 7 | |a lineární logika |2 CZ-BrMU |
| 650 | 0 | 7 | |a pravděpodobnostní automaty |7 ph124559 |2 czenas |
| 650 | 0 | 7 | |a pravděpodobnostní metody |7 ph220676 |2 czenas |
| 650 | 0 | 7 | |a počítačové modelování |7 ph124513 |2 czenas |
| 650 | 0 | 9 | |a linear logic |2 eCZ-BrMU |
| 650 | 0 | 9 | |a probabilistic automata |2 eczenas |
| 650 | 0 | 9 | |a probabilistic methods |2 eczenas |
| 650 | 0 | 9 | |a computer modelling |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 Křetínský, Mojmír, |d 1950- |7 mub2012718728 |% UČO 631 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Katedra teorie programování |4 dgg | |
| 856 | 4 | 1 | |u http://is.muni.cz/th/143254/fi_d/ |
| CAT | |c 20170301 |l MUB01 |h 0420 | ||
| CAT | |a POSPEL |b 02 |c 20170302 |l MUB01 |h 0826 | ||
| CAT | |a POSPEL |b 02 |c 20170302 |l MUB01 |h 0828 | ||
| CAT | |a HANAV |b 02 |c 20170306 |l MUB01 |h 1113 | ||
| CAT | |a POSPEL |b 02 |c 20180314 |l MUB01 |h 0814 | ||
| CAT | |a VESELA |b 02 |c 20180426 |l MUB01 |h 1410 | ||
| CAT | |a POSPEL |b 02 |c 20180503 |l MUB01 |h 0729 | ||
| CAT | |c 20180514 |l MUB01 |h 1102 | ||
| 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 1023 | ||
| CAT | |c 20210614 |l MUB01 |h 2009 | ||
| CAT | |a BATCH |b 00 |c 20210724 |l MUB01 |h 1252 | ||
| 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 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 1337 | ||
| CAT | |a VESELAX |b 02 |c 20240517 |l MUB01 |h 1338 | ||
| CAT | |a VESELAX |b 02 |c 20240517 |l MUB01 |h 1339 | ||
| 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 2016 |5 42005D2680 |8 20180426 |f 72 |f Týdenní |r 20180426 |
| AVA | |a INF50 |b FI |d Diz. práce 2016 |e available |t K dispozici |f 1 |g 0 |h N |i 0 | ||