Due to its expressiveness and unambiguous nature, First-Order Logic (FOL) is a powerful formalism for representing concepts expressed in natural language (NL). This is useful, e.g., for specifying and verifying desired system properties. While translating FOL into human-readable English is relatively straightforward, the inverse problem, converting NL to FOL (NL-FOL translation), has remained a longstanding challenge, for both humans and machines. Although the emergence of Large Language Models (LLMs) promised a breakthrough, recent literature provides contrasting results on their ability to perform NL-FOL translation. In this work, we provide a threefold contribution. First, we critically examine existing datasets and protocols for evaluating NL-FOL translation performance, revealing key limitations that may cause a misrepresentation of LLMs' actual capabilities. Second, to overcome these shortcomings, we propose a novel evaluation protocol explicitly designed to distinguish genuine semantic-level logical understanding from superficial pattern recognition, memorization, and dataset contamination. Third, using this new approach, we show that state-of-the-art, dialogue-oriented LLMs demonstrate strong NL-FOL translation skills and a genuine grasp of sentence-level logic, whereas embedding-centric models perform markedly worse.

In runtime verification, monitoring consists of analyzing the current execution of a system and determining, on the basis of the observed finite trace, whether all its possible continuations satisfy or violate a given specification. This is typically done by synthesizing a monitor–often a Deterministic Finite State Automaton (DFA)–from logical specifications expressed in Linear Temporal Logic (LTL) or in its finite-word variant (LTLf). Unfortunately, the size of the resulting DFA may incur a doubly exponential blow-up in the size of the formula. In this paper, we identify some conditions under which monitoring can be done without constructing such a DFA. We build on the notion of intentionally safe and cosafe formulas to show that monitoring of these formulas can be carried out through trace-checking, that is, by directly evaluating them on the current system trace, with a polynomial complexity in the size of both the trace and the formula. In addition, we investigate the complexity of recognizing intentionally safe and cosafe formulas for the safety and cosafety fragments of LTL and LTLf. As for LTLf, we show that all formulas in these fragments are intentionally safe and cosafe, thus removing the need for the check. As for LTL, we prove that the problem is in PSPACE, significantly improving over the EXPSPACE complexity of full LTL.

We investigate a fragment of Linear Temporal Logic (LTL) comprising the tomorrow (X) and eventually (F) modalities, and present a singly exponential time algorithm for the pastification problem within this fragment. The pastification problem consists of constructing, for a given LTL formula, an equivalent formula that exclusively employs past temporal operators. While the best known algorithms for this task in full LTL–and in the fragment under consideration–exhibit triply exponential time complexity, our approach achieves optimal complexity for this fragment. The proposed algorithm proceeds in two main stages: (i) the input formula is first translated into a tailored normal form, and then (ii) a pure past formula is synthesized from a tree-like structure derived from the normalized formula. With minor adaptations, the algorithm extends to handle the fragment of LTL featuring the tomorrow and globally modalities. We provide an implementation of the algorithm in the temporal reasoning tool BLACK, and report on an experimental evaluation of its performance.1

First-order linear temporal logic (FOLTL) is a flexible and expressive formalism capable of naturally describing complex behaviors and properties. Although the logic is in general highly undecidable, the idea of using it as a specification language for the verification of complex infinite-state systems is appealing. However, a missing piece, which has proved to be an invaluable tool in dealing with other temporal logics, is an automaton model capable of capturing the logic. In this paper we address this issue, by defining and studying such a model, which we call first-order automaton. We define this very general class of automata, and the corresponding notion of regular first-order language (of finite words), showing their closure under most language-theoretic operations. We show how they can capture any FOLTL formula over finite words, over any signature and theory, and provide sufficient conditions for the semi-decidability of their non-emptiness problem. Then, to show the usefulness of the formalism, we prove the decidability of monodic FOLTL, a classic result known in the literature, with a simpler and direct proof.

Monitoring is a runtime verification technique that allows one to check whether an ongoing computation of a system (partial trace) satisfies a given formula. It does not need a complete model of the system, but it typically requires the construction of a deterministic automaton doubly exponential in the size of the formula (in the worst case), which limits its practicality. In this paper, we show that, when considering finite, discrete traces, monitoring of pure past (co)safety fragments of Signal Temporal Logic (STL) can be reduced to trace checking, that is, evaluation of a formula over a trace, that can be performed in time polynomial in the size of the formula and the length of the trace. By exploiting such a result, we develop a GPU-accelerated framework for interpretable early failure detection based on vectorized trace checking, that employs genetic programming to learn temporal properties from historical trace data. The framework shows a 2–10% net improvement in key performance metrics compared to the state-of-the-art methods.

