|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulation-based inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.
|
|
|
One-Sided Random Context Grammars
Zemek, Petr ; Černá, Ivana (oponent) ; Doc. In.g Petr Sosík, Dr. (oponent) ; Meduna, Alexandr (vedoucí práce)
This thesis introduces the notion of a one-sided random context grammar as a context-free-based regulated grammar, in which a set of permitting symbols and a set of forbidding symbols are attached to every rule, and its set of rules is divided into the set of left random context rules and the set of right random context rules . A left random context rule can rewrite a nonterminal if each of its permitting symbols occurs to the left of the rewritten symbol in the current sentential form while each of its forbidding symbols does not occur there. A right random context rule is applied analogically except that the symbols are examined to the right of the rewritten symbol. The thesis is divided into three parts. The first part gives a motivation behind introducing one-sided random context grammars and places all the covered material into the scientific context. Then, it gives an overview of formal language theory and some of its lesser-known areas that are needed to fully grasp some of the upcoming topics. The second part forms the heart of the thesis. It formally defines one-sided random context grammars and studies them from many points of view. Generative power, relations to other types of grammars, reduction, normal forms, leftmost derivations, generalized and parsing-related versions all belong between the studied topics. The final part of this thesis closes its discussion by adding remarks regarding its coverage. More specifically, these remarks concern application perspectives, bibliography, and open problem areas.
|
|
|
On Parallel Processing in Formal Models: Jumping Automata and Normal Forms
Kocman, Radim ; Černá, Ivana (oponent) ; Janoušek, Jan (oponent) ; Meduna, Alexandr (vedoucí práce)
The present thesis introduces and studies new possibilities of parallel processing in formal models. More specifically, it focuses its attention on parallel versions of jumping finite automata and on normal forms of grammars with interesting parallel properties. In the first part of this thesis, we give an initial motivation for studying parallel processing in formal models. We briefly introduce jumping models and normal forms of grammars and grammar systems. Finally, we state the precise focus and goals of our research. The second part of this thesis is focused on new results on jumping finite automata. First, we introduce n-parallel jumping finite automata that enhance the original jumping finite automaton model with multiple reading heads. The rest of the chapter then studies the accepting power of the model under two different jumping modes. Second, we introduce double-jumping finite automata and explore advanced jumping modes utilizing two heads. We study the accepting power of the models and also the closure properties of the related language families. Lastly, we introduce jumping 5'->3' Watson-Crick finite automata that combine the jumping behavior with the biology-inspired Watson-Crick finite automata that process double-stranded DNA sequences. The rest of this chapter then studies the accepting power of the model under unrestricted and various restricted conditions. The third part of this thesis is focused on new results on CD grammar systems. We introduce two types of transformations that turn arbitrary general grammars into equivalent two-component general CD grammar systems of very reduced and simplified forms. Apart from the reduction and simplification, we describe several other useful properties concerning these systems and the way they work. In the last part, we mention possible application perspectives for the introduced models and normal forms, and we conclude the thesis with the final summary and the description of theoretical perspectives for the achieved results.
|
|
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Pasareanu, Corina (oponent)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
|
Towards thread aware component behavior specifications
Poch, Tomáš ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Hennicker, Rolf (oponent)
Komponentový přístup je již poměrně zavedenou metodologií používanou při vývoji software. Při komerčním vývoji aplikací, se však ještě nevyužívají modely chování komponent a jejich následná analýza, ačkoliv by to zaručilo, že komunikace mezi složenými komponentami nebude obsahovat chyby. Reálnému použití v praxi brání jkk relativně omezené výrazové prostředky modelovacích jazyků tak i náročnost psaní modelů. Abychom usnadnili použití modelů chování, navrhujeme modelovací jazyk Threaded Behavior Protocols (TBP), který se snaží překlenout rozdíly mezi modelovacími a imperativními programovacími jazyky. Tím, že umožníme programátorům používat koncepty z imperativních jazyků, na které jsou zvyklí, usnadníme přípravu modelů. Teorie TBP de finuje pojem správnosti kompozice komponent jako absenci dvou pevně daných komunikačních chyb a poskytuje relaci zjemňovíní modelu, která zachovává správnost vzhledem k libovolnému prostředí. Díky tomu, přináší analýza TBP podobné výhody jako starší modelovací jazyky, přičemž bere v úvahu i koncepty z imperativních jazyků.
|
|
|
Hodnocení individuálně připravovaných polotuhých přípravků
Černá, Ivana ; Šnejdrová, Eva (vedoucí práce) ; Šklubalová, Zdeňka (oponent)
Cílem rigorózní práce bylo zhodnotit technologii přípravy vybraných polotuhých přípravků magistraliter připravovaných v lékárně, provést případně optimalizaci složení a postupu přípravy a revidovat technologické předpisy, podle kterých se v lékárně postupuje. Bylo hodnoceno reologické chování polotuhých přípravků, adhezivní vlastnosti gelů a doba rozpouštění dávkovaných gelů určených k aplikaci do dutiny ústní. Viskozita byla měřena digitálním viskozimetrem Brookfield nebo Ubbelohdeho kapilárním viskozimetrem. Nebyl zjištěn významný rozdíl v reologickém chování polotuhých přípravků připravených v unguátoru a polotuhých přípravků připravených v třence. Adhezivita byla testována na mucinový podklad dvěma metodami; metodou průtokovou a metodou odtrhávání adheziva od podkladu za využití materiálového zkušebního stroje firmy Zwick/Roell. Provedené testy adheze prokázaly, že pro aplikaci na sliznici dutiny ústní jsou z hlediska síly a doby adheze nejvhodnější gely methylcelulosy. Gely určené k rozpuštění v dutině ústní byly vylity do forem na vaginální kuličky, čímž bylo zpřesněno dávkování. Byla provedena zkouška doby rozpadu kuliček lékopisnou metodou. Bylo zjištěno, že gely agaru nejsou pro tuto aplikaci vhodné z důvodu extrémně dlouhé doby rozpouštění. Byly formulovány gely želatiny s přídavkem...
|
|
|
Towards thread aware component behavior specifications
Poch, Tomáš ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Hennicker, Rolf (oponent)
Komponentový přístup je již poměrně zavedenou metodologií používanou při vývoji software. Při komerčním vývoji aplikací, se však ještě nevyužívají modely chování komponent a jejich následná analýza, ačkoliv by to zaručilo, že komunikace mezi složenými komponentami nebude obsahovat chyby. Reálnému použití v praxi brání jkk relativně omezené výrazové prostředky modelovacích jazyků tak i náročnost psaní modelů. Abychom usnadnili použití modelů chování, navrhujeme modelovací jazyk Threaded Behavior Protocols (TBP), který se snaží překlenout rozdíly mezi modelovacími a imperativními programovacími jazyky. Tím, že umožníme programátorům používat koncepty z imperativních jazyků, na které jsou zvyklí, usnadníme přípravu modelů. Teorie TBP de finuje pojem správnosti kompozice komponent jako absenci dvou pevně daných komunikačních chyb a poskytuje relaci zjemňovíní modelu, která zachovává správnost vzhledem k libovolnému prostředí. Díky tomu, přináší analýza TBP podobné výhody jako starší modelovací jazyky, přičemž bere v úvahu i koncepty z imperativních jazyků.
|
|
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Pasareanu, Corina (oponent)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
|
Quantitative binding of different analogues of vancomycine to D-Ala-D-Ala using surface plasmon resonance
Černá, Ivana ; Szotáková, Barbora (vedoucí práce) ; Kubíček, Vladimír (oponent)
Univerzita Karlova v Praze Farmaceutická fakulta v Hradci Králové Katedra biochemických věd Titul, jméno, příjmení kandidáta: Ivana Černá Titul, jméno, příjmení školitele: Drª María José Hernáiz Gómez-Dégano Doc. Ing. Barbora Szotáková, PhD. Název diplomové práce: Kvantitativní vazba různých analogů vankomycinu na D-Ala-D-Ala za použití povrchové plasmonové resonance Tato diplomová práce pojednává o interakcích glykopeptidových antibiotik: teicoplaninu; MDL 63,246; mideplaninu; BI 397 (dalbavancin); A 40926 a vancomycinu s dipeptidem D-Ala-D-Ala. Pro tato antibiotika byly stanoveny a optimalizovány podmínky HPLC analýzy. Pro výzkum vazby uvedených antibiotik na bakteriální stěnu byly připravovány a zkoušeny samotvořící vrstvy (SAM) různých vlastností a různé délky řetězce, prezentující D-Ala-D-Ala. Výsledky dokazují, že nejvhodnější způsob přípravy SAM je inkubace čipu přes noc v etanolovém roztoku alkanthiolu. Nejvhodnější pro studium interakce antibiotikum - D-Ala-D-Ala je SAM tvořena osmiuhlíkovým řetězcem a s několika polyethylenglykolovými skupinami na druhé straně, zakončené karboxylovou skupinou. Na tomto povrchu jsme provedli měření interakcí. Všechny zkoumané glykopeptidy mají k povrchu vyšší afinitu než vankomycin, zvláště BI 397 - dalbavancin.
|
|
|
Behavior Composition in Component Systems
Adámek, Jiří ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Madelaine, Erik (oponent)
In order to formally verify a component application, it is suitable to structure the formal specification of its behavior according to the application architecture. Such an approach eases the maintenance of the specification and allows utilizing efficient verification algorithms that are based on decomposition of the application into several communicating parts. How those parts cooperate is formally described via an operation that is called behavior composition. In this thesis we claim that in current software component systems behavior composition has typically two drawbacks: (1) it lacks support for composition error detection and (2) it does not address the problem of unbounded parallelism specification. While detection of composition errors allows checking design inconsistencies at a design time, unbounded parallelism specification is necessary for precise formal description of reentrant components that are used in practice very often. Therefore we introduce two new concepts - the consent operator and the behavior templates - in order to address both the issues (1) and (2). Our solutions are demonstrated on the SOFA component model [35], behavior protocols [32] are used as a behavior specification language.
|
host ::
RSS.