Search Results

Documents authored by Mogavero, Fabio

Document
DOI: 10.4230/LIPIcs.FSTTCS.2024.9
Plan Logic

Authors: Dylan Bellier, Massimo Benerecetti, Fabio Mogavero, and Sophie Pinchinat

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

Abstract
When reasoning about games, one is often interested in verifying more intricate strategic properties than the mere existence of a winning strategy for a given coalition. Several languages, among which the very expressive Strategy Logic (SL), have been proposed that explicitly quantify over strategies in order to express and verify such properties. However, quantifying over strategies poses serious issues: not only does this lead to a non-elementary model-checking problem, but the classic Tarskian semantics is not fully adequate, both from a conceptual and practical viewpoint, since it does not guarantee the realisability of the strategies involved. In this paper, we follow a different approach and introduce Plan Logic (PL), a logic that takes plans, i.e., sequences of actions, as first-class citizens instead of strategies. Since plans are much simpler objects than strategies, it becomes easier to enforce realisability. In this setting, we can recover strategic reasoning by means of a compositional hyperteams semantics, inspired by the well-known team semantics. We show that the Conjunctive-Goal and Disjunctive-Goal fragments of SL are captured by PL, with an effective polynomial translation. This result relies on the definition of a suitable game-theoretic semantics for the two fragments. We also investigate the model-checking problem for PL. For the full prenex fragment, the problem is shown to be fixed-parameter-tractable: it is polynomial in the size of the model, when the formula is fixed, and 2-ExpTimeC in the size of the formula. For the Conjunctive-Goal and Disjunctive-Goal fragments of PL this result can be improved to match the optimal polynomial complexity in the size of the model, regardless of the size of the formula.
Cite as

Dylan Bellier, Massimo Benerecetti, Fabio Mogavero, and Sophie Pinchinat. Plan Logic. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bellier_et_al:LIPIcs.FSTTCS.2024.9,
  author =	{Bellier, Dylan and Benerecetti, Massimo and Mogavero, Fabio and Pinchinat, Sophie},
  title =	{{Plan Logic}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.9},
  URN =		{urn:nbn:de:0030-drops-221988},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.9},
  annote =	{Keywords: Logic for strategic reasoning, Strategy Logic, Realisable strategies, Strategies vs. plans, Hyperteam semantics}
}
Document
DOI: 10.4230/LIPIcs.TIME.2024.18
Full Characterisation of Extended CTL*

Authors: Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron

Published in: LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024)

Abstract
The precise identification of the expressive power of logic languages used in formal methods for specifying and verifying run-time properties of critical systems is a fundamental task and characterisation theorems play a crucial role as model-theoretic tools in this regard. While a clear picture of the expressive power of linear-time temporal logics in terms of word automata and predicate logics has long been established, a complete mapping of the corresponding relationships for branching-time temporal logics has proven to be a more elusive task over the past four decades with few scattered results. Only recently, an automata-theoretic characterisation of both CTL* and its full-ω-regular extension ECTL* has been provided in terms of Symmetric Hesitant Tree Automata (HTA), with and without a suitable counter-freeness restriction on their linear behaviours. These two temporal logics also correspond to the bisimulation-invariant semantic fragments of Monadic Path Logic (MPL) and Monadic Chain Logic (MCL), respectively. Additionally, it has been proven that the counting extensions of CTL* and ECTL*, namely CCTL* and CECTL*, enjoy equivalent graded versions of the HTAs for the corresponding non-counting logics. However, while Moller and Rabinovich have proved CCTL* to be equivalent to full MPL, thus filling the gap for the standard branching-time logic, no similar result has been given for CECTL*. This work completes the picture, by proving the expressive equivalence of CECTL* and full MCL, by means of a composition theorem for the latter logic. This also indirectly establishes the equivalence between HTAs and their first-order extensions HFTAs, as originally introduced by Walukiewicz.
Cite as

Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron. Full Characterisation of Extended CTL*. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{benerecetti_et_al:LIPIcs.TIME.2024.18,
  author =	{Benerecetti, Massimo and Bozzelli, Laura and Mogavero, Fabio and Peron, Adriano},
  title =	{{Full Characterisation of Extended CTL*}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-349-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{318},
  editor =	{Sala, Pietro and Sioutis, Michael and Wang, Fusheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.18},
  URN =		{urn:nbn:de:0030-drops-212259},
  doi =		{10.4230/LIPIcs.TIME.2024.18},
  annote =	{Keywords: Branching-Time Temporal Logics, Monadic Chain Logic, Tree Automata}
}
Document
DOI: 10.4230/LIPIcs.TIME.2024.19
Model Checking Linear Temporal Properties on Polyhedral Systems

Authors: Massimo Benerecetti, Marco Faella, and Fabio Mogavero

Published in: LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024)

Abstract
We study the problem of model checking linear temporal logic formulae on finite trajectories generated by polyhedral differential inclusions, thus enriching the landscape of models where such specifications can be effectively verified. Each model in the class comprises a static and a dynamic component. The static component features a finite set of observables represented by (non-necessarily convex) polyhedra. The dynamic one is given by a convex polyhedron constraining the dynamics of the system, by specifying the possible slopes of the trajectories in each time instant. We devise an exact algorithm that computes a symbolic representation of the region of points that existentially satisfy a given formula φ, i.e., the points from which there exists a trajectory satisfying φ.
Cite as

