Spelling suggestions: "subject:"buchi automata"" "subject:"wuchi automata""
1 |
Large Scale Geometries of Infinite Strings / 無限文字列の大規模幾何Takisaka, Toru 26 March 2018 (has links)
京都大学 / 0048 / 新制・課程博士 / 博士(理学) / 甲第20886号 / 理博第4338号 / 新制||理||1623(附属図書館) / 京都大学大学院理学研究科数学・数理解析専攻 / (主査)教授 長谷川 真人, 教授 向井 茂, 准教授 照井 一成 / 学位規則第4条第1項該当 / Doctor of Science / Kyoto University / DFAM
|
2 |
Using Live Sequence Chart Specifications for Formal VerificationKumar, Rahul 11 July 2008 (has links) (PDF)
Formal methods play an important part in the development as well as testing stages of software and hardware systems. A significant and often overlooked part of the process is the development of specifications and correctness requirements for the system under test. Traditionally, English has been used as the specification language, which has resulted in verbose and difficult to use specification documents that are usually abandoned during product development. This research focuses on investigating the use of Live Sequence Charts (LSCs), a graphical and intuitive language directly suited for expressing communication behaviors of a system as the specification language for a system under test. The research presents two methods for using LSCs as a specification language: first, by translating LSCs to temporal logic, and second, by translating LSCs to an automaton structure that is directly suited for formal verification of systems. The research first presents the translation for each method and further, identifies the pros and cons for each verification method.
|
3 |
Efektivní automatové techniky a jejich aplikace / Efficient Automata Techniques and Their ApplicationsHavlena, Vojtěch January 2021 (has links)
Tato práce se zabývá vývojem efektivních technik pro konečné automaty a jejich aplikace. Zejména se věnujeme konečným automatům použitých pří detekci útoků v síťovém provozu a automatům v rozhodovacích procedurách a verifikaci. V první části práce navrhujeme techniky přibližné redukce nedeterministických automatů, které snižují spotřebu zdrojů v hardwarově akcelerovaném zkoumání obsahu paketů. Druhá část práce je je věnována automatům v rozhodovacích procedurách, zejména slabé monadické logice druhého řádů k následníků (WSkS) a teorie nad řetězci. Navrhujeme novou rozhodovací proceduru pro WS2S založenou na automatových termech, umožňující efektivně prořezávat stavový prostor. Dále studujeme techniky předzpracování WSkS formulí za účelem snížení velikosti konstruovaných automatů. Automaty jsme také aplikovali v rozhodovací proceduře teorie nad řetězci pro efektivní reprezentaci důkazového stromu. V poslední části práce potom navrhujeme optimalizace rank-based komplementace Buchiho automatů, které snižuje počet generovaných stavů během konstrukce komplementu.
|
Page generated in 0.0323 seconds