The cross-situational word learning paradigm argues that word meanings can be approximated by word-object associations, computed from co-occurrence statistics between words and entities in the world. Lexicon acquisition involves simultaneously guessing (1) which objects are being talked about (the ”meaning”) and (2) which words relate to those objects. However, most modeling work focuses on acquiring meanings for isolated words, largely neglecting relationships between words or physical entities, which can play an important role in learning. Semantic parsing, on the other hand, aims to learn a mapping between entire utterances and compositional meaning representations where such relations are central. The focus is the mapping between meaning and words, while utterance meanings are treated as observed quantities. Here, we extend the joint inference problem of word learning to account for compositional meanings by incorporating a semantic parsing model for relating utterances to non-linguistic context. Integrating semantic parsing and word learning permits us to explore the impact of word-word and concept-concept relations. The result is a joint-inference problem inherited from the word learning setting where we must simultaneously learn utterance-level and individual word meanings, only now we also contend with the many possible relationships between concepts in the meaning and words in the sentence. To simplify design, we factorize the model into separate modules, one for each of the world, the meaning, and the words, and merge them into a single synchronous grammar for joint inference. There are three main contributions. First, we introduce a novel word learning model and accompanying semantic parser. Second, we produce a corpus which allows us to demonstrate the importance of structure in word learning. Finally, we also present a number of technical innovations required for implementing such a model.

This paper explores graph grammar and constructive solutions for settlement generation in Minecraft. It uses graph grammar to flatten parts of the surface in order to increase the space for the buildings. Buildings are then generated with a constructive solution that follows a step-by-step model where different parts of the building are created in a certain order. Different parts include the shape of the foundation itself, the walls, the roof and the furniture. The algorithm picks which blocks to use on different parts of the house through an object called district palette. The buildings are divided up into areas called districts, where all the houses within the district follow a similar aesthetic style. The goal is to compare our solution with existing solutions from the Generative Design in Minecraft (GDMC) competition to see how it holds up against the other submissions. To evaluate, a user study was performed where each jury has to score four criteria: adaptivity, functionality, evocative narrative, and aesthetics. The results show that the solution had a strong aesthetics but fell behind in adaptivity, functionality, and evocative narrative. Most of it was due to not being able to generate different structures, and not cleaning up the trees around the buildings and the roads.

There are different phases in any design activity, one of them being concept generation. Research in automating the conceptual design process in planar mechanisms is always challenging due to the existence of many different elements and their endless combinations. There may be instances where designers arrive at a concept without considering all the alternatives. Computational synthesis aims to arrive at a design by considering the entire space of valid designs. Different researchers have adopted various methods to automate the design process that includes existence of similar graph grammar approaches. But few methods replicate the way humans’ design. An attempt is being made in the thesis in this direction and as a first step, we focus on representing and evaluating planar mechanisms designed using graph grammars. Graph grammars have been used to represent planar mechanisms but there are disadvantages in the methods currently available. This is due to the lack of information in understanding the details of a mechanism represented by the graph since the graphs do not include information about the type of joints and components such as revolute links, prismatic blocks, gears and cams. In order to overcome drawbacks in the existing methods, a novel representation scheme has been developed. In this method, labels and x, y position information in the nodes are used to represent the different mechanism types. A set of sixteen grammar rules that construct different mechanisms from the basic seed is developed, which implicitly represents a tree of candidate solutions. The scheme is tested to determine its capability in capturing the entire set of feasible planar mechanisms of one degree of freedom including Stephenson and double butterfly linkages. In addition to the representation, another important consideration is the need for an accurate and generalized evaluator for kinematic analysis of mechanisms which, given the lack of information, may not be possible with current design automation schemes. The approach employed for analysis is purely kinematic and hence the instantaneous center of rotation method is employed in this research. The velocities of pivots and links are obtained using the instant center method. Once velocities are determined, the vector polygon approach is used to obtain accelerations and geometrical intersection to determine positions of pivots. The graph grammar based analysis module is implemented in an existing object-oriented grammar framework and the results have found this to be superior to or equivalent to existing commercial packages such as Working Model and SAM for topologies consisting of four-bar loop chain with single degree of freedom. / text

