Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely re exive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as an MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., \"every time the agent does X, it will do Y later\"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS\'s and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or an inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose with respect to the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again. In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into an MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach. / Sistemas multi-agentes (SMAs) podem ser usados para modelar fenômenos que podem ser decompostos em diversos agentes que interagem entre si dentro de um ambiente. Em particular, eles podem ser usados para modelar sociedades humanas e animais, com a finalidade de se analisar as suas propriedades computacionalmente. Esta tese trata da análise automatizada de um tipo particular de tais modelos sociais, a saber, aqueles baseados em princípios behavioristas, o que contrasta com as abordagens cognitivas mais dominante na literatura de SMAs. A principal característica das teorias behaviorista é a ênfase na descrição do comportamento em termos da interação entre agentes e seu ambiente. Desta forma, não apenas ações refl exivas, mas também de aprendizado, motivações, e as emoções podem ser definidas. Mais especificamente, nesta tese apresentamos uma arquitetura de agentes formal (especificada através da Notação Z) baseada na teoria da Análise do Comportamento de B. F. Skinner, e fornecemos uma noção adequada e formal de ambiente (com base na álgebra de processos pi-calculus) para colocar tais agentes juntos em um SMA. Simulações são freqüentemente utilizadas para se analisar SMAs. As técnicas envolvidas tipicamente consistem em simular um SMA diversas vezes, seja para coletar estatísticas, seja para observar o que acontece através de animações. Contudo, simulações podem ser usadas de forma a pertmitir a realização de verificações automatizadas do SMA caso sejam entendidas como explorações de grandes espaços-de-estados. Nesta tese propomos uma técnica de verificação baseada nessa observação, que consiste em simular um SMA de uma forma guiada, a fim de se determinar se uma dada hipótese sobre ele é verdadeira ou não. Para tal fim, tiramos proveito da importância que os ambientes têm nesta tese: a especificação formal do ambiente de um SMA serve para calcular as evoluções possíveis do SMA como um sistema de transição, estabelecendo assim o espaço-de-estados a ser investigado. Neste cálculo, os agentes são levados em conta simulando-os, a fim de determinar, em cada estado do ambiente, quais são suas ações. Cada execução da simulação é uma seqüência de estados nesse espaço-de-estados, que é calculado em tempo de execução, conforme a simulação progride. A hipótese a ser investigada, por sua vez, é dada como um outro sistema de transição, chamado propósito de simulação, o qual define as simulações desejáveis e indesejáveis (e.g., \"sempre que o agente fizer X, ele fará Y depois\"). Em seguida, é possível verificar se o SMA satisfaz o propósito de simulação de acordo com uma série de relações de satisfatibilidade precisamente definidas. Algoritmicamente, isso corresponde a construir um produto síncrono desses dois sistemas de transições (i.e., o do SMA e o do propósito de simulação) em tempo de execução e usá-lo para operar um simulador. Ou seja, o propósito de simulação é usado para guiar o simulador, de modo que somente os estados relevantes sejam efetivamente simulados. Ao terminar, um tal algoritmo pode fornecer um veredito conclusivo ou inconclusivo. Se conclusivo, descobre-se se o SMA satisfaz ou não o propósito de simulação com relação às observações feitas durante as simulações. Se inconclusivo, é possível realizar alguns ajustes e tentar novamente. em resumo, portanto, nesta tese propomos quatro novos elementos: (i) uma arquitetura de agente, (ii) uma especificação formal do ambiente desses agentes, de modo que possam ser compostos em um SMA, (iii) uma estrutura para descrever a propriedade de interesse, a qual chamamos de propósito de simulação, e (iv) uma técnica para se analisar formalmente o SMA resultante com relação a um propósito de simulação. Esses elementos estão implementados em uma ferramenta, denominada Simulador Formalmente Guiado (FGS, do inglês Formally Guided Simulator). Estudos de caso executáveis no FGS são fornecidos para ilustrar a abordagem.

Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely re exive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as an MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., \"every time the agent does X, it will do Y later\"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS\'s and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or an inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose with respect to the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again. In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into an MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach. / Sistemas multi-agentes (SMAs) podem ser usados para modelar fenômenos que podem ser decompostos em diversos agentes que interagem entre si dentro de um ambiente. Em particular, eles podem ser usados para modelar sociedades humanas e animais, com a finalidade de se analisar as suas propriedades computacionalmente. Esta tese trata da análise automatizada de um tipo particular de tais modelos sociais, a saber, aqueles baseados em princípios behavioristas, o que contrasta com as abordagens cognitivas mais dominante na literatura de SMAs. A principal característica das teorias behaviorista é a ênfase na descrição do comportamento em termos da interação entre agentes e seu ambiente. Desta forma, não apenas ações refl exivas, mas também de aprendizado, motivações, e as emoções podem ser definidas. Mais especificamente, nesta tese apresentamos uma arquitetura de agentes formal (especificada através da Notação Z) baseada na teoria da Análise do Comportamento de B. F. Skinner, e fornecemos uma noção adequada e formal de ambiente (com base na álgebra de processos pi-calculus) para colocar tais agentes juntos em um SMA. Simulações são freqüentemente utilizadas para se analisar SMAs. As técnicas envolvidas tipicamente consistem em simular um SMA diversas vezes, seja para coletar estatísticas, seja para observar o que acontece através de animações. Contudo, simulações podem ser usadas de forma a pertmitir a realização de verificações automatizadas do SMA caso sejam entendidas como explorações de grandes espaços-de-estados. Nesta tese propomos uma técnica de verificação baseada nessa observação, que consiste em simular um SMA de uma forma guiada, a fim de se determinar se uma dada hipótese sobre ele é verdadeira ou não. Para tal fim, tiramos proveito da importância que os ambientes têm nesta tese: a especificação formal do ambiente de um SMA serve para calcular as evoluções possíveis do SMA como um sistema de transição, estabelecendo assim o espaço-de-estados a ser investigado. Neste cálculo, os agentes são levados em conta simulando-os, a fim de determinar, em cada estado do ambiente, quais são suas ações. Cada execução da simulação é uma seqüência de estados nesse espaço-de-estados, que é calculado em tempo de execução, conforme a simulação progride. A hipótese a ser investigada, por sua vez, é dada como um outro sistema de transição, chamado propósito de simulação, o qual define as simulações desejáveis e indesejáveis (e.g., \"sempre que o agente fizer X, ele fará Y depois\"). Em seguida, é possível verificar se o SMA satisfaz o propósito de simulação de acordo com uma série de relações de satisfatibilidade precisamente definidas. Algoritmicamente, isso corresponde a construir um produto síncrono desses dois sistemas de transições (i.e., o do SMA e o do propósito de simulação) em tempo de execução e usá-lo para operar um simulador. Ou seja, o propósito de simulação é usado para guiar o simulador, de modo que somente os estados relevantes sejam efetivamente simulados. Ao terminar, um tal algoritmo pode fornecer um veredito conclusivo ou inconclusivo. Se conclusivo, descobre-se se o SMA satisfaz ou não o propósito de simulação com relação às observações feitas durante as simulações. Se inconclusivo, é possível realizar alguns ajustes e tentar novamente. em resumo, portanto, nesta tese propomos quatro novos elementos: (i) uma arquitetura de agente, (ii) uma especificação formal do ambiente desses agentes, de modo que possam ser compostos em um SMA, (iii) uma estrutura para descrever a propriedade de interesse, a qual chamamos de propósito de simulação, e (iv) uma técnica para se analisar formalmente o SMA resultante com relação a um propósito de simulação. Esses elementos estão implementados em uma ferramenta, denominada Simulador Formalmente Guiado (FGS, do inglês Formally Guided Simulator). Estudos de caso executáveis no FGS são fornecidos para ilustrar a abordagem.