Massimo Benerecetti, Marco Faella, and Fabio Mogavero. Model Checking Linear Temporal Properties on Polyhedral Systems. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{benerecetti_et_al:LIPIcs.TIME.2024.19,
  author =	{Benerecetti, Massimo and Faella, Marco and Mogavero, Fabio},
  title =	{{Model Checking Linear Temporal Properties on Polyhedral Systems}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{19:1--19:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-349-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{318},
  editor =	{Sala, Pietro and Sioutis, Michael and Wang, Fusheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.19},
  URN =		{urn:nbn:de:0030-drops-212267},
  doi =		{10.4230/LIPIcs.TIME.2024.19},
  annote =	{Keywords: Model Checking, Real-Time Systems, LTLf, RTLf}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.128
Automata-Theoretic Characterisations of Branching-Time Temporal Logics

Authors: Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Characterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and verification of properties in formal methods. While complete connections have been established for the linear-time case between temporal logics, predicate logics, algebraic models, and automata, the situation in the branching-time case remains considerably more fragmented. In this work, we provide an automata-theoretic characterisation of some important branching-time temporal logics, namely CTL* and ECTL* interpreted on arbitrary-branching trees, by identifying two variants of Hesitant Tree Automata that are proved equivalent to those logics. The characterisations also apply to Monadic Path Logic and the bisimulation-invariant fragment of Monadic Chain Logic, again interpreted over trees. These results widen the characterisation landscape of the branching-time case and solve a forty-year-old open question.
Cite as

Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron. Automata-Theoretic Characterisations of Branching-Time Temporal Logics. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 128:1-128:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{benerecetti_et_al:LIPIcs.ICALP.2024.128,
  author =	{Benerecetti, Massimo and Bozzelli, Laura and Mogavero, Fabio and Peron, Adriano},
  title =	{{Automata-Theoretic Characterisations of Branching-Time Temporal Logics}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{128:1--128:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.128},
  URN =		{urn:nbn:de:0030-drops-202716},
  doi =		{10.4230/LIPIcs.ICALP.2024.128},
  annote =	{Keywords: Branching-Time Temporal Logics, Monadic Second-Order Logics, Tree Automata}
}
Document
DOI: 10.4230/LIPIcs.TIME.2022.14
Taming Strategy Logic: Non-Recurrent Fragments

Authors: Massimo Benerecetti, Fabio Mogavero, and Adriano Peron

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

Abstract
Strategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-Complete, respectively.
Cite as

Massimo Benerecetti, Fabio Mogavero, and Adriano Peron. Taming Strategy Logic: Non-Recurrent Fragments. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{benerecetti_et_al:LIPIcs.TIME.2022.14,
  author =	{Benerecetti, Massimo and Mogavero, Fabio and Peron, Adriano},
  title =	{{Taming Strategy Logic: Non-Recurrent Fragments}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{14:1--14:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.14},
  URN =		{urn:nbn:de:0030-drops-172611},
  doi =		{10.4230/LIPIcs.TIME.2022.14},
  annote =	{Keywords: Strategic Reasoning, Multi-Agent Systems, Temporal Logics, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.648
Binding Forms in First-Order Logic

Authors: Fabio Mogavero and Giuseppe Perelli

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.
Cite as

Fabio Mogavero and Giuseppe Perelli. Binding Forms in First-Order Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 648-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{mogavero_et_al:LIPIcs.CSL.2015.648,
  author =	{Mogavero, Fabio and Perelli, Giuseppe},
  title =	{{Binding Forms in First-Order Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{648--665},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.648},
  URN =		{urn:nbn:de:0030-drops-54443},
  doi =		{10.4230/LIPIcs.CSL.2015.648},
  annote =	{Keywords: First-Order Logic, Decidable Fragments, Satisfiability, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.133
Reasoning About Strategies

Authors: Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
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 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. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by SL-CHP, with the aim of getting a powerful framework for reasoning explicitly about strategies. SL-CHP is obtained by using first-order quantifications over strategies and it has been investigated in the specific setting of two-agents turn-based game structures where a non-elementary model-checking algorithm has been provided. While SL-CHP 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. We prove that SL strictly includes SL-CHP, 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 SL-CHP. We also consider the satisfiability problem and show that it is undecidable already for the sub-logic SL-CHP under the concurrent game semantics.
Cite as

Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning About Strategies. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 133-144, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{mogavero_et_al:LIPIcs.FSTTCS.2010.133,
  author =	{Mogavero, Fabio and Murano, Aniello and Vardi, Moshe Y.},
  title =	{{Reasoning About Strategies}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{133--144},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.133},
  URN =		{urn:nbn:de:0030-drops-28597},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.133},
  annote =	{Keywords: open systems, multi-agent systems, verification, strategy quantifier, alternating temporal logic, model-checking}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact