Conference articles
2010
[6]
Relentful Strategic Reasoning in Alternating-Time Temporal Logic
Temporal logics are a well investigated formalism for the specification verification, and synthesis of
reactive systems.
Within this family, alternating temporal logic, ATL*, has been introduced as a useful generalization of
classical linear- and branching-time temporal logics by allowing temporal operators to be indexed by
coalitions of agents.
Classically, temporal logics are memoryless: once a path in the computation tree is quantified at a given
node, the computation that has led to that node is forgotten.
Recently, mCTL* has been defined as a memoryful variant of CTL*, where path quantification is memoryful.
In the context of multi-agent planning, memoryful quantification enables agents to "relent" and change their
goals and strategies depending on their past history.
In this paper, we define mATL*, a memoryful extension of ATL*, in which a formula is satisfied at a certain
node of a path by taking into account both the future and the past.
We study the expressive power of mATL*, its succinctness, as well as related decision problems.
We also investigate the relationship between memoryful quantification and past modalities and show their
equivalence.
We show that both the memoryful and the past extensions come without any computational price; indeed, we
prove that both the satisfiability and the model-checking problems are 2ExpTime-Complete, as they are for
ATL*.
16th International Conference on Logic for Programming Artificial Intelligence and Reasoning
(LPAR 2010),
Dakar, Senegal, April 25 - May 1, 2010, Springer-Verlag.
(Joint work with Aniello Murano and
Moshe Y. Vardi.)
[To appear in proceedings.]
[Abstract]
[5]
Quantitative Fairness Games
We consider two-player games played on finite colored graphs where the goal is the construction of an
infinite path with one of the following frequency-related properties: (i) all colors occur with the same
asymptotic frequency, (ii) there is a constant that bounds the difference between the occurrences of any two
colors for all prefixes of the path, or (iii) all colors occur with a fixed asymptotic frequency.
These properties can be viewed as quantitative refinements of the classical notion of fair path in a
concurrent system, whose simplest form checks whether all colors occur infinitely often.
In particular, the first two properties enforce equal treatment of all the jobs involved in the system,
while the third one represents a way to assign a given priority to each job.
For all the above goals, we show that the problem of checking whether there exists a winning strategy is
Co-NP-Complete.
8th Workshop on Quantitative Aspects of Programming Languages
(QAPL 2010),
Paphos, Cyprus, March 27-28, 2010, EPTCS.
(Joint work with Alessandro Bianco,
Marco Faella, and
Aniello Murano.)
[To appear in proceedings.]
[Abstract]
2009
[4]
Balanced Paths in Colored Graphs
Given a finite graph whose edges are labeled with integer colors, we study the problem of determining
whether there is an infinite path where either (i) all colors occur with the same asymptotic frequency, or
(ii) there is a constant which bounds the difference between the occurrences of any two colors for all
prefixes of the path.
These two notions can be viewed as refinements of the classical notion of fair path, whose simplest form
checks whether all colors occur infinitely often.
Our notions provide stronger criteria, particularly suitable for scheduling applications based on a
coarse-grained model of the jobs involved.
We show that both problems are solvable in polynomial time, by reducing them to the feasibility of a linear
program.
34th International Symposium on Mathematical Foundation of Computer Science
(MFCS 2009),
Novy Smokovec, High Tatras, Slovakia, August 24-28, 2009, Springer-Verlag,
LNCS 5734,
ISBN 978-3-642-03815-0,
pages
149-161.
(Joint work with Alessandro Bianco,
Marco Faella, and
Aniello Murano.)
[MFCS'09 acceptance rate: 56/148 ~ 37.84%.]
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[TarGz]
[3]
Graded Computation Tree Logic
In modal logics, graded (world) modalities have been deeply investigated as a useful framework for
generalizing standard existential and universal modalities in such a way that they can express statements
about a given number of immediately accessible worlds.
These modalities have been recently investigated with respect to the mu-Calculus, which have provided
succinctness, without affecting the satisfiability of the extended logic, i.e., it remains solvable in
ExpTime.
A natural question that arises is how logics that allow reasoning about paths could be effected by
considering graded path modalities.
In this paper, we investigate this question in the case of the branching-time temporal logic CTL (GCTL,
for short).
We prove that, although GCTL is more expressive than CTL, the satisfiability problem for GCTL remains
solvable in ExpTime.
This result is obtained by exploiting an automata-theoretic approach.
In particular, we introduce the class of partitioning alternating Büchi tree automata and show that the
emptiness problems for them is ExpTime-Complete.
The satisfiability result turns even more interesting as we show that GCTL is exponentially more succinct
than graded mu-Calculus.
24th IEEE Symposium on Logic in Computer Science
(LICS 2009),
Los Angeles, California, USA, August 11-14, 2009, IEEE Computer Society,
LICS,
ISBN
978-0-7695-3746-7,
pages 342-351.
(Joint work with Alessandro Bianco and
Aniello Murano.)
[LICS'09 acceptance rate: 39/130 ~
30.00%.]
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[Talk] -
[TarGz]
[2]
Branching-Time Temporal Logics with Minimal Model Quantifiers
Temporal logics are a well investigated formalism for the specification and verification of reactive
systems.
Using formal verification techniques, we can ensure the correctness of a system with respect to its desired
behavior (specification), by verifying whether a model of the system satisfies a temporal logic formula
modeling the specification.
From a practical point of view, a very challenging issue in using temporal logic in formal verification is
to come out with techniques that automatically allow to select small critical parts of the system to be
successively verified.
Another challenging issue is to extend the expressiveness of classical temporal logics, in order to model
more complex specifications.
In this paper, we address both issues by extending the classical branching-time temporal logic CTL* with
minimal model quantifiers (MCTL*).
These quantifiers allow to extract, from a model, minimal submodels on which we check the specification
(also given by an MCTL* formula).
We show that MCTL* is strictly more expressive than CTL*.
Nevertheless, we prove that the model checking problem for MCTL* remains decidable and in particular in
PSpace.
Moreover, differently from CTL*, we show that MCTL* does not have the tree model property, is not
bisimulation-invariant and is sensible to unwinding.
As far as the satisfiability concerns, we prove that MCTL* is highly undecidable.
We further investigate the model checking and satisfiability problems for MCTL* sublogics, such as MPML,
MCTL, and MCTL+, for which we obtain interesting results.
Among the others, we show that MPML retains the finite model property and the decidability of the
satisfiability problem.
13th International Conference on Developments in Language Theory
(DLT 2009),
Stuttgart, Germany, June 30 - July 3, 2009, Springer-Verlag,
LNCS 5583,
ISBN 978-3-642-02736-9,
pages
396-409.
(Joint work with Aniello Murano.)
[DLT'09 acceptance rate: 35/70 ~ 50.00%.]
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[Talk] -
[TarGz]
2008
[1]
Comparing Rule-Based Policies
Policy comparison is useful for a variety of applications, including policy validation and policy-aware
service selection.
While policy comparison is somewhat natural for policy languages based on description logics, it becomes
rather difficult for rule-based policies.
When policies have recursive rules, the problem is in general undecidable.
Still most policies require some form of recursion to model — say — subject and object hierarchies, and
certificate chains.
In this paper, we show how policies with recursion can be compared by adapting query optimization techniques
developed for the relational algebra.
We prove soundness and completeness of our method, discuss the compatibility of the restrictive assumptions
we need w.r.t. our reference application scenarios, and report the results of a preliminary set of
experiments to prove the practical applicability of our approach.
9th IEEE Workshop on Policies for Distributed Systems and Networks
(POLICY 2008),
Palisades, NewYork, USA, June 2-4, 2008, IEEE Computer Society,
POLICY,
ISBN
978-0-7695-3133-5,
pages 11-18.
(Joint work with Piero A. Bonatti.)
[POLICY'08 acceptance rate: 17/74 ~
22.97%.]
[Abstract] -
[Full text] -
[BibTeX] -
[TarGz]
Workshop notes
2009
[1]
Balance Games on Colored Graphs
2nd Workshop of the ESF Networking Programme on Games for Design and Verification
(GAMES 2009),
Udine, Italy, September 14-17, 2009.
(Joint work with Alessandro Bianco,
Marco Faella, and
Aniello Murano.)
[Text] -
[Talk] -
[TarGz]
Technical reports
2008
[2]
Graded Computation Tree Logic
In modal logics, graded (world) modalities have been deeply investigated as a useful framework for
generalizing standard existential and universal modalities, in such a way they can express statements about
a given number of immediately accessible worlds.
These modalities have been recently investigated with respect to the mu-calculus, which have provided
succinctness, without affecting the satisfiability of the extended logic, i.e., it remains solvable in
ExpTime.
A natural question that arises is how logics that allow reasoning about paths could be effected by
considering graded path modalities.
In this paper, we investigate this question in the case of the branching-time temporal logic CTL and we call
the extended logic GCTL, for short.
We show several results for this logic.
Among the others we prove that, although GCTL is more expressive than CTL, the satisfiability problem for
GCTL remains solvable in ExpTime.
This result is obtained by exploiting an automata-theoretic approach.
In particular, we introduce the class of partitioning alternating Büchi tree automata and show that the
emptiness problems for them is ExpTime-Complete.
Report n° 21, Department of Mathematics and Applications "R. Caccioppoli",
University of Naples "Federico II", Italy, April, 2008.
(Joint work with Alessandro Bianco and
Aniello Murano.)
[Abstract] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
Actually, this is an update of the original technical report n° 21 of April 2008.
Note:
A fully reviewed version of this work is appeared in LICS 2009.
[1]
Formal Policy Analysis Techniques for Comparison and Validation
Policy comparison is useful for a variety of applications, including policy validation and policy-aware
service selection.
While policy comparison is somewhat natural for policy languages based on description logics, it becomes
rather difficult for rule-based policies.
When the policy has recursive rules the problem is in general undecidable.
Still most policies require some form of recursion to model subject and object hierarchies, and certificate
chains.
In this paper, we show how policies with recursion can be compared by adapting query optimization techniques
developed for the relational algebra.
We prove soundness and completeness of our method, discuss the compatibility of the restrictive assumptions
we need w.r.t. our reference application scenarios, and report the results of a preliminary set of
experiments to prove the practical applicability of our approach.
Report n° I2-D14, Computer Science Division, Department of Physical Science,
University of Naples "Federico II", Italy, April, 2008.
(Joint work with Piero A. Bonatti.)
[Abstract] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
A fully reviewed version of this work is appeared in POLICY 2008.
Submitted papers
2010
[2]
Graded Computation Tree Logic with Binary Coding
Graded path quantifiers have been recently introduced and investigated as a useful framework for
generalizing standard existential and universal path quantifiers in the branching-time temporal logic CTL
(GCTL), in such a way that they can express statements about a minimal and conservative number of accessible
paths.
These quantifiers naturally extend to paths the concept of graded world modalities, which has been deeply
investigated for the mu-Calculus (Gmu-Calculus) where it allows to express statements about a given number
of immediately accessible worlds.
As for the “non-graded” case, it has been shown that the satisfiability problem for GCTL and the
Gmu-Calculus coincides and, in particular, it remains solvable in ExpTime.
However, GCTL has been only investigated w.r.t. graded numbers coded in unary, while Gmu-Calculus uses for
this a binary coding, and it was left open the problem to decide whether the same result may or may not hold
for binary GCTL.
In this paper, by exploiting an automata theoretic-approach, which involves a model of alternating automata
with satellites, we answer positively to this question. We further investigate the succinctness of binary
GCTL and show that it is at least exponentially more succinct than Gmu-Calculus.
Finally, we discuss the extension of the exploited technique to the case of binary graded CTL* (GCTL*).
In this case, the satisfiability problem becomes solvable in 3ExpTime.
(Joint work with Alessandro Bianco, and
Aniello Murano.)
[Abstract]
2009
[1]
Synthesis of Hierarchical Systems
In automated synthesis, given a specification, we automatically create a system that is guaranteed to
satisfy the specification.
In the classical temporal synthesis algorithms, one usually creates a "flat" system.
In such a system a component may be inadvertently repeated many times.
However, real-life software and hardware systems can be exponentially more succinct since repeated
sub-systems are usually described only once.
In this work we provide an algorithm for the synthesis of hierarchical systems, which follows the
"bottom-up" approach to system design.
We suggest mimicking this design process by synthesizing in many rounds, when at each round the system
designer provides the specification of the currently desired module, which is then automatically synthesized
using the previously constructed modules (together with basic atomic components) as sub-modules.
To ensure that the synthesized module actually takes advantage of the previously synthesized high-level
modules, we guide the algorithm by enforcing certain modularity criteria.
An important part of our work is an algorithm for synthesizing a hierarchical system from a library of
hierarchical systems.
We show that this problem is ExpTime-Complete for mu-calculus, and 2ExpTime-Complete for LTL, both in the
cases of complete and incomplete information.
Thus, in all cases, it is not harder than the classical synthesis problem (of synthesizing flat systems
"from scratch"), even though the synthesized hierarchical system may be exponentially smaller than a flat
one.
(Joint work with Benjamin Aminof and
Aniello Murano.)
[Abstract]
Theses
2007
[2]
Branching-Time Temporal Logics (Theoretical Issues and a Computer Science Application)
Master of engineering thesis, University of Naples "Federico II", Italy, October, 2007.
[Full text] -
[BibTeX] -
[TarGz]
2005
[1]
Sui Metodi e gli Algoritmi di Fattorizzazione [in Italian]
Bachelor of engineering thesis, University of Naples "Federico II", Italy, September, 2005.
[Full text] -
[BibTeX] -
[TarGz]