Search

Automatic event detection from images or wearable sensors is a fundamental step towards the development of advanced sport analytics and broadcasting software. However, the collection and annotation of large scale sport datasets is hindered by technical obstacles, cost of data acquisition and annotation, and commercial interests. In this paper, we present the Soccer Event Recognition (SoccER) data generator, which builds upon an existing, high quality open source game engine to enable synthetic data generation. The software generates detailed spatio-temporal data from simulated soccer games, along with fine-grained, automatically generated event ground truth. The SoccER software suite includes also a complete event detection system entirely developed and tested on a synthetic dataset including 500 min of game, and more than 1 million events. We close the paper by discussing avenues for future research in sports event recognition enabled by the use of synthetic data.

Decision trees are simple, yet powerful, classification models used to classify categorical and numerical data, and, despite their simplicity, they are commonly used in operations research and management, as well as in knowledge mining. From a logical point of view, a decision tree can be seen as a structured set of logical rules written in propositional logic. Since knowledge mining is rapidly evolving towards temporal knowledge mining, and since in many cases temporal information is best described by interval temporal logics, propositional logic decision trees may evolve towards interval temporal logic decision trees. In this paper, we define the problem of interval temporal logic decision tree learning, and propose a solution that generalizes classical decision tree learning.

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as first-class citizens. Their expressive power and computational behavior mainly depend on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we consider all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the rationals, and we provide a complete classification of them in terms of their expressiveness and computational complexity by solving the last few open problems.

Model checking allows one to automatically verify a specification of the expected properties of a system against a formal model of its behavior (generally, a Kripke structure). Point-based temporal logics, such as LTL, CTL, and CTL⁎, that describe how the system evolves state-by-state, are commonly used as specification languages. They proved themselves quite successful in a variety of application domains. However, properties constraining the temporal ordering of temporally extended events as well as properties involving temporal aggregations, which are inherently interval-based, can not be properly dealt with by them. Interval temporal logics (ITLs), that take intervals as their primitive temporal entities, turn out to be well-suited for the specification and verification of interval properties of computations (we interpret all the tracks of a Kripke structure as computation intervals). In this paper, we study the model checking problem for some fragments of Halpern and Shoham's modal logic of time intervals (HS). HS features one modality for each possible ordering relation between pairs of intervals (the so-called Allen's relations). First, we describe an EXPSPACE model checking algorithm for the HS fragment of Allen's relations meets, met-by, starts, started-by, and finishes, which exploits the possibility of finding, for each track (of unbounded length), an equivalent bounded-length track representative. While checking a property, it only needs to consider tracks whose length does not exceed the given bound. Then, we prove the model checking problem for such a fragment to be PSPACE-hard. Finally, we identify other well-behaved HS fragments which are expressive enough to capture meaningful interval properties of systems, such as mutual exclusion, state reachability, and non-starvation, and whose computational complexity is less than or equal to that of LTL.

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by checking the formula against the model. Classically, system behaviour is expressed by a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those constraining the temporal relations between pairs of temporally extended events or involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over finite Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against finite Kripke structures is decidable by a suitable small model theorem, and we provide a lower bound to its computational complexity., In Journal: Acta Informatica, Springer Berlin Heidelber, 2015

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL∗, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted “point-wise” describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted “interval-wise” express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this article, we study the expressiveness of Halpern and Shoham's interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL∗. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al. in [30, 34], that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL∗, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL∗). © 2018 Association for Computing Machinery.

The problem of temporal dataset evaluation consists in establishing to what extent a set of temporal data (histories) complies with a given temporal condition. It presents a strong resemblance with the problem of model checking enhanced with the ability of rating the compliance degree of a model against a formula. In this paper, we solve the temporal dataset evaluation problem by suitably combining the outcomes of model checking an interval temporal logic formula against sets of histories (finite interval models), possibly taking into account domain-dependent measures/criteria, like, for instance, sensitivity, specificity, and accuracy. From a technical point of view, the main contribution of the paper is a (deterministic) polynomial time algorithm for interval temporal logic model checking over finite interval models. To the best of our knowledge, this is the first application of a (truly) interval temporal logic model checking in the area of temporal databases and data mining rather than in the formal verification setting.