Made available in DSpace on 2016-06-02T20:12:15Z (GMT). No. of bitstreams: 1 2974.pdf: 1170859 bytes, checksum: 9277e347f6b6da604f23c3cbae14d73f (MD5) Previous issue date: 2010-03-08 / Universidade Federal de Minas Gerais / Through a critical reading of Skinner s works it was intended to clarify ambiguitiesconcerning scientific and philosophical communities regarding the concepts of rule and verbalstimulus. It was also sought an appropriate statement of creative behavior and thoughtconcepts according to Skinner s Radical Behaviorism. This research had, therefore, a twofoldobjective which was to identify: (1) Skinnerian interpretation of creative behavior and thoughtand (2) Skinner s conception of rule and rule-governed behavior. The steady relation pointedout by B. F. Skinner among the concepts of verbal stimulus, rule and creative behavior and, atthe same time, the controversy spread out by Skinner s commentators and scientists, seeking asufficient and non-ambiguous definition of rule, mainly justifies this study enterprise. Usually, these commentators treat verbal stimulus and rule concepts as identical, being thisidentity a satisfying condition for a definition of the latter as a corollary of the statementsrelating to the Verbal Behavior matter. Moreover, commonly Skinner s work reviewersdefine creative behavior as a variation or unit recombination, which implies supposing thatcreative behavior does not differ from other emissions of operant behavior, since the variationis a ubiquitous characteristic on behavior emissions according to Skinnerian model ofselection by consequences. Part of this study consisted in demonstrating how an explanationof the distinctions existing between verbal stimulus and rule can collaborate with a preciseand productive definition of complex and creative human behavior without losing sight of thebehavioral interpretation object s inherent characteristics. Aiming these goals, the course ofresearch went the following route: (1) identification, in texts by the author, of the conceptsunderlying behavioral interpretation; (2) a systematic analysis of the verbal stimulus concepton its possible behavioral functions and, thus, also its relation to the rule concept; (3) theformulation of an alternate interpretation of creative behavior and rule-governed behaviorbased on Skinnerian explanatory system. Finally, there was a brief foray into formulations ofDewey and Wertheimer on creative behavior and thinking in order to, thereby, outlinepossible convergence on interpretative perspectives brought by the three authors. Among themost important results, it was demonstrated that: (1) simply presume variability does notexplain creative behavior, not only from B. F. Skinner perspective, but neither from JohnDewey s and Max Wertheimer s; (2) four Skinner notions are fundamental in a conceptualrelation between behavioral analysis and interpretation: strength, property, continuum andcomplexity; (3) rule is not defined as verbal stimulus and neither it is a conceptual subcategoryof this kind of stimulation; (4) creative behavior is necessarily complex andorganized, and its structure is functionally defined; (5) rule is one of the creative complexbehavior elements; and (6) rule is a new complex discriminative stimulus with a functionalcomplication typical of a creative emission, although it is not restricted to this behavioralcontext. / Por meio de uma leitura crítica da obra skinneriana, pretendeu-se esclarecer as ambiguidades presentes na comunidade científica e filosófica no que diz respeito aos conceitos de regra e estímulo verbal. Também buscou-se uma formulação satisfatória das concepções de comportamento criativo e pensamento, conforme o comportamentalismo radical de B. F. Skinner. A presente investigação teve, portanto, um duplo objetivo, que consistiu em identificar: (1) a interpretação skinneriana de comportamento criativo e pensamento e (2) a concepção skinneriana de regra e comportamento controlado por regra. A principal justificativa para tal empreendimento está na constante relação que B. F. Skinner apresenta entre os conceitos de estímulo verbal, regra e comportamento criativo e, ao mesmo tempo, na controvérsia, disseminada pelos comentadores e cientistas da área, que caracteriza a busca de uma definição suficiente e sem ambiguidades de "regra". Geralmente, os comentadores apresentam uma identificação entre estímulo verbal e regra que parece satisfazer a definição desse como um corolário dos argumentos envolvidos no tópico "Comportamento Verbal." Por outro lado, é comum que comentadores da obra de B. F. Skinner definam o comportamento criativo como variação ou recombinação de unidades, o que implica em supor que o comportamento criativo não se diferenciaria de outras emissões do comportamento operante,uma vez que a variação é, segundo o modelo skinneriano de seleção pelas consequências,aspecto onipresente das emissões comportamentais. Parte do trabalho consistiu em demonstrar como uma explicitação das distinções que existem entre estímulo verbal e regra podem colaborar com uma definição precisa e produtiva do comportamento humano complexo e criativo, sem perder de vista as características inerentes ao objeto da interpretação comportamental. Visando tais objetivos, o curso da investigação seguiu o seguinte itinerário:(1) identificação, em textos do autor, das noções que fundamentam a interpretação comportamental; (2) análise sistemática do conceito de estímulo verbal em suas possíveis funções comportamentais e, desse modo, também sua relação com o conceito de regra; (3)formulação de uma interpretação alternativa do comportamento criativo e controle por regra baseada no sistema explicativo skinneriano. Por fim, realizou-se uma breve incursão nas formulações de Dewey e Wertheimer sobre o comportamento criativo e o pensamento visando, desse modo, delinear possíveis convergências na perspectiva interpretativa apresentada pelos três autores. Dentre os resultados mais importantes, demonstrou-se que: (1)a simples suposição de variabilidade não explica o comportamento criativo, segundo a perspectiva não somente de B. F. Skinner, mas também de John Dewey e Max Wertheimer;(2) quatro noções skinnerianas são fundamentais na relação conceitual entre análise e interpretação comportamentais: força, propriedade, contínuo e complexidade; (3) regra não se define como estímulo verbal, e nem é uma subcategoria conceitual desse tipo de estímulo; (4) o comportamento criativo é necessariamente complexo e organizado, apresentando uma estrutura funcionalmente definida; (5) regra é um dos elementos do comportamento complexo criativo; e (6) regra é estímulo discriminativo complexo novo com uma complicação funcional característica da emissão criativa, embora não se restrinja a esse contexto comportamental.