Models of true concurrency have gained a lot of interest over the last decades as models of concurrent or distributed systems which avoid the well-known problem of state space explosion of the interleaving models. In this thesis, we study such models from two perspectives. Firstly, we study the relation between Petri nets and stable event structures. Petri nets can be considered as one of the most general and perhaps wide-spread models of true concurrency. Event structures on the other hand, are simpler models of true concurrency with explicit causality and conflict relations. Stable event structures expand the class of event structures by allowing events to be enabled in more than one way. While the relation between Petri nets and event structures is well understood, the relation between Petri nets and stable event structures has not been studied explicitly. We define a new and more compact unfoldings of safe Petri nets which is directly translatable to stable event structures. In addition, the notion of complete finite prefix is defined for compact unfoldings, making the existing model checking algorithms applicable to them. We present algorithms for constructing the compact unfoldings and their complete finite prefix. Secondly, we study probabilistic models of true concurrency. We extend the definition of probabilistic event structures as defined by Abbes and Benveniste to a newly defined class of stable event structures, namely, jump-free stable event structures arising from Petri nets (characterised and referred to as net-driven). This requires defining the fundamental concept of branching cells in probabilistic event structures, for jump-free net-driven stable event structures, and by proving the existence of an isomorphism among the branching cells of these systems, we show that the latter benefit from the related results of the former models. We then move on to defining a probabilistic logic over probabilistic event structures (PESL). To our best knowledge, this is the first probabilistic logic of true concurrency. We show examples of expressivity achieved by PESL, which in particular include properties related to synchronisation in the system. This is followed by the model checking algorithm for PESL for finite event structures. Finally, we present a logic over stable event structures (SEL) along with an account of its expressivity and its model checking algorithm for finite stable event structures.

Submitted by Samuel Paulino dos Santos null (samuelp.santos@hotmail.com) on 2018-02-20T18:11:03Z No. of bitstreams: 1 Samuel Dissertacao.pdf: 1684097 bytes, checksum: f23b4c4291af5720876a40f4fad8bc75 (MD5) / Rejected by Elza Mitiko Sato null (elzasato@ibilce.unesp.br), reason: Solicitamos que realize correções na submissão seguindo as orientações abaixo: Problema 01) O arquivo contém 07(sete) páginas em branco, as mesmas devem retiradas. Problema 02) Na Folha de rosto deve constar a financiadora. Ex.: Financiadora: FAPESP – Proc. Problema 03) Na capa e folha de rosto devem constar somente o ano Problema 04) A ficha catalográfica deve ser refeita pois na contagem entraram as páginas em branco.. Na página da Seção de pós-graduação, em Instruções para Qualificação e Defesas de Dissertação e Tese, você pode acessar o modelo das páginas pré-textuais. Lembramos que o arquivo depositado no repositório deve ser igual ao impresso. Agradecemos a compreensão. on 2018-02-21T19:46:00Z (GMT) / Submitted by Samuel Paulino dos Santos null (samuelp.santos@hotmail.com) on 2018-02-22T17:32:54Z No. of bitstreams: 1 Samuel Dissertacao.pdf: 1684097 bytes, checksum: f23b4c4291af5720876a40f4fad8bc75 (MD5) / Rejected by Elza Mitiko Sato null (elzasato@ibilce.unesp.br), reason: Solicitamos que realize correções na submissão seguindo as orientações abaixo: Problema 01) O arquivo contém 07(sete) páginas em branco, as mesmas devem retiradas, pois não pode haver páginas em branco no arquivo. Problema 02) Na Folha de rosto deve constar a financiadora. Ex.: Financiadora: FAPESP – Proc. Problema 03) Na capa e folha de rosto devem constar somente o ano Problema 04) A ficha catalográfica deve ser refeita pois na contagem entraram as páginas em branco. Estamos encaminhando via e-mail o modelo das páginas pré-textuais para que você possa fazer as correções. Lembramos que o arquivo depositado no repositório deve ser igual ao impresso. Agradecemos a compreensão. on 2018-02-22T18:21:23Z (GMT) / Submitted by Samuel Paulino dos Santos null (samuelp.santos@hotmail.com) on 2018-02-22T19:27:58Z No. of bitstreams: 1 Dissertacao-Samuel-CORRECOES.pdf: 1777749 bytes, checksum: 414449c29a5a2c7be6d6e5dc4eb7fbe0 (MD5) / Submitted by Samuel Paulino dos Santos null (samuelp.santos@hotmail.com) on 2018-02-22T19:46:16Z No. of bitstreams: 1 Dissertacao-Samuel-CORRECOES.pdf: 1777749 bytes, checksum: 414449c29a5a2c7be6d6e5dc4eb7fbe0 (MD5) / Approved for entry into archive by Elza Mitiko Sato null (elzasato@ibilce.unesp.br) on 2018-02-23T18:32:09Z (GMT) No. of bitstreams: 1 santos_sp_me_sjrp.pdf: 1777749 bytes, checksum: 414449c29a5a2c7be6d6e5dc4eb7fbe0 (MD5) / Made available in DSpace on 2018-02-23T18:32:09Z (GMT). No. of bitstreams: 1 santos_sp_me_sjrp.pdf: 1777749 bytes, checksum: 414449c29a5a2c7be6d6e5dc4eb7fbe0 (MD5) Previous issue date: 2018-02-08 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP) / Seja S uma superf´ıcie regular em R3 sem pontos parab´olicos. O conjunto focal de S ´e o lugar geom´etrico dos centros das esferas que possuem contato degenerado com S em cada ponto. Tal contato ´e medido pelas singularidades da fam´ılia de func¸˜oes distaˆncia ao quadrado D associada a` S. O conjunto focal ´e uma superf´ıcie, por´em n˜ao necessariamente regular, e pode tamb´em ser visto como o conjunto bifurca¸ca˜o da fam´ılia D. A t´ecnica de associar uma variedade singular X(S) a uma subvariedade suave S do espa¸co euclidiano e descobrir alguns aspectos da geometria de S a partir daqueles de X(S) esta´ na essˆencia das aplica¸co˜es da Teoria das Singularidades `a Geometria Diferencial. Neste trabalho, estudamos os modelos, a menos de difeomorfismos, para o conjunto focal de superf´ıcies imersas em R3 gen´ericas, reunimos os principais resultados sobre a geometria da superf´ıcie focal encontrados na literatura e os apresentamos de forma mais explicativa e com uma linguagem moderna. Al´em disso, mostramos que a superf´ıcie focal pode ser parametrizada por uma frente de onda e utilizamos resultados conhecidos para tais aplica¸co˜es no estudo da geometria da superf´ıcie focal. / Let S be a immersed surface in R3 without parabolic points. The focal set of S is the locus of the centres of spheres that have a degenerate contact with S in each point. This contact is measured by singularities of the family of distance squared function D associated with S. The focal set is a surface, but is not necessarily regular, and it can also be seen as the bifurcation set of the family D. The approach of associating a singular variety X(S) to a smooth submanifold S in an Euclidian space and recover some aspects of the geometry of S from that of X(S) is at the essence of applications of singularity theory to the Differential Geometry. In this work, we study models, unless diffeomorphism, of focal set of the immersed generics surfaces in R3. We have also gathered some results about the geometry of the focal set of the literature and we present them in a more explanatory way and in a modern notation. Furthermore, we show that the focal surface can be parametrized by a wave front and use the known results of such applications in the study of the focal set. / Fapesp: 2016/21226-5

No description available.

This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

