AgentLang - Programovací jazyk pre agentovo orientované modelovanie
Boďa, Tomáš; Petříček, Tomáš; Bednárek, David
2024 - anglický With the increasing popularity of the agent-based simulation technique in various scientific fields, there is a demand for an all-in-one framework for modeling agent-based simulations. Although there are numerous agent-based tools available, these in most cases feature complex syntax and language structures or are aimed to be used in specific domains only. In response this thesis presents a new approach to modeling agent-based simulations by developing a brand new agent-based framework - AgentLang. The frame- work features a programming language with a unified and simple syntax for defining agents and their properties. Moreover, it provides a web-based interface with a spread- sheet module for manipulating agents and their values using the familiar spreadsheet format as well as a visualisation module for rendering the simulation in real-time. These three features of the AgentLang framework aim to introduce a new way to modeling agent-based simulations and attempt to make agent-based modeling more accessible to people of all scientific fields. S rastúcou popularitou techniky agentovo orientovaného modelovania v rôznych ve- deckých oblastiach vzniká dopyt po jednotnom nástroji na modelovanie simulácií. Aj keď je na trhu dostupné množstvo nástrojov na agentovo orientované modelovanie, vo vač- šine prípadov sa vyznačujú zložitou jayzkovou syntaxou a štruktúrou alebo sú určené na použitie iba v špecifických oblastiach. Vzhľadom na tieto nevýhody táto práca poskytuje nový pohľad na agentovo orientované modelovanie tým, že vyvíja nový nástroj na mo- delovanie agentovo orientovaných simulácií - AgentLang. Tento nástroj poskytuje nový programovací jazyk s jednotnou, ucelenou a jednoduchou syntaxou na definovanie agen- tov a ich vlastností. Okrem toho poskytuje webovú aplikáciu s tabulkovým rozhraním na manipuláciu agentov a ich hodnôt. V neposlednom rade obsahuje vizualizačný modul na zobrazovanie simulácií v reálnom čase. Tieto tri vlastnosti nástroja AgentLang majú za cieľ poskytnúť nový spôsob modelovania agentovo orientovaných simulácií a sprístupniť agentovo orientované modelovanie používateľom zo všetkých vedeckých odvetví. Klíčová slova: agentovo orientované modelovanie|simulácie|programovací jayzk|interpreter; agent-based modeling|simulation|programming language|interpreter Plné texty jsou dostupné v digitálním repozitáři NUŠL AgentLang - Programovací jazyk pre agentovo orientované modelovanie

With the increasing popularity of the agent-based simulation technique in various scientific fields, there is a demand for an all-in-one framework for modeling agent-based simulations. Although there ...

Boďa, Tomáš; Petříček, Tomáš; Bednárek, David
Univerzita Karlova, 2024

Průhlednost nezávislá na pořadí
Rožek, Matúš; Kahoun, Martin; Iser, Tomáš
2024 - anglický Rendering transparent geometry in realtime brings a set of problems as the transpar- ent objects need to be sorted first and rendered in order from back to front for their correct overlaying. A set of rendering algorithms called Order Independent Transparency (OIT) tries to accomplish this without sorting the geometry in advance. We create a program implementing five algorithms and compare their weaknesses, strengths, and properties. Some algorithms might excel in certain conditions and produce great results, yet fall short in slightly different environments. We aim to answer the question of which OIT algorithm is best suited for which scenarios. Vykresľovanie priehľadnej geometrie v reálnom čase spôsobuje sadu problémov, pre- tože jednotlivé objekty potrebujú byť zoradené a vykreslené v poradí odzadu dopredu pre korektný výsledok. Existuje avšak trieda algoritmov, ktorá sa snaží o vykreslenie obrazu aj bez potreby priehľadné objekty najprv zoradiť. Tieto algoritmy sa nazývajú "priehľadnosť nezávislá na poradí" (anglicky Order Independent Transparency, skratka OIT). Vytvorili sme program, ktorý obsahuje 5 rôznych OIT algoritmov. Poukazujeme na silné a slabé stránky jednotlivých prístupov - niektoré môžu excelovať v určitých pod- mienkach, ale zato podávať výrazne slabšie výsledky v odlišnom prostredí. Snažíme sa odpovedať na otázku, ktorý OIT algoritmus je najlepšie využiť v akej situácii. Klíčová slova: priehľadnosť nezávislá na poradí|vykresľovanie priehľadnosti|alfa kompozícia|realtime rendering; order independent transparency|transparency rendering|alpha compositing|realtime rendering Plné texty jsou dostupné v digitálním repozitáři NUŠL Průhlednost nezávislá na pořadí

