Mogavero, Fabio
(2010)
Logics in Computer Science.
[Tesi di dottorato]
(Unpublished)
| Item Type: |
Tesi di dottorato
|
| Resource language: |
English |
| Title: |
Logics in Computer Science |
| Creators: |
| Creators | Email |
|---|
| Mogavero, Fabio | fm@fabiomogavero.com |
|
| Date: |
30 November 2010 |
| Number of Pages: |
132 |
| Institution: |
Università degli Studi di Napoli Federico II |
| Department: |
Matematica e applicazioni "Renato Caccioppoli" |
| Scuola di dottorato: |
Scienze matematiche e informatiche |
| Dottorato: |
Scienze computazionali e informatiche |
| Ciclo di dottorato: |
23 |
| Coordinatore del Corso di dottorato: |
| nome | email |
|---|
| Ricciardi, Luigi Maria | luigi.ricciardi@unina.it |
|
| Tutor: |
| nome | email |
|---|
| De Luca, Aldo | aldo.deluca@unina.it | | Murano, Aniello | murano@na.infn.it |
|
| Date: |
30 November 2010 |
| Number of Pages: |
132 |
| Keywords: |
Branching-Time Temporal Logics, Satisfiability, Model-Checking, Game Theory, Formal methods |
| Settori scientifico-disciplinari del MIUR: |
Area 01 - Scienze matematiche e informatiche > INF/01 - Informatica
Area 01 - Scienze matematiche e informatiche > MAT/01 - Logica matematica |
[error in script]
[error in script]
| Date Deposited: |
02 Dec 2010 15:40 |
| Last Modified: |
30 Apr 2014 19:44 |
| URI: |
http://www.fedoa.unina.it/id/eprint/8069 |
| DOI: |
10.6092/UNINA/FEDOA/8069 |
Collection description
In this thesis, we introduce and examine four new temporal logic formalisms that
can be used as specification languages for the automated verification of the
reliability of hardware and software designs with respect to a desired behavior.
The work is organized in two parts. In the first one, we reason about two logics
for computations, GCTL* and MCTL*, which are useful to describe a correct
execution of monolithic closed systems. In the second one, instead, we focus on
two logics for strategies, SL and mATL*, which are useful to formalize several
interesting properties about interactive plays in multi-entities systems modeled
as multi-agent games.
In the “Logics for Computations” part, we first study the immersion of the idea
of graded quantifications into the temporal-logic framework. In first order
logic, existential and universal quantifiers express the concepts of the
existence of at least one individual object satisfying a formula, or that all
individual objects satisfy a formula. In other logics, these quantifiers have
been generalized to express that, for a given non-negative integer n, at least n
or all but n individuals satisfy a particular formula. Here, we consider GCTL, a
temporal logic with graded path quantifiers, which allows to describe properties
like “there exist at least n different classes of computational fluxes in which a
system reaches a predetermined state”, where the classes over paths are computed
by means of a predetermined equivalence relation. More precisely, we uniformly
extend the classic concept of graded quantifiers from states to paths, through
the use of a concept of path equivalence with respect to a given path formula.
About this logic, in particular, we study the expressiveness and succinctness
relationships with respect to GµCalculus and the complexity of the
satisfiability problem, which results to be ExpTime-Complete. This research is
partially based on the works [BMM09] “Graded Computation Tree Logic” and [BMM10]
“Graded Computation Tree Logic with Binary Coding” published, respectively, in
the proceedings of the “IEEE Symposium on Logic in Computer Science, 2009” and
“EACSL Annual Conference on Computer Science Logic, 2010”. Preliminary results
can be also found in [Mog07].
Furthermore, we consider special quantifiers over substructures, which allow to
select, using parametric criteria, small critical parts of a system to be
successively verified. In literature, there are some attempts to define a logic
that allows to modify the underlying structure under exam and then to verify on
it some assigned property. However, as far as we know, none of them is able to
select minimal submodels of a given property describing the criteria on which
then execute the verification process. Here, we base our work on the search of a
new operator that merges the concept of quantifiers on structures with that one
derived by a generalization of the concept of pruning. The results of this work,
is a class of three different extensions of CTL* with minimal model quantifiers,
which we name MCTL*. Regarding these logics, we study several reductions among
them, as well as the satisfiability problem that we prove to be highly
undecidability, i.e., Σ_1^1-Hard, for two out of the three cases. This research
is partially based on the work [MM09] “Branching-Time Temporal Logics with
Minimal Model Quantifiers” published in the proceedings of the “International
Conference on Developments in Language Theory, 2009”.
In the “Logics for Strategies” part, we first study the problem of defining a
new specification language through which it is possible to express several
important properties of multi-entities systems that are neither expressible
using classical monolithic temporal logics, such as CTL*, nor using
two-agent-teams temporal logics, such as ATL*. In literature, we can found some
proposal of logics that try to achieve this goal, but unfortunately, none of
them succeeds completely on all the aspects. Among them, one of the most
important attempts is CHP-SL, a logics in which one can use variables over
strategies. However, this logic has a deep weakness, since it does not allow to
describe games with more than two players and even two-players concurrent games.
Here, we introduce SL, a logic with a syntax similar in some aspects to the
first order logic, in which the strategies of the agent building the game are
treated as first order objects on which we can quantify. This logic generalizes
CHP-SL, by allowing the specification of the correct behavior of multi-agent
concurrent games. In SL, for example, we are able to express very complex but
useful Nash equilibria that are not expressible with CHP-SL. We enlighten that
Nash equilibrium is one of the most important concepts in game theory. For the
introduced logic, we solve two problems left open in the work on CHP-SL.
Precisely, we show that the related model-checking problem is 2ExpTime-Complete,
thus not harder of the same problem for several subsumed logics, while we prove
that its satisfiability problem is highly undecidable, i.e., Σ_1^1-Hard. This
research is partially based on the work [MMV10a] “Reasoning About Strategies”
published in the proceedings of the “IARCS Annual Conference on Foundations of
Software Technology and Theoretical Computer Science, 2010”.
Finally, we consider the concept of relentful strategic reasoning, i.e., a
formalism that expresses the ability of a strategy to be used not only to
achieve a first given goal, but also to change its final goal in dependence of
the history of the play. In the context of planning, memoryful quantification,
i.e., quantification over computations that does not lose information about the
past along the time, is one of the principal way to express the fact that a
system is able to achieve a desired result, and shift to a different goal if
some event happens. However, this kind of quantification was not considered
before in the context of multi-agent planning. Here, we introduce mATL*, a
fusion of the classic alternating temporal logic ATL* with memoryful
quantification, with the aim of covering the previous idea. About this logics,
we prove that, although it is equivalent to ATL*, it is exponentially more
succinct. Nevertheless, we prove that both the model-checking and the
satisfiability problems remain 2ExpTime-Complete, as for ATL*. This research
is partially based on the work [MMV10b] “Relentful Strategic Reasoning in
Alternating-Time Temporal Logic” published in the proceedings of the
“International Conference on Logic for Programming Artificial Intelligence and
Reasoning, 2010”.
Downloads per month over past year
Actions (login required)
 |
View Item |