Krohn-Rhodes theory encompasses the techniques for the study of finite automata and their decomposition into elementary automata. The famous result of Krohn and Rhodes roughly states that each finite automaton can be decomposed into elementary components which correspond to permutation and reset automata connected by a cascade product. However, this outcome is not easy to access for the working computer scientist. This paper provides a short introduction into Krohn-Rhodes theory based on the valuable work of Ginzburg.

Linear Temporal Logic over finite traces ( LTL f ) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL f ( pLTL ) is the variant of LTL f featuring only past temporal modalities, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL f is also definable in pLTL , and vice versa (they are expressively equivalent). The same goes for the safety and cosafety fragments of Linear Temporal Logic over infinite traces ( LTL ), when compared to G ( pLTL ) and F ( pLTL ) formulas, respectively, that is, pLTL formulas prefixed by a globally and an eventually modality. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. Moreover, when considering (co)safety fragments of LTL devoid of binary temporal modalities, there are no known characterizations based on pLTL . In this paper, we investigate succinctness issues for LTL f and (co)safety fragments of LTL when compared with their pure past counterparts. First, we provide a pure past characterization of the (co)safety fragments of LTL devoid of binary temporal modalities. Then, we prove that the (co)safety fragments of LTL have pure past counterparts that can be exponentially more succinct. Finally, we show that the same holds for LTL f with respect to pLTL , and viceversa: LTL f and pLTL are incomparable when succinctness is concerned.

Given a specification of Linear-time Temporal Logic interpreted over finite traces (LTLf), the reactive synthesis problem asks to find a finitely-representable, terminating controller that reacts to the uncontrollable actions of an environment in order to enforce a desired system specification. In this paper we study, for the first time, the foundations of reactive synthesis for DECLARE, a well-established declarative, pattern-based business process modelling language grounded in LTLf. We provide a threefold contribution. First, we define a reactive synthesis problem for DECLARE. Second, we show how an arbitrary DECLARE specification can be polynomially encoded into an equivalent pure-past one in LTLf, and exploit this to define an EXPTIME algorithm for DECLARE synthesis. Third, we derive a symbolic version of this algorithm, by introducing a novel translation of pure-past temporal formulas into symbolic deterministic finite automata.

Abstract Operator Precedence Languages (OPL) have been recently identified as a suitable formalism for model checking recursive procedural programs, thanks to their ability of modeling the program stack. OPL requirements can be expressed in thePrecedence Oriented Temporal Logic(), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other advanced programming constructs that previous approaches, such as Visibly Pushdown Languages, cannot model effectively. Existing approaches for model checking of have been designed following the explicit-state, automata-based approach, a feature that severely limits their scalability. In this paper, we give the first symbolic, SMT-based approach for model checking properties. While previous approaches construct the automaton for both the formula and the model of the program, we encode them into a (sequence of) SMT formulas. The search of a trace of the model witnessing a violation of the formula is then carried out by an SMT-solver, in a Bounded Model Checking fashion. We carried out an experimental evaluation, which shows the effectiveness of the proposed solution.

Abstract This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past ( $$\textsf{LTL}$$ LTL ) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages $$(\mathcal {L}_n)_{n \ge 1}$$ ( L n ) n ≥ 1 such that $$\mathcal {L}_n$$ L n can be expressed with a pure future formula of size $$\mathcal {O}(n)$$ O ( n ) , but it requires formulae of size $$2^{\varOmega (n)}$$ 2 Ω ( n ) to be captured with past formulae. As a by-product, such a succinctness result shows the optimality of the pastification algorithm proposed in [Artale et al., KR, 2023]. We show that, in the considered case, succinctness cannot be proven by relying on the classical automata-based method introduced in [Markey, Bull. EATCS, 2003]. In place of this method, we devise and apply a combinatorial proof system whose deduction trees represent $$\textsf{LTL}$$ LTL formulae. The system can be seen as a proof-centric (one-player) view on the games used by Adler and Immerman to study the succinctness of $$\textsf{CTL}$$ CTL .

Abstract Linear temporal logic( $$\textsf{LTL}\,$$ LTL ) and its variant interpreted onfinite traces( $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf ) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the satisfiability problem for $$\textsf{LTL}\,$$ LTL and $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf formulas, for which many techniques have been devised during the last decades. Among these aretableau systems, of which the most recent is Reynolds’ tree-shaped tableau. We provide a SAT-based algorithm for $$\textsf{LTL}\,$$ LTL and $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf satisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.

