The thesis introduces new models for formal languages, the m-limited state   grammar and the deep pushdown automaton. Their basic definitions are presented,   so is their mutual equivalence and the characteristics of the language family they describe.   Following, a parsing method based on these models is presented. The method is an extension   of a similar method used for context-free languages, the table driven parsing.   The final part of the thesis describes the implementation of a parser based on the method.

Linear Temporal Logic (LTL), as one of the temporal logic, can generate a fully automated correct-by-design controller synthesis approach for single or multiple autonomous vehicles, under much more complex missions than the traditional point-to-point navigation.In this master thesis, a framework which combines model- checking-based robot motion planning with action planning is proposed based on LTL for-mulas. The specifications implicitly require both sequential regions for multi-agent to visit and the desired actions to perform at these regions while avoid-ing collision with each other and fixed obstacles. The high level motion and task planning and low level navigation function based collision avoidance controller are verified by nontrivial simulation and implementation on real quadcopter in Smart Mobility Lab.

Although being quite inexpressive, the description logic (DL) FL₀, which provides only conjunction, value restriction and the top concept as concept constructors, has an intractable subsumption problem in the presence of terminologies (TBoxes): subsumption reasoning w.r.t. acyclic FL₀ TBoxes is coNP-complete, and becomes even ExpTime-complete in case general TBoxes are used. In the present paper, we use automata working on infinite trees to solve both standard and non-standard inferences in FL₀ w.r.t. general TBoxes. First, we give an alternative proof of the ExpTime upper bound for subsumption in FL₀ w.r.t. general TBoxes based on the use of looping tree automata. Second, we employ parity tree automata to tackle non-standard inference problems such as computing the least common subsumer and the difference of FL₀ concepts w.r.t. general TBoxes.

The verification problem for action logic programs with non-terminating behaviour is in general undecidable. In this paper, we consider a restricted setting in which the problem becomes decidable. On the one hand, we abstract from the actual execution sequences of a non-terminating program by considering infinite sequences of actions defined by a Büchi automaton. On the other hand, we assume that the logic underlying our action formalism is a decidable description logic rather than full first-order predicate logic.

Weighted automata can be seen as a natural generalization of finite state automata to more complex algebraic structures. The standard reasoning tasks for unweighted automata can also be generalized to the weighted setting. In this report we study the problems of intersection, complementation, and inclusion for weighted automata on infinite trees and show that they are not harder complexity-wise than reasoning with unweighted automata. We also present explicit methods for solving these problems optimally.

No / This paper presents a stochastic automaton approach to stock ordering for retailers of time-limited goods, in the modern supply chain network. The rationale applied is that by ordering in small quantities frequently, overstocking will be reduced, capital liquidity improved and wastage limited. A consequence for the complete supply chain is that such an approach could substantially minimise the reactive bullwhip effect, leading to more efficient utilisation, production and agility throughout the chain. Such agility and flexibility can only be achieved by full integration of stock inventory monitoring technologies (such as RFID) with enterprise integration systems (such as ERP) connected to suppliers, mediated by the internet. We undertake a comparative simulation study of stock ordering using a stochastic automaton and a naive traditional approach. This shows that stochastic ordering, prompted by a stochastic automaton, exhibits characteristic properties that are a prerequisite for reducing the bullwhip effect, thus enabling agile inventory management.

Tato práce se zabývá problematikou popisu síťového provozu pomocí automaticky vytvořeného modelu komunikace. Hlavním zaměřením jsou komunikace v řídicích systémech , které využívají speciální protokoly, jako je například IEC 60870-5-104 . V této práci představujeme metodu charakteristiky síťového provozu z pohledu obsahu komunikace i chování v čase. Tato metoda k popisu využívá deterministické konečné automaty , prefixové stromy  a analýzu opakovatelnosti. Ve druhé části této diplomové práce se zaměřujeme na implementaci programu, který je schopný na základě takového modelu komunikace verifikovat síťový provoz v reálném čase.

Η διατριβή αφορά την ανάπτυξη και υλοποίηση ενός τετραδιάστατου, διακριτού μοντέλου προσομοίωσης της συμπεριφοράς καρκινικών κυτταρικών συστημάτων σε ελεύθερη ανάπτυξη και της απόκρισής τους σε χημειοθεραπευτική ή και ακτινοθεραπευτική αγωγή. Υλοποιήθηκαν δύο εκδοχές του μοντέλου: η χωρική και η μη χωρική προσέγγιση. Η χωρική προσέγγιση αναφέρεται στην τετραδιάστατη προσομοίωση συμπαγών όγκων. Η μη χωρική προσέγγιση βρίσκει εφαρμογή στην περίπτωση μη συμπαγών όγκων, καθώς και συμπαγών όγκων, όταν δεν δίνεται έμφαση στη χωρική εξέλιξή τους. Η ερευνητική εργασία έχει επικεντρωθεί σε τρεις τύπους καρκινικών όγκων: καρκίνος του μαστού, καρκίνος του πνεύμονα και πολύμορφο γλοιοβλάστωμα και σε θεραπευτικά σχήματα χορήγησης των σκευασμάτων: επιρουβικίνη (epirubicin), τεμοζολομίδη (temozolomide), σισπλατίνη (cisplatin), γεμσιταμπίνη (gemcitabine), βινορελμπίνη (vinorelbine) και δοσεταξέλη (docetaxel). Σκοπός της εργασίας είναι η ανάπτυξη ενός εργαλείου για την αξιόπιστη υποστήριξη ιατρών στη λήψη αποφάσεων σχετικά με την επιλογή θεραπευτικών σχημάτων και την εξατομικευμένη βελτιστοποίηση της θεραπευτικής αγωγής. Η αφετηρία είναι η μοντελοποίηση του κυτταρικού κύκλου και των πιθανών μεταβάσεων μεταξύ των καταστάσεων που μπορεί να βρεθεί ένα κύτταρο. Το μοντέλο βασίζεται στην υπόθεση ότι ο καρκινικός όγκος διατηρείται από μια συγκεκριμένη κατηγορία κυττάρων, τα καρκινικά βλαστικά κύτταρα (cancer stem cells), και έχει επεκταθεί ώστε να περιλαμβάνει σε μεγαλύτερη λεπτομέρεια διάφορους βιολογικούς μηχανισμούς σε μοριακό (πχ. εκφράσεις γονιδίων) και κυτταρικό επίπεδο. Ο μηχανισμός δράσης, η φαρμακοκινητική και η φαρμακοδυναμική των θεωρούμενων σκευασμάτων έχουν μελετηθεί βιβλιογραφικά και έχουν ενσωματωθεί στο μοντέλο. Επίσης, το μοντέλο έχει αναπτυχθεί ώστε να λαμβάνει υπόψη του την κλινική εικόνα του ασθενούς με χρήση εξατομικευμένων κλινικών δεδομένων, όπως απεικονιστικά δεδομένα (π.χ. CT, MRI, PET), ιστοπαθολογικά δεδομένα (π.χ. τύπος όγκου, βαθμός διαφοροποίησης) και μοριακά δεδομένα (π.χ. έκφραση γονιδίων). Στα πλαίσια της διατριβής πραγματοποιούνται έλεγχοι αξιοπιστίας και εκτενείς παραμετρικές μελέτες για την αποσαφήνιση της ευαισθησίας του μοντέλου στη διακύμανση των παραμέτρων του τόσο κατά την προσομοίωση της ελεύθερης ανάπτυξης όσο και κατά την εφαρμογή της χημειοθεραπευτικής αγωγής. Η ποσοτική αξιολόγηση, προσαρμογή και βελτιστοποίηση του μοντέλου πραγματοποιείται στα πλαίσια των ευρωπαϊκών ερευνητικών προγραμμάτων ACGT (Advancing Clinicogenomic Trials on Cancer, FP6-2005-IST-026996), ContraCancrum (Clinically Oriented Cancer Multilevel Modelling, FP7-ICT-2007-2-223979) και P-medicine (From data sharing and integration via VPH models to Personalized medicine, FP7-ICT-2009-6-270089) μέσω της αξιοποίησης πραγματικών κλινικών δεδομένων. Στην παρούσα διατριβή παρουσιάζονται τα αποτελέσματα της προσαρμογής του μοντέλου σε κλινικά δεδομένα του καρκίνου του μαστού, του καρκίνου του πνεύμονα και του πολύμορφου γλοιοβλαστώματος. Επιπλέον, διάφορες εκδόσεις του μοντέλου έχουν αξιοποιηθεί για ‘την επάνδρωση’ μιας ευρωπαϊκής βάσης μοντέλων για τον καρκίνο, που υλοποιείται στα πλαίσια του ευρωπαϊκού ερευνητικού προγράμματος TUMOR (Transatlantic Tumour Model Repositories, FP7-ICT-2009-5-247754). Το μοντέλο υλοποιείται σε γλώσσα προγραμματισμού C++. / In the present thesis, a clinically oriented, multiscale, discrete simulation model of cancer free growth and response to chemotherapy and/or radiotherapy is presented and investigated. Two versions of the model have been implemented: the spatial and the non spatial approach. The spatial model concerns the spatiotemporal evolution of solid tumours, whereas the non spatial model can be applied in the case of non solid cancers, as well as solid tumours, when no emphasis is put on the spatial features of a tumour evolution. The research work has been focused on the paradigms of early breast cancer treated with the single agent epirubicin, primary lung cancer treated with various combinations of cisplatin, gemcitabine, vinorelbin and docetaxel and glioblastoma multiforme treated with combined modality treatment using radiation and chemotherapy with temozolomide. The goal is to end up with a reliable simulation system able to assist clinicians in selecting the most appropriate therapeutic pattern, extracted from several candidate therapeutic schemes in the context of patient individualized treatment optimization. The model incorporates the biological mechanisms of cell cycling, quiescence, recruitment (reentry into the cell cycle), differentiation and death. It is based on the well documented assumption that tumour sustenance is due to the existence of cancer stem cells, i.e. cells which have the ability to preserve their own population, as well as give birth to cells that follow the path towards terminal differentiation. Furthermore, the mechanism of action, pharmacokinetics and pharmacodynamics of all considered agents have been bibliographically studied and incorporated into the model. Finally, the model has been developed to support and incorporate individualized clinical data such as imaging data (e.g. CT, MRI, PET slices, possibly fused), including the definition of the tumour contour and internal tumour regions (proliferating, necrotic), histopathologic (e.g., type of tumour) and genetic data (e.g., gene expression). An exhaustive and in-depth examination of the model behaviour with respect to the variation of its input parameters has been performed, in order to determine the impact of its parameters, guarantee a biologically relevant virtual tumour behaviour and enlighten aspects of the interplay and possible interdependencies of the biological mechanisms modeled. Finally, the model has been quantitativily validated and adaptated in the framework of the ACGT (Advancing Clinicogenomic Trials on Cancer, FP6-2005-IST-026996), ContraCancrum (Clinically Oriented Cancer Multilevel Modelling, FP7-ICT-2007-2-223979) and P-medicine (From data sharing and integration via VPH models to Personalized medicine, FP7-ICT-2009-6-270089) European Commission-funded projects by exploiting real clinical data. In the present thesis, the clinical adaptation of the model focuses on breast cancer, lung cancer and glioblastoma multiforme clinical cases. Moreover, various versions of the model have been uploaded to the EU cancer model repository developed by the TUMOR (Transatlantic Tumour Model Repositories, FP7-ICT-2009-5-247754) European Commission-funded project. The model has been developed in the C++ programming language.

Cette thèse contribue à l’étude de la fiabilité et de la sécurité-innocuité des systèmes informatisés, modélisés par des systèmes à événements discrets. Les principales contributions concernent la théorie des Systèmes de Contrôle (notés C Systems) et l’approche par Monitoring des modèles.Dans la première partie de la thèse, nous étudions la théorie des Systèmes de Contrôle qui combine et étend de façon significative, les systèmes de réécriture de la théorie des langages et le contrôle supervisé. Un système de contrôle est une structure générique qui contient deux composants : le composant contrôlé et le composant contrôlant qui restreint le comportement du composant contrôlé. Les deux composants sont exprimés en utilisant le même formalisme comme des automates ou des grammaires. Nous considérons différentes classes de systèmes de contrôle basés sur différents formalismes comme, par exemple, les automates, les grammaires, ainsi que leurs versions infinies et concurrentes. Ensuite, une application de cette théorie est présentée. Les systèmes de contrôle basés sur les automates de Büchi sont utilisés pour vérifier par model-checking, des propriétés définissant la correction sur des traces d’exécution spécifiées par une assertion de type nevertrace.Dans la seconde partie de la thèse, nous investiguons l’approche de monitoring des modèles dont la théorie des systèmes de contrôle constitue les fondations formelles. Le principe pivot de cette approche est la «spécification de propriétés comme contrôleur». En d’autres termes, pour un système, les exigences fonctionnelles, d’une part, et des propriétés, d’autre part, sont modélisées et implantées séparément, les propriétés spécifiées contrôlant le comportement issu des exigences fonctionnelles. De cette approche découle ainsi deux techniques alternatives, respectivement nommées monitoring de modèle et génération de modèle. Cette approche peut être utilisée de diverses manières pour améliorer la fiabilité et la sécurité-innocuité de divers types de systèmes. Nous présentons quelques applications qui montrent l’intérêt pratique de cette contribution théorique. Tout d’abord, cette approche aide à prendre en compte les évolutions des spécifications des propriétés. En second lieu, elle fournit une base théorique à la sécurité fonctionnelle, popularisée par la norme IEC 61508. En troisième lieu, l’approche peut être utilisée pour formaliser et vérifier l’application de guides de bonnes pratiques ou des règles de modélisation appliquées par exemple pour des modèles UML.Ces résultats constituent les bases pour des études futures de dispositifs plus perfectionnés, et fournissent une nouvelle voie pour s’assurer de la fiabilité et de la sécurité-innocuité des systèmes / This thesis contributes to the study of reliability and safety of computer and software systems which are modeled as discrete event systems. The major contributions include the theory of Control Systems (C Systems) and the model monitoring approach.In the first part of the thesis, we study the theory of control systems which combines and significantly extends regulated rewriting in formal languages theory and supervisory control. The control system is a generic framework, and contains two components: the controlled component and the controlling component that restricts the behavior of the controlled component. The two components are expressed using the same formalism, e.g., automata or grammars. We consider various classes of control systems based on different formalisms, for example, automaton control systems, grammar control systems, and their infinite versions and concurrent variants. After that, an application of the theory is presented. The Büchi automata based control system is used to model and check correctness properties on execution traces specified by nevertrace claims.In the second part of the thesis, we investigate the model monitoring approach whose theoretical foundation is the theory of control systems. The key principle of the approach is “property specifications as controllers”. In other words, the functional requirements and property specification of a system are separately modeled and implemented, and the latter one controls the behavior of the former one. The model monitoring approach contains two alternative techniques, namely model monitoring and model generating. The approach can be applied in several ways to improve reliability and safety of various classes of systems. We present some typical applications to show its strong power. First, the approach provides better support for the change and evolution of property specifications. Second, it provides the theoretical foundation of safety-related systems in the standard IEC 61508 for ensuring the functional validity. Third, it is used to formalize and check guidelines and consistency rules of UML.These results lay out the foundations for further study of more advanced control mechanisms, and provide a new way for ensuring reliability and safety

Cette dissertation explore la carrière de la rencontre manquée Lacanienne dans la littérature canonique américaine du dix-neuvième siècle à travers le prisme de la psychanalyse, la déconstruction, le postmodernisme et le postcolonialisme. Je me concentre particulièrement sur La Lettre Écarlate de Hawthorne et Moby-Dick de Melville, en montrant comment ils sont investis dans l'économie narrative de la rencontre manquée, l'économie de ce qui est au-delà de la symbolisation et l'assimilation. L’introduction examine les contours et les détours historiques, philosophiques et théoriques du concept de la rencontre manquée. Cette dissertation a donc deux objectifs: d'une part, elle tente d'examiner le statut et la fonction de la rencontre manquée dans la littérature américaine du dix-neuvième siècle, et d’autre part, elle explore comment la théorisation de la rencontre manquée pourrait nous aider à aller au-delà de la théorisation binaire qui caractérise les scènes géopolitiques actuelles. Mon premier chapitre sur La Lettre Écarlate de Hawthorne, tente de tracer la carrière du signifiant comme une navette entre l'archive et l'avenir, entre le sujet et l'objet, entre le signifiant et le signifié. Le but de ce chapitre est de rendre compte de la temporalité du signifiant et la temporalité de la subjectivité et d’expliquer comment ils répondent à la temporalité du tuché. En explorant la dimension crypto-temporelle de la rencontre manquée, ce chapitre étudie l'excès de cryptes par la poétique (principalement prosopopée, anasémie, et les tropes d'exhumation). Le deuxième chapitre élabore sur les contours de la rencontre manquée. En adoptant des approches psychanalytiques et déconstructives, ce chapitre négocie la temporalité de la rencontre manquée (la temporalité de l'automaton et de la répétition). En explorant la temporalité narrative (prolepse et analepse) conjointement à la psycho-poétique du double, ce chapitre essaie de dévoiler les vicissitudes de la mélancolie et la “dépression narcissique” dans Moby-Dick (en particulier la répétition d'Achab lors de sa rencontre originelle dénarrée ou jamais racontée avec le cachalot blanc et sa position mélancolique par rapport à l'objet qu'il a perdu). En exposant la nature du trauma comme une rencontre manquée, dont les résidus se manifestent symptomatiquement par la répétition (et le doublement), ce chapitre explique le glissement de la lettre (par l'entremise du supplément et de la différance). Le troisième chapitre élargit la portée de la rencontre manquée pour inclure les Autres de l'Amérique. Le but principal de ce chapitre est d'évaluer les investitures politiques, culturelles, imaginaires et libidinales de la rencontre manquée dans le Réel, le Symbolique nationale des États-Unis et la réalité géopolitique actuelle. Il traite également de la relation ambiguë entre la jouissance et le Symbolique: la manière dont la jouissance anime et régit le Symbolique tout en confondant la distinction entre le Réel et la réalité et en protégeant ses manœuvres excessives. / This dissertation explores the career of the Lacanian missed encounter in canonical nineteenth-century American literature through the lens of psychoanalysis, deconstruction, postmodernism, and postcolonialism. In particular, I concentrate on Hawthorne’s The Scarlet Letter and Melville’s Moby-Dick, showing how they are invested in the narrative economy of the missed encounter, the economy of that which is beyond symbolization and assimilation. The introductory chapter investigates the historical, philosophical, and theoretical contours and detours of the concept of the missed encounter. This dissertation, then, has two goals: on the one hand, it attempts to examine the status and function of the missed encounter in nineteenth-century American literature, and on the other, it explores how theorizing the missed encounter might help us move beyond the binarist theorization that characterizes the current geopolitical scenes. My first chapter on Hawthorne’s The Scarlet Letter attempts to map the career of the signifier as a shuttling between the archive and the future, between the subject and the object, and between the signifier and the signified. The aim of this chapter is to account for the temporality of the signifier and the temporality of subjectivity and how they meet the temporality of the Tuché. By exploring the crypto-temporal dimension of the missed encounter, this chapter studies the excess of crypts through poetics (mainly prosopopeia, anasemia, and tropes of exhumation). The second chapter elaborates the contours of the missed encounter. This chapter approaches, from psychoanalytic and deconstructive viewpoints, the temporality of the missed encounter (the temporality of automaton and repetition). By exploring the narrative temporality (prolepsis and analepsis) in conjunction with the psycho-poetics of the double, this chapter attempts to lay bare the vicissitudes of melancholia and “narcissistic depression” in Moby-Dick (especially Ahab’s repetition of his unnarrated or disnarrated original encounter with the White Whale and his melancholic position in relation to the object he lost). By exposing the nature of trauma as a missed encounter, the residues of which manifest symptomatically through repetition (and doubling), this chapter explains the glissement of the letter (through the work of the supplement and différance). Chapter three broadens the scope of the missed encounter to the Others of America. The main purpose of this chapter is to assess the political, cultural, imaginary, and libidinal investitures of the missed encounter in the Real, the national Symbolic of the United States, and the current geopolitical reality. It also deals with the ambiguous relationship between jouissance and the Symbolic: the way in which jouissance animates and governs the Symbolic, while at the same time it blurs the boundary lines between the Real and reality and protects its excessive maneuvers.