{'fraction_non_alphanumeric': 0.03801295896328294, 'fraction_numerical': 0.008207343412526998, 'mean_word_length': 5.176, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
EMBEDDING-BASED APPROACHES TO TEMPORAL LOGICS : A SURVEY

Embedding LTL into IL. Linear-time temporal logic (LTL) is known to be one of the most useful logics in Computer Science, and infinitary logic (IL) is known to be an important logic in Mathematical Logic. The research fields of both LTL and IL have independently developed each other, and the relationship between them has not yet been discussed. In [1], the relationship between LTL and IL was clarified by showing some theorems for embedding LTL into IL. This embedding shows that globally and eventually operators in LTL can, respectively, be represented by infinitary conjunction and infinitary disjunction in IL. Using these embedding theorems, cut-elimination theorem was proved for LTL [1]. Extensions and generalizations of LTL. By extending and modifying the embedding theorems proposed in [1], some results on extended LTLs were obtained as follows. Cutelimination theorems were obtained for some epistemic extensions of LTL [1], cutelimination and completeness theorems were proved for a generalized first-order LTL [6], cut-elimination and completeness theorems were shown for a 3-dimensional extension of LTL [7], and completeness and decidability theorems were proved for some extensions of both a description logic and some modified LTLs [4]. A feasible and expressive variant of LTL, which is a combination of LTL and a branching-time temporal logic, was studied based on a modified embedding theorem [3]. Modifications and subsystems of LTL. In Computer Science, the decidability and complexity issues are important to implement algorithms on computers. For this aim, some subsystems of LTL have been studied based on the embedding-based methods proposed in [1]. Some decidable or NP-complete subsystems of LTL were proposed and studied in [2, 5, 9] based on the embedding-based methods. In [5, 9], decidability completeness and (strong) normalization theorems were proved for some constructive (or intuitionistic) versions of LTL. Some decidable modifications of LTL were studied in [8, 10] from the point of view of applications to Artificial Intelligence. References [1] N. Kamide, Embedding linear-time temporal logic into infinitary logic: application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic,