3,563 research outputs found
An Optimal Tableau-based Decision Algorithm for Propositional Neighborhood Logic
No full textIn this paper we focus our attention on the decision problem for Propositional Neighborhood Logic (PNL for short). PNL is the proper subset of Halpern and Shoham's modal logic of intervals whose modalities correspond to Allen's relations meets and met by. We show that the satisfiability problem for PNL over the integers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure and we prove its optimality
Adding an equivalence relation to the interval logic ABBbar: complexity and expressiveness
No full textInterval temporal logics provide a general framework
for temporal representation and reasoning, where classical
(point-based) linear temporal logics can be recovered as special
cases. In this paper, we study the effects of the addition of an
equivalence relation ∼ to one of the most representative interval
temporal logics, namely, the logic ABBbar of Allen’s relations meets, begun by, and begins.We first prove that the satisfiability problem for the resulting logic ABBbarTilde remains decidable over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over N.. We also show that decidability over N can be recovered by restricting to a suitable subset of models. Then, we show that ABBbarTilde s expressive enough to define omegaS-regular languages, thus establishing a promising connection between interval temporal logics and extended omega-regular languages
Interval Logics and ωB-Regular Languages
No full textIn the recent years, interval temporal logics are emerging as a workable alternative to more standard point-based ones. In this paper, we establish an original connection between these logics and ωB-regular languages. First, we provide a logical characterization of regular (resp., ω-regular) languages in the interval logic ABB ̄ of Allen’s relations meets, begun by, and begins over finite linear orders (resp., N). Then, we lift such a correspondence to ωB-regular languages by substituting ABB ̄A ̄ for ABB ̄ (ABB ̄A ̄ is obtained from ABB ̄ by adding a modality for Allen’s relation met by). In addition, we show that new classes of extended
(ω-)regular languages can be naturally defined in ABB ̄A ̄
An Optimal Tableau System for the Logic of Temporal Neighborhood over the Reals
No full textThe propositional logic of temporal neighborhood (PNL) features two modalities that make it possible to access intervals adjacent to the right and to the left of the current one. PNL has been extensively studied in the last years. In particular, decidability and complexity of its satisfiability problem have been systematically investigated, and optimal decision procedures have been developed, for various (classes of) linear orders, including N, Z, and Q. The only missing piece is that for R. It is possible to show that PNL is expressive enough to separate Q and R. Unfortunately, there is no way to reduce the satisfiability problem for PNL over R to that over Q. In this paper, we first prove the NEXPTIME-completeness of the satisfiability problem for PNL over R, and then we devise an optimal tableau system for it
Interval logics and omegaB-regular languages
No full textIn the recent years, interval temporal logics are emerging as a workable alternative to more standard point-based ones. In this paper, we establish an original connection between these logics and ωB-regular languages. First, we provide a logical characterization of regular (resp., omega-regular) languages in the interval logic ABBbar of Allen's relations meets, begun by, and begins over finite linear orders (resp., N). Then, we lift such a correspondence to omegaB-regular languages by substituting
AAbarBBbar for ABBbar (AAbarBBbar is obtained from ABBbar by adding a modality for Allen's relation met by). In addition, we show that new classes of extended (omega-)regular languages can be naturally defined in AAbarBbar
Interval-based Synthesis
No full textIn this paper, we introduce the synthesis problem for Halpern and Shoham's interval temporal logic extended with an equivalence relation sim over time points (HSsim for short). In analogy to the case of monadic second-order logic of one successor, given an HSsim formula phi and a finite set Sigma^T_spoiler of proposition letters and temporal requests, the problem consists of establishing whether or not, for all possible evaluations of elements in Sigma^T_spoiler in every interval structure, there is an evaluation of the remaining proposition letters and temporal requests such that the resulting structure is a model for phi. We focus our attention on the decidability of the synthesis problem for some meaningful fragments of HSsim, whose modalities are drawn from
{meets, met by, begun by, begins}, interpreted over finite linear orders and natural numbers. We prove that the synthesis problem for ABBbar+sim over finite linear orders is decidable (non-primitive recursive hard), while AAbarBBbatr$ turns out to be undecidable. In addition, we show that if we replace finite linear orders by
natural numbers, then the problem becomes undecidable even for ABBbar
Progetto di sistemazione della piazza pubblica nella corte di Villa Marazzi con restauro e ridestinazione a sala consiliare delle ex-scuderie a Cesano Boscone a Milano
No full textPubblicato in: R. Neri, Praça e sala do conselho em Cesano Boscone, Milão (1996-1999). De pátio privado a práça pública, in “Arquitectura e Vida”, n. 12, gennaio 2001; M. Biraghi, Il “dispositivo” dell’ordine. La corte, la piazza, in “Abitare la Terra”, n. 10, 200
A framework for temporal functional dependencies with multiple granularities
No full textTemporal functional dependencies (TFDs) add a temporal component to classical functional dependencies to deal with temporal data. As an example, while functional dependencies model constraints like "employees with the same role get the same salary", TFDs can represent constraints like "for any given month, employees with the same role get the same salary (but their salary may change from one month to the next one)" or "current salaries of employees uniquely depend on their current and previous roles". In this paper, we propose a general framework for specifying TFDs, possibly involving different time granularities, and for checking whether or not a given database instance satisfies them. The proposed framework subsumes existing formalisms for TFDs and it allows one to encode TFDs which are not captured by them
I "Registri Litterarum" di Bergamo (1363-1410). Il carteggio dei signori di Bergamo
No full textL'edizione integrale di cinque volumi di lettere conservati presso la Civica Biblioteca e Archivi storici "Angelo Mai" di Bergamo intende fornire non solo la possibilità di una consultazione più agevole ma anche una lettura in sequenza del carteggio scambiato in un arco di cinquant'anni fra il governo visconteo di Milano, e poi Pandolfo Malatesti signore di Brescia e di Bergamo, e gli ufficiali a Bergamo. Il primo manoscritto è opera di Sozzone Suardi, che utilizzò quale copialettere degli ordini mandati da Milano un suo "diario" personale.Il secondo registro contiene le missive inviate da Giorgio Chizola, referendario a Bergamo. I rimanenti tre volumi raccolgono le lettere inviate sotto la signoria di Gian Galeazzo Visconti (1400), Giovanni Maria Visconti (1407) e Pandolfo Malatesti (1410. La trscrizione è preceduta dai saggi introduttivi di Patrizia Mainoni, Patrizia Merati e Arveno Sala, ed è corredata dal repertorio delle lettere e dagli indici
Reactive synthesis from interval temporal logic specifications
No full textIn this paper, we deal with the synthesis problem for Halpern and Shoham's interval temporal logic HS extended with an equivalence relation over time points (HSsim for short). The definition of the problem is analogous to that for MSO(omega, <). Given an HSsim formula and a finite set of proposition letters and temporal requests, it consists of determining, whether or not, for all possible valuations of elements in in every interval structure, there is a valuation of the remaining proposition letters and temporal requests such that the resulting structure is a model for . We focus on the decidability and complexity of the problem for some meaningful fragments of HSsim, whose modalities are drawn from the set interpreted over finite linear orders and . We prove that, over finite linear orders, the problem is decidable ( extsc{Ackermann}-hard) for and undecidable for . Moroever, we show that if we replace finite linear orders by , then it becomes undecidable even for . Finally, we study the generalization of to , where is the number of distinct equivalence relations. Despite the fact that the satisfiability problem for , with k>1, over finite linear orders, is already undecidable, we prove that, under a natural semantic restriction (refinement condition), the synthesis problem turns out to be decidable
- …
