Author name cluster

Massimo Franceschet

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

1 author row

CSL Conference 2005 Conference Paper

On the Complexity of Hybrid Logics with Binders

Balder ten Cate
Massimo Franceschet

Abstract Hybrid logic refers to a group of logics lying between modal and first-order logic in which one can refer to individual states of the Kripke structure. In particular, the hybrid logic HL(@, ↓ ) is an appealing extension of modal logic that allows one to refer to a state by means of the given names and to dynamically create new names for a state. Unfortunately, as for the richer first-order logic, satisfiability for the hybrid logic HL(@, ↓ ) is undecidable and model checking for HL(@, ↓ ) is PSpace -complete. We carefully analyze these results and we isolate large fragments of HL(@, ↓ ) for which satisfiability is decidable and model checking is below PSpace.

Details

TIME Conference 2004 Conference Paper

CTL Model Checking for Processing Simple XPath Queries

Loredana Afanasiev
Massimo Franceschet
Maarten Marx
Maarten de Rijke

The eXtensible Markup Language (XML) was designed to describe the content of a document and its hierarchical structure, and the XML Path language (XPath) is a language for selecting elements from XML documents. There is a close connection between the query processing problem for XPath and the model checking problem for temporal logics. Both boil down to checking which nodes of a graph satisfy a property. We investigate the potential of a technique based on computation tree logic (CTL) model checking for evaluating queries expressed in (a subset of) XPath. To this aim, we isolate a simple fragment of XPath that is naturally embeddable into CTL. We report on experiments based on the model checker NuSMV, and compare our results with alternative academic XPath processors. We comment on the advantages and drawbacks of the application of our model checking-based approach to XPath processing.

Details

TIME Conference 2003 Conference Paper

Definability and decidability of binary predicates for time granularity

Massimo Franceschet
Angelo Montanari
Adriano Peron
Guido Sciavicco

In this paper, we study the definability and decidability of binary predicates for time granularity with respect to monadic theories over finitely and infinitely layered structures. We focus our attention on the equi-level (resp. equi-column) predicate constraining two time points to belong to the same layer (resp. column) and on the horizontal (resp. vertical) successor predicate relating a time point to its successor within a given layer (resp. column). We give a number of positive and negative results by reduction to/from a wide spectrum of decidable/undecidable problems.

Details

TIME Conference 2003 Conference Paper

Hybrid Logics on Linear Structures: Expressivity and Complexity

Massimo Franceschet
Maarten de Rijke
Bernd-Holger Schlingloff

We investigate expressivity and complexity of hybrid logics on linear structures. Hybrid logics are an enrichment of modal logics with certain first-order features which are algorithmically well behaved. Therefore, they are well suited for the specification of certain properties of computational systems. We show that hybrid logics are more expressive than usual modal and temporal logics on linear structures, and exhibit a hierarchy of hybrid languages. We determine the complexities of the satisfiability problem for these languages and define an existential fragment of hybrid logic for which satisfiability is still NP-complete. Finally, we examine the linear time model checking problem for hybrid logics and its complexity.

Details

TIME Conference 2002 Conference Paper

A Logical Approach to Represent and Reason about Calendars

Carlo Combi
Massimo Franceschet
Adriano Peron

We propose a logical approach to represent and reason about different time granularities. We identify a time granularity as a discrete infinite sequence of time points properly labelled with proposition symbols marking the starting and ending points of the corresponding granules, and we intensively model sets of granularities with linear time logic formulas. Some real-world granularities are provided to motivate and exemplify our approach. The proposed framework permits to algorithmically solve the consistency, the equivalence, and the classification problems in a uniform way, by reducing them to the validity problem for the considered linear time logic.

Details

TIME Conference 1999 Conference Paper

A Graph-Theoretic Approach to Efficiently Reason about Partially Ordered Events in the Event Calculus

Massimo Franceschet
Angelo Montanari

We exploit graph-theoretic techniques to efficiently reason about partially ordered events in the Event Calculus. We replace the traditional generate-and-test reasoning strategy by a more efficient generate-only one that operates on the underlying directed acyclic graph of events representing ordering information by pairing breadth-first and depth-first visits in a suitable way. We prove the soundness and completeness of the proposed strategy, and thoroughly analyze its computational complexity. Furthermore, we show how it can be generalized to deal with the Modal Event Calculus, that provides a uniform modal framework for the basic Event Calculus and its skeptical and credulous variants.

Details

TIME Conference 1998 Conference Paper

Event Calculus with Explicit Quantifiers

Iliano Cervesato
Massimo Franceschet
Angelo Montanari

Kowalski and Sergot's (1986) Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. We extend this calculus to give a semantic foundation to our Quantifiers and Connectives Event Calculus (QCEC). In particular, we extend the range of queries accepted by EC, which has so far been limited to Boolean combinations of MVI verification or computation requests, to admit arbitrary quantification over events and properties. We demonstrate the added expressive power by encoding a medical diagnosis problem as a case study. Moreover, we give a /spl lambda/Prolog implementation of this formalism and analyze the computational complexity of the extended calculus.

Details

TIME Conference 1997 Conference Paper

Modal Event Calculi with Preconditions

Iliano Cervesato
Massimo Franceschet
Angelo Montanari

Kowalski and Sergot's (1986) event calculus (EC) is a simple temporal formalism that, given a set of event occurrences, allows the derivation of the maximal validity intervals (MVIs) over which properties initiated or terminated by those events hold. The limited expressive power of EC is notably augmented by permitting events to initiate or terminate a property only if a given set of preconditions hold at their occurrence time. We define a semantic formalization of the event calculus with preconditions. We gain further expressiveness by considering modal variants of this formalism, and show how to adapt our semantic characterization to encompass the additional operators. We discuss the complexity of MVI validation and describe examples showing that modal event calculi with preconditions can be successfully exploited to deal with real-world applications.

Details