[pt] Confiança é um aspecto fundamental em sistemas distribuídos abertos de larga-escala. Ela está no núcleo de todas as interações entre as entidades que precisam operar em ambientes com muita incerteza e que se modificam constantemente. Dada essa complexidade, esses componentes, e o sistema resultante, são cada vez mais contextualizados, desenhados e construídos usando técnicas baseadas em agentes. Portanto, confiança é fundamental em um sistema multi-agentes (MAS) aberto. Logo, este trabalho investiga como se ter um modelo de confiança explicitamente em um agente inteligente, que possui crenças (Beliefs), desejos (Desires) e intenções (Intentions), chamado de agente BDI. Ou seja, o agente passa a ter um quarto componente chamado confiança (Trust). Dessa forma, é necessário uma lógica para englobar o conceito de confiança em um MAS BDI aberto. Isso é feito usando uma lógica multi-modal indexada, onde os mundos possíveis que modelam um sistema multi-agentes representam quais agentes estão presentes em um dado instante de tempo. E, para cada uma três componentes originais de um agente BDI, há também uma representação de mundos possíveis, pois as mesmas são tratadas como modalidades. Já a confiança é modelada como sendo um predicado, e não uma modalidade. / [en] Trust is a fundamental concern in large-escale open distributed sytems. It lies at the core of all interactios between the entities that have to operate in such uncertain and constantly changing environmonts. Given the complexity of the interactions, these components, and the ensuing system, are increasingly being conceptualised, desined, and built using agent-based techiques. Therefore, the presence of trust is imperative in a multi-agent system (MAS). Consequently, this work studies how to have a explicit trust model in intelligent agent, which has beliefs, desires and intentions (BDI agent). Thas is, the agent now has a fourth component called Trust. This way, a logic to include the concept of trust in an open BDI MAS is interesting, so that the different aspects of a trust model can be expressed formally and accuratelly. This is achieved by using an indexed multi-modal logic, where the possible worlds which model a multi-agent system represent which agents are in the system in a given moment. Moreover, for each one of the three original components of a BDI agent, where the components represent beliefs, desires and intentions, there is a representation of possible worlds, because these are treated as modalities. However, trust is modelled as predicate, not as a modality.

FREIRE, Cibele Matos. Complexidade descritiva das lógicas de ordem superior com menor ponto fixo e análise de expressividade de algumas lógicas modais. 2010. 54 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2010. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-11T12:35:52Z No. of bitstreams: 1 2010_dis_cmfreire.pdf: 426798 bytes, checksum: 4ad13c09839833ee22b0396a445e8a26 (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-15T12:43:24Z (GMT) No. of bitstreams: 1 2010_dis_cmfreire.pdf: 426798 bytes, checksum: 4ad13c09839833ee22b0396a445e8a26 (MD5) / Made available in DSpace on 2016-07-15T12:43:24Z (GMT). No. of bitstreams: 1 2010_dis_cmfreire.pdf: 426798 bytes, checksum: 4ad13c09839833ee22b0396a445e8a26 (MD5) Previous issue date: 2010 / In Descriptive Complexity, we investigate the use of logics to characterize computational classes os problems through complexity. Since 1974, when Fagin proved that the class NP is captured by existential second-order logic, considered the rst result in this area, other relations between logics and complexity classes have been established. Wellknown results usually involve rst-order logic and its extensions, and complexity classes in polynomial time or space. Some examples are that the rst-order logic extended by the least xed-point operator captures the class P and the second-order logic extended by the transitive closure operator captures the class PSPACE. In this dissertation, we will initially analyze the expressive power of some modal logics with respect to the decision problem REACH and see that is possible to express it with temporal logics CTL and CTL . We will also analyze the combined use of higher-order logics extended by the least xed-point operator and obtain as result that each level of this hierarchy captures each level of the deterministic exponential time hierarchy. As a corollary, we will prove that the hierarchy of HOi(LFP), for i 2, does not collapse, that is, HOi(LFP) HOi+1(LFP). / Em Complexidade Descritiva investigamos o uso de l ogicas para caracterizar classes problemas pelo vi es da complexidade. Desde 1974, quando Fagin provou que NP e capturado pela l ogica existencial de segunda-ordem, considerado o primeiro resultado da area, outras rela c~oes entre l ogicas e classes de complexidade foram estabelecidas. Os resultados mais conhecidos normalmemte envolvem l ogica de primeira-ordem e suas extens~oes, e classes de complexidade polinomiais em tempo ou espa co. Alguns exemplos são que a l ogica de primeira-ordem estendida com o operador de menor ponto xo captura a clsse P e que a l ogica de segunda-ordem estendida com o operador de fecho transitivo captura a classe PSPACE. Nesta dissertação, analisaremos inicialmente a expressividade de algumas l ogicas modais com rela cão ao problema de decisão REACH e veremos que e poss vel express a-lo com as l ogicas temporais CTL e CTL . Analisaremos tamb em o uso combinado de l ogicas de ordem superior com o operador de menor ponto xo e obteremos como resultado que cada n vel dessa hierarquia captura cada n vel da hierarquia determin stica em tempo exponencial. Como corol ario, provamos que a hierarquia de HOi(LFP) não colapsa, ou seja, HOi(LFP) HOi+1(LFP).

[pt] Lógica Proposicional Dinâmica (PDL) é um sistema lógico multi-modal utilizada para especificar e verificar propriedades em programas sequenciais. Redes de Petri são um formalismo largamente utilizado na especificação de sistemas concorrentes e possuem uma interpretação gráfica bastante intuitiva. Neste trabalho apresentam-se extensões da Lógica Proposicional Dinâmica onde os programas são substituídos por Redes de Petri. Define-se uma codificação composicional para as Redes de Petri através de redes básicas, apresentando uma semântica composicional. Uma axiomatização é definida para a qual o sistema é provado ser correto, e completo em relação à semântica proposta. Três Lógicas Dinâmicas são apresentadas: uma para efetuar inferências sobre Redes de Petri Marcadas ordinárias e duas para inferências sobre Redes de Petri Estocásticas marcadas, possibilitando a modelagem de cenários mais complexos. Alguns sistemas dedutivos para essas lógicas são apresentados. A principal vantagem desta abordagem concerne em possibilitar efetuar inferências sobre Redes de Petri [Estocásticas] marcadas sem a necessidade de traduzí-las a outros formalismos. / [en] Propositional Dynamic Logic (PDL) is a multi-modal logic used for specifying and reasoning on sequential programs. Petri Net is a widely used formalism to specify and to analyze concurrent programs with a very intuitive graphical representation. In this work, we propose some extensions of Propositional Dynamic Logic for reasoning about Petri Nets. We define a compositional encoding of Petri Nets from basic nets as terms. Second, we use these terms as PDL programs and provide a compositional semantics to PDL Formulas. Then we present an axiomatization and prove completeness regarding our semantics. Three versions of Dynamic Logics to reasoning with Petri Nets are presented: one of them for ordinary Marked Petri Nets and two for Marked Stochastic Petri Nets yielding to the possibility of model more complex scenarios. Some deductive systems are presented. The main advantage of our approach is that we can reason about [Stochastic] Petri Nets using our Dynamic Logic and we do not need to translate it into other formalisms. Moreover our approach is compositional allowing for construction of complex nets using basic ones.

Em Complexidade Descritiva investigamos o uso de logicas para caracterizar classes problemas pelo vies da complexidade. Desde 1974, quando Fagin provou que NP e capturado pela logica existencial de segunda-ordem, considerado o primeiro resultado da area, outras relac~oes entre logicas e classes de complexidade foram estabelecidas. Os resultados mais conhecidos normalmemte envolvem logica de primeira-ordem e suas extens~oes, e classes de complexidade polinomiais em tempo ou espaco. Alguns exemplos sÃo que a logica de primeira-ordem estendida com o operador de menor ponto xo captura a clsse P e que a logica de segunda-ordem estendida com o operador de fecho transitivo captura a classe PSPACE. Nesta dissertaÃÃo, analisaremos inicialmente a expressividade de algumas logicas modais com relacÃo ao problema de decisÃo REACH e veremos que e possvel expressa-lo com as logicas temporais CTL e CTL. Analisaremos tambem o uso combinado de logicas de ordem superior com o operador de menor ponto xo e obteremos como resultado que cada nvel dessa hierarquia captura cada nvel da hierarquia determinstica em tempo exponencial. Como corolario, provamos que a hierarquia de HOi(LFP) nÃo colapsa, ou seja, HOi(LFP) HOi+1(LFP) / In Descriptive Complexity, we investigate the use of logics to characterize computational classes os problems through complexity. Since 1974, when Fagin proved that the class NP is captured by existential second-order logic, considered the rst result in this area, other relations between logics and complexity classes have been established. Wellknown results usually involve rst-order logic and its extensions, and complexity classes in polynomial time or space. Some examples are that the rst-order logic extended by the least xed-point operator captures the class P and the second-order logic extended by the transitive closure operator captures the class PSPACE. In this dissertation, we will initially analyze the expressive power of some modal logics with respect to the decision problem REACH and see that is possible to express it with temporal logics CTL and CTL. We will also analyze the combined use of higher-order logics extended by the least xed-point operator and obtain as result that each level of this hierarchy captures each level of the deterministic exponential time hierarchy. As a corollary, we will prove that the hierarchy of HOi(LFP), for i 2, does not collapse, that is, HOi(LFP) HOi+1(LFP)

Submitted by guaracy araujo (guaraa3355@gmail.com) on 2016-06-14T19:46:59Z No. of bitstreams: 1 2010_dis_cmfreire.pdf: 426798 bytes, checksum: 4ad13c09839833ee22b0396a445e8a26 (MD5) / Approved for entry into archive by guaracy araujo (guaraa3355@gmail.com) on 2016-06-14T19:48:16Z (GMT) No. of bitstreams: 1 2010_dis_cmfreire.pdf: 426798 bytes, checksum: 4ad13c09839833ee22b0396a445e8a26 (MD5) / Made available in DSpace on 2016-06-14T19:48:16Z (GMT). No. of bitstreams: 1 2010_dis_cmfreire.pdf: 426798 bytes, checksum: 4ad13c09839833ee22b0396a445e8a26 (MD5) Previous issue date: 2010 / In Descriptive Complexity, we investigate the use of logics to characterize computational classes os problems through complexity. Since 1974, when Fagin proved that the class NP is captured by existential second-order logic, considered the rst result in this area, other relations between logics and complexity classes have been established. Wellknown results usually involve rst-order logic and its extensions, and complexity classes in polynomial time or space. Some examples are that the rst-order logic extended by the least xed-point operator captures the class P and the second-order logic extended by the transitive closure operator captures the class PSPACE. In this dissertation, we will initially analyze the expressive power of some modal logics with respect to the decision problem REACH and see that is possible to express it with temporal logics CTL and CTL . We will also analyze the combined use of higher-order logics extended by the least xed-point operator and obtain as result that each level of this hierarchy captures each level of the deterministic exponential time hierarchy. As a corollary, we will prove that the hierarchy of HOi(LFP), for i 2, does not collapse, that is, HOi(LFP) HOi+1(LFP) / Em Complexidade Descritiva investigamos o uso de logicas para caracterizar classes problemas pelo vies da complexidade. Desde 1974, quando Fagin provou que NP e capturado pela logica existencial de segunda-ordem, considerado o primeiro resultado da area, outras relac~oes entre logicas e classes de complexidade foram estabelecidas. Os resultados mais conhecidos normalmemte envolvem logica de primeira-ordem e suas extens~oes, e classes de complexidade polinomiais em tempo ou espaco. Alguns exemplos são que a l ogica de primeira-ordem estendida com o operador de menor ponto xo captura a clsse P e que a l ogica de segunda-ordem estendida com o operador de fecho transitivo captura a classe PSPACE. Nesta dissertação, analisaremos inicialmente a expressividade de algumas l ogicas modais com rela cão ao problema de decisão REACH e veremos que e poss vel express a-lo com as l ogicas temporais CTL e CTL . Analisaremos tamb em o uso combinado de l ogicas de ordem superior com o operador de menor ponto xo e obteremos como resultado que cada n vel dessa hierarquia captura cada n vel da hierarquia determin stica em tempo exponencial. Como corol ario, provamos que a hierarquia de HOi(LFP) não colapsa, ou seja, HOi(LFP) HOi+1(LFP) / FREIRE, Cibele Matos. Complexidade descritiva das lógicas de ordem superior com menor ponto fixo e análise de expressividade de algumas lógicas modais. 2010. 54 f. : Dissertação (mestrado) - Universidade Federal do Ceará, Centro de Ciências, Departamento de Computação, Fortaleza-CE, 2010.

[pt] O termo jogo tem sido utilizado como uma metáfora, em várias áreas do conhecimento, para modelar e analisar situações onde agentes(jogadores) interagem em ambientes compartilhados para a realização de seus objetivos sejam eles individuais ou coletivos. Existem diversos modelos propostos para jogos por diferentes áreas do conhecimento, tais como matemática, ciência da computação, ciência política e social, entre outras. Dentre as diversas formas de modelar jogos examinamos a Teoria dos Jogos e as lógicas para jogos. Neste trabalho apresentamos uma lógica modal de primeira-ordem baseada na lógica CTL, chamada de Game Analysis nalysis Logic, para raciocinar sobre jogos. Relacionamos os principais modelos da Teoria dos Jogos (jogo estratégico, extensivo, e de coalizão) e seus principais conceitos de soluções(equilíbrio de Nash, equilíbrio de subjogo perfeito,e core) aos modelos de GAL e às fórmulas de GAL, respectivamente. Além disso, estudamos as alternativas de quantificação De Re e De Dicto no contexto dos jogos extensivos, caracterizando o conceito de equilíbrio de Nash e equilíbrio de subjogo perfeito de acordo com as alternativas de quantificação. Relacionamos as lógicas Alternating-time lternating-Tempomporal Logic (A ATL) TL) e Coalitional Game Logic (CGL) com a lógica GAL, demonstrando que ambas as lógicas são fragmentos da lógica GAL. Outro resultado deste trabalho é caracterizar uma classe de sistemas multi- agentes,que é baseada na arquitetura de agentes Belief-Desir Desire- Intention(BDI), para a qual existem jogos extensivos e vice-v versa. Como conseqüência, os critérios de racionalidade da Teoria dos Jogos podem ser aplicados diretamente para agentes BDI e vice-versa. Assim, a abordagem deste trabalho pode ser utilizada para analisar sistemas multi-agentes. Do ponto de vista prático, apresentamos um verificador de modelos para a lógica GAL. Diversos estudos de casos são realizados utilizando o verificador de modelos. / [en] Games are abstract models of decision-making in which decision-makers(players)interact in a shared environment to accomplish their goals. Several models have been proposed to analyze a wide variety of applications in many disciplines such as mathematics, computer science and even political and social sciences among others. In this work, we focus on Game Theory and Game Logics. We present a first-order modal logic based on CTL, namely Game Analysis Logic (GAL), to model and reason about out games. The standard models of Game Theory (strategic games, extensiv games and coalition games) as well as their solution concepts (Nash equilibrium, subgame perfect equilibrium and co re),respectively, are express as models dels of GAL and formulas of GAL. Moreover, we study the alternatives of De Re and De Dicto quantification in the context of extensive games. We also show that two of the most representative game logics, namely Alternating-time lternating-Temp empor oral Logic (A ATL) TL) and Coalitional Game Logic (CGL), are fragments of GAL. We also characterize haracterize a class of multi-agent systems, which is based on the architecture Belief-Desire- Intention (BDI), for which there is a somehow equivalent class of games and vice-versa. As a consequence, criteria of rationality for agents can be directly applied to players and vice-versa. Game analysis formal tools can be applied to MAS as well. From a practical poin of view, we provide and develop a model-checker for GAL. In addition, we perform case studies using our prototype.