Rendering transparent geometry in realtime brings a set of problems as the transpar- ent objects need to be sorted first and rendered in order from back to front for their correct overlaying. A set of ...

Rožek, Matúš; Kahoun, Martin; Iser, Tomáš
Univerzita Karlova, 2024

Intravitální diagnostika neurodegenerativních onemocnění.
Baranová, Soňa; Holada, Karel; Kaňovský, Petr; Žáková, Dana
2024 - anglický Prionopathies, also called transmissible spongiform encephalopathies (TSE) and synucleinopathies are neurodegenerative diseases that are associated with the accumulation of misfolded proteins (prion and α-synuclein) mostly in the central nervous system. To this day, early and definite diagnosis remains unavailable during the patient's lifetime, mainly due to the absence of reliable biomarker which makes clinical diagnosis more challenging. Therefore, the gold standard in diagnostics remains direct post-mortem evaluation of misfolded proteins within brain tissue by western blot and immunohistochemistry. In the recent years, seeding amplification assays (SAAs) like Real-Time Quacking-Induced Conversion (RT-QuIC) emerged for ultra-sensitive ante-mortem diagnosis of neurodegenerative diseases. SAAs exploit ability of pathological misfolded proteins present in patient's samples to change the conformation and initiate aggregation of native recombinant protein substrate by prion-like seeding mechanism. In the presented dissertation thesis, we exploited second-generation RT-QuIC assay (55řC, 700 rpm, cycles of 1 min double-orbital shaking and 1 min incubation) utilizing recombinant hamster shortened prion protein (rHAPrP90-231) to evaluate prion seeding activity in post-mortem TSE (n=38) and non-TSE (n=30)... Prionopatie, taktiež nazývané transmisívne spongiformné encefalopatie (TSE), a synukleínopatie predstavujú skupinu neurodegeneratívnych ochorení, ktoré sú asociované s akumuláciou nesprávne zložených proteínov (prión a α-synukleín) prevažne v centrálnom nervovom systéme. Kvôli absencii spoľahlivého biomarkera je včasná a definitívna diagnostika počas života pacienta nedostupná. Zlatým štandardom preto zostáva priama post-mortem detekcia patologicky zložených proteínov v mozgovom tkanive pomocou western blotu a imunohistochémie. Avšak v posledných rokoch sa pre ultra-senzitívnu ante-mortem diagnostiku zaviedli metódy so spoločným názvom ʺseeding amplification assays (SSAs)ʺ akou je aj Real-Time Quacking-Induced Conversion (RT-QuIC). SAAs využívajú schopnosť patologicky zložených proteínov, ktoré sú prítomné v pacientskej vzorke, zmeniť konformáciu a iniciovať agregáciu monomérneho rekombinantného proteínu v substráte vďaka ʺprion-likeʺ mechanizmu. V prezentovanej dizertačnej práci sme analyzovali prión konvertujúcu aktivitu v post- mortem TSE (n=38) a non-TSE (n=30) vzorkách cerebrospinálneho moku (CSF) a korešpondujúcich vzoriek koží pomocou druhej generácie RT-QuIC metódy (55řC, 700 rpm, cykly 1 min dvoj orbitálneho trepania a 1 min inkubácia) s využitím rekombinantného skráteného priónového... Klíčová slova: diagnostika; neurodegeneratívne ochorenia; prión; CJCH; α-synukleín; synukleínopatia; RT-QuIC; diagnosis; neurodegenerative diseases; prion; CJD; α-synuclein; synucleinopathy; RT-QuIC Plné texty jsou dostupné v digitálním repozitáři NUŠL Intravitální diagnostika neurodegenerativních onemocnění.

