Distributed systems depend on correct protocol implementations, but testing them remains complex due to concurrency and data-dependent behaviors. We explore the use of First-Order Linear Temporal Logic (FOLTL) for both ofline and online monitoring, enabling precise specification of system properties over execution traces. While, in general, FOLTL is undecidable, recent advances in automated reasoning tools make reasoning in practical fragments feasible, opening new directions for validating real-world distributed systems. We present example specifications of real-world distributed protocols and outline research avenues that could facilitate the use of FOLTL fragments in testing such systems.
Distributed systems are crucial in the modern world, as they underpin essential services such as social networks, banking infrastructures, and cloud applications. Consequently, they must remain available at all times. For these systems to operate correctly, protocols are required to ensure communication and coordination among nodes. However, these distributed protocols are error-prone and inherently challenging to test. Ideally, we would like to formally prove that they are error-free. However, such proofs typically target the theoretical protocol rather than real-world implementations, as verifying production code with existing formal tools is a labour-intensive, complex task beyond the skillset of the standard developer. Hence, these proofs often ensure algorithmic correctness, but do not guarantee that implementations are free of bugs.
Despite this, implementations of widely known consensus algorithms, such as FaB Paxos [
Specification-based testing approaches for distributed protocols have long been used to identify violations of desired properties. These approaches rely on formal specification languages to model expected behaviors, such as Alloy [9]—used to uncover counterexamples in the Chord protocol [10] by generating traces through the Alloy Analyzer model checker [11]. Similarly, TLA+ [12] has been employed to prevent bugs in AWS protocols from reaching production [13], and to detect violations in protocol implementations through ofline monitoring —that is, checking whether execution traces comply with a specification after system execution has completed [ 14]. Ofline monitoring techniques have also been explored using specifications written in fragments of interval temporal logics [15].
Recent work has investigated online monitoring of execution traces—checking properties at runtime as the system executes—using specifications expressed in fragments of First-Order Linear Temporal Logic (FOLTL) [16, 17, 18], which extends classic Linear Temporal Logic (LTL) [19] with first-order theories.
For example, Decker et al. [20] monitor temporal logic over structures within some theory; Felli et al. [21] introduce ALTLf, which supports arithmetic constraints over finite traces; and Faella et al. [ 22] propose monitoring using LTLfMT [23], another fragment with first-order theories. These approaches typically rely on tightly integrated reasoning engines, such as Satisfiability Modulo Theories ( SMT) solvers [24], tableaux procedures, or automata-based methods.
Performing online monitoring with FOLTL is challenging, as it requires solving satisfiability problems, and satisfiability in FOLTL is highly undecidable, since the set of valid formulas in the full FOLTL formalism is not even recursively enumerable [25]. However, several (semi-)decidable fragments have been identified for satisfiability and model checking tasks, and are already used in state-of-the-art tools. For instance, a notable line of research in verification has studied linear-time properties enriched with first-order conditions for specific datatypes, such as arithmetic constraints: in these settings, variables can store numeric values subject to (linear) arithmetic operations [26, 27, 28]. Other fragments involving arithmetics have been studied in [29], where an SMT-based decision procedure has been implemented. The aforementioned LTLfMT, supported by the general-purpose BLACK satisfiability checker [30] and introduced by Geatti et al. [23], led to decidable fragments studied further [31], which are tractable thanks to the eficient SMT solvers used as backend (e.g., Z3 [32] and cvc5 [33]). Another SMT solver based on decidable fragments of FOLTL is the model checker LinDMT [34], which significantly extends [29] to support general first-order theories and richer datatypes. In contrast, the ofline monitoring of distributed protocols using FOLTL remains largely unexplored, despite not facing the same undecidability barriers.
Beyond its role as a formalism, FOLTL is significant for motivating the development of reasoning techniques for expressive fragments in the context of satisfiability, reactive synthesis and realizability, as demonstrated by the approaches by Rodríguez et al. [35, 36, 37].
The choice of FOLTL over LTL alone is motivated by expressiveness. While LTL sufices for reasoning about propositional temporal properties, it lacks the ability to express constraints involving structured data and quantification over variables [ 38], capabilities required to specify the correctness of distributed protocols. For instance, verifying a key-value store’s behavior requires reasoning about relationships between keys and values, which necessitates first-order constructs and theories. When extended with past temporal operators, something not supported by TLA+, despite its widespread use, FOLTL becomes more readable and allows properties to be expressed more naturally, making it a strong candidate for general-purpose specification and monitoring of complex systems.
This paper investigates how specifications written in FOLTL can be used to express correctness properties for testing a wide range of distributed protocol implementations. The proposed approach involves instrumenting the system under test to produce logs that capture operations and relevant state changes during execution. These logs form execution traces, which are then checked against FOLTL specifications defining the desired system behavior.
A central challenge lies in designing a monitor that, given a trace and a formula from a generalpurpose fragment of FOLTL, can determine whether the trace satisfies the specified property. While ofline monitoring is typically more tractable than online monitoring from a theoretical standpoint, practical scalability remains an open question. Execution traces and domains over which quantifiers range may be large.
To demonstrate the feasibility of this approach, we provide example specifications for real-world distributed protocols and highlight research directions that could support the use of first-order temporal logic fragments in testing complex systems.
FOLTL [16, 17, 18] extends LTL [19] with first-order quantification, allowing precise specification of time-dependent, data-rich, dynamic behaviors of complex systems that evolve over time. The following syntax is based on that presented by Geatti et al. [39].
Let Σ = ∪ ∪ ℱ ∪ be a first-order signature over mutually disjoint, finite sets of constants, variables, functions, and predicate symbols, respectively. The syntax of Σ -terms is defined as follows: := | | (1, . . . , ) where ∈ , ∈ , ∈ ℱ , and 1, . . . , are Σ -terms. The syntax of Σ -formulas is defined as follows: := (1, . . . , ) | 1 = 2 | ¬ | ∨ | ∃ . | X | Y | U | S where ∈ , 1, . . . , are Σ -terms, ∈ , and the temporal operators X, Y, U, and S are called next, yesterday, until and since. Derived constructs, such as ∧, ⇒, ⊤, ∀, F, G, O, H, are defined as usual.
Let : (, , ℱ → ) be an environment that maps Σ -terms to values in their domains. The evaluation of under , denoted , is defined as: = , = (), and (1, . . . , ) = (1 , . . . , ).
Let = (1, ..., ) be an event, where ∈ is an -ary predicate symbol and 1, . . . , are domain values. An event states that a certain predicate with arguments is true.
Let be a finite sequence of finite sets of events, henceforth referred to as a trace, where each set corresponds to a discrete time point ∈ N. A trace emulates an execution of a system, representing the sequence of events that occur over time in a specific run: = [{1, . . . , }, . . . , {, . . . , }].
The satisfaction of a FOLTL formula with respect to an environment and a trace at time point ∈ N is denoted by , , |= . The inductive semantics for boolean connectives, quantifiers, and temporal operators follow standard definitions (e.g., the one presented by Geatti et al. [ 39]), except for the following adaptation to our custom trace: , , |= (1, . . . , ) if [] ∋ (1 , . . . , ).
The general-purpose FOLTL fragment provides a framework for validating execution traces. In order for us to get traces, the system under test must be instrumented. In distributed systems, this includes correlating events across nodes. These traces are then checked against specifications by a monitor.
Formally, given an execution trace , a property specification is verifiable if and only if there exists an environment such that , , 0 |= , i.e., if holds at the initial time point of the trace.
Using two distributed protocol examples, we illustrate how to express both safety—“nothing bad ever happens”—and liveness—“something good eventually happens”—properties using FOLTL that can be later tested against concrete implementations. The modeled specifications are mostly event-based and applicable to both online and ofline trace monitoring.
2PCs [40, 41] are fundamental to distributed systems, enabling atomic commitment across multiple nodes, i.e., all participants in a transaction either commit or abort together. Unlike consensus algorithms, which rely on majority voting, 2PC requires unanimous agreement. Though conceptually simple, the protocol must handle failures and asynchronous communication.
Our model includes a single coordinator and multiple uniquely identified participants. Upon receiving a prepare request, a participant writes the transaction data to disk, checks database consistency and constraints, and, if valid, votes to commit, locking all the necessary resources. Example properties, modeled as FOLTL formulas, use predicates parameterized by nodes , transactions , and data . • prepare(, , ): the coordinator requests node to prepare for the transaction with data . • v-commit(, ): node votes to commit transaction and sends the response to the coordinator. • v-abort(, ): node votes not to commit transaction and sends the response to the coordinator. • i-commit(): the coordinator instructs all participant nodes to commit transaction . • i-abort(): the coordinator instructs all participant nodes not to commit transaction . • commit(, ): node commits transaction .
LIVENESS Eventual decision: if the coordinator asks some participant node to prepare for transaction , that transaction will eventually be either committed or aborted.
∀ . G︁( (︀ ∃ . prepare(, , − ) ⇒ F︀( i-commit() ∨ i-abort())︀ ︀) ︁) SAFETY Atomic commitment: if the coordinator instructs to commit transaction , then all participants must have voted to commit it; if it instructs to abort , then at least one node has voted to abort it. ∀ . G︁( (︀ i-commit() ⇒ ¬∃ . O v-abort(, ))︀ ∧ ︀( i-abort() ⇒ ∃ . O v-abort(, ))︀ ︁) SAFETY Commit justification : if a node commits a transaction, then the coordinator must have instructed the commit, which must have been preceded by a vote to commit from that node, and in turn, a prepare. ∀ , . G commit(, ) ⇒ O︀( i-commit() ∧ O(v-commit(, ) ∧ O prepare(, , − )))︀ )︁ ︁(
DHTs [10, 41] are central to peer-to-peer systems, ofering scalable, decentralized key–value storage. However, their dynamic topology and inherent concurrency make correctness testing particularly challenging.
In our model, the network consists of uniquely identified nodes that store key–value pairs. While network states span multiple time points, operations take inputs and yield outputs only upon completion. Thus, for this DHT scenario, we model them as instantaneous, with explicit FOLTL predicates marking their beginning and end. Efects of operations are defined to occur between these events. Predicates are parameterized by nodes , keys , values , and unique identifiers that link related predicates. For readability, these identifiers appear as subscripts but are semantically just additional arguments. Examples of operations, network states, and properties include: • b-store(, , ): the client requests node to store the key-value pair (, ) in the DHT. • e-store(′): the operation completes at node ′, which notifies the client upon completion. • b-lookup(, ): the client requests the value for key from node in the DHT. • e-lookup(′, ): the operation completes at the node ′ storing (, ) and returns to the client. • stable: the network remains unchanged, with no node joins, departures, or failures. SAFETY Lookup consistency: if a lookup obtains a value for a given key , then the (, ) pair was previously written by a store operation and there are no fabricated values.
︁( ∀ , . G ∀ .(︀ b-lookup(− , ) ∧ F e-lookup(− , ))︀ ⇒ O b-store(− , , ) ︁) SAFETY Value freshness: if a lookup obtains a value for a given key , then is the latest stored value for key , that is, any past store of a diferent value ′ for must have been followed by a store of . ∀ , . G︁( ∀ .(︀ b-lookup(− , ) ∧ F e-lookup(− , ))︀ ⇒ ︀( ∀ ′ ̸= . O(︀ b-store(− , , ′) ⇒ F b-store(− , , ))︀ )︁ LIVENESS Operation termination: if the network is stable, then every store or lookup operation eventually completes, that is, for any operation , once it starts, it will eventually end.
︁( ∀ . G stable ⇒ ︀( b-store(. . .) ⇒ F e-store(− )︀) ∧ ︀( b-lookup(. . .) ⇒ F e-lookup(. . .))︀ )︁
Online monitoring is the process of checking a system’s execution at runtime to determine whether its ongoing behavior satisfies a specification formula. At each step, only a finite prefix of the trace is available, requiring the monitor to evaluate compliance with respect to all possible future extensions. This setting demands incremental reasoning under uncertainty and involves decision procedures such as (FOLTL) SAT solving, making the problem challenging and at least as hard as satisfiability checking.
For a given trace and a FOLTL formula , the online monitoring problem is the task of determining the monitoring state ∈ {, , , } that satisfies one of the following conditions [22]: • = if |= and ′ ̸|= for some trace ′ • = if |= and ′ |= for every trace ′ • = if ̸|= and ′ |= for some trace ′ • = if ̸|= and ′ ̸|= for every trace ′ current satisfaction permanent satisfaction current violation permanent violation While satisfiability for general-purpose FOLTL is undecidable, several fragments are known to be tractable or (semi-)decidable, with dedicated reasoning techniques [20, 21, 22]. Tools like BLACK [23], based on SAT/SMT solving, and analyzers like Alloy [9], have been developed to target fragments and are good candidates to be adapted for online monitoring by encoding specifications into their languages.
Ofline monitoring , on the other hand, refers to the post-execution analysis of a system, where a complete trace is checked against a specification formula . Since the entire finite trace is available beforehand, the monitor can evaluate with full access to past and future events.
This setting often avoids SAT solving, remaining decidable, as variable domains are bounded by the trace. Verification becomes concrete: variables are instantiated with observed values, reducing the task to checking over known data. Eficient monitoring can possibly leverage pattern matching, automata, or symbolic rewriting, aided by preprocessing and static analysis. Despite ofline monitoring not requiring SAT tools, FOLTL fragments remain valuable for their expressiveness, as they support quantification, temporal reasoning, and predicates for specifying rich properties.
Because this work focuses on testing distributed protocols, it is important to acknowledge that obtaining suitable execution traces is a non-trivial challenge. Instrumenting distributed systems requires correlating and ordering events across independent nodes, often in the presence of delays, clock skew, or failures. Although this is a separate concern and beyond the scope of this work, reliably constructing such traces is a necessary prerequisite and it directly impacts the feasibility of monitoring.
The protocols in Section 3 are simplified case studies meant to illustrate the expressive power of FOLTL in capturing correctness properties. They use a limited set of operations and deliberately abstract away system-level complexities. For example, our 2PC model omits fault tolerance, but aspects like crashes or retries could be incorporated by adding operations and node states, as the FOLTL formalism is expressive enough to accommodate such extensions.
For the DHT protocol, operations were modeled using paired begin and end events rather than single predicates spanning multiple time points. While this increases the verbosity of specifications, it better reflects the client-server nature of the operations, where efects occur between invocation and response, and makes it more intuitive to distinguish input from output arguments. It also provides a useful contrast with the 2PC example, highlighting FOLTL flexibility in supporting diferent modeling styles.
Although FOLTL, as a general approach, allows specifying any property, fragments with syntactic variations may be particularly tailored for the DHT case or other protocols where operations are continuous and there is a clear distinction between inputs and outputs, so that complex properties can have simpler specifications.
While the theoretical study of online monitoring with fragments of FOLTL is not novel, despite inherent undecidability, semi-decidable fragments and tools such as BLACK remain useful for this task. Key challenges include adapting existing solvers for online monitoring and identifying fragments that balance expressiveness with decidability.
Although online monitoring is widely used, ofline monitoring with FOLTL has received little attention. In scenarios where complete executions are available, treating the problem ofline can enable more eficient violation detection. This is a promising and relatively unexplored direction. Future challenges involve identifying useful fragments of FOLTL for both online and ofline monitoring and developing scalable decision procedures and optimizations for evaluating quantifier-heavy specifications over large complete traces. We leave for future work to determine whether the presented example specifications of distributed protocols fall into some already known decidable fragment of FOLTL.
We believe that many problems over distributed protocols can be efectively expressed using FOLTL, and expect specification-based testing with first-order temporal logics to gain broader attention and adoption. We are also interested in investigating the use of FOLTL for expressing properties over protocols used in public administration processes, which we believe would largely benefit from this work. This work positions FOLTL as a viable and flexible formalism for validating distributed protocols in both online and ofline settings, with expressive fragments capable of capturing meaningful correctness properties. It opens the way for practical monitoring systems that bridge the gap between formal logic and implementation-level testing.
This work was partially supported by the ‘OptiGov’ project, with ref. n. 2024.07385.IACDC (DOI: 10.54499/2024.07385.IACDC), fully funded by the ‘Plano de Recuperação e Resiliência’ (PRR) under the investment ‘RE-C05-i08 - Ciência Mais Digital’ (measure ‘RE-C05-i08.m04’), framed within the financing agreement signed between the ‘Estrutura de Missão Recuperar Portugal’ (EMRP) and Fundação para a Ciência e a Tecnologia, I.P. (FCT) as an intermediary beneficiary. This work was also partly supported by Portuguese national funds through Fundação para a Ciência e a Tecnologia, I.P. (FCT), under projects UID/50021/2025 and UID/PRR/50021/2025.
During the preparation of this work, the author(s) used Grammarly and ChatGPT for grammar and spelling checks, as well as to identify other writing mistakes. After using these tool(s)/service(s), the author(s) reviewed and edited the content as needed and take(s) full responsibility for the publication’s content [7] C. Cachin, M. Vukolic, Blockchain consensus protocols in the wild, CoRR abs/1707.01873 (2017).
arXiv:1707.01873. [8] J. Neu, E. N. Tas, D. Tse, Ebb-and-flow protocols: A resolution of the availability-finality dilemma, in: Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021, pp. 446–465. doi:10. 1109/SP40001.2021.00045. [9] D. Jackson, Alloy: A language and tool for exploring software designs, Communications of the
ACM 62 (2019) 66–76. doi:10.1145/3338843. [10] I. Stoica, R. Morris, D. Karger, M. F. Kaashoek, H. Balakrishnan, Chord: A scalable peer-to-peer lookup service for internet applications, SIGCOMM Computer Communication Review 31 (2001) 149–160. doi:10.1145/964723.383071. [11] P. Zave, Using lightweight modeling to understand chord, Computer Communication Review 42 (2012) 49–57. doi:10.1145/2185376.2185383. [12] L. Lamport, Specifying Systems: the TLA+ language and tools for hardware and software engineers, volume 388, Addison-Wesley, 2002. URL: http://research.microsoft.com/users/lamport/tla/book. html. [13] C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, M. Deardeuf, How Amazon Web Services uses formal methods, Communications of the ACM 58 (2015) 66–73. doi:10.1145/ 2699417. [14] H. Cirstea, M. A. Kuppe, B. Loillier, S. Merz, Validating traces of distributed programs against TLA+ specifications, in: Proceedings of the 22nd International Conference on Software Engineering and Formal Methods, 2024, pp. 126–143. doi:10.1007/978-3-031-77382-2\_8. [15] N. Policarpo, J. F. Santos, A. Cunha, J. Leitão, P. Á. Costa, Specifying distributed hash tables with Allen Temporal Logic, in: Proceedings of the 13th IEEE/ACM International Conference on Formal Methods in Software Engineering, 2025, pp. 63–73. doi:10.1109/FORMALISE66629. 2025.00013. [16] I. M. Hodkinson, F. Wolter, M. Zakharyaschev, Decidable fragments of first-order temporal logics,
Annals of Pure and Applied Logic 106 (2000) 85–134. doi:10.1016/S0168-0072(00)00018-X. [17] T. Braüner, S. Ghilardi, First-order modal logic, in: Handbook of Modal Logic, Studies in logic and practical reasoning, North-Holland, 2007, pp. 549–620. doi:10.1016/S1570-2464(07)80012-7. [18] A. Artale, A. Mazzullo, A. Ozaki, First-order temporal logic on finite traces: Semantic properties, decidable fragments, and applications, ACM Transactions on Computational Logic 25 (2024) 13:1–13:43. doi:10.1145/3651161. [19] A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th Annual Symposium on
Foundations of Computer Science, 1977, pp. 46–57. doi:10.1109/SFCS.1977.32. [20] N. Decker, M. Leucker, D. Thoma, Monitoring modulo theories, International Journal on Software
Tools for Technology Transfer 18 (2016) 205–225. doi:10.1007/S10009-015-0380-3. [21] P. Felli, M. Montali, F. Patrizi, S. Winkler, Monitoring arithmetic temporal properties on finite traces, in: Proceedings of the 37th AAAI Conference on Artificial Intelligence, 2023, pp. 6346–6354. doi:10.1609/AAAI.V37I5.25781. [22] M. Faella, G. Parlato, A unified automata-theoretic approach to LTL f modulo theories, in: Proceedings of the 27th European Conference on Artificial Intelligence, 2024, pp. 1254–1261. doi:10.3233/FAIA240622. [23] L. Geatti, A. Gianola, N. Gigante, Linear temporal logic modulo theories over finite traces, in: Proceedings of the 31st International Joint Conference on Artificial Intelligence, 2022, pp. 2641– 2647. doi:10.24963/IJCAI.2022/366. [24] C. W. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli, Satisfiability modulo theories, in: Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2021, pp. 1267–1329. doi:10.3233/FAIA201017. [25] D. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Fragments of first-order temporal logics, in: Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics, Elsevier, 2003, pp. 465–545. doi:https://doi.org/10.1016/ S0049-237X(03)80012-5.