On s’intéresse à la dynamique dans un voisinage d’un point fixe d’une fonction antiholomorphe d’une variable. Dans un premier temps, on cherche à décrire et à comprendre l’espace des orbites dans un voisinage d’un point fixe multiple, appelé point parabolique, et à explorer les propriétés géométriques préservées par les changements de coordonnée. En particulier, on résout le problème de classification analytique des points paraboliques. Résoudre ce problème consiste à définir un module de classification complet qui permet de déterminer si deux germes de difféomorphismes antiholomorphes sont analytiquement conjugués dans un voisinage de leur point fixe parabolique. On examine également les applications du module à différents problèmes : i) extraction d’une racine n-ième antiholomorphe, ii) existence d’une courbe analytique invariante sous la dynamique d’un germe antiholomorphe parabolique et iii) centralisateur d’un germe antiholomorphe parabolique. Dans un second temps, on étudie les déploiements génériques d’un point fixe double, soit un point parabolique de codimension 1. Les questions sont de nature similaire, à savoir comprendre l’espace des orbites et les propriétés géométriques des déploiements. Afin de classifier les déploiements génériques, on déploie le module de classification pour les points paraboliques, ce qui permet d’obtenir des conditions nécessaires et suffisantes pour déterminer lorsque deux déploiements génériques sont équivalents. / We are interested in the dynamics in a neighbourhood of a fixed point of an antiholomorphic function of one variable. First, we want to describe and understand the space of orbits in a neighbourhood of a multiple fixed point, called a parabolic point, and to explore the geometric properties preserved by changes of coordinate. In particular, we solve the problem of analytical classification of parabolic fixed points. To solve this problem, we define a complete modulus of classification that allows to determine whether two germs of antiholomorphic diffeomorphisms are analytically conjugate in a neighbourhood of their parabolic fixed point. We also consider the applications of the modulus to different problems: i) extraction of an n-th antiholomorphic root, ii) existence of an invariant real analytical curve under the dynamics of a parabolic antiholomorphic germ, and iii) centraliser of a parabolic antiholomorphic germ. In the second part, we study generic unfoldings of a double fixed point, i.e. a parabolic point of codimension 1. The questions are similar in nature, namely to understand the space of orbits and the geometric properties of unfoldings. In order to classify generic unfoldings, the modulus of classification of the parabolic point is unfolded, thus providing the necessary and sufficient conditions to determine when two generic unfoldings are equivalent.

This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.

Ce travail est consacré à la problématique du suivi des systèmes répartis temps réel. Plus précisément, il se concentre sur les aspects formels de la supervision basée sur des modèles ainsi que sur les problèmes qui lui sont liés. Dans la première partie du travail, nous présentons les propriétés de base de deux modèles formels bien connus utilisés pour la modélisation de systèmes répartis : les réseaux d'automates temporisés et les réseaux de Petri temporels. Nous montrons que le comportement de ces modèles peut être représenté par les procédés dits de branchement. Nous introduisons également les éléments conceptuels clés du système de surveillance. La deuxième partie du travail est consacrée à la question des dépliages avec contraintes qui permettent le suivi des relations causales entre les événements dans un système réparti. Ce type de structure peut reproduire des processus sur la base d'un ensemble totalement non-ordonné d'évènements. Dans notre travail, nous soulevons les problèmes des contraintes de temps et de leurs paramétrages. Les méthodes proposées sont illustrées par des études de cas. La troisième partie du travail traite de la problématique des boucles inobservables qui peuvent résulter de comportements cycliques inobservables des systèmes considérés. Ce type de comportement conduit à un nombre infini d'événements dans les dépliages avec contraintes. La quatrième et dernière partie du travail est consacrée à l'implémentation des méthodes décrites précédemment. / This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

Cette thèse s'intéresse à la modélisation et à l'analyse dessystèmes temps-réel distribués.Un système distribué est constitué de plusieurs composantsqui évoluent de manière partiellement indépendante. Lorsque des actionsexécutables par différentscomposants sont indépendantes, elles sont dites concurrentes.Dans ce cas, elles peuvent être exécutées dans n'importe quel ordre, sanss'influencer, et l'état atteint après ces actions ne dépend pas de leur ordred'exécution.Dans les systèmes temps-réel distribués, les contraintes de temps créent desdépendances complexes entre les composants et les événements qui ont lieu surces composants. Malgré l'omniprésence et l'aspect critique de ces systèmes,beaucoup de leurs propriétés restent encore à étudier.En particulier, la nature distribuée de ces systèmes est souvent laissée de côté.Notre travail s'appuie sur deux formalismesde modélisation: les réseaux de Petri temporels et les réseaux d'automatestemporisés, et est divisé en deux parties.Dans la première partie, nous mettons en évidence les différences entre lessystèmes temporisés centralisés et les systèmes temporisés distribués. Nouscomparons les formalismes principaux et leurs extensions, avec une approcheoriginale qui considère la concurrence.En particulier, nous montrons comment transformer un réseau de Petri temporelen un réseau d'automates temporisés qui a le même comportement distribué.Nous nous intéressons ensuite aux horloges partagées dans lesréseaux d'automates temporisés. Les horloges partagées sont problématiqueslorsque l'on envisage d'implanter ces modèles sur des architecturesdistribuées. Nous montrons comment se passer des horloges partagées, touten préservant le comportement distribué, lorsque cela est possible.Dans la seconde partie, nous nous attachons à formaliser les dépendancesentre les événements dans les représentations en ordre partieldes exécutions des réseaux de Petri (temporels ou non).Les réseaux d'occurrence sont une de ces représentations, et leur structuredonne directement les relations de causalité, conflit et concurrence entreles événements. Cependant, nous montrons que, même dans le cas non temporisé,certaines relations logiques entre les événements nepeuvent pas être directement décrites par ces relations structurelles.Après avoir formalisé les relations logiques en question, nous résolvons leproblème de synthèse suivant: étant donnée une formule logique qui décrit unensemble d'exécutions, construire un réseau d'occurrence associé,quand celui-ci existe.Nous étudions ensuite les relations logiques dans un cadre temporisé simplifié,et montrons que le temps crée des dépendances complexes entre les événements.Ces dépendances peuvent être utilisées pour définir des dépliages canoniques deréseaux de Petri temporels, dans ce cadre simplifié. / This thesis is concerned with the modeling and the analysis of distributedreal-time systems. In distributed systems, components evolve partlyindependently: concurrent actions may be performed in any order, withoutinfluencing each other and the state reached after these actions does notdepends on the order of execution. The time constraints in distributed real-timesystems create complex dependencies between the components and the events thatoccur. So far, distributed real-time systems have not been deeply studied, andin particular the distributed aspect of these systems is often left aside. Thisthesis explores distributed real-time systems. Our work on distributed real-timesystems is based on two formalisms: time Petri nets and networks of timedautomata, and is divided into two parts.In the first part, we highlight the differences between centralized anddistributed timed systems. We compare the main formalisms and their extensions,with a novel approach that focuses on the preservation of concurrency. Inparticular, we show how to translate a time Petri net into a network of timedautomata with the same distributed behavior. We then study a concurrency relatedproblem: shared clocks in networks of timed automata can be problematic when oneconsiders the implementation of a model on a multi-core architecture. We showhow to avoid shared clocks while preserving the distributed behavior, when thisis possible.In the second part, we focus on formalizing the dependencies between events inpartial order representations of the executions of Petri nets and time Petrinets. Occurrence nets is one of these partial order representations, and theirstructure directly provides the causality, conflict and concurrency relationsbetween events. However, we show that, even in the untimed case, some logicaldependencies between event occurrences are not directly described by thesestructural relations. After having formalized these logical dependencies, wesolve the following synthesis problem: from a formula that describes a set ofruns, we build an associated occurrence net. Then we study the logicalrelations in a simplified timed setting and show that time creates complexdependencies between event occurrences. These dependencies can be used to definea canonical unfolding, for this particular timed setting.