Search Results

Documents authored by Molinari, Alberto

Document
DOI: 10.4230/LIPIcs.ICALP.2017.120
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption

Authors: Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
In this paper, we investigate the finite satisfiability and model checking problems for the logic D of the sub-interval relation under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over all its points. First, we prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete; then, we show that its model checking problem, over finite Kripke structures, is PSPACE-complete as well.
Cite as

Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 120:1-120:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.ICALP.2017.120,
  author =	{Bozzelli, Laura and Molinari, Alberto and Montanari, Angelo and Peron, Adriano and Sala, Pietro},
  title =	{{Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{120:1--120:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.120},
  URN =		{urn:nbn:de:0030-drops-74703},
  doi =		{10.4230/LIPIcs.ICALP.2017.120},
  annote =	{Keywords: Interval Temporal Logic, Satisfiability, Model Checking, Decidability, Computational Complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.26
Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison

Authors: Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
Model checking is a powerful method widely explored in formal verification to check the (state-transition) model of a system against desired properties of its behaviour. Classically, properties are expressed by formulas of a temporal logic, such as LTL, CTL, and CTL*. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. On the contrary, Halpern and Shoham's interval temporal logic (HS) is "interval-wise" interpreted, thus allowing one to naturally express properties of computation stretches, spanning a sequence of states, or properties involving temporal aggregations, which are inherently "interval-based". In this paper, we study the expressiveness of HS in model checking, in comparison with that of the standard logics LTL, CTL, and CTL*. To this end, we consider HS endowed with three semantic variants: the state-based semantics, introduced by Montanari et al., which allows branching in the past and in the future, the linear-past semantics, allowing branching only in the future, and the linear semantics, disallowing branching. These variants are compared, as for their expressiveness, among themselves and to standard temporal logics, getting a complete picture. In particular, HS with linear (resp., linear-past) semantics is proved to be equivalent to LTL (resp., finitary CTL*).
Cite as

Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 26:1-26:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.FSTTCS.2016.26,
  author =	{Bozzelli, Laura and Molinari, Alberto and Montanari, Angelo and Peron, Adriano and Sala, Pietro},
  title =	{{Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{26:1--26:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.26},
  URN =		{urn:nbn:de:0030-drops-68615},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.26},
  annote =	{Keywords: Interval Temporal Logics, Expressiveness, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.193
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives

Authors: Alberto Molinari, Angelo Montanari, and Adriano Peron

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

Abstract
Model checking is commonly recognized as one of the most effective tool in system verification. While it has been systematically investigated in the context of classical, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACE-hardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones.
Cite as

Alberto Molinari, Angelo Montanari, and Adriano Peron. A Model Checking Procedure for Interval Temporal Logics based on Track Representatives. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 193-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{molinari_et_al:LIPIcs.CSL.2015.193,
  author =	{Molinari, Alberto and Montanari, Angelo and Peron, Adriano},
  title =	{{A Model Checking Procedure for Interval Temporal Logics based on Track Representatives}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{193--210},
  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.193},
  URN =		{urn:nbn:de:0030-drops-54150},
  doi =		{10.4230/LIPIcs.CSL.2015.193},
  annote =	{Keywords: Interval Temporal Logic, Model Checking, Complexity}
}
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