Search

In the timeline-based approach to planning, the evolution over time of a set of state variables (the timelines) is governed by a set of temporal constraints. Traditional timeline-based planning systems excel at the integration of planning with execution by handling temporal uncertainty. In order to handle general nondeterminism as well, the concept of timeline-based games has been recently introduced. It has been proved that finding whether a winning strategy exists for such games is 2EXPTIME-complete. However, a concrete approach to synthesize controllers implementing such strategies is missing. This paper fills this gap, by providing an effective and computationally optimal approach to controller synthesis for timeline-based games.

In several domains, systems generate continuous streams of data during their execution, including meaningful telemetry information, that can be used to perform tasks like preemptive failure detection. Deep learning models have been exploited for these tasks with increasing success, but they hardly provide guarantees over their execution, a problem which is exacerbated by their lack of interpretability. In many critical contexts, formal methods, which ensure the correct behavior of a system, are thus necessary. However, specifying in advance all the relevant properties and building a complete model of the system against which to check them is often out of reach in real-world scenarios. To overcome these limitations, we design a framework that resorts to monitoring, a lightweight runtime verification technique that does not require an explicit model specification, and pairs it with machine learning. Its goal is to automatically derive relevant properties, related to a bad behavior of the considered system, encoded by means of formulas of Signal Temporal Logic ( $\mathsf {STL}$ ). Results based on experiments performed on well-known benchmark datasets show that the proposed framework is able to effectively anticipate critical system behaviors in an online setting, providing human-interpretable results.

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.

Measurement(s) Nasal airflow • Snoring • Oxygen Saturation Measurement • Body Position • Thoracic movement • Abdominal movement • 3 Lead ECG Extracted From 12 Lead Continuous ECG Recording ( http://ncicb.nci.nih.gov/xml/owl/EVS/Thesaurus.owl#C123445 ) • Heart rate • premature ventricular contractions AE • Respiratory Rate • Perfusion index • obstructive sleep apnea • photoplethysmography Technology Type(s) Pressure transducer connected to a nasal cannula • photoplethysmography • Accelerometer • Plethysmography • Ag-AgC1 electrodes, 12-lead (I, II, III, aVR, aVL, aVF, V1, V2, V3, V4, V5, V6) • Lead II ECG Ag-AgC1 electrodes • Physician’s annotation Sample Characteristic - Organism Homo sapiens Sample Characteristic - Environment hospital Sample Characteristic - Location Province of Udine

In many application domains, position information is of fundamental importance. However, unlike the case of outdoor positioning, producing an accurate position estimation in the indoor setting turns out to be quite difficult. One of the most common localisation strategies makes use of fingerprinting. Research in this area has been faced with a number of challenges, leading to the proposal of a number of localisation algorithms, sampling strategies, benchmark datasets, and representations of building information. This proliferation made the modeling of the indoor positioning domain quite hard from both a theoretical and a practical point of view. In this paper, we propose a general and extensible framework, based on a relational database, that pairs fingerprints with building information. We show how the proposed system successfully deals with a number of problems that affect indoor positioning, supporting a large set of relevant tasks. The source code of the framework is available online, as well as an implementation of it, that provides an interactive open repository of indoor positioning data.

The expressive power of interval temporal logics (ITLs) makes them one of the most natural choices in a number of application domains, ranging from the specification and verification of complex reactive systems to automated planning. However, for a long time, because of their high computational complexity, they were considered not suitable for practical purposes. The recent discovery of several computationally well-behaved ITLs has finally changed the scenario. In this paper, we investigate the finite satisfiability and model checking problems for the ITL D, that has a single modality for 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). We first prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete, and then we show that the same holds for its model checking problem, over finite Kripke structures. In such a way, we enrich the set of tractable interval temporal logics with a new meaningful representative.

Positioning via outdoor fingerprinting, which exploits the radio signals emitted by cellular towers, is fundamental in many applications. In most cases, the localization performance is affected by the availability of information about the emitters, such as their coverage. While several projects aim at collecting cellular network data via crowdsourcing observations, none focuses on information about the structure of the networks, which is paramount to correctly model their topology. The difficulty of such a modeling is exacerbated by the inherent differences among cellular technologies, the strong spatio-temporal nature of positioning, and the continuously evolving configuration of the networks. In this paper, we first show how to synthesize a detailed conceptual schema of cellular networks on the basis of the signal fingerprints collected by devices. We turned it into a logical one, and we exploited that to build a relational spatio-temporal database capable of supporting a crowdsourced collection of data. Next, we populated the database with heterogeneous cellular observations originating from multiple sources. In addition, we illustrate how the developed system allows us to properly deal with the evolution of the network configuration, e.g., by detecting cell renaming phenomena and by making it possible to correct inconsistent measurements coming from mobile devices, fostering positioning tasks. Finally, we provide a wide range of basic, spatial, and temporal analyses about the arrangement of the cellular network and its evolution over time, demonstrating how the developed system can be used to reconstruct and maintain a deep knowledge of the cellular network, possibly starting from crowdsourced information only.

The widespread availability of mobile communication makes mobile devices a resource for the collection of data about mobile infrastructures and user mobility. In these contexts, the problem of reconstructing the most likely trajectory of a device on the road network on the basis of the sequence of observed locations (map-matching problem) turns out to be particularly relevant. Different contributions have demonstrated that the reconstruction of the trajectory of a device with good accuracy is technically feasible even when only a sparse set of GNSS positions is available. In this paper, we face the problem of coping with sparse sequences of cellular fingerprints. Compared to GNSS positions, cellular fingerprints provide coarser spatial information, but they work even when a device is missing GNSS positions or is operating in an energy saving mode. We devise a new map-matching algorithm, that exploits the well-known Hidden Markov Model and Random Forests to successfully deal with noisy and sparse cellular observations. The performance of the proposed solution has been tested over a medium-sized Italian city urban environment by varying both the sampling of the observations and the density of the fingerprint map as well as by including some GPS positions into the sequence of fingerprint observations.

In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time temporal logic, with an EXPSPACE-complete satisfiability problem, which has been successfully applied to the verification of real-time systems. In contrast to LTL, adding past operators to TPTL makes the satisfiability problem for the resulting logic (TPTL+P) non-elementary. In this paper, we devise a one-pass and tree-shaped tableau for both TPTL and bounded TPTL+P (TPTLb+P), a syntactic restriction introduced to encode timeline-based planning problems, which recovers the EXPSPACE-complete complexity. The tableau systems for TPTL and TPTLb+P are presented in a unified way, being very similar to each other, providing a common skeleton that is then specialised to each logic. In doing that, we characterise the semantics of TPTLb+P in terms of a purely syntactic fragment of TPTL+P, giving a translation that embeds the former into the latter. Soundness and completeness of the system are proved fully. In particular, we give a greatly simplified model-theoretic completeness proof, which sidesteps the complex combinatorial argument used by known proofs for the one-pass and tree-shaped tableau systems for LTL and LTL+P.

In this paper, we address complexity issues for timeline-based planning over dense temporal domains. The planning problem is modeled by means of a set of independent, but interacting, components, each one represented by a number of state variables, whose behavior over time (timelines) is governed by a set of temporal constraints (synchronization rules). While the temporal domain is usually assumed to be discrete, here we consider the dense case. Dense timeline-based planning has been recently shown to be undecidable in the general case; decidability (NP-completeness) can be recovered by restricting to purely existential synchronization rules (trigger-less rules). In this paper, we investigate the unexplored area of intermediate cases in between these two extremes. We first show that decidability and non-primitive recursive-hardness can be proved by admitting synchronization rules with a trigger, but forcing them to suitably check constraints only in the future with respect to the trigger (future simple rules). More "tractable" results can be obtained by additionally constraining the form of intervals in future simple rules: EXPSPACE-completeness is guaranteed by avoiding singular intervals, PSPACE-completeness by admitting only intervals of the forms [0,a] and [b,+∞[.

In this paper, we investigate the model checking (MC) problem for Halpern and Shoham's interval temporal logic HS. In the last years, interval temporal logic MC has received an increasing attention as a viable alternative to the traditional (point-based) temporal logic MC, which can be recovered as a special case. Most results have been obtained under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over each component state. Recently, Lomuscio and Michaliszyn proposed a way to relax such an assumption by exploiting regular expressions to define the behaviour of proposition letters over intervals in terms of their component states. When homogeneity is assumed, the exact complexity of MC is a difficult open question for full HS and for its two syntactically maximal fragments AA'BB'E' and AA'EB'E'. In this paper, we provide an asymptotically optimal bound to the complexity of these two fragments under the more expressive semantic variant based on regular expressions by showing that their MC problem is AEXP_pol-complete, where AEXP_pol denotes the complexity class of problems decided by exponential-time bounded alternating Turing Machines making a polynomially bounded number of alternations.

In the last years, various extensions of ω-regular languages have been proposed in the literature, including ωB-regular (ω-regular languages extended with boundedness), ωS-regular (ω-regular languages extended with strict unboundedness), and ωBS-regular languages (the combination of ωB- and ωS-regular ones). While the first two classes satisfy a generalized closure property, namely, the complement of an ωB-regular (resp., ωS-regular) language is an ωS-regular (resp., ωB-regular) one, the last class is not closed under complementation. The existence of non-ωBS-regular languages that are the complements of some ωBS-regular ones and express fairly natural properties of reactive systems motivates the search for other well-behaved classes of extended ω-regular languages. In this paper, we introduce the class of ωT-regular languages, that includes meaningful languages which are not ωBS-regular. We first define it in terms of ωT-regular expressions. Then, we introduce a new class of automata (counter-check automata) and we prove that (i) their emptiness problem is decidable in PTIME and (ii) they are expressive enough to capture ωT-regular languages (whether or not ωT-regular languages are expressively complete with respect to counter-check automata is still an open problem). Finally, we provide an encoding of ωT-regular expressions into S1S+U.

Real-time estimation of temperatures in indoor environments is critical for several reasons, including the upkeep of comfort levels, the fulfillment of legal requirements, and energy efficiency. Unfortunately, setting an adequate number of sensors at the desired locations to ensure a uniform monitoring of the temperature in a given premise may be troublesome. Virtual sensing is a set of techniques to replace a subset of physical sensors by virtual ones, allowing the monitoring of unreachable locations, reducing the sensors deployment costs, and providing a fallback solution for sensor failures. In this paper, we deal with temperature monitoring in an open space office, where a set of physical sensors is deployed at uneven locations. Our main goal is to develop a black-box virtual sensing framework, completely independent of the physical characteristics of the considered scenario, that, in principle, can be adapted to any indoor environment. We first perform a systematic analysis of various distance metrics that can be used to determine the best sensors on which to base temperature monitoring. Then, following a genetic programming approach, we design a novel metric that combines and summarizes information brought by the considered distance metrics, outperforming their effectiveness. Thereafter, we propose a general and automatic approach to the problem of determining the best subset of sensors that are worth keeping in a given room. Leveraging the selected sensors, we then conduct a comprehensive assessment of different strategies for the prediction of temperatures observed by physical sensors based on other sensors’ data, also evaluating the reliability of the generated outputs. The results show that, at least in the given scenario, the proposed black-box approach is capable of automatically selecting a subset of sensors and of deriving a virtual sensing model for an accurate and efficient monitoring of the environment.

In the plethora of fragments of Halpern and Shoham's modal logic of time intervals (HS), the logic AB of Allen's relations Meets and Started-by is at a central position. Statements that may be true at certain intervals, but at no sub-interval of them, such as accomplishments, as well as metric constraints about the length of intervals, that force, for instance, an interval to be at least (resp., at most, exactly) k points long, can be expressed in AB. Moreover, over the linear order of the natural numbers N, it subsumes the (point-based) logic LTL, as it can easily encode the next and until modalities. Finally, it is expressive enough to capture the ω-regular languages, that is, for each ω-regular expression R there exists an AB formula Φ such that the language defined by R coincides with the set of models of Φ over N. It has been shown that the satisfiability problem for AB over N is EXPSPACE-complete. Here we prove that, under the homogeneity assumption, its model checking problem is Δ^p_2 = P^NP-complete (for the sake of comparison, the model checking problem for full HS is EXPSPACE-hard, and the only known decision procedure is nonelementary). Moreover, we show that the modality for the Allen relation Met-by can be added to AB at no extra cost (AA'B is P^NP-complete as well).

We introduce the synthesis problem for Halpern and Shoham's modal logic of intervals extended with an equivalence relation over time points, abbreviated HSeq. In analogy to the case of monadic second-order logic of one successor, the considered synthesis problem receives as input an HSeq formula phi and a finite set Sigma of propositional variables and temporal requests, and it establishes whether or not, for all possible evaluations of elements in Sigma in every interval structure, there exists an evaluation of the remaining propositional variables and temporal requests such that the resulting structure is a model for phi. We focus our attention on decidability of the synthesis problem for some meaningful fragments of HSeq, whose modalities are drawn from the set A (meets), Abar (met by), B (begins), Bbar (begun by), interpreted over finite linear orders and natural numbers. We prove that the fragment ABBbareq is decidable (non-primitive recursive hard), while the fragment AAbarBBbar turns out to be undecidable. In addition, we show that even the synthesis problem for ABBbar becomes undecidable if we replace finite linear orders by natural numbers.

Temporal information plays a very important role in many analysis tasks, and can be encoded in at least two different ways. It can be modeled by discrete sequences of events as, for example, in the business intelligence domain, with the aim of tracking the evolution of customer behaviors over time. Alternatively, it can be represented by time series, as in the stock market to characterize price histories. In some analysis tasks, temporal information is complemented by other kinds of data, which may be represented by static attributes, e.g., categorical or numerical ones. This paper presents J48SS, a novel decision tree inducer capable of natively mixing static (i.e., numerical and categorical), sequential, and time series data for classification purposes. The novel algorithm is based on the popular C4.5 decision tree learner, and it relies on the concepts of frequent pattern extraction and time series shapelet generation. The algorithm is evaluated on a text classification task in a real business setting, as well as on a selection of public UCR time series datasets. Results show that it is capable of providing competitive classification performances, while generating highly interpretable models and effectively reducing the data preparation effort.

Interval temporal logics provide a general framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. 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. We classify them in terms of both their relative expressive power and their complexity. We show that there are exactly 44 expressively different decidable fragments, whose complexity ranges from NP to EXPSPACE. In addition, we identify some new undecidable fragments (all the remaining HS fragments were already known to be undecidable over strongly discrete linear orders). We conclude the paper by an analysis of the specific case of natural numbers, whose behavior slightly differs from that of the whole class of strongly discrete linear orders. The number of decidable fragments over natural numbers raises up to 47: three undecidable fragments become decidable with a non-primitive recursive complexity.

Interval temporal logics provide a natural framework for qualitative and quantitative temporal reason- ing over interval structures, where the truth of formulae is defined over intervals rather than points. In this paper, we study the complexity of the satisfiability problem for Metric Propositional Neigh- borhood Logic (MPNL). MPNL features two modalities to access intervals "to the left" and "to the right" of the current one, respectively, plus an infinite set of length constraints. MPNL, interpreted over the naturals, has been recently shown to be decidable by a doubly exponential procedure. We improve such a result by proving that MPNL is actually EXPSPACE-complete (even when length constraints are encoded in binary), when interpreted over finite structures, the naturals, and the in- tegers, by developing an EXPSPACE decision procedure for MPNL over the integers, which can be easily tailored to finite linear orders and the naturals (EXPSPACE-hardness was already known).

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.