Journal articles
2011
[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 muCalculus, 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 affected 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, even in the case that the graded numbers are coded in binary.
This result is obtained by exploiting an automata-theoretic approach, which involves a model of alternating
automata with satellites.
The satisfiability result turns out to be even more interesting as we show that GCTL is at least
exponentially more succinct than graded muCalculus.
[Accepted for publication in Transactions on Computational Logic, ACM, 2011.]
(TOCL)
(Joint work with Alessandro Bianco and
Aniello Murano.)
[Abstract] -
[Text]
Note:
This is the journal version of the articles appeared in LICS 2009 and
CSL 2010.
[2]
Quantitatively Fair Scheduling
We consider finite graphs whose edges are labeled with elements, called colors, taken from a fixed finite
alphabet.
We study the problem of determining whether there is an infinite path where either (i) all colors occur with
a fixed asymptotic frequency, (ii) there is a constant that bounds the difference between the occurrences of
any two colors for all prefixes of the path.
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.
Our notions provide stronger criteria, particularly suitable for scheduling applications based on a
coarse-grained model of the jobs involved.
In particular, they enforce a given set of priorities among the jobs involved in the system.
We show that both problems we address are solvable in polynomial time, by reducing them to the feasibility
of a linear program.
We also consider two-player games played on finite colored graphs where the goal is one of the above
frequency-related properties.
For all the goals, we show that the problem of checking whether there exists a winning strategy is
CoNP-Complete.
Theoretical Computer Science, volume 413, number 1, pages 160-175, 2012, Elsevier.
(TCS)
(Joint work with Alessandro Bianco,
Marco Faella, and
Aniello Murano.)
[Accepted for publication in 2011.]
doi:
http://dx.doi.org/10.1016/j.tcs.2011.06.029
[Abstract] -
[Text] -
[BibTeX] -
[TarGz]
Note:
This is the journal version of the articles appeared in MFCS 2009 and
QAPL 2010.
[1]
Exploring the Boundary of Half-Positionality
Half positionality is the property of a language of infinite words to admit positional winning strategies,
when interpreted as the goal of a two-player game on a graph.
Such problem applies to the automatic synthesis of controllers, where positional strategies represent
efficient controllers.
As our main result, we present a novel sufficient condition for half positionality, more general than what
was previously known.
Moreover, we compare our proposed condition with several others, proposed in the recent literature,
outlining an intricate network of relationships, where only few combinations are sufficient for half
positionality.
Annals of Mathematics and Artificial Intelligence, volume 62, number 1-2, pages 55-77, 2011, Springer.
(AMAI)
(Joint work with Alessandro Bianco,
Marco Faella, and
Aniello Murano.)
doi:
http://dx.doi.org/10.1007/s10472-011-9250-1
[Abstract] -
[Text] -
[BibTeX] -
[TarGz]
Note:
This is the journal version of the article appeared in CLIMA 2010.
Conference articles
2011
[10]
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 "from scratch".
However, real-life software and hardware systems are usually created using preexisting libraries of reusable
components, and are not "flat" since repeated sub-systems are described only once.
In this work we describe an algorithm for the synthesis of a hierarchical system from a library of
hierarchical components, which follows the ``bottom-up'' approach to system design.
Our algorithms works 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 initial
library and the previously constructed modules.
To ensure that the synthesized module actually takes advantage of the available high-level modules, we guide
the algorithm by enforcing certain modularity criteria.
We show that the synthesis of a hierarchical system from a library of hierarchical components is
ExpTime-Complete for muCalculus, 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.
8th International Symposium on Formal Aspects of Component Software
(FACS 2011),
Oslo, Norway, September 14-16, 2011.
(Joint work with Benjamin Aminof and
Aniello Murano.)
[To appear in proceedings.]
[Abstract]
2010
[9]
Reasoning about Strategies
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model
the interaction between open entities and express that the open system is correct no matter how the
environment behaves.
An important contribution in this context is given by modal logics for strategic ability, in the setting of
multi-agent games, such as ATL, ATL*, and the like.
In particular, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by
CHP-SL, with the aim of getting a powerful framework for reasoning explicitly about strategies.
It is obtained by using first-order quantification over strategies and it has been investigated in the
specific setting of two-agents turned-based game structures where a non-elementary model-checking algorithm
has been provided.
While CHP-SL is a very expressive logic, we claim that it does not fully capture the strategic aspects of
multi-agent systems.
In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about
strategies in multi-agent concurrent systems.
In particular, we show that SL strictly includes CHP-SL, while maintaining a decidable model-checking
problem.
Indeed, we show that it is 2ExpTime-Complete, thus not harder than that for ATL* and a remarkable
improvement of the same problem for CHP-SL.
We also consider the satisfiability problem and show that it is undecidable already for the sub-logic CHP-SL
under the concurrent game semantics.
30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
(FSTTCS 2010),
Chennai, India, December 15-18, 2010,
LIPIcs 8,
ISBN 978-3-939897-23-1,
pages 133-144.
(Joint work with Aniello Murano and
Moshe Y. Vardi.)
[FSTTCS'10 acceptance rate: 38/128
~ 29.69%.]
doi:
http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.133
[Abstract] -
[BibTeX] -
[Talk]
Cited by 3 works.
-
Proprietes de Jeux Multi-Agents.
(Ph.D. thesis.)
A. Da Costa. 2011. -
Verification of Embedded Systems.
(Ph.D. thesis.)
N. Markey. 2011. -
A Temporal Logic for the Interaction of Strategies.
(Conference article.)
F. Wang, C.H. Huang, and F. Yu. 2011.
[8]
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.
19th EACSL Annual Conference on Computer Science Logic
(CSL 2010),
Brno, Czech Republic, August 23-27, 2010, Springer,
LNCS 6247,
ISBN 978-3-642-15204-7,
pages 125-139.
(Joint work with Alessandro Bianco and
Aniello Murano.)
[CSL'10 acceptance rate: 33/103 ~ 32.04%.]
doi:
http://dx.doi.org/10.1007/978-3-642-15205-4_13
[Abstract] -
[Text] -
[BibTeX] -
[Talk]
Note:
A journal version of this article appeared in TOCL.
[7]
Exploring the Boundary of Half Positionality
Half positionality is the property of a language of infinite words to admit positional winning strategies,
when interpreted as the goal of a two-player game on a graph.
Such problem applies to the automatic synthesis of controllers, where positional strategies represent
efficient controllers.
As our main result, we describe a novel sufficient condition for half positionality, more general than what
was previously known.
Moreover, we compare our proposed condition with several others, proposed in the recent literature,
outlining an intricate network of relationships, where only few combinations are sufficient for half
positionality.
11th International Workshop on Computational Logic in Multi-Agent Systems
(CLIMA 2010),
Lisbon, Portugal, August 16-17, 2010, Springer,
LNAI 6245,
ISBN 978-3-642-14976-4,
pages 171-185.
(Joint work with Alessandro Bianco,
Marco Faella, and
Aniello Murano.)
[CLIMA'10 acceptance rate: 14/31 ~ 45.16%.]
doi:
http://dx.doi.org/10.1007/978-3-642-14977-1_14
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
A journal version of this article appeared in AMAI.
[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,
LNAI 6355,
ISBN 978-3-642-17510-7,
pages 371-386.
(Joint work with Aniello Murano and
Moshe Y. Vardi.)
[LPAR'10 acceptance rate: 27/47 ~ 58.70%.]
doi:
http://dx.doi.org/10.1007/978-3-642-17511-4_21
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[TarGz]
Cited by 2 works.
-
Towards Practical Privacy Policy Enforcement.
(Technical report.)
W.H. Winsborough, J. von Ronne, O. Chowdhury, J. Niu, and Md.S. Ashik. 2011. -
Formalizing Operator Task Analysis.
(Ph.D. thesis.)
A. Yasmeen. 2011.
[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 28,
ISSN 2075-2180,
pages 48-63.
(Joint work with Alessandro Bianco,
Marco Faella, and
Aniello Murano.)
[QAPL'10 acceptance rate: 11/? ~ ?%.]
doi:
http://dx.doi.org/10.4204/EPTCS.28.4
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
A journal version of this article appeared in TCS.
Cited by 1 work.
-
Emptiness and Universality Problems in Timed Automata with Positive Frequency.
(Conference article.)
N. Bertrand, P. Bouyer, T. Brihaye, and A. Stainer. 2011.
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,
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%.]
doi:
http://dx.doi.org/10.1007/978-3-642-03816-7_14
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
A journal version of this article appeared in TCS.
[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%.]
doi: http://dx.doi.org/10.1109/LICS.2009.28
[Abstract] -
[Text] -
[Full text] -
[BibTeX] -
[Talk] -
[TarGz]
Note:
A journal version of this article appeared in TOCL.
Cited by 3 works.
-
Raisonnement Automatisé sur les Arbres avec des Contraintes de Cardinalité.
(Ph.D. thesis.)
E. Barcenas. 2011. -
On the Count of Trees.
(Technical report.)
E. Barcenas, P. Geneves, N. Layaida, and A. Schmitt. 2010. -
Graded-CTL: Satisfiability and Symbolic Model Checking.
(Conference article.)
A. Ferrante, M. Napoli, and M. Parente. 2009.
[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,
LNCS 5583,
ISBN 978-3-642-02736-9,
pages 396-409.
(Joint work with Aniello Murano.)
[DLT'09 acceptance rate: 35/70 ~ 50.00%.]
doi:
http://dx.doi.org/10.1007/978-3-642-02737-6_32
[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%.]
doi: http://dx.doi.org/10.1109/POLICY.2008.16
[Abstract] -
[Full text] -
[BibTeX] -
[TarGz]
Cited by 10 works with 4 self-citations by P.A. Bonatti.
-
A Data-centric View on Expressing Privacy Policies.
(Technical report.)
S. Speiser. 2012. -
Datalog for Security, Privacy, and Trust.
(Conference article.)
P.A. Bonatti. 2011. -
Expressing Self-Referential Usage Policies for the Semantic Web.
(Technical report.)
M. Krotzsch and S. Speiser. 2011. -
A Rule-Based Trust Negotiation System.
(Journal article.)
P.A. Bonatti, J.L. De Coi, D. Olmedilla, and L. Sauro. 2010. -
PROTUNE: A Rule-Based PROvisional TrUst NEgotiation Framework.
(Technical report.)
P.A. Bonatti, J.L. De Coi, D. Olmedilla, and L. Sauro. 2010. -
ShareAlike Your Data: Self-Referential Usage Policies for the Semantic Web.
(Conference article.)
M. Krotzsch and S. Speiser. 2010. -
A Self-Policing Policy Language.
(Conference article.)
S. Speiser and R. Studer. 2010. -
Access Control: What Is Required in Business Collaboration?
(Conference article.)
D.D. He, M. Compton, K. Taylor, and J. Yang. 2009. -
Authorization Control in Collaborative Healthcare Systems.
(Journal article.)
D.D. He and J. Yang. 2009. -
A Semantic Stateless Service Description Language.
(Conference article.)
P.A. Bonatti and L. Sauro. 2008.
Workshop notes
2011
[4]
Synthesis of Hierarchical Systems from a Library
4th Workshop of the ESF Networking Programme on Games for Design and Verification
(GAMES 2011),
Paris, France, August 31 - September 3, 2011.
(Joint work with Benjamin Aminof and
Aniello Murano.)
[Text] -
[TarGz]
2010
[3]
Relentful Strategic Reasoning in Alternating-Time Temporal Logic
3rd Workshop of the ESF Networking Programme on Games for Design and Verification
(GAMES 2010),
Oxford, UK, September 20-23, 2010.
(Joint work with Aniello Murano and
Moshe Y. Vardi.)
[Text] -
[Talk] -
[TarGz]
[2]
Graded Computation Tree Logic
3rd Workshop of the ESF Networking Programme on Games for Design and Verification
(GAMES 2010),
Oxford, UK, September 20-23, 2010.
(Joint work with Alessandro Bianco and
Aniello Murano.)
[Text] -
[Talk] -
[TarGz]
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
2011
[3]
Reasoning About Strategies: On the Model-Checking Problem
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model
the interaction between agents and express the correctness of the system no matter how the environment
behaves.
An important contribution in this context is given by modal logics for strategic ability, in the setting of
multi-agent games, such as ATL, ATL∗, and the like.
Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-SL,
with the aim of getting a powerful framework for reasoning explicitly about strategies.
CHP-SL is obtained by using first-order quantifications over strategies and has been investigated in the
very specific setting of two-agents turned-based games, where a non-elementary model-checking algorithm has
been provided.
While CHP-SL is a very expressive logic, we claim that it does not fully capture the strategic aspects of
multi-agent systems.
In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about
strategies in multi-agent concurrent games.
We prove that SL includes CHP-SL, while maintaining a decidable model-checking problem.
In particular, the algorithm we propose is computationally not harder than the best one known for CHP-SL.
Moreover, we prove that such a problem for SL is NonElementarySpace-Hard.
This negative result has spurred us to investigate here syntactic fragments of SL, strictly subsuming ATL∗,
with the hope of obtaining an elementary model-checking problem.
Among the others, we study the sublogics SL[NG], SL[BG], and SL[1G].
They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean
combinations of goals and, a single goal at a time.
About these logics, we prove that the model-checking problem for SL[1G] is 2ExpTime-Complete, thus not
harder than the one for ATL∗.
In contrast, SL[NG] turns out to be NonElementarySpace-Hard, strengthening the corresponding result for SL.
Finally, we observe that SL[BG] includes CHP-SL, while its model-checking problem relies between
NonElementaryTime and 2ExpTime.
CoRR 1112.6275, arXiv, December, 2011.
(Joint work with Aniello Murano,
Giuseppe Perelli, and
Moshe Y. Vardi.)
[Abstract] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
This is actually an update of the original technical report CoRR 1112.6275 of December 2011.
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",
Università degli Studi di Napoli "Federico II", Italy, April, 2008.
(Joint work with Alessandro Bianco and
Aniello Murano.)
[Abstract] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
This is actually an update of the original technical report n° 21 of April 2008.
Note:
A fully reviewed version of this work 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,
Università degli Studi di Napoli "Federico II", Italy, April, 2008.
(Joint work with Piero A. Bonatti.)
[Abstract] -
[Full text] -
[BibTeX] -
[TarGz]
Note:
A fully reviewed version of this work appeared in POLICY 2008.
Journal submitted papers
2012
[1]
Reasoning About Strategies: On the Model-Checking Problem
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model
the interaction between agents and express the correctness of the system no matter how the environment
behaves.
An important contribution in this context is given by modal logics for strategic ability, in the setting of
multi-agent games, such as ATL, ATL∗, and the like.
Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-SL,
with the aim of getting a powerful framework for reasoning explicitly about strategies.
CHP-SL is obtained by using first-order quantifications over strategies and has been investigated in the
very specific setting of two-agents turned-based games, where a non-elementary model-checking algorithm has
been provided.
While CHP-SL is a very expressive logic, we claim that it does not fully capture the strategic aspects of
multi-agent systems.
In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about
strategies in multi-agent concurrent games.
We prove that SL includes CHP-SL, while maintaining a decidable model-checking problem.
In particular, the algorithm we propose is computationally not harder than the best one known for CHP-SL.
Moreover, we prove that such a problem for SL is NonElementarySpace-Hard.
This negative result has spurred us to investigate here syntactic fragments of SL, strictly subsuming ATL∗,
with the hope of obtaining an elementary model-checking problem.
Among the others, we study the sublogics SL[NG], SL[BG], and SL[1G].
They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean
combinations of goals and, a single goal at a time.
About these logics, we prove that the model-checking problem for SL[1G] is 2ExpTime-Complete, thus not
harder than the one for ATL∗.
In contrast, SL[NG] turns out to be NonElementarySpace-Hard, strengthening the corresponding result for SL.
Finally, we observe that SL[BG] includes CHP-SL, while its model-checking problem relies between
NonElementaryTime and 2ExpTime.
(Joint work with Aniello Murano,
Giuseppe Perelli, and
Moshe Y. Vardi.)
[Abstract]
Conference submitted papers
2012
[1]
A Decidable Fragment of Strategy Logic
Strategy Logic (SL, for short) has been recently introduced by Mogavero, Murano, and Vardi as a useful
formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent
games.
This logic turns to be very powerful, subsuming all major previously studied modal logics for strategic
reasoning, including ATL, ATL*, and the like.
Unfortunately, due to its expressiveness, SL has a non-elementarily decidable model-checking problem and a
highly undecidable satisfiability problem, specifically, $\Sigma_{1}^{1}$-Hard.
In order to obtain a decidable sublogic, we introduce and study here One-Goal Strategy Logic (SL[1G], for
short).
This logic is a syntactic fragment of SL, strictly subsuming ATL*, which encompasses formulas in prenex
normal form having a single temporal goal at a time, for every strategy quantification of agents.
SL[1G] is known to have an elementarily decidable model-checking problem.
Here we prove that, unlike SL, it has the bounded tree-model property and its satisfiability problem is
decidable in 2ExpTime, thus not harder than the one for ATL*.
(Joint work with Aniello Murano,
Giuseppe Perelli, and
Moshe Y. Vardi.)
[Abstract]
Theses
2011
[3]
Logics in Computer Science
Ph.D. thesis, Università degli Studi di Napoli "Federico II", Italy, January, 2011.
[BibTeX] -
[Talk]
2007
[2]
Branching-Time Temporal Logics (Theoretical Issues and a Computer Science Application)
Master of engineering thesis, Università degli Studi di Napoli "Federico II", Italy, October,
2007.
[Full text] -
[BibTeX] -
[TarGz]
2005
[1]
Sui Metodi e gli Algoritmi di Fattorizzazione [in Italian]
Bachelor of engineering thesis, Università degli Studi di Napoli "Federico II", Italy, September,
2005.
[Full text] -
[BibTeX] -
[TarGz]