In the timeline-based approach to planning, the evolution over time of a set of state variables (the timelines) is governed by a set of temporal constraints. Traditional timeline-based planning systems excel at the integration of planning with execution by handling temporal uncertainty. In order to handle general nondeterminism as well, the concept of timeline-based games has been recently introduced. It has been proved that finding whether a winning strategy exists for such games is 2EXPTIME-complete. However, a concrete approach to synthesize controllers implementing such strategies is missing. This paper fills this gap, by providing an effective and computationally optimal approach to controller synthesis for timeline-based games.

Abstract Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past ( ) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response ( $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P for short) has been introduced. It allows one to express safety languages definable in and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce - , an extension of $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P in practice. Second, we the expressiveness of - starting from the expressiveness of its fragments. In particular, we prove that: (1) $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P is expressively complete with respect to the safety fragment of , (2) the removal of past operators from $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P results into a loss of expressive power, and (3) - is expressively equivalent to the logic of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from - specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) . The experimental evaluation shows promising results.

Linear Temporal Logic (LTL) is the de-facto standard temporal logic for system specification, whose foundational properties have been studied for over five decades. Safety and cosafety properties of LTL define notable fragments of LTL, where a prefix of a trace suffices to establish whether a formula is true or not over that trace. In this paper, we study the complexity of the problems of satisfiability, validity, and realizability over infinite and finite traces for the safety and cosafety fragments of LTL. As for satisfiability and validity over infinite traces, we prove that the majority of the fragments have the same complexity as full LTL, that is, they are PSPACE-complete. The picture is radically different for realizability: we find fragments with the same expressive power whose complexity varies from 2EXPTIME-complete (as full LTL) to EXPTIME-complete. Notably, for all cosafety fragments, the complexity of the three problems does not change passing from infinite to finite traces, while for all safety fragments the complexity of satisfiability (resp., realizability) over finite traces drops to NP-complete (resp., Πᴾ₂- complete).

We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLMTf), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by first-order formulas and where first-order variables referring to different time points can be compared. In general, LTLMTf was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics), with a tableau-based semi-decision procedure. In this paper we present a sound and complete pruning rule for the LTLMTf tableau. We show that for any LTLMTf formula that satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with the new rule is also guaranteed to terminate. Last but not least, this technique allows us to establish novel decidability results for the satisfiability of several fragments of LTLMTf, as well as to give new decidability proofs for classes that are already known.

Confronting the past can be hard. This is true even in Linear Temporal Logic (LTL), interpreted on either infinite or finite traces, when faced with the problem of transforming a temporally future formula into an equivalent one that contains past temporal modalities only. To our knowledge, the best among the available pastification procedures for full LTL, as well as for expressive enough fragments of it (that is, containing at least one temporal modality other than tomorrow), are triply exponential in the size of the input. In this paper, we focus on the fragment of LTL that features the tomorrow and eventually modalities, and provide a singly exponential pastification algorithm for it. The transformation is based on a normalisation procedure that requires a non-trivial complexity analysis, and on the subsequent generation of a pure past formula from suitably-defined dependency tree structures. Moreover, leveraging its purely syntactic nature, we present an implementation of our procedure in a temporal satisfiability checking tool that deals with both future and past modalities.

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.

Abstract Linear Temporal Logic ( $$\mathsf {LTL}$$ LTL ) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Its widespread use is also due to its strong foundational properties. One of them is Kamp’s theorem, showing that $$\mathsf {LTL}$$ LTL and the first-order theory of one successor ( $$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] ) are expressively equivalent. Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not or does belong to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for $$\mathsf {LTL}$$ LTL . $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL (resp., $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL ) is a fragment of $$\mathsf {LTL}$$ LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. In this paper, we introduce a fragment of $$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] , called $$\mathsf {Safety\text {-} FO}$$ Safety - FO , and its dual $$\mathsf {coSafety\text {-} FO}$$ coSafety - FO , which are expressively complete with regards to the $$\mathsf {LTL}$$ LTL -definable safety languages. In particular, we prove that they respectively characterise exactly $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL and $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL , a result that joins Kamp’s theorem, and provides a clearer view of the charactisations of (fragments of) $$\mathsf {LTL}$$ LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in $$\mathsf {LTL}$$ LTL is definable in $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL interpreted over finite and infinite traces.

This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and describing such use cases, we provide a sound and complete semi-decision procedure for LTLfMT based on the SMT encoding of a one-pass tree-shaped tableau system. The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks.

LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.

Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades.It consists in the synthesis of a controller that reacts to environment's inputs satisfying a given temporal logic specification.Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability.In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (LTL EBR ), that allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases), and we show that reactive synthesis from LTL EBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification.We prove the correctness of the proposed approach and we successfully evaluate it on various benchmarks.