Ákvarðanleiki og tjáningarkraftur tímabilarökfræði - verkefni lokið

Fréttatilkynning verkefnisstjórans

23.2.2017

The research project focused on the area of mathematical logic. In particular, we addressed several research problems in the study of interval temporal logics. Temporal reasoning plays a major role in computer science. According to the standard approach, time points are taken as the basic temporal entities and temporal domains are represented as ordered sequences of time points.

Interval temporal logics arise from a more natural perspective on time, according to which the primitive ontological entity is the time interval instead of the time point. Such an alternative approach can be justified by means of philosophical as well as practical arguments. As a matter of fact, real-world events have an intrinsic duration and thus “durationless” points are not suitable to properly deal with them.

Heiti verkefnis: Ákvarðanleiki og tjáningarkraftur tímabilarökfræði / Decidability and Expressiveness for Interval Temporal Logics
Verkefnisstjóri: Dario Della Monica, Háskólanum í Reykjavík
Tegund styrks: Rannsóknastöðustyrkur
Styrkár: 2013-2015
Fjárhæð styrks: 14,07 millj. kr. alls
Tilvísunarnúmer Rannís: 130802-05

The Modal Logic of Time Intervals HS, introduced in by Halpern and Shoham, can be viewed as the logic of Allen's relations, since it features one modal operator for each one of the 12 basic temporal relations (excluding identity) that may hold between any pair of intervals (on a linear ordering).

Unfortunately, in the area of interval logics undecidability is the rule and decidability the exception, the case of HS being paradigmatic. Indeed, Halpern and Shoham showed that the satisfiability problem for such a logic is undecidable under very weak assumptions on the class of interval structures over which it is interpreted.

For a long time, results of this nature have discouraged attempts at practical applications and further research on interval temporal logics.
A renewed interest for interval temporal logics has been recently stimulated by the discovery of expressive decidable fragments of HS.

Consequently, the identification of expressive enough, decidable fragments of HS has been added to the current research agenda for (interval) temporal logic.
While the algebra of Allen's relations, the so-called Allen's Interval Algebra, has been extensively studied and its fragments have been completely classified with respect to their relative expressive power as well as to their computational complexity (tractability/intractability of the consistency problem of fragments of Interval Algebra), the logical counterpart of these problems for HS is considerably harder and is the main subject of our research project.

By restricting the set of 12 modalities of HS, 2^12 (=4096) syntactically different languages arise.

The main results we obtained, according to the goal we intended to pursue in our proposal, are the following.

We obtained a complete classification of HS and its fragments with respect to decidability/undecidability of their satisfiability problem over the class of dense linear orders. In addition, we were able to classify all decidable fragments with respect to the computational complexity of their satisfiability problem.

We obtained a complete classification of HS and its fragments with respect to their expressive power for (i) the class of all temporal structures, (ii) the class of all dense temporal structures, (iii) the class of all discrete temporal structures, and (iv) the class of all finite temporal structures

We studied other problems on interval tempral logics, such as model checking and the problem of automated syntesis of automated synthesis of tableau systems for interval temporal logics.

From a technical point of view, interval temporal logics are much more expressive than point-based ones and more appropriate for a number of applications. In particular, interval-based temporal reasoning naturally arises in artificial intelligence (temporal knowledge representation, systems for temporal planning and maintenance, qualitative reasoning, theories of events), temporal databases (event modelling, temporal aggregation), computational linguistics (analysis of progressive tenses, semantics and processing of natural languages), and formal specification and verification of complex systems (hardware verification, protocol analysis). Therefore, during this project we laid the foundations for a systematic use of interval temporal logics in several application domains such as the above-mentioned ones.

Our investigation led us to study problems not directly related to the area of (interval) temporal logics, but yet in the macro-area of logic and formal verification for computer science.

As an example, while addressing the above-mentioned expressiveness problems, we discovered an interesting connection among modal logics, Horn theories, and hypergraph theory. We explored such a connection and we devised a new algorithm for the enumeration of maximal models of a given Horn theory, which, thanks to the connection between modal logic and Horn theories, is also useful when applied to the expressiveness issues for HS that we are interested in. A further exploration of such a connection let us to the study of new solution for the hitting set problem, in hypergraph theory.

As furhter examples, we studied:

• model checking problem for  logics for strategic reasoning in multi-agent systems,
  
• the properties of a series of formalisms for process semantics characterization
  
• a combined approach to formal verification of classic temporal logics, merging together two well-establishded techniques, such as model checking and runtime verification,
  
• extensions of omega-regular languages, characterized in terms of  extended omega-regular expressions, automata, and fragments of second-order logic,
  
• a notion for characterization of process distances, having in mind, as our ultimate goal, to solve the open problem of identifying an upper bound in the process of determining the distance between two processes.
  
• In particular, this last invetigation produced a brand-new project, having the same PI as the present one, that has been awarded an INdAM-COFUND Fellowship in Mathematics and/or Applications for experienced researchers co-founded by "Marie Curie Actions", for 2 years (2016-2018).
  

Publications produced within the projects (more are in the writing or review phase):

• L. Aceto, D. Della Monica, V. Goranko, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. A complete classification of the expressiveness of interval logics of Allen's relations: The general and the dense cases. Acta Informatica, 53(3):207-246, 2016 (DOI: 10.1007/s00236-015-0231-4,online since May 2015).
  
• Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity. Theoretical Computer Science (TCS), 560(Part 3):269-291,2014 (DOI: 10.1016/j.tcs.2014.03.033, online since April 2014).
  
• D. Romero-Hérnandez, D. de Frutos-Escrig, and D. Della Monica. Proving Continuity of Coinductive Global Bisimulation Distances: A Never Ending Story. In Proc. of the 15th Jornadas sobre PROgramación y LEnguajes (PROLE), EPTCS, 2015.
  
• Aceto, D. Della Monica, I. Fábregas, and A. Ingólfsdóttir. When are prime formulae characteristic?. In Proc. of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS), LNCS 9234, pages 76-88, 2015.
  
• Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. On the Complexity of Fragments of the Modal Logic of Allen's Relations over Dense Structures. In Proc. of the 9th International Conference on Language and Automata Theory and Applications (LATA), 2015.
  
• Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. On the expressiveness of the interval logic of Allen's relations over finite and discrete linear orders. In Proc. of the 14th European Conference on Logics in Artificial Intelligence (JELIA), LNAI 8761, pages 267-281, 2014.
  
• D. Della Monica, A. Montanari, G. Sciavicco, and D. Tishkovsky. First steps towards automated synthesis of tableau systems for interval temporal logics. In Proc. of the 5th International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking (COMPUTATION TOOLS), pages 32-37, 2014 (winner of the Best paper award).
  
• L. Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics. In Proc. of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS 8312, pages 1-17, Stellenbosch, South Africa, December 15th-19th, Springer, 2013.
  
• D. Della Monica, M. Napoli, and M. Parente. Model checking coalitional games in shortage resource scenarios. In Proc. of the 4th International International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Borca di Cadore, Dolomites, Italy, August 29th-31st, 2013.
  
• L. Aceto, D. Della Monica, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco. A complete classification of the expressiveness of interval logics of Allen's relations over dense linear orders. In Proc. of the 20th International Symposium on Temporal Representation and Reasoning (TIME), Pensacola, FL (USA), September 26th-28th, pages 65-72, 2013.
  
• D. Bresolin, D. Della Monica, A. Montanari, and G. Sciavicco. A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: an Implementation. In Proc. of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Nancy, France, September 16th-19th, LNCS 8123, pages 74-80, 2013.