Broadcasting is a fundamental primitive in local area networks (LANs).Operations of many data link protocols, for example, ARP (Address Resolution Protocol) and IGMP (Internet Group Management Protocol), must rely on this LAN primitive. To develop the broadcasting service in mobile ad hoc wireless LANs (WLANs) is a challenge. This is because a mobile ad hoc WLAN is a multi-hop wireless network in which messages may travel along several links from the source to the destination via a certain path. Additionally, there is no fixed network topology because of host moving. Furthermore, the broadcast nature of a radio channel makes a packet be transmitted by a node to be able to reach all neighbors. Therefore, the total number of transmissions (forward nodes) is generally used as the cost criterion for broadcasting. The problem of finding the minimum number of forward nodes in a static radio network is NP-complete. Almost all previous works, therefore, for broadcasting in the WLAN are focusing on finding approximation approaches in a, rather than, environment. In this paper, we propose a novel distributed protocol in WLANs to significantly reduce or eliminate the communication overhead in addition to maintaining positions of neighboring nodes. The important features of our proposed protocol are the adaptability to dynamic network topology change and the localized and parameterless behavior. The reduction in communication overhead for broadcasting operation is measured experimentally. From the simulation results, our protocol not only has the similar performance as the approximation approaches in the static network, but also outperforms existing ones in the adaptability to host moving.

At the present time, wireless sensor networks are becoming more and more  common and energy consumption is a key factor in the deployment and  maintenance of these networks. This thesis compares non-SFN multi-hop and  a single frequency network (SFN) or cooperative diversity algorithms with  respect to the energy consumed by the nodes. Since the nodes have limited  power capacity it is extremely important to have an efficient algorithm. In  addition, the behaviour of the network when SFN is employed must be  studied and advice offered with regards to improvements in order to achieve  preferential results. The effect on the network regarding macro diversity is  positive but, the battery energy consumption is still higher and has a drainage  effect on the network for simple multi-hop. The report will include  background information regarding mobile ad-hoc networks and the  relationship with cooperative diversity. It will also deal with how different  algorithms affect the energy consumption in multi-hop networks. Simulations  will also be presented in Matlab plots for two single frequency network  scenarios against a simple multi-hop regarding node energy during the  network discovery and decline. Results will include comparative figures which  are followed by a discussion concerning the simulation results and its effects.  The applications for wireless sensor networks include area monitoring,  environmental monitoring, data logging, industrial monitoring, agriculture  and the idea can additionally be used for wireless radio and TV distribution.  The simulations have been conducted for cooperative diversity algorithms  (SFN-A and SFN-D) against an algorithm which does not use cooperative  diversity in Matlab. The node energy consumption is compared for both  scenarios with regards to both  network reachability and decline. The node  power is analysed during the reachability of the network from the start to  attaining 100% of the discovered network. During network decline, the  behaviour of the node energy is studied for algorithms with SFN-A, SFN-D  and non SFN.  Also, the number of times node transmission occurs with  regards to  node discovery is also analysed.

This thesis deals with reachability and freeness problems for systems with linear dynamics, including hybrid systems and matrix semigroups. Hybrid systems are a type of dynamical system that exhibit both continuous and discrete dynamic behaviour. Thus they are particularly useful in modelling practical real world systems which can both flow (continuous behaviour) and jump (discrete behaviour). Decision questions for matrix semigroups have attracted a great deal of attention in both the Mathematics and Theoretical Computer Science communities. They can also be used to model applications with only discrete components. For a computational model, the reachability problem asks whether we can reach a target point starting from an initial point, which is a natural question both in theoretical study and for real-world applications. By studying this problem and its variations, we shall prove in a formal mathematical sense that many problems are intractable or even unsolvable. Thus we know when such a problem appears in other areas like Biology, Physics or Chemistry, either the problem itself needs to be simplified, or it should by studied by approximation. In this thesis we concentrate on a specific hybrid system model, called an HPCD, and its variations. The objective of studying this model is twofold: to obtain the most expressive system for which reachability is algorithmically solvable and to explore the simplest system for which it is impossible to solve. For the solvable sub-cases, we shall also study whether reachability is in some sense easy or hard by determining which complexity classes the problem belongs to, such as P, NP(-hard) and PSPACE(-hard). Some undecidable results for matrix semigroups are also shown, which both strengthen our knowledge of the structure of matrix semigroups, and lead to some undecidability results for other models.