La vérification de propriétés de sûreté des logiciels distribués basés sur des canaux fifo non bornés et fiables mène directement au model checking de systèmes infinis. Nous introduisons la famille des (q)ueueing (c)oncurrent (p)rocesses (QCP) composant des systèmes de transitions locaux, par exemple des automates finis/à pile, qui communiquent entre eux par des files fifo. Le problème d'atteignabilité des états de contrôle est indécidable pour des automates communicants et des automates à plusieurs piles, et par conséquent pour QCP.Nous présentons deux solutions pour contourner ce résultat négatif :Primo, une sur-approximation basée sur l'approche abstraire-tester-raffiner qui s'appuie sur notre nouveau concept de raffinement par chemin. Cette approche mène à permettre d'écrire un semi-algorithme du type CEGAR qui est implémenté avec des QDD et réalisé dans le framework McScM dont le banc d'essai conclut notre présentation.Secundo, nous proposons des restrictions pour les QCP à des piles locales pour démêler l'interaction causale entre les données locales (la pile), et la synchronisation globale. Nous montrons qu'en supposant qu'il existe une borne existentielle sur les exécutions et qu'en ajoutant une condition sur l'architecture, qui entrave la synchronisation de deux piles, on arrive à une réponse positive pour le problème de décidabilité de l'atteignabilité qui est EXPTime-complet (et qui généralise des résultats déjà connus). La construction de base repose sur une simulation du système par un automate à une pile équivalent du point de vue de l'atteignabilité --- sous-jacente, nos deux restrictions restreignent les exécutions à une forme hors-contexte. Nous montrons aussi que ces contraintes apparaissent souvent dans des situations ``concrètes''et qu'elles sont moins restrictives que celles actuellement connues. Une autre possibilité pour arriver à une solution pratiquement utilisable consiste à supposer une borne du problème de décidabilité : nous montrons que l'atteignabilité par un nombre borné de phases est décidable par un algorithme constructif qui est 2EXPTime-complet.Finalement, nous montrons qu'élargir les résultats positifs ci-dessus à la vérification de la logique linéaire temporelle demande soit de sacrifier l'expressivité de la logique soit d'ajouter des restrictions assez fortes aux QCP --- deux restrictions qui rendent cette approche inutilisable en pratique. En réutilisant notre argument de type ``hors-contexte'', nous représentons l'ordre partiel sous-jacent aux exécutions par des grammaires hypergraphes. Cela nous permet de bénéficier de résultats connus concertant le model checking des formules de la logique MSO sur les graphes (avec largeur arborescente bornée), et d'arriver aux premiers résultats concernant la vérification des propriétés sur l'ordre partiel des automates (à pile) communicants. / The safety verification of distributed programs, that are based on reliable, unbounded fifo communication, leads in a straight line to model checking of infinite state systems. We introduce the family of (q)ueueing (c)oncurrent (p)rocesses (QCP): local transition systems, e.g., (pushdown-)automata, that are globally communicating over fifo channels. QCP inherits thus the known negative answers to the control-state reachability question from its members, above all from communicating automata and multi-stack pushdown systems. A feasible resolution of this question is, however, the corner stone for safety verification.We present two solutions to this intricacy: first, an over-approximation in the form of an abstract-check-refine algorithm on top of our novel notion of path invariant based refinement. This leads to a \cegar semi-algorithm that is implemented with the help of QDD and realized in a small software framework (McScM); the latter is benchmarked on a series ofsmall example protocols. Second, we propose restrictions for QCP with local pushdowns that untangle the causal interaction of local data, i.e., thestack, and global synchronization. We prove that an existential boundedness condition on runs together with an architectural restriction, that impedes the synchronization of two pushdowns, is sufficient and leads to an EXPTime-complete decision procedure (thus subsuming and generalizing known results). The underlying construction relies on a control-state reachability equivalent simulation on a single pushdown automaton, i.e., the context-freeness of the runs under the previous restrictions. We can demonstrate that our constraints arise ``naturally'' in certain classes of practical situations and are less restrictive than currently known ones. Another possibility to gain a practicable solution to safety verification involves limiting the decision question itself: we show that bounded phase reachability is decidable by a constructive algorithms in 2ExpTime, which is complete.Finally, trying to directly extend the previous positive results to model checking of linear temporal logic is not possible withouteither sacrificing expressivity or adding strong restrictions (i.e., that are not usable in practice). However, we can lift our context-freeness argument via hyperedge replacement grammars to graph-like representation of the partial order underlying each run of a QCP. Thus, we can directly apply the well-known results on MSO model checking on graphs (of bounded treewidth) to our setting and derive first results on verifying partial order properties on communicating (pushdown-) automata.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

No description available.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

No description available.

L’Internet des Objets (IoT) est déjà omniprésent aujourd’hui : domotique, bâtiments connectés ou ville intelligente, beaucoup d’initiatives et d’innovations sont en cours et à venir. Le nombre d’objets connectés ne cesse de croître à tel point que des milliards d’objets sont attendus dans un futur proche.L’approche de cette thèse met en place un système de gestion autonomique pour des systèmes à base d’objets connectés, en les combinant avec d’autres services comme par exemple des services météo accessibles sur internet. Les modèles proposés permettent une prise de décision autonome basée sur l’analyse d’évènements et la planification d’actions exécutées automatiquement. Des paramètres comme le temps d’exécution ou l’énergie consommée sont aussi considérés afin d’optimiser les choix d’actions à effectuer et de services utilisés. Un prototype concret a été réalisé dans un scénario de ville intelligente et de bus connectés dans le projet investissement d'avenir S2C2. / The Internet of Things (IoT) is already everywhere today: home automation, connected buildings or smart city, many initiatives and innovations are ongoing and yet to come. The number of connected objects continues to grow to the point that billions of objects are expected in the near future.The approach of this thesis sets up an autonomic management architecture for systems based on connected objects, combining them with other services such as weather services accessible on the Internet. The proposed models enable an autonomous decision making based on the analysis of events and the planning of actions executed automatically. Parameters such as execution time or consumed energy are also considered in order to optimize the choices of actions to be performed and of services used. A concrete prototype was realized in a smart city scenario with connected buses in the investment for future project: S2C2.