International audience; We introduce a modal logic, called Cone Logic, whose formulas describe properties of points in the plane and spatial relationships between them. Points are labelled by proposition letters and spatial relations are induced by the four cone-shaped cardinal directions. Cone Logic can be seen as a weakening of Venema's Compass Logic. We prove that, unlike Compass Logic and other projection-based spatial logics, its satisfiability problem is decidable (precisely, PSPACE-complete). We also show that it is expressive enough to capture meaningful interval temporal logics - in particular, the interval temporal logic of Allen's relations `Begins', `During', and `Later', and their transposes.

The chop operator C is a binary modality that plays an important role in interval temporal logics. Such an operator, which is not definable in Halpern and Shoham's modal logic of time intervals HS, allows one to split an interval into two parts and to specify what is true over them. C appears both in Moszkowski's PITL (that pairs it with a modal constant Pi which is true on all and only the intervals with coincident endpoints) and in Venema's CDT (that also features the binary modalities D and T, and Pi). Without the so-called locality principle, which restricts the semantics of proposition letters, the satisfiability problem for both PITL and CDT turns out to be undecidable over all meaningful classes of linear orders. The problem has been shown to be undecidable also for the fragment C, that is, PITL without Pi, over infinite linear orders. In this paper, we prove that the same holds for C over finite linear orders. To this end, we exploit the close relation between C and the reflexive version of the HS fragment BE, whose modalities correspond to Allen's relations starts and finishes: we prove that the satisfiability problem for reflexive BE is undecidable, undecidability of the same problem for C comes as a corollary.

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. Their computational behaviour and expressive power mainly depend on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we consider all fragments of Halpern and Shoham’s interval temporal logic HS with a decidable satisfiability problem over the class of all dense linear orders, and we provide a complete classification of them in terms of their complexity and expressiveness by solving the last two open cases.

International audience; The classification of the fragments of Halpern and Shoham's logic with respect to decidability/undecidability of the satisfiability problem is now very close to the end. We settle one of the few remaining questions concerning the fragment AA*BB*, which comprises Allen's interval relations "meets" and "begins" and their symmetric versions. We already proved that AA*BB* B is decidable over the class of all finite linear orders and undecidable over ordered domains isomorphic to N. In this paper, we first show that AA*BB* is undecidable over R and over the class of all Dedekind-complete linear orders. We then prove that the logic is decidable over Q and over the class of all linear orders.

This special issue contains a selection of revised and expanded versions of papers originally presented in a special track on Interval Temporal Logics (ITLs) at the 18th International Symposium on Temporal Representation and Reasoning (TIME 2011). The conference was held in Lubeck, Germany on 12–14 September, 2011, and another special track on ITLs is planned for TIME 2014 in Verona, Italy. The articles reflect the varied nature of research on the theory and application of ITLs. Two aims of this preface are to discuss the study of ITLs, and in the context of that to give summaries of the articles. A previous journal special issue on ITLs appeared about ten years ago. In its preface [12] the guest editors Valentin Goranko and Angelo Montanari pointed out that the concept of time intervals is naturally appealing and intuitive, with research on associated logical formalisms having compelling multidisciplinary origins arising from Philosophy, Linguistics, Artificial Intelligence and Computer Science. This has certainly helped in no small measure to perpetuate the study of ITLs and ensure that the investigation of their theory and application continues to be seen as worthwhile. As a reflection of the numerous sources of motivation, the earlier special issue contained an extensive “roadmap” survey of such formalisms by Goranko, Montanari and Sciavicco [13]. Nevertheless, research on ITLs has continued to face major hurdles already noted in [12]. These result from two kinds of complexity often exhibited by the notations

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. Their computational behavior mainly depends on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we identify all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the class of strongly discrete linear orders as well as over its relevant subclasses (the class of finite linear orders, Z , N , and Z - ). We classify them in terms of both their relative expressive power and their complexity, which ranges from NP-completeness to non-primitive recursiveness.

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g. A Kripke structure, and a formula specifying its expected behavior, one can verify whether the system meets the behavior by checking the formula against the model. Classically, system behavior is given as a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against Kripke structures is decidable by a suitable small model theorem, and we outline a PSpace decision procedure for the meaningful fragments AAbarBBbar and AAbarEEbar.

Interval temporal logics are temporal logics that take time intervals, instead of time instants, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham's modal logic of time intervals (HS), which has a distinct modality for each binary relation between intervals over a linear order. As HS turns out to be undecidable over most classes of linear orders, the study of HS fragments, featuring a proper subset of HS modalities, is a major item in the research agenda for interval temporal logics. A characterization of HS fragments in terms of their relative expressive power has been given for the class of all linear orders. Unfortunately, there is no easy way to directly transfer such a result to other meaningful classes of linear orders. In this paper, we provide a complete classification of the expressiveness of HS fragments over the class of (all) dense linear orders.

International audience; In this paper, we focus our attention on the interval temporal logic of the Allen's relations "meets", "begins", and "begun by" (ABBar for short), interpreted over natural numbers. We first introduce the logic and we show that it is expressive enough to model distinctive interval properties,such as accomplishment conditions, to capture basic modalities of point-based temporal logic, such as the until operator, and to encode relevant metric constraints. Then, we prove that the satisfiability problem for ABBar over natural numbers is decidable by providing a small model theorem based on an original contraction method. Finally, we prove the EXPSPACE-completeness of the problem

The validity/satisfiability problem for most propositional interval temporal logics is (highly) undecidable, under very weak assumptions on the class of interval structures in which they are interpreted. That, in particular, holds for most fragments of Halpern and Shoham's interval modal logic HS. Still, decidability is the rule for the fragments of HS with only one modal operator, based on an Allen's relation. In this paper, we show that the logic O of the Overlap relation, when interpreted over discrete linear orderings, is an exception. The proof is based on a reduction from the undecidable octant tiling problem. This is one of the sharpest undecidability result for fragments of HS.

Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the `right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXPSPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

International audience; We introduce a spatial modal logic based on cone-shaped cardinal directions over the rational plane and we prove that, unlike projection-based ones, such as, for instance, Compass Logic, its satis- ability problem is decidable (PSPACE-complete). We also show that it is expressive enough to subsume meaningful interval temporal logics, thus generalizing previous results in the literature, e.g., its decidability implies that of the subinterval/superinterval temporal logic interpreted over the rational line.

We investigate fragments of Halpern-Shoham's interval logic HS involving the modal operators for the relations of left or right overlap of intervals. We prove that most of these fragments are undecidable, by employing a non-trivial reduction from the octant tiling problem.

Interval-based temporal reasoning naturally arises in a variety of fields, including artificial intelligence (temporal knowledge representation, systems for temporal planning and maintenance, qualitative reasoning, theories of events), theoretical computer science (specification and design of hardware components, concurrent real-time processes), temporal databases (event modeling, temporal aggregation), and computational linguistics (analysis of progressive tenses, semantics and processing of natural languages) [10].

Interval temporal logics are based on temporal structures where time intervals, rather than time instants, are the primitive ontological entities. They employ modal operators corresponding to various relations between intervals, known as Allen’s relations. Technically, validity in interval temporal logics translates to dyadic second-order logic, thus explaining their complex computational behavior. The full modal logic of Allen’s relations, called HS, has been proved to be undecidable by Halpern and Shoham under very weak assumptions on the class of interval structures, and this result was discouraging attempts for practical applications and further research in the field. A renewed interest has been recently stimulated by the discovery of interesting decidable fragments of HS. This paper contributes to the characterization of the boundary between decidability and undecidability of HS fragments. It summarizes known positive and negative results, it describes the main techniques applied so far in both directions, and it establishes a number of new undecidability results for relatively small fragments of HS.

Propositional interval temporal logics come into play in many areas of artificial intelligence and computer science. Unfortunately, most of them turned out to be (highly) undecidable. Some positive exceptions, belonging to the classes of neighborhood logics and of logics of subinterval relations, have been recently identified. In this paper, we address the decision problem for the future fragment of Propositional Neighborhood Logic (Right Propositional Neighborhood Logic) interpreted over trees and we positively solve it by providing a tableau-based decision procedure that works in exponential space. Moreover, we prove that the decision problem for the logic is EXPSPACE-hard, thus showing the optimality of the proposed procedure.

Interval logics are an important area of computer science. Although attention has been mainly focused on unary operators, an early work by Venema (1991) introduced an expressively complete interval logic language called CDT, based on binary operators, which has many potential applications and a strong theoretical interest. Many very natural questions about CDT and its fragments, such as (non-)finite axiomatizability and (un-)decidability, are still open (as a matter of fact, only a few undecidability results, including the undecidability of CDT, are known). In this paper, we answer most of these questions, showing that almost all fragments of CDT, containing at least one binary operator, are neither finitely axiomatizable with standard rules nor decidable. A few cases remain open.

The study of interval temporal logics on linear orders is a meaningful research area in computer science and artificial intelligence. Unfortunately, even when restricted to propositional languages, most interval logics turn out to be undecidable. Decidability has been usually recovered by imposing severe syntactic and/or semantic restrictions. In the last years, tableau-based decision procedures have been obtained for logics of the temporal neighborhood and logics of the subinterval relation over specific classes of temporal structures. In this paper, we develop an optimal NEXPTIME tableau-based decision procedure for the future fragment of Propositional Neighborhood Logic over the whole class of linearly ordered domains.

We construct a sound, complete, and terminating tableau system for the interval temporal logic ${{\rm D}_\sqsubset}$ interpreted in interval structures over dense linear orderings endowed with strict subinterval relation (where both endpoints of the sub-interval are strictly inside the interval). In order to prove the soundness and completeness of our tableau construction, we introduce a kind of finite pseudo-models for our logic, called ${{\rm D}_\sqsubset}$ -structures, and show that every formula satisfiable in ${{\rm D}_\sqsubset}$ is satisfiable in such pseudo-models, thereby proving small-model property and decidability in PSPACE of ${{\rm D}_\sqsubset}$ , a result established earlier by Shapirovsky and Shehtman by means of filtration. We also show how to extend our results to the interval logic ${{\rm D}_\sqsubset}$ interpreted over dense interval structures with proper (irreflexive) subinterval relation, which differs substantially from ${{\rm D}_\sqsubset}$ and is generally more difficult to analyze. Up to our knowledge, no complete deductive systems and decidability results for ${{\rm D}_\sqsubset}$ have been proposed in the literature so far.

In this paper, we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema’s CDT logic interpreted over partial orders (BCDT + for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented. © 2005 Elsevier B.V. All rights reserved.

In this paper we focus our attention on the problem of finding propositional interval temporal logics which are expressive enough to express meaningful statements about time intervals and decidable.

Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various areas of artificial intelligence and computer science. Unfortunately, most interval temporal logics proposed in the literature have been shown to be (highly) undecidable. Decidable fragments of these logics have been obtained by imposing severe restrictions on their expressive power.In this paper, we propose a new interval temporal logic, called Split Logic, which is equipped with operators borrowed from other interval temporal logics, but is interpreted over specific interval structures based on a layered view of the temporal domain. We show that there exists a straightforward correspondence between Split Logic and the first-order fragments of the monadic theories of time granularity proposed in the literature. This connection allows us to transfer existing decidability results for such theories to Split Logic.