1 |
[en] AN APPROACH FOR DEALING WITH INCONSISTENCIES IN DATA MASHUPS / [pt] UMA ABORDAGEM PARA LIDAR COM INCONSISTÊNCIAS EM COMBINAÇÕES DE DADOSEVELINE RUSSO SACRAMENTO FERREIRA 24 May 2016 (has links)
[pt] A grande quantidade de dados disponíveis na Web permite aos usuários
combinarem e rapidamente integrarem dados provenientes de fontes diferentes,
pertencentes ao mesmo domínio de aplicação. Entretanto, combinações de dados
construídas a partir de fontes de dados independentes e heterogêneas podem gerar
inconsistências e, portanto, confundir o usuário que faz uso de tais dados. Esta
tese aborda o problema de criação de uma combinação consistente de dados a
partir de fontes de dados mutuamente inconsistentes. Especificamente, aborda o
problema de testar quando os dados a serem combinados são inconsistentes em
relação a um conjunto pré-definido de restrições. As principais contribuições desta
tese são: (1) a formalização da noção de combinação consistente de dados,
tratando os dados retornados pelas fontes como uma Teoria de Defaults e
considerando uma combinação consistente de dados como uma extensão desta
teoria; (2) um verificador de modelos para uma família de Lógicas de Descrição,
usado para analisar e separar os dados consistentes e inconsistentes, além de testar
a consistência e completude das combinações de dados obtidas; (3) um
procedimento heurístico para computar tais combinações consistentes de dados. / [en] With the amount of data available on the Web, consumers can mashup
and quickly integrate data from different sources belonging to the same
application domain. However, data mashups constructed from independent and
heterogeneous data sources may contain inconsistencies and, therefore, puzzle the
user when observing the data. This thesis addresses the problem of creating a
consistent data mashup from mutually inconsistent data sources. Specifically, it
deals with the problem of testing, when data to be combined is inconsistent with
respect to a predefined set of constraints. The main contributions of this thesis are:
(1) the formalization of the notion of consistent data mashups by treating the data
returned from the data sources as a default theory and considering a consistent
data mashup as an extension of this theory; (2) a model checker for a family of
Description Logics, which analyzes and separates consistent from inconsistent
data and also tests the consistency and completeness of the obtained data
mashups; (3) a heuristic procedure for computing such consistent data mashups.
|
2 |
[en] ANALYSIS OF STRATEGIES USING MODEL CHECKING / [pt] ANÁLISE DE ESTRATÉGIAS UTILIZANDO VERIFICAÇÃO FORMAL DE MODELOSDAVI ROMERO DE VASCONCELOS 29 December 2003 (has links)
[pt] Em métodos formais, uma das abordagens que vem obtendo
sucesso nos últimos anos é a de verificação formal.
Dentro
desta, vem se destacando uma técnica chamada de
verificação
de modelos (model checking), na qual se verifica
automaticamente a validade de propriedades em sistemas
acerca do funcionamento de um sistema. Atualmente, a
verificação de modelos é muito empregada em informática
na
verficação formal de software e hardware, mas tem sido
utilizada em outra áreas, como em matemática e em
economia.
Esta dissertação visa aplicar verificação de modelos a
problemas de economia. O tema da pesquisa seria
delimitado
à Teoria dos Jogos. Algumas inadequações foram
observadas, fazendo-se necessário algumas novas
definições:
uma definição de qualitativa que se utiliza de uma
linguagem lógica denominada de Game Analysis Logic (GAL);
uma linguagem para descrever jogo denominada de RollGame
(Romero - All Game); uma tradução de RollGame na
linguagem de especificação de modelos; uma tradução da
definição de jogo em estrutura de Kripke. Observou-se
ainda
que com a utilização de model checking em jogos
consegue-
se analisar estratégias de jogadores. Uma ferramenta para
automatizar a tradução de RollGame em model checking foi
desenvolvida, chamada de StratAn-RollGame (Strategy
Analyzed using RollGame). Assim, a presente dissertação
demonstrou que de fato é possível utilizar verificação de
modelos em outras areas. / [en] In formal methods, one of the approaches that have been
successful lately is Model Checking, which consists in a
technique to achieve automatic verification about a system
behavior. Nowadays, the model checking is very frequently
employed in computer science to formal verification of
software and hardware, but it is not used in other
knowledge fields, such as mathematics and economics. The
purpose of this research is to apply model checking in
economics problems, using Game Theory. Some inadequacies
have been observed. Therefore, it is necessary to create
new definitions: a generic and qualitative definition of
game that uses one logic language called Game Analysis
Logic (GAL); a new language to describe game called
RollGame (Romero + All Game); a translation from RollGame
to a language of model specification; a translation from
game definition to Kripke structure. It is also been
observed that the use of model checking makes it possible
to analyze players strategies. One tool, called
StratAn-RollGame (Strategy Analyzed using RollGame), makes
the translation from RollGame to model Checking automatic.
Thus, the present research has demonstrated that is
possible indeed to use model checking in other knowledge
fields.
|
3 |
[en] FIRST-ORDER MODAL LOGIC FOR REASONING ABOUT GAMES / [pt] LÓGICA MODAL DE PRIMEIRA-ORDEM PARA RACIOCINAR SOBRE JOGOSDAVI ROMERO DE VASCONCELOS 25 June 2007 (has links)
[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.
|
Page generated in 0.0579 seconds