Our main focus during this visit was to investigate possible leads for new decidable fragments of counting temporal logics. There are several natural ways to augment classical temporal logics with the ability to count. One possibility is to express constraints on the number of occurrences of certain events a path, by labeling temporal modalities with expressions of the kind “at most k occurrences”, “exactly k occurrences”, and so on. Both Kamal Lodaya (together with A. V. Sreejith) and Antoine Meyer (with François Laroussinie and Eudes Petonnet) have proposed some work on this topic in the past, in the context of the logics LTL and CTL. During this visit we examined more recent work on graded temporal logics (where counting constraints relate to the number of paths satisfying a given formula), both in terms of model-checking as in a 2009 journal paper by Ferrante et al., and in terms of satisfiability as studied by Bianco et al. in a journal paper in 2012. We also studied a general coalgebraic approach for model checking by Hasuo et al. in POPL 2016. Unfortunately the algorithmic properties are quite varying. We formulated an approach for systematically studying the model checking problem for a fragment of temporal logics combining path counting and counting along paths, and hope to obtain some results over the next few months.
Some time was also dedicated to following and understanding an exposition of the proof of Cobham’s Theorem by Jean-Marc Deshouillers, who was also present at the time of this stay and gave a three-part lecture on this topic. This ties into the theme of a regional project with researchers from the Réunion Island, on the topic of automatic numbers and strings.