We present an on-the-fly synthesis framework for Linear Temporal Logic over Finite Traces ( LTL \({}_{f}\) ) based on top-down deterministic automata construction. Existing approaches rely on constructing a complete Deterministic Finite Automaton ( DFA ) corresponding to the LTL \({}_{f}\) specification, a process with doubly exponential complexity relative to formula size in the worst case. In this case, the synthesis cannot be conducted until the entire DFA is constructed. This inefficiency is the main bottleneck of existing approaches. To address this challenge, we first present a method for converting LTL \({}_{f}\) into Transition-Based DFA ( TDFA ) by directly leveraging LTL \({}_{f}\) semantics, incorporating intermediate results as direct components of the final automaton to enable parallelized synthesis and automata construction. We then explore the relationship between LTL \({}_{f}\) synthesis and TDFA games and subsequently develop an algorithm for performing LTL \({}_{f}\) synthesis via on-the-fly TDFA game solving. This algorithm traverses the state space in a global forward manner combined with a local backward method, along with detecting strongly connected components. Moreover, we introduce two optimization techniques—model-guided synthesis and state entailment—to enhance the practical efficiency of our approach. Experimental results demonstrate that our on-the-fly approach achieves the best performance on the tested benchmarks and effectively complements existing approaches.

Reactive synthesis from Linear Temporal Logic over finite traces (LTLf) can be reduced to a two-player game over a Deterministic Finite Automaton (DFA) of the LTLf specification. The primary challenge here is DFA construction, which is 2EXPTIME-complete in the worst case. Existing techniques either construct the DFA compositionally before solving the game, leveraging automata minimization to mitigate state-space explosion, or build the DFA incrementally during game solving to avoid full DFA construction. However, neither is dominant. In this paper, we introduce a compositional on-the-fly synthesis framework that integrates the strengths of both approaches, focusing on large conjunctions of smaller LTLf formulas common in practice. This framework applies composition during game solving instead of automata (game arena) construction. While composing all intermediate results may be necessary in the worst case, pruning these results simplifies subsequent compositions and enables early detection of unrealizability. Specifically, the framework allows two composition variants: pruning before composition to take full advantage of minimization or pruning during composition to guide on-the-fly synthesis. Compared to state-of-the-art synthesis solvers, our framework is able to solve a notable number of instances that other solvers cannot handle. A detailed analysis shows that both composition variants have unique merits.

Abstract In this paper, we consider the minimal unsatisfiable core (MUC) problem for linear temporal logic over finite traces (LTL$_{f}$), which nowadays is a popular formal-specification language for AI-related systems. Efficient algorithms to compute such MUCs can help locate the inconsistency rapidly in the written LTL$_{f}$ specification and are very useful for the system designers to amend the flawed requirement. As far as we know, there are no available tools off-the-shelf so far that provide MUC computation for LTL$_{f}$. We present here two generic approaches NaiveMUC and BinaryMUC to compute an MUC for LTL$_{f}$. Moreover, we introduce heuristics that are based on the Boolean unsatisfiable core (UC) technique to accelerate the two approaches, which are named NaiveMUC+UC and BinaryMUC+UC, respectively. In particular, for global LTL$_{f}$ formulas, we show that the MUC computation can be reduced to the pure Boolean MUC computation, which therefore conducts the GlobalMUC approach. Our experiments show that GlobalMUC performs the best to compute an MUC for global formulas, and BinaryMUC+UC is the best for an arbitrary unsatisfiable formula.

Linear Temporal Logic over finite traces, or LTL f , is a popular logic to describe specifications with finite behaviors in AI scenarios such as motion planning.Satisfiability is one of the fundamental problems of LTL f and extensive studies have been conducted to speed up the process to check whether a given LTL f formula is satisfiable.This paper presents a new approach, namely LSCFP, to solve the problem of LTL f satisfiability checking by leveraging the formula progression technique.Compared to previous work, LSCFP utilizes formula progression to gather more information propagated along with the search path such that it can find satisfiable models more quickly if the input formula is satisfiable.A comprehensive experimental evaluation has been conducted to show the efficiency of LSCFP, and the results suggest that LSCFP is able to gain at least 15% performance improvement on checking satisfiable formulas when compared to the state-of-the-art LTL f satisfiability checker aaltaf.

Abstract We present , a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats for word-level hardware model checking and was used in the most recent hardware model checking competition. Compared to bit-level one, word-level model checking is a more complex research field at an earlier stage of development. Therefore, it is necessary to develop a tool that can produce a large number of test cases in Btor2 format to test either existing or under-developed word-level model checkers. To evaluate the practicality of , we tested the state-of-the-art word-level model checkers and with the generated benchmarks. Experimental results show that both tools are buggy and not mature enough, which reflects the practical value of .

