In September 2013, we organized the 20th International Symposium on Temporal Representation and Reasoning (TIME’13) that took place in Pensacola, FL (USA). After 20 years, the Symposium returned to the venue where it originally started. TIME has grown since its original incarnation as a workshop to become an international symposium encompassing several different areas of computer science which deal, in some way or another, with the concept of time, its representation, reasoning and applications. This event has provided an opportunity for scientific exchange for researchers coming from different areas such as artificial intelligence, databases, temporal logic, and formal methods. The work presented at the 2013 Symposium concerned several different temporal aspects of information and computation and comprises a unique combination of innovative theoretical results and successful applications.

This special issue of Acta Informatica originates from a call for papers sent out right after the symposium, in which we invited the authors of the highest ranked papers—according to the reviews carried out by the Program Committee members—to submit an extended version. After two rounds of reviews performed by additional experts the following papers were selected for publication in the special issue. We thank all reviewers for their commitment and dedication.

The paper “A Faster Execution Algorithm for Dynamically Controllable Simple Temporal Networks with Uncertainty”, by Luke Hunsberger, presents novel algorithms for managing the execution of dynamically controllable simple temporal networks with uncertainty. For the first time, full proofs of the correctness of these algorithms in a self-contained manner are presented.

The paper “Optimization in Temporal Qualitative Constraint Networks” by Jean-François Condotta, Souhila Kaci and Yakoub Salhi presents a variety of results about temporal qualitative constraint networks (TQCNs) where the constraints are those from the point or interval algebras. The paper focuses on the MinCons problem, showing that it is NP-complete for TQCNs over both algebras, but polynomial when the TQCNs are restricted to be defined over convex relations.

The paper “A Tool for Deciding the Satisfiability of Continuous-time Metric Temporal Logic” by Marcello M. Bersani, Matteo Rossi and Pierluigi San Pietro introduces a new extension of linear temporal logic for specifying real-time properties, namely CLTL over clocks, and presents an approach for the satisfiability problem for CLTLoc via a reduction to a satisfiability modulo theory (SMT). Since several other real-time temporal logics can be translated into CLTLoc, these results enable the use of SMT for the satisfiability problem of these logics.

The paper “A complete classification of the expressiveness of interval logics of Allen’s relations over dense linear orders” by Luca Aceto, Dario Della Monica, Anna Ingólfsdóttir, Angelo Montanari and Guido Sciavicco studies the well-known interval temporal logic HS in the case of two classes of orders: the class of all the linear orders and the class of all the dense linear orders. This work carries out a major systematic categorisation of these fragments of HS motivated in part by the desire to identify which of the fragments might be especially suitable for applications and tools.

The paper “Extracting Unsatisfiable Cores for LTL via Temporal Resolution” by Viktor Schuppan presents a method to extract unsatisfiable cores from a given unsatisfiable LTL formula, based on temporal resolution. The method takes a resolution proof and extracts an explanation of why the formula is unsatisfiable. The method presented is experimentally evaluated on various LTL formulas, including system specifications of reactive systems from the literature.

The paper “Metric temporal logic revisited” by Mark Reynolds introduces a new metric temporal logic, 1CMTL and shows its decidability through translation into a previously introduced decidable logic, MRTL. Since the translation involves an exponential blowup and the decision procedure for MRTL is PSPACE, the resulting algorithm for 1CMTL with the defined semantics is EXPSPACE.

We hope the readers will enjoy this special issue as much as we enjoyed assembling it.