Dans le cadre de ce travail de thèse, nous nous sommes intéressés aux relations étroites qu'entretiennent processus moteurs et sensoriels pour déterminer les régions de l'espace où une action directe est possible. Dans ce but, nous nous sommes centrés sur la perception de l' "atteignabilité" d'un objet, c'est-à-dire sur les processus cérébraux qui vont permettre de décider si cet objet pourrait être atteignable ou pas par un mouvement du bras. Pour cela, nous faisons l'hypothèse que ces jugements requièrent la prise en compte de connaissances motrices et corporelles fonctionnelles en plus des informations visuelles extraites de l'environnement. Plus particulièrement, nous proposons qu'ils reposent sur une prédiction des conséquences des actes moteurs potentiels suggérés par cet objet et donc de leur faisabilité à un instant donné. Les études réalisées au cours de cette thèse ont ainsi permis d'écarter l'hypothèse de l'influence de l'effort associé à des actions sur la perception de l'espace atteignable. En revanche, le rôle critique de la prédiction des conséquences sensorimotrices des actions a été mis en évidence, grâce à la démonstration d'une relation forte entre d'une part les correspondances entre la distance visuelle et l'amplitude des mouvements, et d'autre part la distance à laquelle la limite d'atteignabilité est perçue. Les processus d'anticipation sensorimotrice ont également été mis en évidence lors de jugements de perception spatiale en présence de cibles dynamiques, rendant compte du caractère spatio-temporel des mécanismes impliqués. Enfin, une dernière étude a montré l'influence des représentations corporelles et de leur plasticité dans la perception de l'espace péripersonnel, mettant ainsi en lumière l'implication du corps en action dans les jugements perceptifs / In this thesis, we assessed the tight relations between motor and sensory processes used to determine the areas of space in which a direct action is possible. We thus focused on the eprception of the reachability of an object, i.e. on the cerebral processes which allow to decide if an object could be reached or not by moving the arm. To do so, we made the hypothesis that theses judgments require to take into account functional motor and body knowledge, in addition to the visual information extracted from the environment. More specifically, we proposed that these judgments rely on a prediction of the consequences of a potential motor act toward the object, thus on the feasibility of the action at a given moment. Our studies discarded the hypothesis of the role of the effort associated to actions on the perception of reachable space. However, the critical role of predicting the sensorimotor consequences of an action has been showed, by demonstrating the strong relation between on the one hand the correspondence between visual distance and movement amplitude, and on the other hand the distance at which the reachability limit is perceived. Sensorimotor anticipation processes have also been showed in spatial perception involving dynamical targets, showing the spatio-temporal aspect of the involved mechanisms. Finally, our last study showed the influence of body representations and of their plasticity on the perception of peripersonal space, highlighting the implication of the body in action in perceptual judgments

