Temporal Reasoning
New Encoding Methods for SAT-Based Temporal Planning
Rankooh, Masood Feyzbakhsh (Sharif University of Technology) | Ghassem-Sani, Gholamreza (Sharif University of Technology)
Although satisfiability checking is known to be an effective approach in classical planning, it has scarcely been investigated in the field of temporal planning. Most notably, the usage of E-step semantics for encoding the problem into a SAT formula, while being demonstrably quite efficient for decreasing the size of the encodings in classical planning, has not yet been employed to tackle temporal planning problems. In this paper, we define temporal versions of classical A-step and E-step plans. We show that when the casual and temporal reasoning phases of a SAT-based temporal planner are separated, these semantics can be used to translate a given temporal planning problem into a SAT formula. We introduce two different types of E-step encodings in temporal planning. The first encoding method is a temporal version of the classical E-step encoding. Like its classical counterpart, in the new encoding we suppose a few restrictive simplifying assumptions. On the other hand, by relaxing one of these assumptions, the second type of E-step encodings, which is often more compact than the first one, is introduced. However, if a temporal planning problem possesses the property that we call required causal simultaneity, neither of our proposed encodings will be expressive enough to represent a valid temporal plan. Nevertheless, we show that this property is rather rare and can be detected in polynomial time. Our experiments indicate that by embedding the proposed encodings into ITSAT, a SAT-based temporal planner based on the A-step encoding, a considerable improvement is achieved in terms of both speed and memory usage of the planner. The resulting planner significantly outperforms POPF, which is currently the state-of-the-art of temporally expressive planners.
Towards The Inductive Acquisition of Temporal Knowledge
The ability to predict the future in a given domain can be acquired by discovering empirically from experience certain temporal patterns that tend to repeat unerringly. Previous works in time series analysis allow one to make quantitative predictions on the likely values of certain linear variables. Since certain types of knowledge are better expressed in symbolic forms, making qualitative predictions based on symbolic representations require a different approach. A domain independent methodology called TIM (Time based Inductive Machine) for discovering potentially uncertain temporal patterns from real time observations using the technique of inductive inference is described here.
A Temporal Analysis of Posting Behavior in Social Media Streams
Lee, Bumsuk (The Catholic University of Korea)
In this work, we investigated the social media streams to understand their characteristics and their temporal aspects. We assumed that each blogger has different temporal preference for posting. To investigate this hypothesis, we analyzed a massive dataset, nearly 700,000 blog articles, with the consideration of two factors which are day of the week and time of the day. The comparison was done in manifold ways: Blogosphere vs. Twitter, commercial blogs vs. non-commercial blogs, and their individuals. We hope that this work provides a hint to develop a personalized system which can be used for the reduction of the system resources for pull/fetch technology.
Exploring Millions of Footprints in Location Sharing Services
Cheng, Zhiyuan (Texas A&M University) | Caverlee, James (Texas A&M University) | Lee, Kyumin (Texas A&M University) | Sui, Daniel Z. (Ohio State University)
Location sharing services (LSS) like Foursquare, Gowalla, and Facebook Places support hundreds of millions of user-driven footprints (i.e., "checkins"). Those global-scale footprints provide a unique opportunity to study the social and temporal characteristics of how people use these services and to model patterns of human mobility, which are significant factors for the design of future mobile+location-based services, traffic forecasting, urban planning, as well as epidemiological models of disease spread. In this paper, we investigate 22 million checkins across 220,000 users and report a quantitative assessment of human mobility patterns by analyzing the spatial, temporal, social, and textual aspects associated with these footprints. We find that: (i) LSS users follow the “Levy Flight” mobility pattern and adopt periodic behaviors; (ii) While geographic and economic constraints affect mobility patterns, so does individual social status; and (iii) Content and sentiment-based analysis of posts associated with checkins can provide a rich source of context for better understanding how users engage with these services.
Unit Testing for Qualitative Spatial and Temporal Reasoning
Schultz, Carl (The University of Auckland) | Amor, Robert (The University of Auckland) | Guesgen, Hans (Massey University)
Commonsense reasoning, in particular qualitative spatial and temporal reasoning (QSTR), provides flexible and intuitive methods for reasoning about vague and uncertain information including spatial orientation, topology and proximity. Despite a number of theoretical advances in QSTR, there are relatively few applications that employ these methods. The central problem is a significant lack of application level standards and validation methods for supporting developers in adapting and integrating QSTR with their domain specific qualitative spatial and temporal models. To address this we present a significantly novel methodology for QSTR application validation, inspired by research in software engineering. In this paper we focus on unit testing, and adapt the software engineering strategy of defining boundary cases. We present two critical boundary concepts, a methodology for isolating the units under testing from other parts of the model, and methods to assist the designer in integrating our critical boundary unit testing approach with a broader validation plan.
The Design and Experimental Analysis of Algorithms for Temporal Reasoning
Many applications -- from planning and scheduling to problems in molecular biology -- rely heavily on a temporal reasoning component. In this paper, we discuss the design and empirical analysis of algorithms for a temporal reasoning system based on Allen's influential interval-based framework for representing temporal information. At the core of the system are algorithms for determining whether the temporal information is consistent, and, if so, finding one or more scenarios that are consistent with the temporal information. Two important algorithms for these tasks are a path consistency algorithm and a backtracking algorithm. For the path consistency algorithm, we develop techniques that can result in up to a ten-fold speedup over an already highly optimized implementation. For the backtracking algorithm, we develop variable and value ordering heuristics that are shown empirically to dramatically improve the performance of the algorithm. As well, we show that a previously suggested reformulation of the backtracking search problem can reduce the time and space requirements of the backtracking search. Taken together, the techniques we develop allow a temporal reasoning component to solve problems that are of practical size.