Model checking is an automatic formal verification method that is widely applied to hardware verification. Safety properties are the mainly verified properties in practice that can be falsified within finite steps if they do not hold for systems. However, state-of-the-art safety model-checking algorithms cannot meet the performance requirement driven by the industry as the sizes of (hardware) systems to be verified increase rapidly. Therefore, more efficient techniques are still eagerly in demand. Recently, a new safety model-checking technique complementary approximate reachability (CAR) was presented and received considerable concerns from the community. CAR has shown its advantages in unsafe checking (bug finding), but cannot be as competitive as other state-of-the-art techniques, e.g., IC3/PDR, on safe checking (proving correctness). In this article, we propose four kinds of heuristics, two inspired by IC3/PDR and another two dedicated to CAR, to improve the performance of CAR. We integrate the heuristics into the open-source model checker SimpleCAR and compare the performance to the original CAR and IC3/PDR on 748 instances from the hardware model-checking competitions. Our results show that by fixing the time and memory resources, CAR can solve 124 more instances with the four proposed heuristics, i.e., 53.4% more instances can be solved comparing to the original CAR. Furthermore, CAR in both forward and backward directions can solve ten more instances than IC3/PDR in corresponding directions, and uniquely solve 44 more instances that IC3/PDR in corresponding directions cannot solve, which increases the capability of the current model-checking portfolio.

Bounded Model Checking (BMC) is so far considered as the best engine for bug-finding in hardware model checking. Given a bound K, BMC can detect if there is a counterexample to a given temporal property within K steps from the initial state, thus performing a global-style search. Recently, a SAT-based model-checking technique called Complementary Approximate Reachability (CAR) was shown to be complementary to BMC, in the sense that frequently they can solve instances that the other technique cannot, within the same time limit. CAR detects a counterexample gradually with the guidance of an over-approximating state sequence, and performs a local-style search. In this paper, we consider three different ways to combine BMC and CAR. Our experiments show that they all outperform BMC and CAR on their own, and solve instances that cannot be solved by these two techniques. Our findings are based on a comprehensive experimental evaluation using the benchmarks of two hardware model checking competitions.

Synthesis techniques for temporal logic specifications are typically based on exploiting symbolic techniques, as done in model checking. These symbolic techniques typically use backward fixpoint computation. Planning, which can be seen as a specific form of synthesis, is a witness of the success of forward search approaches. In this paper, we develop a forward-search approach to full-fledged Linear Temporal Logic on finite traces (LTLf) synthesis. We show how to compute the Deterministic Finite Automaton (DFA) of an LTLf formula on-the-fly, while performing an adversarial forward search towards the final states, by considering the DFA as a sort of AND-OR graph. Our approach is characterized by branching on suitable propositional formulas, instead of individual evaluations, hence radically reducing the branching factor of the search space. Specifically, we take advantage of techniques developed for knowledge compilation, such as Sentential Decision Diagrams (SDDs), to implement the approach efficiently.

We present a new synthesis framework based on the on-the-fly DFA construction for LTL over finite traces (LTLf ). Extant approaches rely heavily on the construction of the complete DFA w.r.t. the input LTLf formula, whose size can be doubly exponential to the size of the formula in the worst case. Under those approaches, the synthesis cannot be conducted unless the whole DFA is completely constructed, which is not only inefficient but also not scalable in practice. Indeed, the DFA construction is the main bottleneck of LTLf synthesis in prior work. To mitigate this challenge, we follow two steps in this paper: Firstly, we present several light-weight pre-processing techniques such that the synthesis result can be obtained even without DFA construction; Secondly, we propose to achieve the synthesis together with the on-the-fly DFA construction such that the synthesis result can be obtained before constructing the whole DFA. The on-the-fly DFA construction is implemented using the SAT-based techniques for automata generation. We compared our new approach with the traditional ones on extensive LTLf synthesis benchmarks. Experimental results showed that the pre-processing techniques have a significant advantage on the synthesis performance in terms of scalability, and the on-the-fly synthesis is able to complement extant approaches on both realizable and unrealizable cases.

In this paper, we consider the automata construction problem for Linear Temporal Logic over finite traces, i.e., LTLf. We propose a SAT-based approach to translate an LTLf formula to both of its equivalent Nondeterministic and Deterministic Finite Automata (NFA and DFA). Notably, the generated automata are transition-based instead of state-based, which may potentially be a better fit for the applications that can be achieved on the fly, e.g. LTLf satisfiability checking and synthesis. Unlike extant approaches to translate LTLf formulas to the equivalent finite automata, which are indirect and have to introduce intermediate procedures, our methodology enables the direct construction from LTLf formulas to the finite automata. We evaluated our NFA construction together with other two LTLf -to-automata approaches implemented in the MONA and SPOT tools, which shows that the performance of our construction is comparable to the other two. We leave the comparison on the DFA construction in the future work.