Broadcasting is an essential and effective data propagation mechanism with several important applications, such as route discovery, address resolution and many other network services. Though data broadcasting has many advantages, it can also cause a high degree of contention, collision and congestion, leading to what is known as ¿broadcast storm problems¿. Broadcasting has traditionally been based on the flooding protocol, which simply overflows the network with a high number of rebroadcast messages until these reach all the network nodes. A good probabilistic broadcast protocol can achieve high saved rebroadcast (SRB), low collision and a lower number of relays. When a node is in a sparse region of the network, rebroadcasting is relatively more important while the potential redundancy of rebroadcast is low because there are few neighbours which might rebroadcast the packet unnecessarily. Further, in such a situation, contention over the wireless medium resulting from Redundant broadcasts is not as serious as in scenarios with medium or high density node populations. This research proposes a dynamic probabilistic approach that dynamically fine-tunes the rebroadcast probability according to the number of neighbouring nodes distributed in the ad-hoc network for routing request packets (RREQs) without requiring the assistance of distance measurements or location-determination devices. The main goal of this approach is to reduce the number of rebroadcast packets and collisions in the network. The performance of the proposed approach is investigated and compared with simple AODV, fixed-probabilistic and adjusted-probabilistic flooding [1] schemes using the GloMoSim network simulator and a number of important MANET parameters, including node speed, traffic load and node density under a Random Waypoint (RWP) mobility model. Performance results reveal that the proposed approach is able to achieve higher SRB and less collision as well as a lower number of relays than fixed probabilistic, simple AODV and adjusted-probabilistic flooding. In this research, extensive simulation experiments have been conducted in order to study and analyse the proposed dynamic probabilistic approach under different mobility models. The mobility model is designed to describe the movement pattern of mobile customers, and how their position, velocity and acceleration change over time. In this study, a new enhanced dynamic probabilistic flooding scheme is presented. The rebroadcast probability p will be calculated dynamically and the rebroadcasting decision will be based on the average number of nodes in the ad-hoc networks. The performance of the new enhanced algorithm is evaluated and compared to the simple AODV, fixed-probabilistic, adjusted-probabilistic and dynamic-probabilistic flooding schemes. It is demonstrated that the new algorithm has superior performance characteristics in terms of collision, relays and SRB. Finally, the proposed schemes are tested and evaluated through a set of experiments under different mobility models to demonstrate the relative merits and capabilities of these schemes.

Genome assembly asks to reconstruct an unknown string from many shorter substrings of it. Its hardness stems both from practical issues (size and errors of real data), and from the fact that problem formulations inherently admit multiple solutions. Given these, at their core, most state-of-the-art assemblers are based on finding non-branching paths (unitigs) in an assembly graph. If one defines a genome assembly solution as a closed arc-covering walk of the graph, then unitigs appear in all solutions, being thus safe partial solutions. All such safe walks were recently characterized as omnitigs, leading to the first safe and complete genome assembly algorithm. Even if omnitig finding was improved to quadratic time, it remained open whether the crucial linear-time feature of finding unitigs can be attained with omnitigs. We describe an O(m)-time algorithm to identify all maximal omnitigs of a graph with n nodes and m arcs, notwithstanding the existence of families of graphs with Θ(mn) total maximal omnitig size. This is based on the discovery of a family of walks (macrotigs) with the property that all the non-trivial omnitigs are univocal extensions of subwalks of a macrotig, with two consequences: a linear-time output sensitive algorithm enumerating all maximal omnitigs and a compact O(m) representation of all maximal omnitigs. This safe and complete genome assembly algorithm was followed by other works improving the time bounds, as well as extending the results for different notions of assembly solution. But it remained open whether one can be complete also for models of genome assembly of practical applicability. In this dissertation, we also present a universal framework for obtaining safe and complete algorithms which unify the previous results, while also allowing to characterize different assembly problems. This is based on a novel graph structure, called the hydrostructure of a walk, which highlights the reachability properties of the graph from the perspective of the walk. Almost all of our characterizations are directly adaptable to optimal verification algorithms, and simple enumeration algorithms. Most of these algorithms are also improved to optimality using an incremental computation procedure and a previous optimal algorithm of a specific model.