Prionopathies, also called transmissible spongiform encephalopathies (TSE) and synucleinopathies are neurodegenerative diseases that are associated with the accumulation of misfolded proteins (prion ...

Baranová, Soňa; Holada, Karel; Kaňovský, Petr; Žáková, Dana
Univerzita Karlova, 2024

Zjednodušení použitelnosti nástrojů pro správu kvality dat pro datové inženýry
Tomis, Zdeněk; Bulej, Lubomír; Škoda, Petr
2024 - anglický In the realm of data quality management, integrating robust data quality rules into automated workflows and data pipelines is essential for maintaining data integrity. This thesis addresses the gap in programmatic accessibility of Ataccama ONE's data qual- ity tools, which primarily leverage the proprietary Ataccama Expression Language. By reimplementing this language in Python, the project enhances its usability for data en- gineers who seek to consume these tools programmatically. The focus is on enabling data engineers to execute Ataccama's rules directly within Python. The viability of this implementation is tested through performance comparisons with similar solutions. V oblasti data quality managementu je pro zachování integrity dat zásadní integrovat pravidla kvality dat do automatizovaných workflows a datových pipelines. Tato práce se zabývá mezerou v programové dostupnosti nástrojů pro kvalitu dat společnosti Ataccama ONE, které využívají především proprietární jazyk Ataccama Expression Language. Re- implementací tohoto jazyka v jazyce Python projekt zvyšuje jeho použitelnost pro datové inženýry, kteří potřebují tyto nástroje využít programmaticky v různým prostředích. Dů- raz je kladen na to, aby datoví inženýři mohli provádět a spravovat pravidla Ataccama přímo v jazyce Python s ohledem na jednoduchost užití a minimální nároky. Užitelnost této implementace je otestována prostřednictvím porovnání výkonu s podobnými řeše- ními. Klíčová slova: data quality management|data engineering|performance evaluation; data quality management|data engineering|performance evaluation Plné texty jsou dostupné v digitálním repozitáři NUŠL Zjednodušení použitelnosti nástrojů pro správu kvality dat pro datové inženýry

In the realm of data quality management, integrating robust data quality rules into automated workflows and data pipelines is essential for maintaining data integrity. This thesis addresses the gap in ...

Tomis, Zdeněk; Bulej, Lubomír; Škoda, Petr
Univerzita Karlova, 2024

Analýza cyklů ve verifikačním frameworku pro LLVM IR
Kubík, Jakub; Kofroň, Jan; Parízek, Pavel
2024 - anglický Bugs in compilers can have severe consequences. Apart from traditional methods like testing, one of the ways of keeping compilers correct that gained traction only in recent years is translation validation, a technique ensuring the semantic correctness of optimizations in compilers. Alive2 is an open-source translation validation framework for LLVM that is currently widely used by LLVM developers. In order to make any static analysis tool usable, the frequency of false alarms must be kept to a minimum. Alive2 was designed to have zero false alarms and has been very successful in this endeavor except in the case of certain loops. Our aim in this thesis is to analyze Alive2's loop algorithms in an attempt to find the cause of these false alarms. This was motivated by personal communication with authors of Alive2 who presented the false alarm issue in loops as one of the more challenging and pressing issues in Alive2. We were successful in pinpointing the cause of false alarms and even providing a fix for the issue. Our solution is now a part of the Alive2 framework. Furthermore, we have identified other potential issues in Alive2 which we discuss in the thesis as well. Chyby v překladačích programovacích jazyků mohou mít vážné následky. Kromě tradičních metod, jako je testování, je jedním ze způsobů zajištění správnosti překladačů translation validation, technika zajišťující sémantic- kou správnost optimalizací v překladačích, která se prosadila teprve v po- sledních pár letech. Alive2 je open-source translation validation framework pro LLVM, který je v současnosti široce používán vývojáři LLVM. Pro za- jištění použitelnosti statických analyzátorů je potřeba minimalizovat četnost falešných pozitiv. Alive2 je navržen tak, aby neměl žádná falešná pozitiva a byl v tomto ohledu velmi úspěšný až na některé programy se smyčkami. Na- ším cílem v této práci je analyzovat algoritmy Alive2 pracující se smyčkami se záměrem identifikace příčiny falešných pozitiv. Naše práce byla motivo- vána komunikací s autory Alive2, kteří považovali problematiku falešných poplachů ve smyčkách jako jeden z náročnějších a závažnějších problémů v Alive2. Podařilo se nám přesně určit podstatu problému falešných poplachů a dokonce i opravit tento problém. Naše řešení je aktuálně součástí Alive2. Kromě toho jsme v Alive2 identifikovali další potenciální problémy, o kterých v této práci také pojednáváme. Klíčová slova: překladače|LLVM|translation validation|formální verifikace; compilers|LLVM|translation validation|formal verification Plné texty jsou dostupné v digitálním repozitáři NUŠL Analýza cyklů ve verifikačním frameworku pro LLVM IR

Bugs in compilers can have severe consequences. Apart from traditional methods like testing, one of the ways of keeping compilers correct that gained traction only in recent years is translation ...

Kubík, Jakub; Kofroň, Jan; Parízek, Pavel
Univerzita Karlova, 2024

Aproximační techniky pro dynamické problémy rozvozu
Zeman, David; Barták, Roman; Fink, Jiří
2024 - anglický This thesis studies the capacitated dynamic vehicle routing problem with changing vehicle availability. It is motivated by the increasing demand for fast and reliable delivery services in recent years. First, we analyze the problem and build its formal model. Then we propose several policies to process dynamically appearing orders. Next, we implement exact and heuristic algorithms like insertion heuristic, mixed integer programming, evo- lutionary algorithm, and ant colony optimization. Finally, we compare the algorithms with different policies and parameters on Kilby's dataset. 1 Tato práce studuje dynamický problém rozvozu s omezenou kapacitou a měnící se dos- tupností vozidel. Motivací pro studium tohoto problému je rostoucí poptávka po rychlých a spolehlivých doručovacích službách v posledních letech. V první části práce analyzujeme problém a vytvoříme jeho formální model. Poté navrhneme a implementujeme strategie pro vypořádání se s dynamickou podstatou problému. Dále implementujeme exaktní a heuristické algoritmy, jako je heuristika vkládáním, celočíselné programování, evoluční algoritmy a optimalizace kolonií mravenců. Nakonec porovnáme algoritmy s různými strategiemi a parametry na Kilbyho datové sadě. 1 Klíčová slova: problém rozvozu|optimalizace|on-line; vehicle routing|optimization|on-line Plné texty jsou dostupné v digitálním repozitáři NUŠL Aproximační techniky pro dynamické problémy rozvozu

This thesis studies the capacitated dynamic vehicle routing problem with changing vehicle availability. It is motivated by the increasing demand for fast and reliable delivery services in recent ...

Zeman, David; Barták, Roman; Fink, Jiří
Univerzita Karlova, 2024

Řízení robotického šachového manipulátoru
Kapustík, Boris; Kruliš, Martin; Kopecký, Michal
2024 - anglický In this thesis, we will use Kinect v2 (from Microsoft Corporation), Stockfish (one of the highest-ranking chess engines), and a custom-made robotic crane capable of accepting simple commands to move across a 3-dimensional plane. The objective is to integrate software for boardgame (Chess) tracking using an easily accessible camera and depth sensor developed by Roman Staněk with an open-source chess engine to create a simple chess robot. Thanks to the tracing, the robot will have the ability to interact with users. The output will be a desktop application for controlling and configuring the robot, switching between game modes, and tracking the game. It will also require creating a virtual mock of the robotic crane to simplify testing and further development. V této práci použijeme Kinect v2 (od Microsoft Corporation), Stockfish (jeden z nej- lépe hodnocených šachových programů), a na zakázku vyrobený robotický manipulátor schopný přijímat jednoduché příkazy k pohybu po 3-rozměrné rovině. Cílem je integrovat software pro sledování deskových her (šachy) pomocí snadno dostupné kamery a hloub- kového senzoru vyvinutýho Romanemem Stankem s open-source šachovým enginem k vytvoření jednoduchého šachového robota. Díky sledování, robot bude mít schopnost ko- munikovat s uživateli. Výstupem bude desktopová aplikace pro ovládání a konfiguraci robota, přepínání mezi herními režimy a sledování hry. Bude to také vyžadovat vytvoření virtuální napodobeniny robotického jeřábu pro zjednodušení testování a dalšího vývoje. Klíčová slova: Kinect|integrace|počítačové vidění|Soubory mapované paměti|robotický šachy hrající manipulátor|Meziprocesová komunikace; Kinect|integration|computer vision|memory-mapped files|robotic chess-playing manipulator|inter-process communication Plné texty jsou dostupné v digitálním repozitáři NUŠL Řízení robotického šachového manipulátoru

In this thesis, we will use Kinect v2 (from Microsoft Corporation), Stockfish (one of the highest-ranking chess engines), and a custom-made robotic crane capable of accepting simple commands to move ...

Kapustík, Boris; Kruliš, Martin; Kopecký, Michal
Univerzita Karlova, 2024

Praktické dávkové důkazy pro mocnění
Ivanova, Svetlana; Hubáček, Pavel; Mareš, Martin
2024 - anglický This thesis studies batch Proofs of Exponentiation (batch PoE). We explore exist- ing batch PoEs and analyze their verification cost. We also introduce two batch PoEs and compare their performance with the performance of the existing approaches. Our batch PoEs outperform the existing ones, both in theory and in practice. We achieve the improvement in the verification costs by decreasing the expected number of group mul- tiplications. For the practical analysis, we choose the values of the protocol parameters as used in practice, and then measure the time of multiplications and exponentiations on the verifier's side of the discussed protocols in our implementation in C++. Tato práce se zabývá dávkovými důkazy pro mocnění (dávké PoE). Zkoumáme exis- tující dávkové PoE a analyzujeme jejich ověřovací náklady. Také představujeme dva dáv- kové PoE a porovnáváme jejich výkon s výkonem existujících přístupů. Naše dávkové PoE překonávají existující, jak teoreticky, tak i prakticky. Zlepšení ověřovacích nákladů dosahujeme snížením očekávaného počtu grupových násobení. Pro praktickou analýzu vybíráme hodnoty parametrů protokolu používané v praxi a pak měříme čas násobení a mocnění na straně ověřovatele pro zkoumané protokoly v naší implementaci v jazyce C++. Klíčová slova: Důkazy pro mocnění|Ověřitelné zpožďovací funkce|Dávkové důkazy; Proof of Exponentiation|Batching|Verifiable Delay Function Plné texty jsou dostupné v digitálním repozitáři NUŠL Praktické dávkové důkazy pro mocnění

This thesis studies batch Proofs of Exponentiation (batch PoE). We explore exist- ing batch PoEs and analyze their verification cost. We also introduce two batch PoEs and compare their performance ...

Ivanova, Svetlana; Hubáček, Pavel; Mareš, Martin
Univerzita Karlova, 2024

Geopolitické základy nového konfucianismu: Případ Qian Mu
Liao, Wei Chun; Doboš, Bohumil; Halamka, Tomáš
2024 - anglický Klíčová slova: Qian Mu; New Confucianism; geopolitics; critical geopolitics; post-Chineseness; Qian Mu; New Confucianism; geopolitics; critical geopolitics; post-Chineseness Plné texty jsou dostupné v digitálním repozitáři NUŠL Geopolitické základy nového konfucianismu: Případ Qian Mu

Liao, Wei Chun; Doboš, Bohumil; Halamka, Tomáš
Univerzita Karlova, 2024

Čínská dluhová past v Demokratické republice Kongo: Neoklasická geopolitika: případová studie zhrouceného státu (2006-2023) v Demokratické republice Kongo
Lempereur, Pauline; Morgado Valentim Albino, Nuno; Riegl, Martin
2024 - anglický Plné texty jsou dostupné v digitálním repozitáři NUŠL Čínská dluhová past v Demokratické republice Kongo: Neoklasická geopolitika: případová studie zhrouceného státu (2006-2023) v Demokratické republice Kongo

Lempereur, Pauline; Morgado Valentim Albino, Nuno; Riegl, Martin
Univerzita Karlova, 2024