A major current challenge consists in extending formal methods in order to handle infinite-state systems. Infiniteness stems from the fact that the system operates on unbounded data structure such as stacks, queues, clocks, integers; as well as parameterization. Systems with unbounded data structure are natural models for reasoning about communication protocols, concurrent programs, real-time systems, etc. While parameterized systems are more suitable if the system consists of an arbitrary number of identical processes which is the case for cache coherence protocols, distributed algorithms and so forth. In this thesis, we consider model checking problems for certain fundamental classes of probabilistic infinite-state systems, as well as the verification of safety properties in parameterized systems. First, we consider probabilistic systems with unbounded data structures. In particular, we study probabilistic extensions of Lossy Channel Systems (PLCS), Vector addition Systems with States (PVASS) and Noisy Turing Machine (PNTM). We show how we can describe the semantics of such models by infinite-state Markov chains; and then define certain abstract properties, which allow model checking several qualitative and quantitative problems. Then, we consider parameterized systems and provide a method which allows checking safety for several classes that differ in the topologies (linear or tree) and the semantics (atomic or non-atomic). The method is based on deriving an over-approximation which allows the use of a symbolic backward reachability scheme. For each class, the over-approximation we define guarantees monotonicity of the induced approximate transition system with respect to an appropriate order. This property is convenient in the sense that it preserves upward closedness when computing sets of predecessors.

<p>A major current challenge consists in extending formal methods in order to handle infinite-state systems. Infiniteness stems from the fact that the system operates on unbounded data structure such as stacks, queues, clocks, integers; as well as parameterization.</p><p>Systems with unbounded data structure are natural models for reasoning about communication protocols, concurrent programs, real-time systems, etc. While parameterized systems are more suitable if the system consists of an arbitrary number of identical processes which is the case for cache coherence protocols, distributed algorithms and so forth. </p><p>In this thesis, we consider model checking problems for certain fundamental classes of probabilistic infinite-state systems, as well as the verification of safety properties in parameterized systems. First, we consider probabilistic systems with unbounded data structures. In particular, we study probabilistic extensions of Lossy Channel Systems (PLCS), Vector addition Systems with States (PVASS) and Noisy Turing Machine (PNTM). We show how we can describe the semantics of such models by infinite-state Markov chains; and then define certain abstract properties, which allow model checking several qualitative and quantitative problems.</p><p>Then, we consider parameterized systems and provide a method which allows checking safety for several classes that differ in the topologies (linear or tree) and the semantics (atomic or non-atomic). The method is based on deriving an over-approximation which allows the use of a symbolic backward reachability scheme. For each class, the over-approximation we define guarantees monotonicity of the induced approximate transition system with respect to an appropriate order. This property is convenient in the sense that it preserves upward closedness when computing sets of predecessors.</p>

Le pré-dimensionnement se situe en amont du processus de conception d'un système : à partir d'un ensemble d'exigences, il consiste à déterminer un ensemble de solutions techniques possibles dans un espace de recherche souvent très grand et structuré par une connaissance partielle et incertaine du futur système et de son environnement. Bien avant de penser au choix définitif des composants et au dimensionnement précis du système complet, les concepteurs doivent s'appuyer sur un premier cahier des charges, des modélisations des principaux phénomènes et divers retours d'expériences pour formaliser des contraintes, faire des hypothèses simplificatrices, envisager diverses architectures et faire des choix sur des données imprécises (i.e. caractérisées sous la forme d'intervalles, de listes de valeurs possibles, etc…). Les choix effectués lors du pré-dimensionnement pouvant être très lourds de conséquences sur la suite du développement, il est primordial de détecter au plus tôt d'éventuelles incohérences et de pouvoir vérifier la satisfaction des exigences dans un contexte incertain. Dans ce travail, une méthodologie de vérification des exigences basée sur l'échange de modèles ensemblistes entre donneurs d'ordre et fournisseurs est proposée. Elle s'inscrit dans le cadre d'un paradigme de conception basé sur la réduction d'incertitudes. Après un travail portant sur la modélisation des systèmes mécatroniques, une attention particulière est portée à la prise en compte d'incertitudes déterministes sur des grandeurs continues : des techniques basées sur l'analyse par intervalles telles que la satisfaction de contraintes (CSP), des calculs d'atteignabilité pour des modèles dynamiques de connaissances ou encore l'identification de modèles de comportements ensemblistes sont ainsi mis en œuvre et développés afin d'outiller la méthodologie proposée et contribuer à répondre à l'objectif d'une vérification à couverture garantie. / The pre-sizing takes place upstream to the process of designing a system: from a set of requirements, it consists in determining a set of possible technical solutions in an often very large search space which is structured by the uncertain and partial knowledge available about the future system and its environment. Long before making the final choice and the final sizing of the system components, the designers have to use specifications, models of the main phenomena, and experience feedbacks to formalize some constraints, make simplifying assumptions, consider various architectures and make choices based on imprecise data (i.e. intervals, finite sets of possible values, etc…). The choices made during the pre-sizing process often involving strong commitments for the further developments, it is very important to early detect potential inconsistencies and to verify the satisfaction of the requirements in an uncertain context. In this work, a methodology based on the exchange of set-membership models between principals and suppliers is proposed for the verification of requirements. This methodology is fully consistent with a design paradigm based on the reduction of uncertainties. After a work dedicated to the modeling of mechatronic systems, a special attention is paid to dealing with deterministic uncertainties affecting continuous values: some techniques based on interval analysis such as constraint satisfaction (interval CSP), reachability computations for knowledge dynamic models or identification of set-membership behavioral models are used and developed, so providing a set of tools to implement the proposed methodology and contribute to reach the goal of a verification with a full and guaranteed coverage.

Planejamento sob incerteza vem sendo cada vez mais requisitado em aplicações práticas de diversas áreas que eequerem soluções confiáveis para metas complexas. Em vista disso, nos últimos anos, algumas abordagens baseadas no uso de métodos formais para síntese automática de planos têm sido propostas na área de Planejamento em Inteligência Artificial. Entre essas abordagens, planejamento baseado em verificação de modelos tem se mostrado uma opção bastante promissora; entretanto, conforme observamos, a maioria dos trabalhos dentro dessa abordagem baseia-se em CTL e trata apenas problemas de planejamento para metas de alcançabilidade simples (como aquelas consideradas no planejamento clássico). Nessa tese, introduzimos uma classe de metas de planejamento mais expressivas (metas de alcançabilidade estendidas) e mostramos que, para essa classe de metas, a semântica de CTL não é adequada para formalizar algoritmos de síntese (ou validação) de planos. Como forma de contornar essa limitação, propomos uma nova versão de CTL, que denominamos alpha-CTL. Então, a partir da semântica dessa nova lógica, implementamos um verificador de modelos (Vactl), com base no qual implementamos também um planejador (Pactl) capaz de resolver problemas de planejamento para metas de alcançabilidade estendidas, em ambientes não-determinísticos com observabilidade completa. Finalmente, discutimos como garantir a qualidade das soluções quando dispomos de um modelo de ambiente onde as probabilidades das transições causadas pela execução das ações são conhecidas. / Planning under uncertainty has being increasingly demanded for practical applications in several areas that require reliable solutions for complex goals. In sight of this, in the last few years, some approaches based on formal methods for automatic synthesis of plans have been proposed in the area of Planning in Artificial Intelligence. Among these approaches, planning based on model checking seems to be a very attractive one; however, as we observe, the majority of the works in this approach are mainly based on CTL and deals only with planning problems for simple reachability goals (as those considered in classical planning). In this thesis, we introduce a more expressive class of planning goals (extended reachability goals) and show that, for this class of goals, the CTL\'s semantics is not adequate to formalize algorithms for synthesis (or validation) of plans. As a way to overcome this limitation, we propose a new version of CTL, called alpha-CTL. Then, based on the semantics of this new logic, we implement a model checker (Vactl), based on which we also implement a planner (Pactl) capable of solving planning problems for extended reachability goals, in nondeterministic planning environments with complete observability. Finally, we discuss how to guarantee the quality of the solutions when we have an environment model where the actions transitions probabilities are known.